{'fraction_non_alphanumeric': 0.06024715024133091, 'fraction_numerical': 0.017115667682196283, 'mean_word_length': 3.9989733059548254, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 13, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Reflexive combinatory algebras

We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer-Scott axiom of combinatory models, which indeed allows us to characterise an equationally definable counterpart of combinatory models. This new structure, called strongly reflexive combinatory algebra, admits a finite axiomatisation with seven closed equations, and the structure is shown to be exactly the retract of combinatory models. Lambda algebras can be characterised as strongly reflexive combinatory algebras which are stable. Moreover, there is a canonical construction of a lambda algebra from a strongly reflexive combinatory algebra. The resulting axiomatisation of lambda algebras by the seven axioms for strong reflexivity together with those for stability is shown to correspond to the axiomatisation of lambda algebras due to Selinger [J.Funct.Programming, 12(6), 549--566, 2002].


Introduction
The paper is written in the hope that the study of structures more general than the established notion of models of the lambda calculus (i.e., lambda algebras) should lead to a better understanding of the properties of these models. To this end, we introduce the notion of reflexivity in a general setting for combinatory algebras, and show how this property relates to models of the lambda calculus.
Recall that a lambda algebra is a combinatory algebra which satisfies Curry's five closed axioms (cf. Definition 6.11). Apart from this succinct axiomatisation, they have nice structural properties: lambda algebras are exactly the retracts of lambda models [11], the first-order models of lambda calculus characterised as lambda algebras satisfying the Meyer-Scott axiom (cf. Definition 4.6). Moreover, lambda algebras correspond to the reflexive objects in cartesian closed categories [6,12]. However, the choice of axioms for lambda algebras by Curry is elusive and looks arbitrary [1,11,13,6]. 1 On the other hand, lambda models can be characterised independently from lambda algebras as combinatory models which are stable [11]. Combinatory models can be characterised simply as combinatory algebras satisfying the Meyer-Scott axiom: [∀c ∈ A (ac = bc)] =⇒ ea = eb where e is a distinguished constant (often defined as s(ki)). Combinatory models are sufficient for interpreting lambda calculus. Moreover, there is a canonical way of stabilising a combinatory model to obtain a lambda model. In this sense, combinatory models encapsulate the essence of lambda models.
The observation above allows us to identify reflexivity as a fundamental property of combinatory algebras, which comes into play as follows: the combinatory completeness implies that there is a surjection ϕ : a → ax from a combinatory algebra A to its polynomial algebra A [x], whose section is provided by any choice of a defined λ-abstraction. The problem is that familiar abstraction mechanisms fail to respect the equality on the polynomials: the question is thus under what conditions this succeeds. Since ϕ is surjective, it induces an equivalence relation ∼ A on A which makes A/∼ A a combinatory algebra isomorphic to A [x]. The key observation is that the relation ∼ A is generated by finite schemas of equations on the elements of A. The above problem is then reduced to the condition, called reflexivity, that the constant e preserves these equations, namely a ∼ A b =⇒ ea = eb, (1.1) or in terms of polynomial algebra, ax = bx =⇒ ea = eb. Reflexivity yields seven simple universal sentences on A, which are equivalent to the requirement that an alternative choice of lambda abstraction, denoted λ † , is a well-defined operation on the polynomial algebra with one indeterminate. Then, taking λ † -closures of these seven sentences yields seven closed equations; these equations correspond to the requirement that the polynomial algebra be reflexive, or equivalently, that λ † be well-defined on polynomial algebras with any finite numbers of indeterminates. We call a combinatory algebra satisfying the seven closed equations as mentioned above a strongly reflexive combinatory algebra. The class of strongly reflexive combinatory algebras provides the algebraic (i.e., equational) counterpart to the notion of combinatory models in that they are precisely the retracts of combinatory models. Indeed, the condition (1.1) can be considered as an equational counterpart of the Meyer-Scott axiom. On the other hand, combinatory models can be characterised as strongly reflexive combinatory algebras satisfying the Meyer-Scott axiom. The relation between strongly reflexive combinatory algebras and lambda algebras can then be captured by stability [1, 5.6.4 (ii)]. Moreover, every strongly reflexive combinatory algebra can be made into a stable one (i.e., a lambda algebra) with an appropriate choice of constants. This passage to a lambda algebra also manifests itself in another form: we can associate a cartesian closed monoid (and thus a cartesian closed category

Lambda algebras
Meyer-Scott axiom u u Lambda models retracts 5 5 Figure 1: Relationship between various structures with a reflexive object) to a strongly reflexive combinatory algebra, from which the above mentioned lambda algebra is obtained. Furthermore, the resulting axiomatisation of lambda algebras with the seven closed equations and the axiom of stability naturally corresponds to the axiomatisation of lambda algebras due to Selinger [13]. Thus, the notion of strongly reflexive combinatory algebras serves as a common generalisation of those of combinatory models and lambda algebras, which moreover is finitely axiomatisable (see Figure 1).
Throughout this paper, we work with combinatory pre-models, combinatory algebras extended with distinguished elements i and e. Of course, these elements can be defined in terms of elements k and s as i = skk and e = s(ki). Nevertheless, the inclusion of e as a primitive, in particular, may be justified given its fundamental role in reflexivity. Accordingly, most of the notions for combinatory algebras mentioned above (such as polynomial algebra, reflexivity, strong reflexivity, stability) will be introduced for combinatory pre-models. The exceptions are lambda algebras and lambda models, which are defined with respect to the conventional notion of combinatory algebras with k and s as the only primitive constants.
Organisation In Section 2, we introduce the notion of combinatory premodels and establish some elementary properties of polynomial algebras. We also introduce an alternative representation of a polynomial algebra without using indeterminates. In Section 3, we introduce the notion of reflexivity for com-binatory pre-models, and show that this can be characterised by seven simple universal sentences. We also introduce a new abstraction mechanism, denoted λ † , in terms of which reflexivity can be rephrased. In Section 4, we introduce the notion of strong reflexivity for combinatory pre-models. We show that the class of strongly reflexive combinatory pre-models is axiomatisable with a finite set of equations which can be obtained by taking λ † -closures of seven axioms of reflexivity. We then show that strongly reflexive combinatory pre-models are exactly the retracts of combinatory models. In Section 5, we generalise the construction of a cartesian closed monoid from a lambda algebra to the setting of strongly reflexive combinatory pre-models. In Section 6, we introduce the notion of stability for strongly reflexive combinatory pre-models and characterise lambda algebras as stable strongly reflexive combinatory pre-models. We then clarify how this characterisation of lambda algebras corresponds to that of Selinger.

Combinatory pre-models
We begin with a preliminary on quotients of applicative structures.
Definition 2.1. An applicative structure is a pair A = (A, ·) where A is a set and · is a binary operation on A, called an application. The application a · b is often written as (ab), and parentheses are omitted following the convention of association to the left.
A homomorphism between applicative structures A = (A, · A ) and B = (B, · B ) is a function f : In what follows, we fix an applicative structure A = (A, ·). Definition 2.2. A congruence relation (or simply a congruence) on A is an equivalence relation ∼ on A such that Notation 2.3. If ∼ is a congruence on A, we often write a for the equivalence class [a] ∼ of ∼ whenever it is clear from the context. In this case, we write a ∼ b for [a] ∼ = [b] ∼ . The convention also applies to the other congruence relations in this paper.
For any binary relation R on A, there is a smallest congruence ∼ R on A containing R, which is inductively generated by the following rules: where a, b, c, d ∈ A. Then, there exists a unique homomorphism f : The fact that f is a homomorphism is clear. The uniqueness of f follows from the fact that π ∼R is surjective.
Throughout the paper, we work with the following notion of combinatory algebras where constants i and e are given as primitives. In what follows, homomorphisms mean homomorphisms between combinatory pre-models unless otherwise noted.
Notation 2.7. We often use a combinatory pre-model denoted by the letter A. Unless otherwise noted, we assume that A has the underlying structure A = (A, ·, k, s, i, e).
We recall the construction of a polynomial algebra, and establish its basic properties.
Definition 2.8. Let S be a set. The set T (S) of terms over S is inductively generated by the following rules: 1. a ∈ T (S) for each a ∈ S, 2. if t, u ∈ T (S), then (t, u) ∈ T (S).
Note that T (S) is a free applicative structure (T (S), ·) over S where t·u = (t, u).
In the rest of this section, we work over a fixed combinatory pre-model A. We assume that a countably infinite set X = {x i | i ≥ 1} of distinct indeterminates is given. For each term t ∈ T (X + A), FV(t) denotes the set of indeterminates that occur in t. As usual, t is said to be closed if FV(t) = ∅. Definition 2.9. Let ≈ X be the congruence relation on T (X + A) generated from the following basic relation: Similarly, for each n ∈ N, the congruence relation ≈ x1...xn on T ({x 1 , . . . , x n }+ A) is generated from the five basic equations above. The polynomial algebra A[x 1 , . . . , x n ] over A in indeterminates x 1 , . . . , x n is then defined as in (2.1), whose underlying set is the quotient of T ({x 1 , . . . , x n } + A) with respect to ≈ x1...xn . Let η n : A → A[x 1 , . . . , x n ] be the homomorphism defined by η n (a) = a. Notation 2.10.

We sometimes write η
. However, we sometimes use x for an arbitrary element of X (cf. Definition 2.16 and Definition 3.7). The meaning of x should be clear from the context.
3. Terms are often written without parentheses and commas; e.g., (t, s) will be written simply as ts. In most cases, the reader should be able to reconstruct the original terms following the convention of association to the left. However, there still remain some ambiguities; e.g., it is not clear whether ab for a, b ∈ A denotes (a, b) or ab ∈ A. In practice, this kind of distinction does not matter as terms are usually considered up to equality of polynomial algebras.
We recall some standard properties of polynomial algebras.
be a combinatory pre-model, and let n ≥ 1. For each homomorphism f : Proof. Let f : A → B be a homomorphism and b 1 , . . . , b n ∈ B. By the freeness of T ({x 1 , . . . , x n } + A), f uniquely extends to a homomorphism of applicative structures f : Since f is a homomorphism of combinatory pre-models, f satisfies the assumption of Proposition 2.5; hence it uniquely extends to a homomorphism f : Similarly, we have the following for A[X].
determines a functor T on the category of combinatory pre-models. The functor T sends each ho- Notation 2.14. As usual, the interpretation of a term t ∈ T (X + A) in A under a valuation ρ : N → A is the unique homomorphism · ρ : T (X + A) → A that extends the identity function id A : A → A with respect to the sequence (ρ(n)) n∈N . When t is a closed term, the interpretation t ρ does not depend on ρ, and thus can be written as t . Because of this, we often identify a closed term t with its interpretation t ∈ A and treat t as if it is an element of A. 3 It should be clear from the context whether closed terms are treated as terms (or elements of A[X]) or elements of A via the interpretation. When a closed term t is treated as an element of A[X], however, this distinction is irrelevant since we have t ≈ X t . The similar notational convention applies to closed terms of Next, recall that an object X of a category is a retract of another object Y if there exist morphisms s : X → Y and r : Y → X such that r • s = id X . In the context of the combinatory pre-model A, we have the following.
Proof. 1. Fix n ∈ N. By Lemma 2.12, there exists a unique homomorphism f : 4 In the other direction, by Lemma 2.11, there is a unique homomorphism ..,xn] by Lemma 2.11.
2. By Lemma 2.12, there exists a unique homomorphism f : In the other direction, there exists a unique homomorphism g : Then, it is straightforward to show that f and h are mutual inverse.
As a corollary of Proposition 2.15 (1) Before proceeding further, we recall one of the standard abstraction mechanisms for combinatory algebras (cf. Barendregt [1,7.3.4]).
Proof. By induction on the complexity of t.
Proof. By Lemma 2.11, the identity id A : A → A extends to a homomorphism id A : To see this, define the following terms (cf. Barendregt [1, Section 6.2]): In the other direction, there exists a unique homomorphism g : The rest of the section concerns an alternative representation of A [x] without using indeterminates. We begin with the following observation: since of f , and let π ∼A : A → A/∼ A be the natural map onto the (set theoretic) quotient of A by ∼ A . Then, f uniquely extends to a bijection γ : induces the following combinatory pre-model structure on A/∼ A : where a • b = sab (note that sabx ≈ x ax(bx)). The point of the following is that the relation ∼ A can be characterised directly without passing through A [x].
For each a ∈ A, define a 1 ∈ A by a 1 = ka.
Let ∼ 1 be the congruence relation on A 1 generated by the following relation: where a, b, c ∈ A. Then, the structurē where (A/∼ 1 , * 1 ) is the quotient of A 1 by ∼ 1 , is a combinatory pre-model.
The crucial axiom of ∼ 1 is Definition 2.19(6), as can be seen from the proof of the following theorem. Then, it is easy to see that f is a homomorphism of combinatory pre-models. In the other direction, a function g : A → A [x] defined by g(a) = ax is a homomorphism of applicative structures A 1 and A [x], and it is easy to see that g preserves (1)-(6) of Definition 2.19. By a similar argument as above, g extends uniquely to a homomorphism g : for each a ∈ A, where the last equality follows from the equation (6). Thus f and g are inverse to each other.
From the proof of Theorem 2.20, we can derive the following correspondence.
Proposition 2.21. For any combinatory pre-model A, we have As an immediate consequence, we have the following.

Reflexivity
The notion of reflexivity introduced below can be understood as an algebraic (rather than first-order) analogue of the Meyer-Scott axiom for combinatory models (cf. Definition 4.6). We still follow the convention of Notation 2.7.
In terms of polynomial algebras, reflexivity can be stated as follows (cf. Proposition 2.21). In the rest of the paper, we sometimes use Lemma 3.2 implicitly. Since the relation ∼ 1 is generated from the equations on the elements on A (cf. Definition 2.19), reflexivity can be characterised by a set of simple universal sentences on A.
Remark 3.4. The condition (7) in Proposition 3.3 does not have a counterpart in Definition 2.19, but it seems to be needed here. This is because e is required to preserve the congruence relation generated by (1)-(6) of Definition 2.19, and not the (weaker) equivalence relation.
Since the seven equations of Proposition 3.3 are simple universal sentences, we have the following corollary. Here, a substructure of a combinatory premodel A is a subset B ⊆ A which contains k, s, i, e, and is closed under the application of A.

Corollary 3.5. Reflexivity is closed under substructures and homomorphic images. In particular, it is closed under retracts.
As a consequence, reflexivity is preserved under the addition of further indeterminates to a polynomial algebra.
First, we note that the choice of abstraction mechanisms does not affect the isomorphism between A[x] andĀ 1 in Theorem 2.20.

