A graph-easy class of mute lambda-terms A. Bucciarelli1 , A. Carraro2 , G. Favro1,2 , and A. Salibra2 1 Univ Paris Diderot, Sorbonne Paris Cité, PPS, UMR 7126, CNRS, Paris, France 2 DAIS, Università Ca’Foscari Venezia, Italy Abstract. Among the unsolvable terms of the lambda calculus, the mute (or root-active) ones are those having the highest degree of un- definedness. In this paper, we define an infinite set S of mute terms, and show that it is graph-easy: for any closed term t of the lambda calculus there exists a graph model equating all the terms of S to t. Keywords: Lambda-calculus, mute terms, graph models, forcing, ultra- products. 1 Introduction It is a well known result by Jacopini [15] that Ω can be consistently equated to any closed term t of the (untyped) lambda-calculus, where Ω is the paradigmatic unsolvable term (λx.xx)(λx.xx) (this is called the easiness of Ω). Baeten and Boerboom [3] gave the first semantic proof of this result by showing that for all closed terms t one can build a graph model satisfying the equation Ω = t. This semantic result extends to other classes of models and to some other terms which share with Ω enough of its good will (cf. [7] for a survey of such results). Mute lambda terms have been introduced by Berarducci [5], for defining models of the lambda calculus that do not identify all the unsolvable terms. Mute terms are somehow the “most undefined” lambda terms, as they are unsolvable of order 0 (zero terms), which are not β-convertible to a zero term applied to something else. For instance, Ω is mute, and Ω3 = (λx.xxx)(λx.xxx) is a zero term that is not mute, since it reduces to Ω3 (λx.xxx). Berarducci proved that the set of mute terms is easy, in the sense that it is consistent with the lambda calculus to simultaneously equate all the mute terms to a fixed arbitrary closed term. Hereafter, a set of lambda terms that can be simultaneously, consistently equated to a fixed arbitrary closed term is called an easy set. Given a class C of models of the lambda calculus, and an easy set S, we say that S is C-easy if, for every closed term t, there exists a model in C that equates all the terms in S to t. Studying C-easiness gives insights on the expressive power of the class C. Concerning filter lambda models, for instance, it had been conjectured [2] that they have full expressive power for singletons, in the sense that any easy single- ton set is filter-easy. Carraro and Salibra [13] showed that this is not the case: there exists a co-r.e. set of easy terms that are not filter-easy. The first negative semantic result was obtained by Kerth [19]: Ω3 I, where I = λx.x, is an easy 59 A.Bucciarelli et al. A graph-easy class of mute lambda-terms term, but no graph model satisfies the identity Ω3 I = I. This result shows a limitation of graph models. The easiness of Ω3 I was proven syntactically in [16] (see also [6]), but it was only given a semantic proof in [1], where the authors build, for each closed t, a filter model of Ω3 I = t. Graph models are arguably the simplest models of the lambda calculus. There are two known methods for building graph models, namely: by forcing or by canonical completion. Both methods consist in completing a partial model into a total one. The canonical completion method was introduced by Plotkin and Engeler and then systematized by Longo [21] for graph models. The word “canonical” refers here to the fact that the graph model is built inductively from the partial one and completely determined by it. This method was then used by Kerth [18] to prove the existence of 2ω pairwise inconsistent graph theories, and by Buc- ciarelli–Salibra [11, 9, 10] to characterize minimal and maximal graph theories. In particular [11] shows that the minimal graph theory is not equal to the min- imal lambda theory λβ, and that the lambda theory B (generated by equating lambda terms with the same Böhm tree) is the greatest sensible graph theory. The forcing method originates with Baeten–Boerboom [3], and it is more flexible than canonical completions. In fact, the inductive construction depends here not only on the initial partial model but also on the consistency problem one is interested in. The method was afterwards generalized to other classes of webbed models by Jiang [17] and Kerth [20]. It was also generalized to families of terms similar to Ω by Zylberajch [23] and Berline–Salibra [8]. One more difference between these methods is that if we start with a recursive partial web, the canonical completion builds a recursive total web, while forcing always generates a non recursive web. In this paper we define an infinite and recursive set of mute terms, the regular mute terms. A regular mute term has the form s0 s1 . . . sn , for some n, and it has the property that, in n steps of head reduction, it reduces to a term of the same shape t0 t1 . . . tn , where t0 = si for some 1 ≤ i ≤ n. As regular mute terms are mute, we know that the set of all regular mute terms is easy, since each subset of an easy set is itself easy. We show that it is actually graph-easy by generalizing the forcing technique used in [8]. More precisely, given a closed λ-term t and a finite set {n1 , . . . , nk } of natural numbers, we construct a graph model which equates to t all the regular mute terms of the form s0 s1 . . . snj , 1 ≤ j ≤ k, using forcing. Then we glue together these graph models in an ultraproduct, using a tech- nique introduced in [12]. This gives rise to a graph model that is an expansion of the ultraproduct, where all the regular mute terms are equated to t, thus concluding the proof that the set of regular mute terms is graph-easy. 2 Theories and models of λ-calculus With regard to the lambda-calculus we follow the notation and terminology of [4]. By Λ and Λo , respectively, we indicate the set of λ-terms and of closed λ- 60 A.Bucciarelli et al. A graph-easy class of mute lambda-terms terms. We denote αβ-conversion by λβ. A λ-theory is a congruence on Λ (with respect to the operators of abstraction and application) which contains λβ. A λ-theory is consistent if it does not equate all λ-terms, inconsistent otherwise. It took some time, after Scott gave his model construction, for consensus to arise on the general notion of a model of the λ-calculus. There are mainly two descriptions that one can give: the category-theoretical and the algebraic one. The categorical notion of model, that of reflexive object in a Cartesian closed category (ccc), is well-suited for constructing concrete models, while the algebraic one is rather used to understand global properties of models (constructions of new models out of existing ones, closure properties, etc.) and to obtain results about the structure of the lattice of λ-theories. The algebraic description of models of λ-calculus proposes two kinds of structures, viz. the λ-algebras and the λ-models, both based on the notion of combinatory algebra. We will focus on λ-models. A combinatory algebra A = (A, ·, k, s) is a structure with a binary operation called application and two distinguished elements k and s called basic combi- nators. The symbol “·” is usually omitted from expressions and by convention application associates to the left, allowing to leave out superfluous parentheses. The class of combinatory algebras is axiomatized by the equations kxy = x and sxyz = xz(yz). A function f : A → A is representable in A if there exists an element a ∈ A such that f (b) = ab for all b ∈ A. For example, the identity function is represented by the combinator i = skk. The axioms of an elementary subclass of combinatory algebras, called λ- models, were expressly chosen to make coherent the interpretation of the λ-terms (see Barendregt [4, Def. 5.2.7]). In addition to five axioms due to Curry (see [4, Thm. 5.2.5]), the Meyer-Scott axiom is the most important one in the definition of a λ-model. In the first-order language of combinatory algebras it is formulated as ∀xy.(∀z. xz = yz) ⇒ εx = εy, where the combinator ε = s(ki) is made into an inner choice operator. Indeed, given any a, the element εa represents the same function as a; by the Meyer-Scott axiom, εc = εd for all c, d representing the same function. Given a set A, we denote by EnvA the set of A-environments, i.e., the func- tions from the set Var of λ-calculus variables to A. For every x ∈ Var and a ∈ A we denote by ρ[x := a] the environment ρ0 which coincides with ρ everywhere except on x, where ρ0 takes the value a. Given a λ-model A, the interpretation |t|A : EnvA → A of a λ-term is defined by induction on the complexity of t in such a way that |x|A ρ = ρ(x); |tu|A A A ρ = |t|ρ |u|ρ ; |λx.t|A ρ = εb where b is any element satisfying ba = |t|A ρ[x:=a] for every a ∈ A. It is important to stress that the class of λ-models is axiomatized by first- order axioms expressed in terms of Horn formulas, so that it is closed under direct products; it is not axiomatized by equations only, so that it is not closed neither under substructures nor under homomorphic images. 61 A.Bucciarelli et al. A graph-easy class of mute lambda-terms 3 Graph models The class of graph models belongs to Scott’s continuous semantics. Graph models owe their name to the fact that continuous functions are encoded in them via (a sufficient fragment of) their graphs, namely their traces. A graph model is a model of untyped λ-calculus, which is generated from a web in a way that will be recalled below. Historically, the first graph model was Plotkin and Scott’s Pω (see e.g. [4]), which is also known in the literature as “the graph model”. The simplest graph model, E, was introduced soon afterwards, and independently, by Engeler [14] and Plotkin [22]. More examples can be found in [7]. As a matter of notation, we denote by D∗ the set of all finite subsets of a set D. Elements of D∗ will be denoted by small roman letters a, b, c, . . . , while elements of D by greek letters α, β, γ, . . . . For short we will confuse the model and its web and so we define: Definition 1. A graph model is a pair (D, p), where D is an infinite set and p : D∗ × D → D is an injective total function. Such a pair will also be called a total pair. In the setting of graph models a partial pair (see [7]) is a pair (A, q) where A is any set and q : A∗ × A * A is a partial (possibly total) injection. Examples of partial pairs are: the empty pair (∅, ∅) and all the graph models. If (D, p) is a partial pair, we write a →p α (or a → α if p is evident from the context) for p(a, α). Moreover, β → α means {β} → α. a1 → a2 → · · · → an−1 → an → α stands for (a1 → (a2 → . . . (an−1 → (an → α)) . . . )). If ā = a1 , a2 , . . . , an , then ā → α stands for (a1 → (a2 → . . . (an−1 → (an → α)) . . . )). A total pair (D, p) generates a λ-model of universe P(D), called graph λ- model. In particular P(D) is endowed with an application operator that makes it a λ-model. The interpretation |t|p : EnvP(D) → P(D) of a λ-term t relative to (D, p) can be described inductively as follows (see Section 2): – |x|pρ = ρ(x) – |tu|pρ = {α : (∃a ⊆ |u|pρ ) a → α ∈ |t|pρ } – |λx.t|pρ = { a → α : α ∈ |t|pρ[x:=a] } Since |t|pρ only depends on the value of ρ on the free variables of t, we only write |t|p if t is closed. A graph model (D, p) satisfies t = u, written (D, p)  t = u, if |t|pρ = |u|pρ for all environments ρ. The λ-theory T h(D, p) induced by (D, p) is defined as T h(D, p) = {t = u : t, u ∈ Λ and |t|p = |u|p }. A λ-theory induced by a graph model will be called a graph theory. 62 A.Bucciarelli et al. A graph-easy class of mute lambda-terms 4 The regular mute λ-terms A first step towards the definition of regular mute terms are the hereditarily n-ary terms, defined below. Definition 2. Let n > 0 and x̄ ≡ x1 , . . . xk be distinct variables. The set of hereditarily n-ary λ-terms over x̄, written Hn [x̄], is the smallest set of λ-terms containing x1 , . . . , xk and satisfying the following property, for all fresh distinct variables ȳ ≡ y1 , . . . , yn and all terms t1 , . . . , tn : t1 , . . . , tn ∈ Hn [x̄, ȳ] ⇒ λȳ.yi t1 . . . tn ∈ Hn [x̄]. We write Hn for Hn [ ]. Example 1. Some unary and binary hereditary λ-terms: – λx.xx ∈ H1 – λy.yx ∈ H1 [x] – λx.x(λy.yx) ∈ H1 – λzy.yzx ∈ H2 [x] – λxy.x(λzy.yzx)y ∈ H2 . Given a natural number n and variables x̄ we define inductively an increasing sequence of sets of λ-terms, starting at Hn [x̄]: Definition 3. Let x̄ ≡ x1 , . . . xk and ȳ ≡ y1 , . . . , yn be distinct fresh variables. – Hn0 [x̄] = Hn [x̄] – Hnm+1 [x̄]S= {s[u/y] : s ∈ Hnm [x̄, ȳ], ū ≡ u1 , . . . , un ∈ Hnm [x̄]} – Sn [x̄] = m Hnm [x̄]. We write Sn for Sn [ ]. For t ∈ Sn [x̄], we denote by rk(t) the smallest number rk(t) such that t ∈ Hn [x̄]. Lemma 1. If ȳ is a sequence of n distinct variables, s ∈ Sn [x̄, ȳ] and t̄ ≡ t1 , . . . , tn ∈ Sn [x̄], then s[t̄/ȳ] ∈ Sn [x̄]. Lemma 2. Let t be a λ-term. Then t ∈ Hnm [x̄] if, and only if, there exist – s ∈ Hn0 [x̄, z̄ 1 , . . . , z̄ m ], – sequences z̄ i (i = 1, . . . , m) of n distinct variables, – sequences t̄i (i = 1, . . . , m) of n terms t̄i ≡ ti1 , . . . , tin ∈ Hnm−i [x̄, z̄ 1 , . . . , z̄ i−1 ] such that t ≡ s[tm /z m ] · · · [t1 /z 1 ]. Proof. Just an unfolding of the previous definition. Proposition 1. For all n > 0, s0 , . . . , sn ∈ Sn , there exist r0 , . . . , rn ∈ Sn and i ≤ n such that s0 s1 . . . sn →nβ r0 r1 . . . rn and r0 ≡ si 63 A.Bucciarelli et al. A graph-easy class of mute lambda-terms Proof. (1) rk(s0 ) = 0. Since s0 ∈ Hn , then s0 ≡ λy1 . . . yn .yi r1 . . . rn with r1 , . . . , rn ∈ Hn [y1 , . . . , yn ]. Hence s0 s1 . . . sn →nβ si r1 [s̄/ȳ] . . . rn [s̄/ȳ]. By Lemma 1 the term ri [s̄/ȳ] ∈ Sn , and we are done. (2) rk(s0 ) = m > 0. By Lemma 2 there exists u ∈ Hn [z̄ 1 , . . . , z̄ m ] such that s0 ≡ u[t̄m /z̄ m ] . . . [t̄1 /z̄ 1 ], for some terms t̄i ∈ Hnm−i [z̄ 1 , . . . , z̄ i−1 ], for 1 ≤ i ≤ m. The term u cannot be a variable because of the rank of s0 . Then by definition u ≡ λȳ.yi u1 . . . un with ui ∈ Hn [z̄ 1 , . . . , z̄ m , ȳ]. Then s0 = λȳ.yi (u1 [t̄m /z̄ m ] . . . [t̄1 /z̄ 1 ]) . . . (un [t̄m /z̄ m ] . . . [t̄1 /z̄ 1 ]) and, if s̄ = s1 , . . . , sn s0 s1 . . . sn →nβ si (u1 [t̄m /z̄ m ] . . . [t̄1 /z̄ 1 ][s̄/ȳ]) . . . (un [t̄m /z̄ m ] . . . [t̄1 /z̄ 1 ][s̄/ȳ]). Theorem 1. For all s0 , . . . , sn ∈ Sn , the term s0 s1 . . . sn is mute. Hereafter, a term s0 s1 . . . sn (si ∈ Sn ) is called a n-regular mute term; Mn will denote the set of all n-regular mute terms. Example 2. Some unary and binary regular mute terms: – (λx.xx)(λx.xx) ∈ M1 – (λx.x(λy.yx))(λx.xx) ∈ M1 – AAA ∈ M2 , where A := λxy.x(λzt.tzx)y. Example 3. Let B := λx.x(λy.xy). Then BB is a mute term that is not regular: BB = (λx.x(λy.xy))B →β B(λy.By) →β BB 5 Forcing for regular mute terms In this section we show that, given a closed λ-term t and a finite set {n1 , . . . , nk } of natural numbers, there exists a graph model which equates all the regular mute terms of the form s0 s1 . . . snj , 1 ≤ j ≤ k, to t, using forcing. 5.1 Some useful lemmas Lemma 3. Let (D, p) be a graph model, ρ be D-environment and β̄ = β, β, . . . , β (n-times). If β = β̄ → α, t ∈ Sn [x̄] and β ∈ ρ(xi ) (i = 1, . . . , k) then β ∈ |t|pρ . Proof. Base case: t ∈ Hn [x̄]. Let ū ∈ Hn [x̄, ȳ] and z ∈ {x̄, ȳ} such that t = λȳ.z ū. β = β̄ → α ∈ |λȳ.z ū|pρ ⇔ α ∈ |z ū|pρ[ȳ:=β̄] Since β ∈ ρ[ȳ := β̄] and by induction hypothesis β ∈ |ui |pρ[ȳ:=β̄] , then α ∈ |z ū|pρ[ȳ:=β̄] . 64 A.Bucciarelli et al. A graph-easy class of mute lambda-terms Let t ∈ Hnm+1 [x̄]. Then t ≡ s[u/y], where s ∈ Hnm [x̄, ȳ] and ū ≡ u1 , . . . , un ∈ Hn [x̄]. By induction hypothesis we have β ∈ |ui |pρ . Since |s[u/y]|pρ = |s|pρ[ȳ:=|ū|pρ ] m and β ∈ ρ[ȳ := |ū|pρ ](yi ), then by induction hypothesis β ∈ |s|pρ[ȳ:=|ū|pρ ] and we get the conclusion. Lemma 4. Let (D, p) be a graph model, s00 s01 . . . s0n ∈ Mn (s0i ∈ Sn ) and γ ∈ |s00 s01 . . . s0n |p . Then there exist a sequence βi ≡ ai1 → · · · → ain → γ (i ∈ ω) of elements of D and a sequence di (i ∈ ω) of natural numbers ≤ n such that βi+1 ∈ aidi . Proof. By Proposition 1 there exists an infinite sequence of mute terms such that s00 s01 . . . s0n →nβ s10 s11 . . . s1n →nβ . . . →nβ sk0 sk1 . . . skn →nβ . . . and sk0 ≡ sk−1 dk−1 for some 1 ≤ dk−1 ≤ n. The number dk−1 is the order of the head variable of the term sk−1 0 . By γ ∈ |s00 s01 . . . s0n |p there exists a01 → · · · → an → γ ∈ |s0 | such that ai ⊆ |s0i |p . We define 0 0 p 0 β0 = a01 → · · · → a0n → γ. Assume βk = ak1 → · · · → akn → γ ∈ |sk0 |p and akj ⊆ |skj |p for every j ≤ n. Since sk0 = λȳ.ydk u1 . . . un for some terms ui and βk ∈ |sk0 |p , then, if ā = a1 , . . . , akn k γ ∈ akdk (u1 [ā/ȳ]) . . . (un [ā/ȳ]). Then there exists βk+1 = ak+1 1 → · · · → ak+1 n → γ ∈ akdk ⊆ |sk+1 0 |p = |skdk |p and k+1 k+1 p aj ⊆ |sj | . 5.2 Forcing at work We recall the notion of weakly continuous operator from [8]. Definition 4. Let D be an infinite countable set. By I(D) we indicate the cpo of partial injections q : D∗ × D * D, ordered by inclusion of their graphs. By a “total p” we will mean “an element of I(D) which is a total map” (equivalently: which is a maximal element of I(D)). The domain and range of q ∈ I(D) are denoted by dom(q) and rg(q). We will also confuse the partial injections and their graphs. Definition 5. A function F : I(D) → P(D) is weakly continuous if it is mono- tone with respect to inclusion and if furthermore, for all total p ∈ I(D), [ F (p) = F (q). q⊆fin p 65 A.Bucciarelli et al. A graph-easy class of mute lambda-terms Let p ∈ I(D). The universe U (p) of p is defined as follows: [ U (p) = (a ∪ {α, p(a, α)}). (a,α)∈dom(p) If p is finite, then the universe of p is also finite. Let p ∈ I(D) be finite, α ∈ D, ¯ ≡ 1 , . . . , k ∈ D \ U (p) and k ∈ N. Then we denote p¯,α the extension of p such that 2 = 1 → α; j+1 = 1 → j (j = 2, . . . , k − 1); 1 = 1 → k . Notice that 1 = 1 → 1 → · · · → 1 → α (k-times) and p¯,α is also finite. S Let e ⊆fin N. We let Me = i∈e Mi the set of n-regular mute terms for n ∈ e. The next theorem is the main technical tool for proving the easiness of the full set of n-regular mute terms. It generalizes [8, Thm. 11]. Theorem 2. Let F : I(D) → P(D) be a weakly continuous function and let e ⊆fin N. Then there exists a total pe : D∗ ×D → D such that (D, pe ) |= t = F (pe ) for all terms t ∈ Me . Proof. We are going to build an increasing sequence of finite injective maps pn , starting from p0 = ∅, and a sequence of elements αn ∈ D ∪ {∗}, where ∗ is a new element, such that: pe =def ∪pn is a total injection, and (D, pe ) |= t = A = F (pe ) for all t ∈ Me , where A =def {αn : n ∈ ω} ∩ D. We fix an enumeration of D and an enumeration of D∗ × D. We start from p0 = ∅. Assume that pn and α0 , . . . , αn−1 have been built. We let – αn = First element of F (pn ) \ {α0 , . . . , αn−1 } in the enumeration of D, if this set is non-empty, and αn = ∗ otherwise; – (bn , δn ) = “the first element in (D∗ × D) \ dom(pn )”; – γn = “the first element in D \ (U (pn ) ∪ bn ∪ {δn } ∪ {α0 , . . . , αn−1 , αn })”. Let r = pn ∪ {γn = bn →r δn }. Case 1: αn = ∗. We let pn+1 = r. Case 2: αn ∈ D. Let e = {k1 , . . . , km }. We define q0 ⊆ q1 ⊆ · · · ⊆ qm ∈ I(D) as follows: q0 = r and pn+1 = qm . Assume we have defined qi . We define qi+1 = (qi )¯n,i ,αn (see above), where ¯n,i ≡ n,i n,i 1 , . . . , ki+1 ∈ D \ (U (qi ) ∪ {αn }) are distinct elements. It is clear that pn is a strictly increasing sequence of well-defined finite injec- tive maps and that pe = ∪pn is total. 66 A.Bucciarelli et al. A graph-easy class of mute lambda-terms It is also clear that each pn (and pe ) is partitioned into two disjoint sets: pn = p1n ∪ p2n , where p1n = {bi → δi = γi : 1 ≤ i ≤ n − 1} is called the gamma part of pn and p2n = pn \ p1n is called the epsilon part. For every γ ∈ D, we define ( 0 if γ ∈ / rg(pe ) deg(γ) = min{n : γ ∈ rg(pn )} if γ ∈ rg(pe ) Moreover, deg(c) = max{deg(x) : x ∈ c} for every c ⊆fin D. The following lemmas easily derive from the construction of pe since (rg(pn+1 )\ rg(pn )) ∩ U (pn ) = ∅. Lemma 5. If deg(a → α) = n and α ∈ / rg(pn ), then α ∈ / rg(pe ). Lemma 6. (i) deg(a → α) ≥ deg(a), deg(α). (ii) If a → α is in the gamma part of pe , then deg(a → α) > deg(a), deg(α). Lemma 7. If αn ∈ rg(pe ) then deg(αn ) ≤ n. Lemma 8. There exists no cycle β = c1 → c2 → . . . cm → β. Proof. Consider a minimal cycle βi = ci → βi+1 (1 ≤ i ≤ m − 1) and βm = cm → β1 . By Lemma 6 we have deg(β1 ) ≥ deg(β2 ) ≥ · · · ≥ deg(βm ) ≥ deg(β1 ). Let us set this common degree equal to k + 1. If β1 = γk = bk →pk+1 δk then δk = β2 has degree k + 1. This is not possible by Lemma 6(ii). If β1 = k,i j then k,i j = c1 → c2 → . . . cm →  k,i j . From this it follows that either α k has degree k+1 k,i k,i (contradicting Lemma 7) or j = j−l (contradicting that the epsilon elements are distinct) or k,i j = αk (contradicting the definition of epsilon elements). This concludes the proof of the lemma. There remains to see that (D, pe ) |= t = A = F (pe ) for every t ∈ Me . A ⊆ F (pe ): it follows from the definition of αn and from the fact that F (pn ) ⊆ F (pe ). F (pe ) ⊆ A: suppose γ ∈ F (pe ); then, since F is weakly continuous, γ ∈ F (pm ) for some m (and for all the larger ones). If γ ∈ / A then, for all n ≥ m, αn ∈ D has smaller rank than γ in the enumeration of D, contradicting the fact that there is only a finite number of such elements. Let m ∈ e and t ≡ s0 s1 . . . sm ∈ Mm . A ⊆ |t|pe : Let αn 6= ∗. The condition (D, pe ) |= αn ∈ |t|pe follows immediately from Lemma 3 and the fact that n,m 1 = n,m 1 → n,m 1 → · · · → n,m 1 → αn (m-times). |t|pe ⊆ A: Assume by contraposition that γ ∈ |t|pe and γ 6= αn for every n. Then by Lemma 4 there exist a sequence βj ≡ aj1 → · · · → ajm → γ (j ∈ ω) of elements of D and a sequence dj (j ∈ ω) of natural numbers ≤ m satisfying the property βj+1 ∈ ajdj . 67 A.Bucciarelli et al. A graph-easy class of mute lambda-terms By Lemma 6 and by βj+1 ∈ ajdj the sequence deg(βj ) is an infinite decreas- ing sequence of natural numbers. Then there exists j such that deg(βj+i ) = deg(βj ) = n for all i ≥ 0. Since pn is finite, it must exist k ≥ j and l > 0 such that βk = βk+l . Moreover, n = deg(βk ) ≥ deg(akdk → akdk +1 → · · · → γ) ≥ deg(βk+1 ) = n because βk+1 ∈ akdk . Then deg(ak+i k dk+i → adk +1 → . . . γ) = n for every i ≤ l. Since ak+i dk+i cannot be {1 } (otherwise βk+i+1 = 1 and γ = αn ) and there is exactly one pair (bn−1 , δn−1 ) such that ((bn−1 , δn−1 ), γn−1 ) ∈ p1n \ pn−1 , then k+j ak+i k k dk+i → (adk+i +1 → . . . γ) = adk+j → (adk+j +1 → . . . γ), for every i, j ≤ l. k+j This implies that ak+i dk+i = adk+j , etc. Since by Lemma 8 there are no cycles, then we get βk = βk+1 = · · · = βk+l−1 = βk+l . It follows that βk ∈ akdk . Since akdk → akdk +1 → · · · → γ belongs to the gamma part of pe , this contradicts Lemma 6(ii). Definition 6. (Forcing) For a term M , a partial pair (D, q), a D-environment ρ and α ∈ D, the abbreviation q ρ α ∈ M means that for all total injections p ⊇ q we have that (D, p) |= α ∈ |M |pρ . Furthermore q ρ X ⊆ M means that q ρ α ∈ M for all α ∈ X. If M is closed we write q α ∈ M for q ρ α ∈ M . Thus, for p is total, p α ∈ M if and only if α ∈ |M |p . Lemma 9. For every term M and environment ρ the function FM,ρ : I(D) → P(D) defined by FM,ρ (q) = { α ∈ D : q ρ α ∈ M } is weakly continuous, and we have FM,ρ (p) = |M |pρ for each total p. Proof. The proof of the weak continuity of FM,ρ is a straightforward induction S the complexity of M on . Let p ∈ Q be total. We have to show that FM,ρ (p) = p q⊆fin p FM,ρ (q) = |M |ρ . If M is a variable x then Fx,ρ (q) = { α ∈ D : q α ∈ ρ(x)} is the constant function with value ρ(x). If M = P Q and α ∈ |M |pρ , then there exists a ⊆ |Q|pρ such that p(a, α) ∈ |P |pρ . Choose such an a and let γ = p(a, α). By induction hypothesis there is a finite q ⊆ p such that q ρ a ⊆ Q and a finite r ⊆ p such that r ρ γ ∈ P ; then it is clear that q ∪ r ∪ {((a, α), γ)} α ∈ M. If M = λx.P and α ∈ |M |pρ then there is a unique pair (b, β) such that α = p(b, β) and β ∈ |P |pρ[x:=b] . By induction hypothesis there is a finite q ⊆ p such that q ρ[x:=b] β ∈ P ; then it is clear that q ∪ {((b, β), α)} ρ α ∈ M. Theorem 3. Let M be a closed term. Then, for every e ⊆fin ω there exists a graph model (D, pe ) such that (D, pe ) |= t = M for all regular mute terms t ∈ Me . Proof. It is sufficient to consider an arbitrary environment ρ, the weakly con- tinuous map FM,ρ : I(D) → P(D) defined in Lemma 9 and the graph model (D, pe ) defined in Theorem 2. 68 A.Bucciarelli et al. A graph-easy class of mute lambda-terms 6 Ultraproducts Ultraproducts result from a suitable combination of the direct product and quo- tient constructions. They were introduced in the 1950’s by Loś. Let I be a non-empty set and let {Ai }i∈I be a family of combinatory algebras. Let U be a proper ultrafilter of the boolean algebra P(I). The relation ∼U , given by a ∼UQb ⇐⇒ {i ∈ I : a(i) = b(i)} ∈ U , is a congruence on the Q combinatory algebra i∈I Ai . The ultraproduct of the family Q {A i }i∈I , noted ( i∈I Ai )/U , is defined Q as the quotient of the product i∈I A i by the congruence ∼U . If a ∈ i∈I Ai , then we denote by a/U the equivalence class of a with respect to the congruence ∼U . If all members Q of {Ai }i∈I are λ-models, by a celebrated theorem of Loś we have that ( i∈I Ai )/U is a λ-model too, because λ-models are Q axiomatized by first-order sentences. The basic combinators of the λ-model ( i∈I Ai )/U are k/U and s/U , and application is given by x/U ·y/U = (x·y)/U , where the application x · y is defined pointwise. We now recall the famous Loś theorem. Theorem 4 (Loś). Let L be a first-order language and {Ai }i∈I be a family of L-structures indexed by a non-empty set I an let U be a proper ultrafilter of P(I). Q Then for every L-formula ϕ(x1 , . . . , xn ) and for every tuple (a1 , . . . , an ) ∈ i∈I A i we have that Y ( Ai )/U |= ϕ(a1 /U, . . . , an /U ) ⇐⇒ {i ∈ I : Ai |= ϕ(a1 (i), . . . , an (i))} ∈ U. i∈I The following theorem is [12, Theorem 4.5]. Theorem 5. Let (Dj , pj )j∈J be a family of total pairs, A = (Aj : j ∈ J) be the corresponding family of graph λ-models, where Aj = (P(Dj ), ·, k, s), and let F be an ultrafilter on J. Then there exists a graph model (E, q) such that the ultraproduct (Πj∈J Aj )/F can be embedded into the graph λ-model determined by (E, q). S Theorem 6. Let M be a closed term and M = n∈N Mn be the set of all regular mute λ-terms. Then there exists a total pair (E, q) such that (E, q) |= M = t, for every t ∈ M. Proof. Let K := {e ⊆ N : e is finite} and F be a non-principal ultrafilter on P(K) that contains the set Kn = {e : n ∈ e}, for each n ∈ N. Hence F contains Ke = {d : e ⊆ d} for each e ⊆fin N. 69 A.Bucciarelli et al. A graph-easy class of mute lambda-terms For every e ⊆ N, let (D, pe ) be the total pair determined by Theorem 3 and define Ae be the corresponding graph λ-model. We show that (Πe∈K Ae )/F |= M = t for every t ∈ M. Let t ∈ Mn . Since Kn ⊆ {e : Ae |= M = t}. and Kn ∈ F then we have that (Πe∈K Ae )/F |= M = t and the conclusion is obtained. References 1. Alessi, F., Dezani-Ciancaglini, M., Honsell, F.: Filter models and easy terms, Italian Conference on Theoretical Computer Science, LNCS 2202, Springer-Verlag, 17–37, 2001. 2. Alessi, F., Lusin, S.: Simple easy terms, in S. van Bakel (ed.), Intersection Types and Related Systems, ENTCS 70, Elsevier, 2002. 3. Baeten, J., Boerboom, B.: Omega can be anything it should not be, in Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, Serie A, Indag. Mathematicae 41, p.111–120, 1979. 4. Barendregt, H.P.: The lambda-calculus, its syntax and semantics, Studies in Logic vol. 103, North Holland, revised edition 1984. 5. Berarducci, A.: Infinite λ-calculus and non-sensible models, in Logic and Algebra, eds. A. Ursini and P. Agliano, Lecture Notes in Pure and Applied Mathematics 180, Marcel Dekker Inc., 1996. 6. Berarducci, A., Intrigila, B.: Some new results on easy λ-terms, Theoretical Com- puter Science 121, 71–88, 1993. 7. Berline, C.: From Computation to foundations via functions and application: The lambda-calculus and its webbed models, Theor. Comput. Sci. 249, 81–161, 2000. 8. Berline, C., Salibra, A.: Easiness in graph models, Theoretical Computer Science 354(1), 4–23, 2006. 9. Bucciarelli, A., Salibra, A.: The minimal graph-model of lambda-calculus, 28th Internat. Symp. on Math. Foundations of Comput. Science, LNCS 2747, Springer- Verlag, 2003. 10. Bucciarelli, A., Salibra, A.: The sensible graph theories of lambda-calculus, LICS’04. 11. Bucciarelli, A., Salibra, A.: Graph lambda-theories, Mathematical Structures in Computer Science 18(5), 975–1004, 2008. 12. Bucciarelli, A., Carraro, A., Salibra, A.: Minimal lambda-theories by ultraproducts, EPTCS 113, 2012. 13. Carraro, A., Salibra, A.: Easy lambda-terms are not always simple, RAIRO - Theor. Inform. and Applic. 46(2), 291–314, 2012. 14. Engeler, E.: Algebras and combinators, Alg. Univ. 13(3), 289–371, 1981. 15. Jacopini, C.: A condition for identifying two elements in whatever model of com- binatory logic, in C. Böhm, ed., LNCS 37, Springer Verlag, 1975. 16. Jacopini, C., Venturini-Zilli, M.: Easy terms in the lambda-calculus, Fundamenta Informaticae VIII.2, 225–233, 1985. 17. Jiang, Y.: Consistency of a λ-theory with n-tuples and easy terms, Archives of Math. Logic, 34(2), 79–96, 1995. 70 A.Bucciarelli et al. A graph-easy class of mute lambda-terms 18. Kerth, R.: Isomorphism and equational equivalence of continuous λ-models, Studia Logica 61, 403–415, 1998. 19. Kerth, R.: Isomorphisme et équivalence équationnelle entre modèles du λ-calcul, Thèse, Université Paris 7, 1995. 20. Kerth, R.: Forcing in stable models of untyped λ-calculus, Indagationas Mathe- maticae 10 , 59–71, 1999. 21. Longo, G.: Set-theoretical models of λ-calculus : theories, expansions and isomor- phisms, Annals of Pure and Applied Logic 24, 153–188, 1983. 22. Plotkin, G.: A set-theoretical definition of application, Memorandum MIP-R-95, School of artificial intelligence, University of Edinburgh, 1972. 23. Zylberajch, C.: Syntaxe et sémantique de la facilité en λ-calcul, Thèse, Université Paris 7, 1991. 71