Intersection types and domain operators
| Autor: | Fabio Alessi, Stefania Lusin, Mariangiola Dezani-Ciancaglini |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Discrete mathematics
General Computer Science Fixed point operators Models of Lambda Calculus Lambda Theories Intersection Types Lambda theories Models of lambda calculus Intersection types Fixed point Theoretical Computer Science Term (time) Interpretation (model theory) Algebra Operator (computer programming) Type theory Intersection Simple (abstract algebra) Filter (mathematics) Computer Science(all) Lambda calculus Mathematics |
| Zdroj: | Theoretical Computer Science. 316:25-47 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/j.tcs.2004.01.022 |
| Popis: | We use intersection types as a tool for obtaining λ-models. Relying on the notion of easy intersection type theory, we successfully build a λ-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the λ-theory where the λ-term (λx.xx)(λx.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of λ-theories. The second result is that for any simple easy term, there is a λ-model, where the interpretation of the term is the minimal fixed point operator. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect