On finite computations in denotational semantics

Finite and, especially, infinite computations in languages with iteration or recursion are studied in the framework of denotational semantics, and a theorem is proved which relates their syntactic and semantic characterizations. A general proof method is presented to establish this type of relations, and it is shown how—in an induction on the structure of the syntactic constructs of the language—the recursive case follows from the non-recursive one by applying a general definitional scheme. The method is applicable to a variety of other problems concerning recursive constructs such as, for example, fixed point characterizations of several notions of weakest precondition. Also, the connections with the theory of languages with infinite words are discussed, in particular with a substitution theorem due to Nivat (1978).