Proposition 3.8. For any combinatory pre-model
Proof. Immediate from Proposition 2.21.
Nevertheless, λ † -abstraction enjoys some properties which λ * -abstraction need not. The following is crucial for our development. We can now characterise reflexivity in terms of λ † -abstraction. The proposition below says that reflexivity amounts to the requirement that the mapping t → λ † x.t be well-defined on the polynomials with one indeterminate.
The reflexivity of polynomial algebras admits similar characterisations.
Proof. By Remark 2.13, it suffices to show that items 2 and 3 are equivalent to the reflexivity of T n A. To this end, consider the following commutative diagram: : : • each π is the quotient map with respect to the congruence relation of Definition 2.9; • the other unnamed maps are the natural inclusions.
By induction on the complexity of terms, one can show that for each t, u ∈ T ({x 1 , . . . , x n+1 } + A) by Proposition 3.10. By equation (3.1) and the commutativity of the above diagram, (3.2) is equivalent to item (2). By the similar argument using Lemma 3.2, T n A is reflexive if and only if for each t, u ∈ T ({x 1 , . . . , x n } + A), which is equivalent to for each t, u ∈ T ({x 1 , . . . , x n }+A). By the commutativity of the above diagram, (3.3) is equivalent to item (3).
To close this section, we show that the reflexivity of A allows us to represent A[x] by a structure on the fixed-points of e. The reader should recall some notations from Definition 2.19. Definition 3.12. For a reflexive combinatory pre-model A, define or equivalently A * = {ea | a ∈ A} (cf. Lemma 3.9). Now, define a combinatory pre-model structure on A * by Proposition 3.13. If A is a reflexive combinatory pre-model, then A * ≃Ā 1 , and hence A * ≃ A [x].
Proof. Let f : A → A * be a function defined by f (a) = ea. As the proof of Proposition 3.3 shows, f extends uniquely to an isomorphismf :Ā 1 → A * of applicative structures. By the very definition ofĀ 1 and A * ,f is a homomorphism of combinatory pre-models.
Remark 3.14. Constructions similar to A * have appeared in the literature [8,2,13]. For example, Krivine [8, Section 6.3] defined an applicative structure B = (A * , •, kk, ks) with a • b = sab for a combinatory algebra A = (A, ·, k, s) under the slightly stronger condition than reflexivity. His condition consists of (1), (2), and (5)  It is clear that the structures A * and B coincide in Krivine's context when one ignores i and e; in this case, B is isomorphic to A [x]. The same representation of A [x] as B can be found in Selinger [13,Proposition 4] in the case where A is a lambda algebra. In view of this, Proposition 3.13 generalises the construction of the previous works.

