Proof principles for reasoning about various semantics of untyped λ-calculus are discussed. The semantics are determined operationally by fixing a particular reduction strategy on λ-terms and a suitable set of values, and by taking the corresponding observational equivalence on terms. These principles arise naturally as co-induction principles, when the observational equivalences are shown to be induced by the unique mapping into a final F-coalgebra, for a suitable functor F. This is achieved either by induction on computation steps or exploiting the properties of some, computationally adequate, inverse limit denotational model. The final F-coalgebras cannot be given, in general, the structure of a “denotational” λ-model. Nevertheless the “final semantics” can count as compositional in that it induces a congruence. We utilize the intuitive categorical setting of hypersets and functions. The importance of the principles introduced in this paper lies in the fact that they often allow to factorize the complexity of proofs (of observational equivalence) by “straight” induction on computation steps, which are usually lengthy and error-prone.

### Final Semantics for untyped lambda-calculus

#### Abstract

Proof principles for reasoning about various semantics of untyped λ-calculus are discussed. The semantics are determined operationally by fixing a particular reduction strategy on λ-terms and a suitable set of values, and by taking the corresponding observational equivalence on terms. These principles arise naturally as co-induction principles, when the observational equivalences are shown to be induced by the unique mapping into a final F-coalgebra, for a suitable functor F. This is achieved either by induction on computation steps or exploiting the properties of some, computationally adequate, inverse limit denotational model. The final F-coalgebras cannot be given, in general, the structure of a “denotational” λ-model. Nevertheless the “final semantics” can count as compositional in that it induces a congruence. We utilize the intuitive categorical setting of hypersets and functions. The importance of the principles introduced in this paper lies in the fact that they often allow to factorize the complexity of proofs (of observational equivalence) by “straight” induction on computation steps, which are usually lengthy and error-prone.
##### Scheda breve Scheda completa Scheda completa (DC)
1995
9783540590484
File in questo prodotto:
File
tlca95.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Non pubblico
Dimensione 4.05 MB
Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11390/745486`