Intersection types and lambda models
| Autor: | Mariangiola Dezani-Ciancaglini, Fabio Alessi, Franco Barbanera |
|---|---|
| Rok vydání: | 2006 |
| Předmět: |
Interpretation (logic)
General Computer Science Semantics (computer science) λ-calculus Intersection types β- and η-reduction/expansion Lambda Theoretical Computer Science Reduction (complexity) λ-models Intersection Filter (mathematics) Algorithm Mathematics Standard model (cryptography) Computer Science(all) |
| Zdroj: | Theoretical Computer Science. 355(2):108-126 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/j.tcs.2006.01.004 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect