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

HONSELL, Furio;LENISA, Marina
1995-01-01

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.
1995
9783540590484
File in questo prodotto:
File Dimensione Formato  
tlca95.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Non pubblico
Dimensione 4.05 MB
Formato Adobe PDF
4.05 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/745486
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? ND
social impact