We use intersection types as a tool for obtaining lambda-models. Relying on the notion of easy intersection type theory, we successfully build a lambda-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 lambda-theory where the lambda-term (lambdax.xx)(lambdax.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of lambda-theories. The second result is that for any simple easy term, there is a lambda-model, where the interpretation of the term is the minimal fixed point operator. (C) 2004 Elsevier B.V. All rights reserved.

Intersection types and domain operators

ALESSI, Fabio;
2004

Abstract

We use intersection types as a tool for obtaining lambda-models. Relying on the notion of easy intersection type theory, we successfully build a lambda-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 lambda-theory where the lambda-term (lambdax.xx)(lambdax.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of lambda-theories. The second result is that for any simple easy term, there is a lambda-model, where the interpretation of the term is the minimal fixed point operator. (C) 2004 Elsevier B.V. All rights reserved.
File in questo prodotto:
File Dimensione Formato  
lusin.pdf

non disponibili

Tipologia: Altro materiale allegato
Licenza: Non pubblico
Dimensione 338.18 kB
Formato Adobe PDF
338.18 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/694794
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 6
social impact