Disproving Termination of Non-Erasing Sole
Combinatory Calculus with Tree Automata
Keisuke Nakano1[0000−0003−1955−4225]
Munehiro Iwami2[0000−0001−9925−450X]
1

Tohoku University, Sendai, Miyagi, Japank.nakano@acm.org
2
Shimane University, Matsue, Shimane, Japan
munehiro@cis.shimane-u.ac.jp

Abstract. We study the termination of sole combinatory calculus, which
consists of only one combinator. Speciﬁcally, the termination for nonerasing combinators is disproven by ﬁnding a desirable tree automatonwith a SAT solver as done for term rewriting systems by Endrullis andZantema. We improved their technique to apply to non-erasing solecombinatory calculus, in which it suﬃces to search for tree automata witha ﬁnal sink state. Our method succeeds in disproving the termination of
8 combinators, whose termination has been an open problem.
Keywords: Combinatory calculus · Non-termination · Tree automata.

1 Introduction
Combinatory logic [15, 3] has been used in computer science as a theoreticalmodel of computation and also as a basis for the design of functional programming languages [18, 13]. It can be viewed as a variant of lambda calculus, inwhich a limited set of combinators, primitive functions without free variables,
is used instead of lambda abstractions.
Combinators in combinatory logic are deﬁned as Zx1 x2 . . . xn → e where
Z is a combinator, x1 , . . . , xn are variables, and e is built from the variables
with a function application. It is known that a small set of combinators
can deﬁne a combinatorial calculus that is suﬃcient to cover all computablefunctions. Well-known sets of such combinators are {S, K} and {B, C, K, W}
with Sxyz → xz(yz), Kxy → x, Bxyz → x(yz), Cxyz → xzy, and Wxy →xyy [1].
The subject of this paper is sole combinatory calculus, which consists of
only one combinator. There have been several studies on sole combinatory
calculi. Waldmann [19] investigated the S combinator to provide a procedurethat decides whether an S-term, built from S alone, has a normal form andfurther showed that the set of normalizing S-terms is recognizable. Probst andStuder [14] proved that the sole combinatory calculus with the J combinator,
deﬁned by Jxyzw → xy(xwz) is strongly normalizing; that is, no J-term

2

K. Nakano and M. Iwami

Pxyz → z(xyz) P3 xyz → y(xzy) D1 xyzw → xz(yw)(xz) D2 xyzw → xw(yz)(xw)
Φxyzw → x(yw)(zw)
S2 xyzw → xzw(yzw)Φ2 xyzw1 w2 → x(yw1 w2 )(zw1 w2 )S3 xyzwv → xy(zv)(wv)

S1 xyzw → xyw(zw)S4 xyzwv → z(xwv)(ywv)Fig. 1. Combinators and their reduction rules

has an inﬁnite reduction sequence. Ikebuchi and Nakano [6] showed thatthe sole combinatory calculus with the B combinator is strongly normalizing
and characterized by equational axiomatization for proving the looping andnon-looping properties of repetitive right applications.
This paper concerns the non-termination of sole combinatory calculi, where
termination means that no term has an inﬁnite reduction. Let us say that a
combinator is terminating when the corresponding sole combinatory calculus
is terminating. Iwami [8] has investigated the termination of 37 combinators
introduced in Smulyan’s book [16] and has reported that 10 of them shown in
Fig. 1 are of unknown termination.
We disprove the termination of 8 of the 10 combinators. The main idea ofdisproving the termination is to give a non-empty recognizable set of terms
closed under the reduction as Endrullis and Zantema have done [4]. They
showed that a SAT solver can ﬁnd the corresponding tree automaton. We improve their method by showing that it suﬃces to search for tree automata witha ﬁnal sink state in our setting and by reducing the number of variables in the
SAT problem. Our implemetation disproves the termination of 8 combinators.

2 Preliminaries
A signature (or alphabet) Σ is a non-empty ﬁnite set of function symbols, eachwith a ﬁxed natural number called arity (or rank)3 . The set of all function
symbols of arity n in Σ is written as Σ (n) . We may write f (n) for f ∈ Σ (n) .
A function symbol of arity 0 is called a constant symbol. A set of variables is acountably inﬁnite set disjoint from Σ. For a set V of variables, a set of terms
over Σ, denoted by TΣ (V), is inductively deﬁned as the smallest set S such thatV ⊆ S and t1 , . . . , tn ∈ S implies f (t1 , . . . , tn ) ∈ S for every f ∈ Σ (n) . The
set of variables occurring in t ∈ TΣ (V) is denoted by FV(t). In the rest of thepaper, the set V of variables is ﬁxed and contains x, x1 , x2 , . . . as its elements.
A substitution is a ﬁnite map from variables to terms. We write dom(α) for
the domain of a substitution α. For a term t and a substitution α, we denoteby tα an instance of t, a term obtained by replacing every variable x in twith α(x). Substitutions may be represented in the set notation as usual: wewrite {x1 7→ t1 , . . . , xn 7→ tn } for substitution α when dom(α) = {x1 , . . . , xn }3

We use the terminology of term rewriting systems, whereas deﬁnitions are given
alongside that of formal language theory for the readers, e.g., a tree and a rank informal language are called a (ground) term and an arity in term rewriting, respectively.

Disproving Termination of Non-Erasing Sole Combinatory Calculus with TA

3and α(xi ) = ti holds for each i and, in particular, ∅ for substitution α whendom(α) = ∅. A term containing no variables is called a ground term, and the setof ground terms is written as TΣ , i.e., TΣ = TΣ (∅). A context C is a term overΣ ∪ {□} with a constant symbol □, called a hole, such that □ occurs exactly
once in C. For a context C and a term t, we denote by C[t] a term obtainedby replacing the hole in C with t. We write CΣ (V) for the set of contexts; inparticular, V is omitted from the notation if it is empty, i.e., CΣ = CΣ (∅). A
term s ∈ TΣ is a subterm of t ∈ TΣ if t = C[s] holds with some C ∈ CΣ . The setof all subterms of t is written as Sub(t).
A term rewriting system (TRS) R over Σ is a set of rewriting rules of the forml → r with l, r ∈ TΣ (V) where FV(r) ⊆ FV(l). A TRS R is said to be non-erasing
if FV(r) = FV(l) holds for every rule l → r ∈ R. A TRS R is said to be left-linear
if each variable in FV(l) occurs exactly once in l for every rule l → r ∈ R.
A left-linear TRS R is said to be orthogonal if every pair of two (possibly thesame) rules in R has no overlapping, which means that the left-hand side of
one rule is not uniﬁable with any non-variable subterm of the left-hand sideof the other rule. A rewrite relation →R over TΣ (V) induced by R is deﬁned by{(C[lα], C[rα]) | C ∈ CΣ (V), l → r ∈ R, α : FV(l) → TΣ (V)}. We write →∗R for
the reﬂexive and transitive closure of →R . A term t is called a redex of R if t = lαholds for some l → r ∈ R and substitution α; that is, a redex means a reducible
part of a term. A term t is said to be in normal form with respect to R if there isno term u such that t →R u; in other words, no subterm of t is a redex of R. A setof normal forms with respect to R is denoted by NF(R). A TRS R is terminatingor strongly normalizing if no inﬁnite rewrite sequence t0 →R t1 →R t2 →R . . .
with ti ∈ TΣ (V) and i ∈ N exists. A TRS R is weakly normalizing if for every
term t there exists a term u ∈ NF(R) such that t →∗R u holds. A rewrite steps →R t is innermost, denoted by s →iR t, if no proper subterm of the contracted
redex is itself a redex [12], that is, the relation →iR is deﬁned by a subset of →R
as {(C[lα], C[rα]) | C ∈ CΣ (V), l → r ∈ R, α : FV(l) → TΣ (V), Sub(lα) ⊆NF(R) ∪ {lα}}. A TRS R is weakly innermost normalizing if for every term t there
exists a term u ∈ NF(R) such that t →iR ∗ u holds. A set S of terms is closed under
R if for every t ∈ S, t →R u implies u ∈ S.
A (non-deterministic bottom-up) tree automaton is a quadruple A = hQ, Σ,F, ∆i where Q is a ﬁnite set of states, F ⊆ Q is a set of ﬁnal states, and ∆is a set of state transition rules of the form f (q1 , . . . , qn ) ⇝ q with f ∈ Σ (n) ,q1 , . . . , qn , q ∈ Q. The set ∆ can be viewed as a TRS where ⇝ is used insteadof →. The arrow ⇝∆ is used for the rewrite relation over TΣ∪Q induced by therules in ∆ where the subscript ∆ may often be omitted if no confusion arises.
We write ⇝∗ for the reﬂexive and transitive closure of ⇝. The set L(A, q) forq ∈ Q is deﬁned by L(A,∪q) ≡ {t ∈ TΣ | t ⇝∗∆ q}. The set of terms accepted by
A is deﬁned by L(A) ≡ q∈F L(A, q). A state q is said to be reachable if L(A, q)
is not empty. A state q is called a sink state when, for every f ∈ Σ (n) (n > 0)
and q 0 , q1 , . . . , qn ∈ Q with qi = q for some i, f (q1 , . . . , qn ) ⇝ q ∈ ∆ holds but
f (q1 , . . . , qn ) ⇝ q 0 ∈ ∆ does not hold with q 0 6= q. When q is a sink state, it iseasy to show that t ∈ L(A, q) implies C[t] ∈ L(A, q) for every context C ∈ CΣ4

K. Nakano and M. Iwami

and every ground term t ∈ TΣ . Two tree automata A1 and A2 are said to beequivalent if L(A1 ) = L(A2 ) holds.

3 Termination of sole combinatory calculus
A combinatory calculus is speciﬁed by certain kinds of combinators andreduction rules for each combinator. A reduction rule for a combinator Z
has the form Z x1 . . . xn → e where e is built by combining x1 , . . . , xn
with function application. One of the most familiar combinatory calculi isgiven by the S and K combinators deﬁned by S x1 x2 x3 → x1 x3 (x2 x3 )and K x1 x2 → x1 . The calculus is well known to be Turing-complete in
the sense that these two combinators are suﬃcient to represent all computable functions. Reductions in combinatory calculus are easily simulated
by a TRS using the set of constant symbols for combinators and a binary
function symbol @ for function application. For example, reduction rules for
the S and K combinatory calculus can be represented by a TRS consistingof @(@(@(S, x1 ), x2 ), x3 ) → @(@(x1 , x3 ), @(x2 , x3 )) and @(@(K, x1 ), x2 ) → x1 ,which is obviously non-terminating because of the Turing-completeness of thecorresponding reduction system.
In this paper, we are interested in the question for sole combinatory calculus, which is built only by one combinator. We start with formal deﬁnitions ofseveral notions on the sole combinatory calculus in terms of term rewriting. For
Z is a combinator, we denote by ΣZ a signature consisting of a constant Z andbinary function symbol @. A Z-term, which is built only from Z in combinatory
calculus, is represented by a term in TΣ . A sole combinatory calculus RZ induced
by a combinator Z is a TRS over TΣZ where RZ is a singleton set of a left-linear
rule of the form @(. . . @(@(Z, x1 ), x2 ) . . . , xn ) → e with a term e built only from@ and variables x1 , . . . , xn . A combinator Z is said to be terminating if RZ is
terminating. It is known that B [6] and J [14] are terminating while O [9, 7, 4]
and S [19] are not.
The following lemma allows us to consider only the case of weakly innermost normalizing instead of terminating since the rule of sole combinatory
calculus is orthogonal.
Lemma 1 ([11, Theorem 11]). An orthogonal TRS R is terminating if and only
if R is weakly innermost normalizing.
The readers might recall a similar result shown by Church [2] that an
orthogonal non-erasing TRS R is terminating if and only if R is weakly
normalizing. Since we are concerned with non-erasing combinatory calculus,
this result may seem more convenient. However, in the context of the present
work, we intend to employ the above lemma because the ‘innermost’ condition
plays a crucial role in our method which will be detailed later.

