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