Abstract
The sixth lecture returned to the question of giving semantics to programs that don't terminate. This question is of historical importance (it put a stop to Strachey's naive denotational semantics), but also practical (reactive programs like network servers must not terminate !)
A first approach, topological in nature, sees the semantics of a program as the limit of its finite behaviors. We have illustrated this on the IMP language, where it suffices to write an interpreter bounded by a maximum depth of computation, then to make this maximum depth tend towards infinity, to obtain a denotational semantics of IMP that characterizes both termination and divergence. For languages handling more complex data types, such as lambda-calculus, denotational semantics requires a richer topological structure, such as Scott domains.
Other approaches, more suited to type-theoretic mechanization, rely on coinductive definitions and reasoning. The lecture showed how to define and mechanize a natural semantics for diverging IMP programs in the form of a coinductive predicate that structures infinite sequences of reductions. Next, we introduced the partiality monad, invented by Capretta in 2005, which provides a coinductive and constructive representation of computations that can terminate or diverge. We studied how to write a reference interpreter for IMP in the partiality monad. With observational equivalence, this interpreter satisfies the equations of IMP's operational semantics, thus providing a constructive alternative to topological approaches.