Disproving Termination of Non-Erasing Sole Combinatory Calculus with TA

5

4 Disproving termination of combinators by tree automata
Endrullis and Zantema have proposed a procedure for disproving weakly andstrongly normalizing by ﬁnding tree automata that disprove termination ofarbitrary forms of left-linear TRSs. This section ﬁrst explains how to disprove
termination using the search for tree automata, and shows that it is suﬃcient
to ﬁnd a restricted form of tree automata to disprove the termination of
non-erasing combinators. Then, we present how to ﬁnd such tree automata
with a SAT solver. Finally, we show the non-termination of 8 combinators with
our implementation of the method.
4.1 Disproving termination with tree automata
The idea of disproving termination of a TRS R by Endrullis and Zantema is
to ﬁnd a non-empty set of reducible ground terms (i.e., not in normal form),
which is closed under the rules in R. It is easy to see that the existence of such a
set implies that R is not weakly normalizing because any reduction from a termin the set is always inﬁnite. Endrullis and Zantema considered the case where
the set is recognizable by a tree automaton as deﬁned below, though they did
not give a name to it.
Deﬁnition 2. A termination-disproving automaton (TDA) for a left-linear TRS R
is a tree automaton A = hQ, Σ, F, ∆i such that (2-1) there exists a state q ∈ Fthat is reachable, (2-2) L(A) ∩ NF(R) = ∅, and (2-3) t ∈ L(A, q) implies u ∈L(A, q) for all q ∈ Q and t, u ∈ TΣ with t →R u.
It is easy to see that the set L(A) for a TDA A for R can disprove weaknormalizability of R: the conditions (2-1) and (2-2) allow us to choose a term
not in normal form, and the conditions (2-2) and (2-3) force any reduction fromthe term to be inﬁnite. The condition (2-3) is a bit strong in the sense thatit requires every set L(A, q) with q ∈ Q to be closed under reductions in R.
The last condition might be relaxed to require the closure property only forﬁnal states in QF . However, we require it for all states in Q to make the SAT
solver–based disproof search easier as done by Endrullis and Zantema.
As we will see later, it is suﬃcient to ﬁnd a TDA with a sink state as the ﬁnal
state. The restricted form of tree automata is deﬁned as follows.
Deﬁnition 3. A termination-disproving automaton with a ﬁnal sink (TDA-S) for
an orthogonal TRS R is a tree automaton A = hQ, Σ, {qF }, ∆i with qF ∈ Q suchthat (3-1) qF is sink and reachable, (3-2) L(A)∩NF(R) = ∅, and (3-3) t ∈ L(A, q)
implies u ∈ L(A, q) ∪ L(A) for all q ∈ Q and t, u ∈ TΣ with t →iR u.
We assume here that R is orthogonal, which is stronger than left-linear,because every sole combinatory calculus is orthogonal. A major diﬀerence
from TDAs is that a TDA-S has a sink state qF as the unique ﬁnal state. The
sink state is reachable so that L(A) is non-empty. In addition, it requires theclosure property only under the innermost reduction and allows the reduction

6

K. Nakano and M. Iwami

onto L(A). The latter relaxation corresponds to a minor improvement done by
Endrullis and Zantema where the closure property allows the reduction onto
terms accepted by the ‘larger’ states in the total order over states, which will
be used for reachability checking with Lemma 6. The following theorem statesthat the existence of a TDA-S for an orthogonal TRS R implies that R is not
terminating.
Theorem 4. An orthogonal TRS R is not terminating if a TDA-S for R exists.
Proof. Let A = hQ, Σ, {qF }, ∆i be a TDA-S for an orthogonal TRS R. By
Lemma 1, it suﬃces to show that R is not weakly innermost normalizing. We
prove by contradiction that for all t ∈ L(A), no reduction sequence from t
reaches a normal form, which disproves the weak innermost normalizabilityof R due to the non-emptiness of L(A) implied by the (3-1) condition of A.
Suppose that there exists a term such that a reduction sequence starting fromthe term reaches a normal form. Let t ∈ L(A) be such a term which has theshortest reduction sequence t = t0 →iR t1 →iR · · · →iR tn with tn ∈ NF(R).
From the (3-2) condition, t is not in normal form, i.e., n > 0. From the (3-3)
condition with q = qF , t1 ∈ L(A) holds. Since we have a reduction sequence
from t1 ∈ L(A) which reaches a normal form, it contradicts the assumptionthat the reduction sequence from t is the shortest one.
We will try to ﬁnd a TDA-S (which has exactly one ﬁnal state) to disprove thetermination of a sole combinatory calculus instead of a TDA. Since the disproof
search will be done by ﬁxing the number of states and increasing it iteratively,
we have to show that the number of states of a TDA-S is not required to be aslarge as that of a TDA. Note that we do not need to ﬁnd a TDA-S equivalent toa TDA if it exists. It is well-known that every non-deterministic tree automaton
can be converted into an equivalent one that has exactly one ﬁnal state (byintroducing a fresh ﬁnal state) but it may have one more state than the originalone. The following lemma guarantees that the number of states of a TDA-S is
not required to be larger than that of a TDA to disprove the termination of an
orthogonal TRS. The proof idea is to construct a TDA-S A from a given TDA A0
by forcing a ﬁnal state of A0 to be the ﬁnal sink state of A and removing statesthat accept only terms whose subterm is accepted by the sink state.
Lemma 5. Let R be an orthogonal TRS. If a TDA A0 = hQ0 , Σ, F0 , ∆0 i for R
exists, then a TDA-S A = hQ, Σ, {qF }, ∆i for R also exists with |Q| ≤ |Q0 |.
Proof. Let A0 = hQ0 , Σ, F0 , ∆0 i be a TDA for an orthogonal TRS R, where A0
satisﬁes the conditions (2-1), (2-2), and (2-3). Without loss of generality, allstates in Q0 are reachable; otherwise, we could remove unreachable states fromQ0 . From (2-1) of A0 , the set F0 is not empty, hence we can choose a ﬁnal stateqF ∈ F0 . Let LF ⊆ TΣ and QF ⊆ Q0 be deﬁned by LF = {C[t] | C ∈ CΣ , t ∈L(A0 , qF )} and QF = {q ∈ Q0 | L(A0 , q) ⊆ LF }, respectively. Note that qF ∈QF holds in particular. Then we deﬁne a tree automaton A = hQ, Σ, {qF }, ∆iDisproving Termination of Non-Erasing Sole Combinatory Calculus with TA

