Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
438874 | Theoretical Computer Science | 2006 | 19 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics