کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
436686 | 690025 | 2006 | 20 صفحه PDF | دانلود رایگان |
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).
Journal: Theoretical Computer Science - Volume 354, Issue 1, 21 March 2006, Pages 4-23