Among the unsolvable terms of the lambda calculus, the mute (or root-active) ones are those having the highest degree of undefinedness. 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.
Introduction
It is a well known result by Jacopini [
Mute lambda terms have been introduced by Berarducci [
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 [
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
Bucciarelli–Salibra [
The forcing method originates with Baeten–Boerboom [
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 s0s1 . . . 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 t0t1 . . . 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 [
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 s0s1 . . . snj , 1 ≤ j ≤ k, using forcing.
Then we glue together these graph models in an ultraproduct, using a
technique introduced in [
Theories and models of λ-calculus
With regard to the lambda-calculus we follow the notation and terminology of
[
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 combinators. 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 functions 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 = |t|ρA|u|ρA; |λ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 firstorder 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. 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. [
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 [
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 a¯ = a1, a2, . . . , an, then a¯ → α 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ρ}
p – |λx.t|pρ = { a → α : α ∈ |t|ρ[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. 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 y¯ ≡ y1, . . . , yn and all terms t1, . . . , tn: t1, . . . , tn ∈ Hn[x¯, y¯] ⇒ λy¯.yit1 . . . tn ∈ Hn[x¯].
Example 1. Some unary and binary hereditary λ-terms:
We write Hn for Hn[ ]. – λ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 y¯ ≡ y1, . . . , yn be distinct fresh variables. – Hn0[x¯] = Hn[x¯] – Hnm+1[x¯] = {s[u/y] : s ∈ Hnm[x¯, y¯], u¯ ≡ u1, . . . , un ∈ Hnm[x¯]} – Sn[x¯] = Sm Hnm[x¯].
We write Sn for Sn[ ]. For t ∈ Sn[x¯], we denote by rk(t) the smallest number such that t ∈ Hnrk(t)[x¯].
Lemma 1. If y¯ is a sequence of n distinct variables, s ∈ Sn[x¯, y¯] and t¯ ≡ t1, . . . , tn ∈ Sn[x¯], then s[t¯/y¯] ∈ 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/zm] · · · [t1/z1].
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 s0s1 . . . sn →βn r0r1 . . . rn and r0 ≡ si
Proof. (1) rk(s0) = 0.
Since s0 ∈ Hn, then s0 ≡ λy1 . . . yn.yir1 . . . rn with r1, . . . , rn ∈ Hn[y1, . . . , yn]. Hence s0s1 . . . sn →βn sir1[s¯/y¯] . . . rn[s¯/y¯]. By Lemma 1 the term ri[s¯/y¯] ∈ 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 ≡ λy¯.yiu1 . . . un with ui ∈ Hn[z¯1, . . . , z¯m, y¯]. Then
s0 = λy¯.yi(u1[t¯m/z¯m] . . . [t¯1/z¯1]) . . . (un[t¯m/z¯m] . . . [t¯1/z¯1]) and, if s¯ = s1, . . . , sn
s0s1 . . . sn →βn si(u1[t¯m/z¯m] . . . [t¯1/z¯1][s¯/y¯]) . . . (un[t¯m/z¯m] . . . [t¯1/z¯1][s¯/y¯]). Theorem 1. For all s0, . . . , sn ∈ Sn, the term s0s1 . . . sn is mute.
Hereafter, a term s0s1 . . . 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 s0s1 . . . snj , 1 ≤ j ≤ k, to t, using forcing. 5.1
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 u¯ ∈ Hn[x¯, y¯] and z ∈ {x¯, y¯} such that t = λy¯.zu¯. β = β¯ → α ∈ |λy¯.zu¯|pρ ⇔ α ∈ |zu¯|pρ[y¯:=β¯] |zu¯|pρ[y¯:=β¯].
Since β ∈ ρ[y¯ := β¯] and by induction hypothesis β ∈ |ui|pρ[y¯:=β¯], then α ∈
Let t ∈ Hnm+1[x¯]. Then t ≡ s[u/y], where s ∈ Hnm[x¯, y¯] and u¯ ≡ u1, . . . , un ∈ Hnm[x¯]. By induction hypothesis we have β ∈ |ui|pρ. Since |s[u/y]|pρ = |s|pρ[y¯:=|u¯|ρp] and β ∈ ρ[y¯ := |u¯|pρ](yi), then by induction hypothesis β ∈ |s|pρ[y¯:=|u¯|ρp] and we get the conclusion.
Lemma 4. Let (D, p) be a graph model, s00s01 . . . s0n ∈ Mn (si0 ∈ Sn) and γ ∈ |s00s01 . . . 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
s00s10 . . . s0n →βn s10s11 . . . s1n →βn . . . →βn s0ks1k . . . skn →βn . . . and s0k ≡ sk−1 for some 1 ≤ dk−1 ≤ n. The number dk−1 is the order of the dk−1 head variable of the term sk−1. By γ ∈ |s00s10 . . . s0n|p there exists a01 → · · · → a0n → γ ∈ |s00|p such that ai0 0⊆ |si0|p. We define
β0 = a01 → · · · → a0n → γ.
Assume βk = a1k → · · · → akn → γ ∈ |s0k|p and ajk ⊆ |sjk|p for every j ≤ n.
Since s0k = λy¯.ydk u1 . . . un for some terms ui and βk ∈ |s0k|p, then, if a¯ = a1k, . . . , akn
γ ∈ adkk (u1[a¯/y¯]) . . . (un[a¯/y¯]).
Then there exists βk+1 = a1k+1 → · · · → akn+1 → γ ∈ adkk ⊆ |s0k+1|p = |sdkk |p and ajk+1 ⊆ |sjk+1|p. 5.2
We recall the notion of weakly continuous operator from [
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 monotone with respect to inclusion and if furthermore, for all total p ∈ I(D), F (p) =
[ F (q). q⊆finp
Let p ∈ I(D). The universe U (p) of p is defined as follows:
U (p) = and p¯,α is also finite.
Let e ⊆fin N. We let Me = Si∈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 ≡ 1n,i, . . . , kni,+i1 ∈ D \ (U (qi) ∪ {αn}) are distinct elements.
It is clear that pn is a strictly increasing sequence of well-defined finite injective maps and that pe = ∪pn is total.
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 deg(γ) = (0
if γ ∈/ rg(pe) 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 = jk,i then k,i = c1 → c2 → . . . cm → jk,i. From this it follows that either αk has degree k+1 j (contradicting Lemma 7) or jk,i = jk−,il (contradicting that the epsilon elements are distinct) or jk,i = α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 ≡ s0s1 . . . 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 = 1n,m 1
n,m → 1
→ · · · → 1n,m → αn (m-times). property βj+1 ∈ ajdj .
t pe ⊆ A: Assume by contraposition that γ ∈j |t|pe and γ 6= αn for every n. The|n| by Lemma 4 there exist a sequence βj ≡ a1 → · · · → ajm → γ (j ∈ ω) of elements of D and a sequence dj (j ∈ ω) of natural numbers ≤ m satisfying the
By Lemma 6 and by βj+1 ∈ ajdj the sequence deg(βj) is an infinite decreasing 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(adkk → adkk+1 → · · · → γ) ≥ deg(βk+1) = n because βk+1 ∈ adkk . Then deg(adkk++ii → adkk+1 → . . . γ) = n for every i ≤ l. Since adkk++ii cannot be { 1} (otherwise βk+i+1 = 1 and γ = αn) and there is exactly 1 one pair (bn−1, δn−1) such that ((bn−1, δn−1), γn−1) ∈ pn \ pn−1, then dk+i → (adkk+i+1 → . . . γ) = adkk++jj → (adkk+j+1 → . . . γ), for every i, j ≤ l. ak+i This implies that adkk++ii = adkk++jj , etc. Since by Lemma 8 there are no cycles, then we get βk = βk+1 = · · · = βk+l−1 = βk+l. It follows that βk ∈ adkk . Since adkk → adkk+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 Thus, for p is total, p
α ∈ M for q ρ α ∈ M .
α ∈ 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 on the complexity of M . Let p ∈ Q be total. We have to show that FM,ρ(p) = Sq⊆finp FM,ρ(q) = |M |pρ.
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 continuous map FM,ρ : I(D) → P(D) defined in Lemma 9 and the graph model (D, pe) defined in Theorem 2. 6
Ultraproducts Ultraproducts result from a suitable combination of the direct product and quotient constructions. They were introduced in the 1950’s by Lo´s.
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 ∼U b ⇐⇒ {i ∈ I : a(i) = b(i)} ∈ U , is a congruence on the combinatory algebra Qi∈I Ai. The ultraproduct of the family {Ai}i∈I , noted (Qi∈I Ai)/U , is defined as the quotient of the product Qi∈I Ai by the congruence ∼U . If a ∈ Qi∈I Ai, then we denote by a/U the equivalence class of a with respect to the congruence ∼U . If all members of {Ai}i∈I are λ-models, by a celebrated theorem of Lo´s we have that (Qi∈I Ai)/U is a λ-model too, because λ-models are axiomatized by first-order sentences. The basic combinators of the λ-model (Qi∈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´s theorem.
Theorem 4 (Lo´s). 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). Then for every L-formula ϕ(x1, . . . , xn) and for every tuple (a1, . . . , an) ∈ Qi∈I Ai 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).
Theorem 6. Let M be a closed term and M = Sn∈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.
K := {e ⊆ N : e is finite} Kn = {e : n ∈ e}, for each n ∈ N.
Ke = {d : e ⊆ d}
for each e ⊆fin N. Hence F contains and F be a non-principal ultrafilter on P(K) that contains the set
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. 18. Kerth, R.: Isomorphism and equational equivalence of continuous λ-models, Studia
Logica 61, 403–415, 1998. 19. Kerth, R.: Isomorphisme et ´equivalence ´equationnelle entre mod`eles du λ-calcul,
Th`ese, Universit´e Paris 7, 1995. 20. Kerth, R.: Forcing in stable models of untyped λ-calculus, Indagationas Mathematicae 10 , 59–71, 1999. 21. Longo, G.: Set-theoretical models of λ-calculus : theories, expansions and isomorphisms, 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´emantique de la facilit´e en λ-calcul, Th`ese, Universit´e Paris 7, 1991.