Akademska digitalna zbirka SLovenije - logo
E-viri
Recenzirano Odprti dostop
  • Intersection types and doma...
    Alessi, Fabio; Dezani-Ciancaglini, Mariangiola; Lusin, Stefania

    Theoretical computer science, 05/2004, Letnik: 316, Številka: 1
    Journal Article

    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.