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

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