scientific article; zbMATH DE number 16188

MaRDI QIDQ3972839zbMATH OpenFDO

Authors Stavros S. Cosmandakis

Publication date 26 June 1992

zbMATH Keywords

computational adequacydomain theoryfull abstractionlambda calculuslazy evaluationrecursive types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55)

Review text

[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.

Recommendations

• Full abstraction in the lazy lambda calculus
• scientific article; zbMATH DE number 3938562
• scientific article; zbMATH DE number 512785
• Lambda-calculi for (strict) parallel functions
• Adequacy for a lazy functional language with recursive and polymorphic types

Cited in

(10)

• Confluence of the lambda calculus with left-linear algebraic rewriting
• Adequacy for a lazy functional language with recursive and polymorphic types
• scientific article; zbMATH DE number 445161 (Why is no real title available?)
• scientific article; zbMATH DE number 3887103 (Why is no real title available?)
• A universality theorem for PCF with recursive types, parallel-or and ∃
• scientific article; zbMATH DE number 5033764 (Why is no real title available?)
• An operational domain-theoretic treatment of recursive types
• A fixed-point semantics for feature type systems
• Type inference with recursive types: Syntax and semantics
• The insensitivity theorem for nonreducing reflexive types

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3972839)