Strong reflexivity
In this section, we introduce a stronger notion of reflexivity, which can be seen as an algebraic analogue of the Meyer-Scott axiom for combinatory models. In the following, the conventions of Notation 2.7 and Notation 2.14 still apply. We first note the following.

Lemma 4.2. A combinatory pre-model A is strongly reflexive if and only if
A[x 1 , . . . , x n ] is reflexive for each n ∈ N.
In particular, strong reflexivity implies reflexivity. From the above lemma, we obtain the following characterisation. Proposition 4.3. The following are equivalent for a combinatory pre-model A: ∈ FV(tu) and t, u ∈ T (X + A).
u for each x ∈ X and t, u ∈ T (X + A). Proof.
(1 ↔ 2) By Lemma 4.2, A is strongly reflexive if and only if Corollary 3.11(3) holds for each n ∈ N. This is equivalent to (2) by a suitable rearrangement of indeterminates FV(tu) ∪ {x} using Lemma 2.11.
In particular, the polynomial algebra of a strongly reflexive combinatory pre-model is closed under the ξ-rule with respect to the abstraction mechanism λ † x. In this way, each strongly reflexive combinatory pre-model gives rise to a model of the lambda calculus.
Next, we show that the class of strongly reflexive combinatory pre-models is axiomatisable with a finite set of closed equations which can be obtained by taking λ † -closures of both sides of the equations (1)-(7) of Proposition 3.3.

