Invariance of interpretation by β-conversion is one of the minimal requirements for any standard model for the λ-calculus. With the intersection type systems being a general framework for the study of semantic domains for the λ-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results for intersection type assignment systems. Instead of considering conversion as a whole, reduction and expansion will be considered separately. Not only for usual computational rules like β, η, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed λ-models.
Intersection types and lambda models
BARBANERA, Franco;
2006-01-01
Abstract
Invariance of interpretation by β-conversion is one of the minimal requirements for any standard model for the λ-calculus. With the intersection type systems being a general framework for the study of semantic domains for the λ-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results for intersection type assignment systems. Instead of considering conversion as a whole, reduction and expansion will be considered separately. Not only for usual computational rules like β, η, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed λ-models.File | Dimensione | Formato | |
---|---|---|---|
abdtcs.pdf
accesso aperto
Tipologia:
Versione Editoriale (PDF)
Licenza:
Non specificato
Dimensione
211.45 kB
Formato
Adobe PDF
|
211.45 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.