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).| 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.