Theorem 4.4. A combinatory pre-model A is strongly reflexive if and only if it satisfies the following equations:
Note that the equations (1)-(7) in Theorem 4.4 are closed in the sense that they correspond to terms built up from k, s, i, e only. Thus, we have the following.
Proposition 4.5. If A is strongly reflexive and f : A → B is a homomorphism of combinatory pre-models, then B is strongly reflexive.
Next, we relate strongly reflexive combinatory pre-models and combinatory models.
Definition 4.6 (Meyer [11]). A combinatory model is a combinatory pre-model A satisfying the Meyer-Scott axiom: Note that every combinatory model is reflexive by Lemma 3.2. Proof. Let A be a combinatory model. It suffices to show that Corollary 3.11(3) holds for n = 1. Let t, u ∈ T ({x} + A) be such that ty ≈ xy uy. Fix c ∈ A.

Cartesian closed monoids
In this section, we generalise the construction of a cartesian closed category with a reflexive object from a lambda algebra due to Scott [12] (see also Koymans [6]) to the setting of strongly reflexive combinatory pre-models. To this end, we construct a cartesian closed monoid from a strongly reflexive combinatory premodel. The connection between cartesian closed monoids and cartesian closed categories with reflexive objects will be reviewed toward the end of this section. The reader is referred to Koymans [7, Chapter 2], Lambek and Scott [10, Part I, 15-17], and Hyland [5,4] for a detailed account of cartesian closed monoids and their relation to untyped lambda calculus.
Throughout this section, we work over a fixed reflexive combinatory premodel A = (A, ·, k, s, i, e).
First, we construct a monoid out of A. For each a, b ∈ A, define Lemma 5.1. For each a, b, c ∈ A, we have Proof. We use Lemma 3.2 and Lemma 3.9.
We recall the following construction from Definition 3.12: Define I ∈ A * by I = ei.
Proof. 1. We verify (1a)-(1b) of Definition 5.3. Fix a, b, c ∈ A * : Thus, the required equations follow from Lemma 3.2 and Lemma 3.9. 2. We verify (2c)-(2f) of Definition 5.3. Fix a ∈ A * : Since A is strongly reflexive (i.e., A [x] is reflexive), we have the required equations as in the first case.
Now, let C A be the Karoubi envelope of the monoid (A * , •, I) seen as a singleobject category (see Koymans [6,Definition 4.1]; Barendregt [1,5.5.11]). If A is strongly reflexive, then C A is a cartesian closed category with a reflexive object U = I by Theorem 5.4 (see Koymans [6,Section 7]). Then, the homset C A (T, U ), where T is a terminal object of C A , has a structure of a lambda algebra, and when A is a lambda algebra, C A (T, U ) is isomorphic to A [6, Sections 3 and 4]. For a strongly reflexive combinatory pre-model A, in general, we would not have an isomorphism between A and C A (T, U ). Instead, we obtain a certain lambda algebra structure on (A, ·) induced by C A (T, U ), which is analogous to the construction of a lambda model from a combinatory model [11,Section 6]. This is the subject of the next section.

