Article ID Journal Published Year Pages File Type
436686 Theoretical Computer Science 2006 20 Pages PDF
Abstract

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

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics