No label defined (Q3972839)

[For the entire collection see Zbl 0713.00018.] The paper is devoted to the correspondence between operational and denotational semantics of lambda terms with recursive types based on type constructs: functional types, cartesian and strict products, coalesced sum and lifting. Analogously to the type-free case, operational semantics is defined to extract only the information on ''nonbottomness'' of arbitrary recursively typed lambda term under some environment. The result of any such computation is (i) a ''canonical (or head normal) form'', which is equivalent to the original term or (ii) ''approximate normal forms'' which are, as in case (i), deliberately of ''non-bottom'' value and which give in the limit the value of the original term. It seems that such specific definition of operational semantics (for arbitrary types and not relativized to any fixed environment) is the reason why in the case of cpo's, in contrast to lattices, it does not look like call-by-name and why the corresponding general evaluation of lazy lambda terms is valid only for the case of lattices. Here lazy abstraction (resp. lazy application) is defined as the ordinary lambda abstraction to which the lift (resp. its inverse drop) operation is applied. Nevertheless, in the case of a fixed ''bottom'' environment an adequate evaluation for lazy terms is defined which fits both for lattice and cpo semantics. Finally, full abstraction and universality is achieved (as in the case of LCF) by adding parallel conditional constructs. No proofs are given.