Stability
It is known that lambda models are combinatory models which are stable (Barendregt [1, 5.6,3, 5.6.6], Koymans [7,Section 1.4]). Having seen that strongly reflexive combinatory pre-models are the retracts of combinatory models in Section 4, it is now straightforward to establish an algebraic analogue of this fact for lambda algebras.
We begin with the following construction, which extends e to finitely many arguments. Note that the conventions of Notation 2.7 and Notation 2.14 continue to apply. Definition 6.1 (Scott [12]). For a combinatory pre-model A, define ε n ∈ A for each n ≥ 1 inductively by ε n+1 = s(ke)(s(kε n )).
If A is a strongly reflexive combinatory pre-model, then the element ε n a for each a ∈ A admits a succinct characterisation. Lemma 6.3. If A is strongly reflexive, then ε n a = λ † x 1 . . . x n .ax 1 · · · x n for each a ∈ A and n ≥ 1. 7 Proof. By straightforward induction n ∈ N.
The construction ε n provides yet another characterisation of strong reflexivity.

Proposition 6.4. A combinatory pre-model A is strongly reflexive if and only if
ax 1 · · · x n ≈ x1...xn bx 1 · · · x n =⇒ ε n a = ε n b for each n ≥ 1 and a, b ∈ A.
The notion of stability for combinatory models also makes sense for strongly reflexive combinatory pre-models (cf. Barendregt [1, 5.6.4]; Meyer [11, Section 6]; Scott [12]). 8 Definition 6.5. Let A = (A, ·, k, s, i, e) be a strongly reflexive combinatory pre-model. Then, A is said to be stable if A combinatory model is stable if it is stable as a strongly reflexive combinatory pre-model (cf. Lemma 4.7).
In a stable strongly reflexive combinatory pre-model, the constants e and i coincide with the usual construction of these constants from k and s. Lemma 6.6. If A is strongly reflexive and stable, then i = skk and e = s(ki).
Since A is stable and reflexive, we have i = ei = e(skk) = skk. Similarly, we have e = s(ki).
The following is immediate from Lemma 6.2. Lemma 6.7. If A is a combinatory pre-model such that i = skk and e = s(ki), then s = ε 3 s implies i = ε 1 i and e = ε 2 e. Remark 6.8. By the above two lemmas, the notion of stable combinatory models in the sense of Definition 6.5 agrees with the corresponding notion in the literature which does not include i as a primitive [1, 5.6.4].
We recall the connection between stable combinatory models and lambda models. As the definition of the latter, we adopt the following characterisation. Definition 6.9 (Barendregt [1, 5.6.3]). A lambda model is a combinatory algebra A = (A, ·, k, s) such that the structure (A, ·, k, s, i, e), where i = skk and e = s(ki), is a combinatory model satisfying k = ε 2 k and s = ε 3 s.
The following is immediate from Lemma 6.6 and Lemma 6.7. We establish an analogue of the above proposition for strongly reflexive combinatory pre-models and lambda algebras. The following characterisation of lambda algebras is often attributed to Curry. Theorem 6.16. If A is a strongly reflexive combinatory pre-model, then (A, ·, ε 2 k, ε 3 s) is a lambda algebra.
Proof. If A is strongly reflexive, then A[X] is a combinatory model by Theorem 4.8. Then, (A[X], ⋆, ε 2 k, ε 3 s) is a lambda model by Proposition 6.15; hence it is a lambda algebra by Proposition 6.12. Since A is a retract of A[X], we see that (A, ·, ε 2 k, ε 3 s) is a lambda algebra.
One can also check that the stable strongly reflexive combinatory pre-model determined by the lambda algebra (A, ·, ε 2 k, ε 3 s) is of the form (A, ·, ε 2 k, ε 3 s, ε 1 i, ε 2 e). Remark 6.17. As we have noted at the end of Section 5, a strongly reflexive combinatory pre-model A determines a cartesian closed category with a reflexive object, which induces a lambda algebra structure on (A, ·). One can verify that the constants k and s of the lambda algebra thus obtained coincide with ε 2 k and ε 3 s, respectively.
We now understand that stable strongly reflexive combinatory pre-models and lambda algebras are equivalent. However, compared with the five axioms of lambda algebras (Definition 6.11), we have seven axioms of strong reflexivity (Definition 4.1) and four axioms of stability (6.1). Nevertheless, since i and e are definable from k and s in a stable strongly reflexive combinatory pre-model, some of the axioms of strong reflexivity and stability concerning the properties of i and e become redundant. Specifically, consider the following conditions for a combinatory pre-model A = (A, ·, k, s, i, e) : (CA) i = skk and e = s(ki); (L1) k = ε 2 k and s = ε 3 s; (L2) The equations 1, 2, 5, and 6 of Definition 4.1:

Proof. By Theorem 4.8, A is stable if and only if A[X]
is stable as a combinatory model. By Lemma 6.21, the latter is equivalent to ek ≈ X k, es ≈ X s, e(kt) ≈ X kt, e(st) ≈ X st, e(stu) ≈ X stu for all t, u ∈ T (X + A), which in turn is equivalent to (6.2). Proposition 6.22 allows us to see the connection between (L1) and (L2) and the following axiomatisation of lambda algebras by Selinger.  Proof. By Proposition 6.22, the conditions (L1) and (L2) imply the nine conditions above. Conversely, the proofs of Lemma 6.18 and Lemma 6.19 show that the conditions (c) and (e)-(i) imply that the structure (A, ·, k, s, i, e) with i = skk and e = s(ki) is a strongly reflexive combinatory pre-model; hence they imply (L2). Then, (L1) follows from (a)-(e) by Proposition 6.22.
The correspondence between (L1)-(L2) and (a)-(i) are evident: in (a)-(i) the conditions (L1) is broken down into an equivalent set of smaller pieces and some e's are omitted from (L2) using (c) and (e).