7

with Q = (Q0 \ QF ) ∪ {qF } and ∆ = ∆1 ∪ ∆2 where∆1 = {f (q1 , . . . , qn ) ⇝ q ∈ ∆0 | {q1 , . . . , qn } ⊆ Q0 \ QF , q ∈ Q} and∆2 = {f (q1 , . . . , qn ) ⇝ qF | f ∈ Σ (n) , qF ∈ {q1 , . . . , qn } ⊆ Q}
so that qF is to be a sink ﬁnal state in A. Since |Q| ≤ |Q0 | obviously holds, it
suﬃces to show that A is a TDA-S for R.
Before proving that A is a TDA-S for R, we show(5-1) t ∈ LF if and only if t ∈ L(A, qF ),(5-2) t ∈ L(A, q) implies t ∈ L(A0 , q) for all q ∈ Q0 \ QF , and(5-3) t ∈ L(A0 , q) implies t ∈ L(A, q) ∪ L(A, qF ) for all q ∈ Q0 \ QF ,for all t ∈ TΣ . These statements can be shown by simultaneous induction on the
structure of t. Suppose that t = f (t1 , . . . , tn ) with f ∈ Σ (n) and t1 , . . . , tn ∈ TΣ .
On the (5-1) statement, we examine two cases according to whether ti ∈ LF
or not for each i. In the case where ti ∈ LF holds for some 1 ≤ i ≤ n, the‘if’-statement of (5-1) is obvious from the deﬁnition of LF , hence we show the‘only if’-statement. Since ti ∈ L(A, qF ) holds from the induction hypothesis,
we have t ∈ L(A, qF ) using a transition rule in ∆2 . Thus, the ‘only if’-statementof (5-1) also holds. In the case where ti 6∈ LF holds for all 1 ≤ i ≤ n, we
ﬁrst show the ‘if’-statement of (5-1). Assume t ∈ L(A, qF ) holds. Then, there
exists q1 , . . . , qn ∈ Q such that f (q1 , . . . , qn ) ⇝ qF ∈ ∆ and ti ∈ L(A, qi ) for
every 1 ≤ i ≤ n. If qi = qF holds for some 1 ≤ i ≤ n, then we have ti ∈ LF
from the induction hypothesis, hence t ∈ LF . If qi ∈ Q0 \ QF holds for all
1 ≤ i ≤ n, then the transition rule is in ∆1 and we have ti ∈ L(A0 , qi ) fromthe induction hypothesis of (5-2) for all i. Using the same transition rule, wehave t ∈ L(A0 , qF ), hence t ∈ LF . Therefore, the ‘if’-statement of (5-1) holds.
For the ‘only if’-statement of (5-1), assume t ∈ LF . Since ti 6∈ LF holds for all
1 ≤ i ≤ n, we have t ∈ L(A0 , qF ) owing to the deﬁnition of LF . Then, there
exists q1 , . . . , qn ∈ Q0 such that f (q1 , . . . , qn ) ⇝ qF ∈ ∆0 and ti ∈ L(A0 , qi ) for
every 1 ≤ i ≤ n. Note that ti 6∈ LF implies qi ∈ Q0 \ QF by the deﬁnition of
QF . Thus, the transition rule is in ∆1 and we have ti ∈ L(A, qi ) ∪ L(A, qF ) fromthe induction hypothesis of (5-3). When ti ∈ L(A, qi ) holds for all i, we havet ∈ L(A, qF ) using the same transition rule. When ti ∈ L(A, qF ) holds for some1 ≤ i ≤ n, we have t ∈ L(A, qF ) using the transition rule in ∆2 . Therefore, the‘only if’-statement of (5-1) holds.
On the (5-2) statement, assume t ∈ L(A, q) with q ∈ Q0 \ QF , that is, q 6= qF .
Then, there exist q1 , . . . , qn ∈ Q such that f (q1 , . . . , qn ) ⇝ q ∈ ∆ and ti ∈L(A, qi ) for every 1 ≤ i ≤ n. Note that qi 6= qF holds for all 1 ≤ i ≤ n becauseof the construction of ∆. Since we have qi ∈ Q0 \ QF for every 1 ≤ i ≤ n, thetransition rule is in ∆1 and ti ∈ L(A0 , qi ) holds from the induction hypothesis
for every 1 ≤ i ≤ n. Using the same transition rule, we have t ∈ L(A0 , q).
Therefore, (5-2) holds.
On the (5-3) statement, assume t ∈ L(A0 , q) with q ∈ Q0 \ QF . Then, there
exist q1 , . . . , qn ∈ Q0 such that f (q1 , . . . , qn ) ⇝ q ∈ ∆0 and ti ∈ L(A0 , qi ) for
every 1 ≤ i ≤ n. When qi ∈ QF holds for some 1 ≤ i ≤ n, we have ti ∈ LF by

8

K. Nakano and M. Iwami

