We generalize Baeten and Boerboom’s method of forcing to show that there is a fixed sequence (u_k) k∈Nat of closed (untyped) lambda-terms satisfying the following properties: (a) For any countable sequence (g_k)k∈Nat of Scott continuous functions (of arbitrary arity) on the power set of an arbitrary countable set, there is a graph model such that (lx.xx)(lx.xx)u_k represents g_k in the model. (b) For any countable sequence (t_k)k∈Nat of closed lambda-terms there is a graph model that satisfies (lx.xx)(lx.xx)u_k = t_k for all k. We apply these two results, which are corollaries of a unique theorem, to prove the existence of (1) a finitely axiomatized lambda-theory L such that the interval lattice constituted by the lambda-theories extending L is distributive; (2) a continuum of pairwise inconsistent graph theories ( = lambda-theories that can be realized as theories of graph models); (3) a congruence distributive variety of combinatory algebras (lambda abstraction algebras, respectively).

Easiness in graph models

SALIBRA, Antonino
2006-01-01

Abstract

We generalize Baeten and Boerboom’s method of forcing to show that there is a fixed sequence (u_k) k∈Nat of closed (untyped) lambda-terms satisfying the following properties: (a) For any countable sequence (g_k)k∈Nat of Scott continuous functions (of arbitrary arity) on the power set of an arbitrary countable set, there is a graph model such that (lx.xx)(lx.xx)u_k represents g_k in the model. (b) For any countable sequence (t_k)k∈Nat of closed lambda-terms there is a graph model that satisfies (lx.xx)(lx.xx)u_k = t_k for all k. We apply these two results, which are corollaries of a unique theorem, to prove the existence of (1) a finitely axiomatized lambda-theory L such that the interval lattice constituted by the lambda-theories extending L is distributive; (2) a continuum of pairwise inconsistent graph theories ( = lambda-theories that can be realized as theories of graph models); (3) a congruence distributive variety of combinatory algebras (lambda abstraction algebras, respectively).
2006
354
File in questo prodotto:
File Dimensione Formato  
VQR-berline-salibra2006.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 314.16 kB
Formato Adobe PDF
314.16 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA 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: https://hdl.handle.net/10278/30116
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact