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).
|Data di pubblicazione:||2006|
|Titolo:||Easiness in graph models|
|Rivista:||THEORETICAL COMPUTER SCIENCE|
|Appare nelle tipologie:||2.1 Articolo su rivista |
File in questo prodotto:
|VQR-berline-salibra2006.pdf||Documento in Post-print||Accesso chiuso-personale||Riservato|