the deﬁnition of QF , hence ti ∈ L(A, qF ) holds from the induction hypothesisof (5-1). Using a transition rule in ∆2 , we have t ∈ L(A, qF ). When qi ∈ Q0 \ QF
holds for all 1 ≤ i ≤ n, the transition rule is in ∆0 and we have ti ∈ L(A, qi ) ∪L(A, qF ) from the induction hypothesis for all 1 ≤ i ≤ n. If ti ∈ L(A, qi ) holds
for all i, then we have t ∈ L(A, q) using the same transition rule. If ti ∈ L(A, qF )holds for some i, then we have t ∈ L(A, qF ) using the transition rule in ∆2 .
Therefore, (5-3) holds.
Now we are ready to show that A is a TDA-S for R. Concerning the (3-1)
condition, the set LF is not empty since qF is reachable in A0 due to the (21) condition of A0 . Then we have qF is reachable also in A owing to (5-1). In
addition, qF is a sink state in A, hence the (3-1) condition holds for A.
The (3-2) condition is shown by contradiction. Suppose that there exists aterm t ∈ L(A) ∩ NF(R). Then we have t ∈ LF from (5-1), hence t = C[t0 ] holds
for some C ∈ CΣ and t0 ∈ L(A0 , qF ). From t0 ∈ L(A0 , qF ) ⊆ L(A0 ) and the (2-2)
condition of A0 , we have t0 6∈ NF(R), and thus t = C[t0 ] 6∈ NF(R) holds. This
contradicts the assumption, hence the (3-2) condition holds for A.
Concerning the (3-3) condition, assume that we have t ∈ L(A, q) with q ∈ Q
and t →iR u for some u ∈ TΣ . In the case of q = qF , we have t ∈ LF by(5-1), hence t = C[t0 ] holds for some C ∈ CΣ and t0 ∈ L(A0 , qF ). Since thet0 is not in normal form by the (2-2) condition of A0 and →iR is an innermost
relation, we have either u = C[u0 ] with t0 →iR u0 ∈ TΣ or u = D[t0 ] withsome D ∈ CΣ . In the former case, we have u0 ∈ L(A0 , qF ) by t0 ∈ L(A0 , qF ) andthe (2-3) condition of A0 . Then u0 ∈ L(A, qF ) holds due to u0 ∈ L(A0 , qF ) ⊆ LF
and (5-1). Since qF is a sink state in A, u ∈ L(A, qF ) holds. In the latter case,u ∈ L(A, qF ) holds because t0 ∈ L(A0 , qF ) ⊆ LF implies t0 ∈ L(A, qF ) by
(5-1) and qF is a sink state in A. Therefore, the (3-3) condition holds for A
in the case of q = qF . In the case of q ∈ Q0 \ QF , we have t ∈ L(A0 , q) by(5-2), hence u ∈ L(A0 , q) holds by the (2-3) condition of A0 . Since we haveu ∈ L(A, q) ∪ L(A, qF ) by (5-3), the (3-3) condition holds for A in the case ofq ∈ Q0 \ QF .
Since we try to ﬁnd a TDA-S in the ascending order of the number ofstates as Endrullis and Zantema have done for a TDA, one of the TDA-Ss fora given TRS with the smallest number of states can be found if it exists. It
might be possible to ﬁnd a TDA-S even with a smaller number of states thana TDA because of the relaxed closure property (3-3). Our experiment resultsin Section 4.3 do not show such a case, though.
4.2 SAT encoding of termination-disproving tree automata
Endrullis and Zantema showed that the problem of ﬁnding TDAs can be
reduced to the boolean satisﬁability problem (SAT, for short) by ﬁxing thenumber of states of tree automata. Although we essentially follow their method,
we will present a method which can ﬁnd a TDA-S more eﬃciently because of
the restriction of its form. The eﬃciency of the disproof search is improved notDisproving Termination of Non-Erasing Sole Combinatory Calculus with TA

9only by ﬁnding a TDA-S instead of a TDA but also by specializing their method
for non-erasing sole combinatory calculus.
We present our SAT encoding method to be self-contained, where thediﬀerences from the method by Endrullis and Zantema (EZ method, for short)
are explicitly explained for each step. We ﬁrst explain problem settings anddeﬁnitions used in our method, introduce propositional variables and their
meaning, and then show propositional formulas over them that must hold.
Problem setting and deﬁnitions Let Z be a non-erasing combinator whose
termination is to be disproved. Recall that the reduction rule of Z is represented
by a singleton TRS RZ over ΣZ = {Z (0) , @(2) }. Let lZ → rZ be the uniquerule of RZ where lZ = @(. . . @(@(Z, x1 ), x2 ) . . . , xMZ ) with some MZ ≥ 1 andrZ is built from the binary function symbol @ and variables x1 , x2 , . . . , xMZ sothat FV(lZ ) = FV(rZ ) holds for RZ to be non-erasing. We write UZ for the set
Sub(lZ )∪Sub(rZ ). The left depth ld(t) of a Z-term t ∈ TΣZ is deﬁned by ld(Z) = 0
and ld(@(t1 , t2 )) = 1 + ld(t1 ). The left depth of a term is useful in determining
whether the term is redex or not. A Z-term t has the left depth MZ if and only
if t is a redex of RZ .
Let A = hQ, Σ, {qF }, ∆i be a TDA-S with a ﬁnal sink state qF ∈ Q, which is
to be found if it exists. We ﬁx the number of states as |Q| = N in our encoding.
We iteratively ask the SAT solver to ﬁnd a TDA-S increasing N one by one,starting with N = MZ + 1 because no automaton with less than MZ + 1 states
can recognize the existence of a redex of RZ . We use a function mldA : Q → N
deﬁned by mldA (q) = mint∈L(A,q) ld(t). The function is total because the TDA-S
to be found has only reachable states.
Propositional variables Our SAT encoding involves three classes of propositional variables. The ﬁrst one has the form of either v@(q1 ,q2 )⇝q or vZ⇝q with
q1 , q2 , q ∈ Q, which identify ∆. These variables are expected to satisfy
v@(q1 ,q2 )⇝q is true iﬀ @(q1 , q2 ) ⇝ q ∈ ∆, for all q1 , q2 , q ∈ Q, andvZ⇝q is true iﬀ Z ⇝ q ∈ ∆, for all q ∈ Q.
This class of variables has been employed in the EZ method.
The second class of propositional variables has the form of either vq,m withq ∈ Q \ {qF } and m < MZ or vq,rdx with q ∈ Q. They are expected to satisfy
vq,m is true iﬀ m = mldA (q), for all q ∈ Q \ {qF } and m < MZ , andvq,rdx is true only if L(A, q) ∩ NF(RZ ) = ∅, for all q ∈ Q.
This class of variables is newly introduced in our method in order to check theexistence of redexes. Instead, the EZ method employs propositional variables
that represent reachability of states of a tree automaton obtained by productconstruction of two tree automata, A and B, where B accepts all terms innormal form of RZ .

10

K. Nakano and M. Iwami

The third class of propositional variables has the form of vt,α,q with a termt ∈ UZ , a substitution α : V(t) → Q \ {qF }, and a state q ∈ Q. Note thatthe number of possible substitutions α is ﬁnite because UZ and Q are ﬁnite.
Therefore the number of this class of variables is also ﬁnite. These variables are
expected to satisfy
vt,α,q is true iﬀ tα ⇝∗ q
for all t ∈ UZ , α : V(t) → Q \ {qF }, and q ∈ Q. This class of variables has been
employed in the EZ method, with the diﬀerence of the domain of substitutions.
In their method, each substitution is deﬁned over the set of all states including
ﬁnal states, while our encoding excludes the ﬁnal state from the domain of
substitutions. The diﬀerence makes the number of this class of variables muchsmaller, which will reduce the number of clauses passed to the SAT solver. We
will explain later the reason why the ﬁnal state can be left out in our encoding
method.
Besides the three classes of propositional variables, our implementation of
the proposed encoding method employs extra variables which is equivalent
to conjunction of the other variables. They are introduced in order for thenumber of clauses to be smaller using a standard technique of Tseitin transformation [17], where sub-formulas are replaced by new propositional variables
to avoid exponential brow-up of the number of clauses. The original method
by Endrullis and Zantema may also have used the technique thought it is
not explicitly mentioned in their article. Their implementation is currently nolonger available, so we cannot be sure how they actually do it.
Propositional formulas Recall that a TDA-S A = hQ, ΣZ , {qF }, ∆i with |Q| =N is to be found by the SAT solver. The Boolean values of the propositionalvariables introduced so far exactly identify ∆. It must also be ensured, however,that there is no inconsistency in the valuation of propositional variables, andthat A satisﬁes the TDA-S conditions. The propositional formulas to be satisﬁed
will be shown in sequence condition by condition. It is assumed that they will
eventually be combined together by conjunction and passed to the SAT solver
to ﬁnd an appropriate valuation.
Firstly, the ﬁnal state qF must be sink according to the (3-1) condition.
Hence the following propositional formulas must hold:()∧∧
v@(q1 ,q2 )⇝qF ∧¬v@(q1 ,q2 )⇝q(1)
qF ∈{q1 ,q2 }⊆Q

q∈Q\{qF }All of these propositional variables are immediately forced to be assigned toeither true or false in the phase of unit propagation of the SAT solver. In
addition, the (3-1) condition requires that qF is reachable. Since we will ﬁnd
a TDA-S with the smallest number of states, we assume that all states in Q arereachable. The reachability of states can be paraphrased as the existence of a
total order on Q with appropriate properties as considered in the EZ method.

Disproving Termination of Non-Erasing Sole Combinatory Calculus with TA11

