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 …