We will employ the following lemma to specify the total order. The proof issimilar to that of the EZ method except that the ﬁnal state is ﬁxed as a sinkstate in our setting. The details of the proof are found in the full version of thispaper [10].
Lemma 6. Let A = hQ, ΣZ , {qF }, ∆i be a tree automaton with a sink state qF .
Then, all states in Q are reachable if and only if there exists a total order <on Q with maximal element qF such that for every q ∈ Q there exists eitherZ ⇝ q ∈ ∆ or @(q1 , q2 ) ⇝ q ∈ ∆ with q1 < q and q2 < q.
Lemma 6 makes it easy to ﬁnd a TDA-S in which all states are reachable.
Without loss of generality, we can ﬁx an ordered sequence of all states in Q as
p1 < p2 < · · · < pN = qF (recall |Q| = N ) and force the states to satisfy theproperty in Lemma 6. The restriction is directly encoded by)∧ (∨vZ⇝q ∨
v@(q1 ,q2 )⇝q ,(2)
q1 ,q2 <qq∈Q

which has been employed also in the EZ method, although our encoding diﬀers
in that the ordered sequence of states should end with the unique ﬁnal state.
Secondly, A must satisfy the (3-2) condition, which requires that A accepts
no terms in normal form. Since L(A) = L(A, qF ), a propositional formula
vqF ,rdx(3)(which is just a unit clause) should hold. To ensure that the Boolean value of
this variable is valid, all of the propositional variables of the form vq,m or vq,rdx
should be properly assigned as follows. The propositional variables vq,m forq ∈ Q \ {qF } and m < MZ are expected to satisfy m = mldA (q). It is easy to
see that mldA (q) can be eﬀectively computed for each q ∈ Q from the transition
rules in ∆. The next lemma claims this fact as a logical statement so as to be
used for giving appropriate propositional formulas. The proof is found in thefull paper [10].
Lemma 7. Let A = hQ, ΣZ , {qF }, ∆i be a tree automaton with a combinator
Z where all states in Q are reachable. Then for every q ∈ Q and m ∈ N, (71) mldA (q) = 0 if and only if Z ⇝ q ∈ ∆, and (7-2) mldA (q) = m > 0 if andonly if there is neither Z ⇝ q ∈ ∆ nor @(q1 , q2 ) ⇝ q ∈ ∆ with mldA (q1 ) < m − 1
and there exists @(q1 , q2 ) ⇝ q ∈ ∆ with mldA (q1 ) = m − 1.
We only need the lemma for non-ﬁnal states though it holds even for theﬁnal state qF because the propositional variables vq,m are given only for q ∈Q \ {qF }. The statement (7-1) indicates that vq,0 for each q ∈ Q \ {qF } has an
appropriate Boolean value by the following propositional formula:∧(vq,0 ⇔ vZ⇝q ) .
(4)
q∈Q\{qF }12

K. Nakano and M. Iwami

We could use the same propositional variable for vq,0 and vZ⇝q in an eﬃcient
implementation, though. Additionally, the statement (7-2) indicates that the
propositional variable vq,m with m > 0 has an appropriate Boolean value by
the following propositional formula:∧∧(vq,m ⇔ (¬vZ⇝q ∧ P1 (q, m) ∧ P2 (q, m)))(5)q∈Q\{qF } m<MZ

where
P1 (q, m) =

∧

∧

(

)
v@(q1 ,q2 )⇝q ⇒ ¬vq1 ,k and0≤k<m−1 q1 ,q2 ∈Q\{qF }P2 (q, m) =∨()
v@(q1 ,q2 )⇝q ∧ vq1 ,m−1 .

q1 ,q2 ∈Q\{qF }The propositional variable vq,rdx for each q ∈ Q is expected to be true only if
L(A, q)∩NF(RZ ) = ∅. The next lemma is used for giving propositional formulasin order for the variables vq,rdx to have an appropriate Boolean value.
Lemma 8. Let A = hQ, ΣZ , {qF }, ∆i be a tree automaton with a sink state qF ,let RZ be a TRS with a combinator Z, and let Q ⊆ Q be a set of states such thatfor all q ∈ Q, (8-1) Z ⇝ q 6∈ ∆ holds, and (8-2) mldA (q1 ) = MZ − 1 holds if
there is @(q1 , q2 ) ⇝ q ∈ ∆ with q1 , q2 ∈ Q \ Q. Then, L(A, q) ∩ NF(RZ ) = ∅ holds
for every q ∈ Q.
The proof is found in the full paper [10]. Let Q ⊆ Q be the set of states q
such that vq,rdx is true. Lemma 8 guarantees that vq,rdx is true only if L(A, q) ∩NF(RZ ) = ∅ whenever Q satisﬁes the conditions (8-1) and (8-2), that is, thefollowing propositional formulas should be true: for (8-1),∧(vq,rdx ⇒ ¬vZ⇝q ) ;(6)q∈Qfor (8-2),
∧

∧

(

)
vq,rdx ∧ v@(q1 ,q2 )⇝q ∧ ¬vq1 ,rdx ∧ ¬vq2 ,rdx ⇒ vq1 ,MZ −1 .

(7)q∈Q q1 ,q2 ∈Q\{qF }Finally, we need to ensure that A is almost closed under RZ in the senseof the (2-3) condition. As the EZ method does, we use the following lemma
which gives a procedure to have the condition. While the EZ method employs
the existing results [5, Proposition 12], we give a proof of this lemma in the full
paper [10] because the (3-3) condition is diﬀerent from the closure property.
Lemma 9. Let A = hQ, Σ, {qF }, ∆i be a tree automaton with a sink state qF , and
let R be a left-linear TRS over Σ. Then, s ∈ L(A, q) implies t ∈ L(A, q)∪L(A) for∗
all q ∈ Q and s, t ∈ TΣ with s →iR t if lα ⇝∗∆ q implies rα ⇝∆q or rα ⇝∗∆ qF
for all q ∈ Q, l → r ∈ R and α : FV(l) → Q.

Disproving Termination of Non-Erasing Sole Combinatory Calculus with TA

13

Recall that the propositional variable vt,α,q is true when a term t is acceptedwith q ∈ Q if every variable x in t is substituted with a term accepted witha state α(x). Following the EZ method, the procedure of computing the stateof each subterm is simulated by imposing relations among the propositionalvariables. Unlike their method, we only need to consider the case where therange of α is Q \ {qF } since the closure property always holds if α(x) = qF
for some x because qF is sink and RZ is non-erasing. This arrangement would
substantially reduce the number of propositional variables. For each subtermt = @(t1 , t2 ) ∈ UZ , we should have
(
)
∧
∧
∨ (
)
vt,α,q ⇔vt1 ,α[t1 ],q1 ∧ vt2 ,α[t2 ],q2 ∧ v@(q1 ,q2 )⇝q(8)
q1 ,q2 ∈Q

q∈Q α:FV(t)→Q\{qF }where α[t] stands for the substition α whose domain is restricted to FV(t). For
each leaf in the subterms UZ , we should have
))
∧ ((
∧ (
∧
)
vx,{x7→q},q ∧¬vx,{x7→q′ },q(9)vZ,∅,q ⇔ vZ⇝q ∧q∈Qx∈FV(lZ )q ′ ∈Q\{q}where the former part indicates that we could use the same propositionalvariable for vZ,∅,q and vZ⇝q . And then, the (3-3) condition requires the
propositional formula∧(vlZ ,α,q ⇒ vrZ ,α,q ∨ vrZ ,α,qF ) .
(10)
α:FV(lZ )→Q

4.3 Applying to non-termination of speciﬁc combinators
We have shown how to construct propositional logic formulas for the existenceof TDA-S with ﬁxed number of states for a sole combinatory calculus. We
have implemented the construction and input the obtained formulas to a SAT
solver to examine termination for combinators shown in Fig. 1, for which
termination is unknown. We conﬁrmed that our method can eﬃciently ﬁnd
a TDA-S compared to the method developed by Endrullis and Zantema for
a TDA. Note that their implementation is not currently publicly available,
so we have re-implemented it. For fairness, we have also applied the same
optimization (e.g., Tseitin transformation) as in the implementation of ourconstruction. Our implementation is written in OCaml and uses the Kissat SAT
solver. We also implement the ability to output the smallest term accepted by
the found TDA-S, thus allowing the output of a non-normalizable term.
The results of the examination for each combinator are shown in Table 1.
Due to page limitation, the details of the TDA-S obtained are found in the full
paper [10] with a found counterexample for termination. Here we only show
the number of states of the TDA-S, the size of the propositional logic formulaused (number of propositional variables and clauses), and the computation
time (the sum of encoding and solving time) including the attempts to fewer

14

K. Nakano and M. Iwami
Table 1. Results of disproving termination of combinators given in Fig. 1.

P
P3
D1
D2
Φ
Φ2
S1
S2

EZ method
Our method#Q#vars#clauses time (s) #Q#vars#clauses
time (s)415,64875,2370.71
4
7,116
33,5430.22
6161,544793,35111.5
6
96,058469,233
5.6
6936,810 4,594,12997.0
6462,5282,264,943
32.6
6
936,810 4,594,12996.6
6462,5282,264,943
32.9
7 1,975,302 9,741,173 260.6
7 1,099,527
5,416,581
108.3
–
—
—
—
9 55,695,683 276,052,931 39,268.4
7 1,975,302 9,741,173 262.1
7 1,099,527
5,416,581
111.6
6745,002 3,655,825
81.6
6
379,278
1,857,693
30.3

states. The ‘EZ method’ column shows the results of (our re-implementationof) the original method by Endrullis and Zantema; the ‘Our method’ column
shows the results of our construction method introduce in the present paper.
The EZ method failed to ﬁnd a TDA for Φ2 within 24-hour computation.
Note that the number of propositional variables and clauses is the same fordiﬀerent combinators. This is because they depend only on the number ofstates, the number of variables in the left-hand side of the combinator’s rule andthe number of subterms in the right-hand side. A major improvement in our
method is a reduction of the number of variables of the form vt,α,q by restricting
the range of α, which is the most signiﬁcant part of the SAT encoding. The
number of possible substitutions is reduced from |Q|N to (|Q| − 1)N , where N
is the number of variables in the left-hand side of the rule. Our method canindeed generate less propositional logic formulas than the original one, andalso succeed in disproving the termination of more combinators. Both method
failed to ﬁnd the disproof of termination for the remaining combinators S3 andS4 in Fig. 1. We have conﬁrmed that their termination cannot be disproven by
a TDA-S with at most 9 states.

5 Concluding remark
We have proposed a method to disprove the termination of sole combinatory
calculi with tree automata by extending the method proposed by Endrullis andZantema. Speciﬁcally, we have shown that a tree automaton with a ﬁnal sinkstate is suﬃcient to disprove termination of non-erasing combinators. We havesucceeded in disproving the termination of 8 combinators which is unknownof their termination found in Smullyan’s book. The remaining two combinators
S3 and S4 still have unknown termination. We may need more improvement
to disprove their termination. However, our method in which termination isdisproved by a tree automaton with a ﬁnal sink state may be applicable to othernon-erasing term rewriting systems. It would be interesting to investigate how
eﬀectual our method is in more general settings.

Disproving Termination of Non-Erasing Sole Combinatory Calculus with TA

15

Acknowledgments. The authors would like to thank the anonymous reviewers
for their valuable comments. This work was partially supported by JSPS
KAKENHI Grant Numbers, JP21K11744, JP22H00520, and JP22K11904.

References
1. Barendregt, H.P.: The lambda calculus – its syntax and semantics, Studies in logic
and the foundations of mathematics, vol. 103. North-Holland (1985)
2. Church, A.: The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics
Studies). Princeton University Press, USA (1985)
3. Curry, H.B.: Grundlagen der kombinatorischen Logik. American Journal of Mathematics 52(3), 509–536 (1930)
4. Endrullis, J., Zantema, H.: Proving non-termination by ﬁnite automata. In: 26th
International Conference on Rewriting Techniques and Applications (RTA 2015).
LIPIcs, vol. 36, pp. 160–176 (2015). https://doi.org/10.4230/LIPICS.RTA.2015.160
5. Genet, T.: Decidable approximations of sets of descendants and sets of normal forms. In: 9th International Conference on Rewriting Techniques andApplications (RTA 1998). LNCS, vol. 1379, pp. 151–165. Springer (1998).
https://doi.org/10.1007/BFB0052368
6. Ikebuchi, M., Nakano, K.: On properties of B-terms. Log. Methods Comput. Sci.
16(2) (2020). https://doi.org/10.23638/LMCS-16(2:8)2020
7. Iwami, M.: On the acyclic and related properties of combinators (in Japanese). IPSJ
Trans. Prog. (PRO) 2(2), 97–104 (Mar 2009)
8. Iwami, M.: Non-ω-strong head normalization, non-ground loop and acyclic ofseveral combinators (in Japanese). IPSJ Trans. Prog. (PRO) 16(3), 14–27 (Aug 2023)
9. Klop, J.W.: New ﬁxed point combinators from old. In: Reﬂections on type theory,
lambda-calculus, and the mind : Essays dedicated to Henk Barendregt on the occasion of his 60th birthday (2007), https://www.cs.ru.nl/barendregt60/essays/klop/
10. Nakano, K., Iwami, M.: Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version). CoRR abs/2406.14305 (2024),
https://arxiv.org/abs/2406.14305
11. O’Donnell, M.J.: Computing in Systems Described by Equations, LNCS, vol. 58.
Springer (1977). https://doi.org/10.1007/3-540-08531-9
12. Ohlebusch, E.: Advanced topics in term rewriting. Springer New York, NY (2002),
http://www.springer.com/computer/swe/book/978-0-387-95250-5
13. Peyton Jones, S.L.: The Implementation of Functional Programming Languages.
Prentice-Hall (1987)
14. Probst, D., Studer, T.: How to normalize the Jay. Theor. Comput. Sci. 254(1-2), 677–
681 (2001). https://doi.org/10.1016/S0304-3975(00)00379-0
15. Schönﬁnkel, M.: Über die Bausteine der mathematischen Logik. Mathematische
Annalen 92(3), 305–316 (Sep 1924). https://doi.org/10.1007/BF01448013
16. Smullyan, R.: Diagonalization and Self-reference. Oxford logic guides, Clarendon
Press (1994)
17. Tseitin, G.S.: Automation of Reasoning 2, chap. On the Complexity of Derivation in Propositional Calculus, pp. 466–483. Springer Berlin Heidelberg (1983).
https://doi.org/10.1007/978-3-642-81955-1_28
18. Turner, D.A.: A new implementation technique for applicative languages. Softw.
Pract. Exp. 9(1), 31–49 (1979). https://doi.org/10.1002/SPE.4380090105
19. Waldmann, J.: The Combinator S. Information and Computation 159(1-2), 2–21
(2000), https://doi.org/10.1006/inco.2000.2874