Turchin’s Relation for Call-by-Name Computations:
A Formal Approach
Antonina Nepeivoda
Program Systems Institute of Russian Academy of Sciences∗
Pereslavl-Zalessky, Russia
a nevod@mail.ru

Supercompilation is a program transformation technique that was first described by V. F. Turchin in
the 1970s. In supercompilation, Turchin’s relation as a similarity relation on call-stack configurations
is used both for call-by-value and call-by-name semantics to terminate unfolding of the program
being transformed. In this paper, we give a formal grammar model of call-by-name stack behaviour.
We classify the model in terms of the Chomsky hierarchy and then formally prove that Turchin’s
relation can terminate all computations generated by the model.

1

Introduction

Supercompilation is a program transformation method based on fold/unfold operations [18, 17, 4]. Given
a program and its parameterized input configuration, a supercompiler partially unfolds the computation
tree of the program on the input configuration and then tries to fold the tree back into a graph, which
presents the residual program. In the general case, the computation tree may be infinite. Thus, the
following question appears: when is it reasonable to stop the unfolding in order to avoid going into an
infinite loop?
One of the ways to solve this problem is based on “configuration similarity” relations. If a path in the
tree contains two configurations, the latter of which resembles the former, that may be a sign that the path
represents an unfolded loop. Thus, when a supercompiler finds two such configurations, it terminates
unfolding of the path where they appear. In general, the loop recognizing problem is undecidable. Hence,
we must make a choice: either to take a risk of an infinite unfolding trying to find all the finite paths, or
to take a risk of terminating the finite paths too early guaranteeing termination of all the infinite paths. In
most supercompilers, the second option is preferred1 [9, 15, 4].
Now we recall an important relation property used for termination.
Definition 1. Given a set T of terms and a set S of sequences of the terms from T , relation R ⊂ T × T
is called a well binary relation with respect to set S, if every sequence {Φn } ∈ S such that ∀i, j(i < j ⇒
(Φi , Φ j ) ∈
/ R) is finite [9].
So, a well binary relation is “a well quasi-order without the order” (i. e., it is not necessarily transitive).
Any relation guaranteeing termination of the unfolding of a computation tree must be a well binary
relation with respect to the set of the traces generated in the tree. The relation most widely used for this
aim, the homeomorphic embedding [9, 1, 15], is well binary with respect to arbitrary term sequences [8].
∗ The

reported study was partially supported by RFBR, research project No. 14-07-00133, and Russian Academy of Sciences, research project No. AAAA-A16-116021760039-0.
1 In supercompiler SCP4 [11], we can choose one of the two options.

G.W. Hamilton, A. Lisitsa, A.P. Nemytykh (Eds): VPT 2016
EPTCS 216, 2016, pp. 137–159, doi:10.4204/EPTCS.216.8

c A. Nepeivoda

138

Turchin’s Relation for Call-by-Name Computations

Some other relations used for termination in program transformations2 are not well binary with respect
to arbitrary term sequences. However, they are well binary with respect to term sequences that can be
generated on any computation path3 .
This paper studies Turchin’s relation, well-binariness of which also can be proved only with respect
to computation paths that appear during unfolding. That relation on call-stack configurations was the
first well binary relation used for trace termination [18] (1986). Although Turchin’s relation is a useful
tool that helps to solve both termination and generalization problems [20] (also see Section 2 of this
paper), the proof of its well-binariness given by V. Turchin in [20] was presented in a semi-formal way.
For the call-by-value semantics, the formal proof of this property of Turchin’s relation is given in [12].
The formalization is based on the prefix rewriting grammars model. But as far as we know, for the
call-by-name semantics, the relation was never formally studied. This paper tries to cover this gap.
Our contributions are the following:
1. We introduce a notion of a multi-layer prefix grammar. Elements of traces generated by such a
grammar are call-stack configurations on computation paths in the call-by-name semantics. We
show that the class of grammars is stronger than the class of context-free grammars.
2. We prove a strengthened version of Turchin’s theorem on well-binariness of Turchin’s relation.
Namely, we prove that every infinite computation path modelled by a trace of a multi-layer prefix grammar contains an infinite chain w.r.t. Turchin’s relation. As a consequence, one can use
Turchin’s relation in composition with the homeomorphic embedding relation (or any other relation, which is well-binary on the arbitrary sequences of terms) without the loss of well-binariness.
4.
The paper is organized as follows. In Section 2, we informally introduce Turchin’s relation for callstack configurations. In Section 3 we define a class of grammars that model call stack behaviour for callby-name computations and describe its computational power. In Section 4 we show how such grammars
can be used for modelling the call stack behaviour of programs in a simple functional language. Finally,
in Section 5 we refine the definition of Turchin’s relation for the new class of the grammars.

1.1

Presentation Language

In this subsection, we informally describe the syntax and semantics of the simple functional language L
used below for demonstrating the modelling method.
The language L is based on the call-by-name semantics. The names of the variables in L are
the words starting with the letter x. Let E (L) denote the set of expressions in L, then:
1. if t is a variable or a constant (a null-ary constructor), then t ∈ E (L),
2. if ti ∈ E (L) (1 ≤ i ≤ n), and C is a constructor of the arity n, then C(t1 , . . . ,tn ) ∈ E (L),
2 Among

them is the relation used in supercompiler SCP4 [11] and the relation used in higher-order supercompiler HOSC

[7].
3 This

property of not being well binary for arbitrary sequences makes it harder to prove the well-binariness of the relations,
because the “minimal bad sequence” reasoning, which is used, e.g., in the classical proof of Kruskal’s theorem in [10], does
not work.
4 The idea behind the composition is to make Turchin’s relation responsible for approximating call-stack behavior of the
program, while the second relation defined on the configurations in the infinite Turchin’s chain has to take into account static
properties of the terms in the infinite chain above. Such a composition may allow a supercompiler to construct more accurate
generalizations (see Example 10).

A. Nepeivoda

139

3. if ti ∈ E (L) (1 ≤ i ≤ n), and f is a function name of the arity n, then f (t1 , . . . ,tn ) ∈ E (L).
For the sake of brevity, we use natural numbers n ∈ N for denoting terms of the form S(S(. . . S(Z) . . . ))
(the unary Peano numbers), where the constant Z stands for 0. Thus, we denote the increment constructor
S(w) by w + 1.
A definition of a function f (x1 , ..., xn ) in L is a sequence of sentences of the form
f (T1 , ..., Tn ) = P;
Here Ti is either a variable or expression C(t1 , . . . ,tn ), where C is a constructor and ti are variables.
The expression on the right-hand side of the definition, P, is an arbitrary expression in E (L) containing
only the variables occurring in f (T1 , ..., Tn ). For every left-hand side of the definition f (T1 , ..., Tn ), no
variable can appear in f (T1 , ..., Tn ) more than once.
The L-program sentences are rewriting rules. The rewriting rules in the programs are ordered from
top to bottom and they should be matched in this order (as in the Haskell and Refal [19] languages).
A simple program in L is given in Example 1.

2
2.1

Turchin’s Relation
Turchin’s Relation for Call-Stack Configurations

The relation we refer to was described in early 1970’s by Valentin Turchin in his seminal works on
supercompilation. Turchin’s relation considers every call stack as a list of the function names, starting
from the top. The idea is the following. If a loop occurs along a computation path, then some prefix of the
list of function names must repeat itself. Then the common suffix (maybe empty) of the lists representing
the function names points to computations after the loop. Turchin’s relation ignores arguments and
considers only call-stack configurations before successful attempts to evaluate a function call. Thus, the
actions of the call stack restructuring are ignored by Turchin’s relation.
Example 1. The following program defines function f (x) = [log2 (x)] + 1 for natural x ≥ 1. A part
of its computation tree starting from the input point f (h(x)) is shown in Figure 1. In the tree, only
stack configurations before evaluating the program rules are present. For example, the first call-stack
configuration out := f (h(x)) is omitted, because the attempt to compute the call f with the argument
h(x) does not lead to any substitutions. It causes only the restructuring of the stack.
A program computing [log2 (x)] + 1
f (0) = 0;
f (x + 1) = f (g(x + 1)) + 1;
g(0) = 0;
g(x + 1) = h(x);
h(0) = 0;
h(x + 1) = g(x) + 1;

The two configurations f (h(g(x3 ) + 1)) + 1 and f (h(x)) have a similar stack structure. Namely, both
their stacks contain the two calls: the top is the call of function h and the bottom is the call of function f .
Turchin’s relation fits well for finding similarities in the call-stack configurations as the one in Example 1. Namely, it checks whether the two call stacks ∆1 and ∆2 on the path can be split into parts

140

Turchin’s Relation for Call-by-Name Computations

Term:
Stack:

f (h(x))
z0 := h(x)
out := f (z0 )

x=0

f (0)

u



x=x1 +1

Term:
Stack:

f (g(x1 ) + 1)
out := f (g(x1 ) + 1)

Term:
Stack:

f (g(g(x1 ) + 1)) + 1
z1 := g(g(x1 ) + 1),
out := f (z1 ) + 1




0


f (h(0)) + 1 o

x1 =0

Term:
Stack:

f (h(g(x1 ))) + 1
z2 := g(x1 ),
z1 := h(z2 ),
out := f (z1 ) + 1


Term:
Stack:


f (0) + 1

x2 =0

w


1

f (h(h(x2 ))) + 1
z2 := h(x2 ),
z1 := h(z2 ),
out := f (z1 ) + 1


Term:
Stack:

f (h(0)) + 1

x1 =x2 +1

x2 =x3 +1

f (h(g(x3 ) + 1)) + 1
z1 := h(g(x3 ) + 1),
out := f (z1 ) + 1

Figure 1: A fragment of the computation tree for the program of Example 1
[Top], [Middle], and [Context] such that ∆1 = [Top][Context], ∆2 = [Top][Middle][Context] and the part
[Context] is never changed on the path segment starting at ∆1 and ending at ∆2 (as shown in Figure 2).
The passive part of data is ignored; only function names in the call stacks are considered. Thus, a call
stack is treated by Turchin’s relation as a word consisting of function names in the call stack (maybe with
some annotation).

Top

Context

...

...

Context

Top

Middle

Context

Figure 2: Turchin’s relation for call-stack configurations
Looking back at Example 1, we can infer that the call-stack configurations for f (h(g(x3 ) + 1)) + 1
and f (h(x)) satisfy Turchin’s relation. But the first two configurations that satisfy Turchin’s relation in
the tree are f (g(g(x1 ) + 1)) + 1 and f (h(g(x1 ))) + 1. The innermost call of the first configuration, g(x1 ),
does not appear in the call stack, because the call is in the passive part of the configuration. Hence, the

A. Nepeivoda

141
f (h(x))
hf

Term:
Stack:

f (0)


0

v



x=0

Term:
Stack:

x=x1 +1

Stack:

f (0)

f (g(g(x1 ) + 1)) + 1

Stack:

t

Term:




let z = g(g(x1 ) + 1) in f (z) + 1



g(g(x1 ) + 1)
g

Term:
Stack:

f

0

t

f (h(g(x1 ))) + 1

f (g(x1 ) + 1)

Stack:

g f


Term:

 x=x1 +1

x=0

f (g(x1 ) + 1)
f


Term:

f (h(x))
hf

Term:
Stack:

Term:

f (z)

Stack:

f

gh f

Generalization of f (g(g(x1 ) + 1)) + 1 and
f (h(g(x1 ))) + 1 is built

Generalization of f (g(x1 ) + 1) and f (z) is built
f (h(x))

Term:
Stack:

hf

x=0

f (0)

u

g(x1 )
g

Term:
Stack:



0

x=x1 +1

let z = g(x1 ) + 1 in f (z)

t


f (z)
f

Term:
Stack:



z=0

u

o

Term:
Stack:

z=z1 +1

f (g(z1 + 1)) + 1
gf


Term:

f (h(z1 )) + 1

Stack:

hf

A fragment of the residual computation graph

Figure 3: Generalization by Turchin’s relation
call stacks of the two configurations are modelled by the words g f and gh f . Moreover, the call f is
unchanged on the path segment starting at f (g(g(x1 ) + 1)) + 1 and ending at f (h(g(x1 ))) + 1. So we can
assign [Top] = g, [Middle] = h, [Context] = f .
It is worth noting that Turchin’s relation additionally provides the following generalization strategy (a
description of generalization can be found in, e. g., [15]). If the two stacks are of the form [Top][Context]
and [Top][Middle][Context], then the former term can be decomposed to let v0 = [Top] in [Context]. After
the decomposition, the parts [Top] and [Context] are developed by supercompilation separately. Thus, the
output format of the part [Top] is not seen any more by the part [Context].
Example 2. Figure 3 shows how the computation tree of Example 1 can be generalized with the use
of Turchin’s relation (Figure 3). For the sake of brevity, the call stacks are represented by the words
consisting of only the function names (from the top to the bottom)5 .
5 We

recall that w + 1 is a notation for S(w), where S is a constructor (see Subsection 1.1).

142

Turchin’s Relation for Call-by-Name Computations

Figure 4 shows the residual programs generated by the final computation graph constructed by generalization w.r.t. Turchin’s relation and by the graph generalized with the use of the homeomorphic
embedding relation (as described in [15]). Turchin’s relation constructs a shorter residual program with
better efficiency. In Example 10 below, we will see that the composition of the two relations allows
us to produce even better generalization. In order to use the composition, we must first prove that the
composition is well-binary. The proof is given in Section 5.

Residual program on the base
of Turchin’s relation (according to Figure 3)
f1 (0) = 0;
f1 (x + 1) = f2 (g1 (x) + 1);
f2 (0) = 0;
f2 (x + 1) = f1 (x) + 1;
g1 (0) = 0;
g1 (1) = 0;
g1 (x + 1 + 1) = g1 (x) + 1;

Residual program on the base
of the homeomorphic embedding
f1 (0) = 0;
f1 (x + 1) = f2 (g1 (x) + 1);
f2 (0) = 0;
f2 (x + 1) = f2 (g2 (x + 1)) + 1;
g1 (0) = 0;
g1 (1) = 0;
g1 (x + 1 + 1) = g1 (x) + 1;
g2 (0) = 0;
g2 (1) = 0;
g2 (x + 1 + 1) = g2 (x) + 1;

Figure 4: Residual programs generated using Turchin’s relation and using the homeomorphic embedding
(Example 2)

2.2

Formalization of Turchin’s Relation for Call-by-Value Semantics

In this subsection we briefly recall notions from the paper [12] where a formal proof of the wellbinariness of Turchin’s relation is given for the call-by-value semantics. Details are omitted. The full
description of the formalization can be found in the original paper [12]. We use some notions from the
paper as a basis to construct the formalization for the call-by-name semantics.
Call stack behaviour of the programs based on the call-by-value semantics can be modelled by prefix
grammars. Namely, the sequence of the call-stack configurations on every computation path can be
represented as a trace generated by a prefix grammar.
Definition 2. A tuple hϒ, R, Γ0 i, where ϒ is a finite alphabet, Γ0 ∈ ϒ+ is an initial word, and R ⊂ ϒ+ ×ϒ∗
is a finite set of rewriting rules, is called a prefix grammar if R : Rl → Rr ∈ R can be applied only to words
of the form Rl Φ (where Rl is a prefix of the word Rl Φ and Φ ∈ ϒ∗ is arbitrary) and generates only words
of the form Rr Φ.
Prefix grammar hϒ, R, Γ0 i is called an alphabetic prefix grammar if the the length of left-hand sides
of all the rules in R is 1 (only the first letter of a word is changed by any rule).
A trace of a prefix grammar G = hϒ, R, Γ0 i is a word sequence {Φi } (finite or infinite) where Φ1 = Γ0
and for all i ∃R(R : Rl → Rr & R ∈ R & Φi = Rl Θ & Φi+1 = Rr Θ) (where Θ is a suffix). In other words,
the elements of the trace are derived from their predecessors by applying the rewriting rules from G.
Henceforth, the empty word is denoted by Λ.

A. Nepeivoda

143

Example 3. The following prefix grammar models the call stack behaviour of the program of Example 1
in the call-by-value semantics6 .
The rules of the program
f (0) = 0;
f (x + 1) = f (g(x + 1)) + 1;

The rewriting rules
f →Λ
f → gf

g(0) = 0;
g(x + 1) = h(x);

g→Λ
g→h

h(0) = 0;
h(x + 1) = g(x) + 1;

h→Λ
h→g

If the initial configuration is f (h(x)) then the initial word Γ0 of the grammar is h f .
Finally, we recall how Turchin’s relation is defined for the traces generated by a prefix grammar.
Given word Φ in a trace {Ψk }, an occurrence of letter a in Φ is said to be changed with respect to a
segment [i, j] (where i < j) of the trace if some rewriting rule was applied to this occurrence of letter a
in the segment starting at Ψi and ending at Ψ j .
Example 4. Consider the grammar given in Example 3. Let us first apply rule h → g to Γ0 , and then
apply rule g → h to the result. In the following trace segment
h→g

g→h

Γ0 : h f −−→ Γ1 : g f −−→ Γ2 : h f
the occurrence of h in Γ2 is not exactly the same as the occurrence of h in Γ0 (it is rewritten by h → g),
so h is changed in Γ2 with respect to [0, 2], while the letter f in Γ2 is unchanged with respect to [0, 2].
Now we formalize the definition of Turchin’s relation for the function call stacks given in [11].
Definition 3. Given a prefix grammar G = hϒ, R, Γ0 i and a trace {Γk } generated by G, we say that two
words Γi , Γ j in {Γk } form a Turchin pair (denoted as Γi  Γ j ) if Γi = ΦΘ0 , Γ j = ΦΨΘ0 and the suffix
Θ0 is not changed in the trace segment [i, j].
In order to develop this formalization for call-by-name languages, below we introduce an extension
of the class of the prefix grammars.

3

Multi-Layer Prefix Grammars

3.1

Motivation

Turchin’s relation considers every stack as a word consisting of function names and ignores the arguments
of the function calls. Hence, from the point of view of the relation, call-stack configurations form a trace
generated by some grammar. So the problem arises: given a program, what class of grammars can
generate words that correspond to the call-stack configurations generated by the program?
For the call-by-value semantics, the construction of the grammar is very straightforward (as can be
seen in Example 3). But in the call-by-name semantics, besides the active part of the stack, function calls
may appear in the passive part of the configuration. Such function calls make it impossible to predict
how the call stack will be transformed if we observe only its active part.
6 The

details of the construction may depend on the interpretation strategy.

144

Turchin’s Relation for Call-by-Name Computations

Example 5. Given a path from the tree of Example 1, we see that applications of the same rule g(x+1) =
h(x) resulted in different stack transformations. In the first case, the call g(x1 ) was popped from the
passive part of the configuration.
Computation path

Applied rule

Call stack

f (h(x))

hf
h(x + 1) = g(x) + 1

f

f (g(g(x1 ) + 1)) + 1

f (x + 1) = f (g(x + 1)) + 1

gf

f (h(g(x1 ))) + 1

g(x + 1) = h(x)

gh f

f (h(h(x2 ))) + 1

g(x + 1) = h(x)

hh f

f (g(x1 ) + 1)

Example 5 shows that the only way to build a consistent grammar model of the call stack behaviour
is to take into account the passive part of the configuration.
Every configuration is a tree of function calls, both active and passive. Given a configuration, the
active call stack forms a path in the configuration tree starting at the root.
Example 6. Given the configuration
b(x1 + 1, b(d(x1 ), d(x2 )) + 1)
we apply the following rule
b(x1 + 1, x2 + 1) = b(d(b(x1 , x2 + 1)), x2 )
to it. The tree representations of the results are given in Figure 5.
b(. . . , . . . )

d(. . . )
b(. . . , . . . )
+1

y
'

u



x1

x1



x

+1



x1


d(. . . )



x2

b(. . . , . . . )



d(. . . )



x1

Term b(x1 + 1, b(d(x1 ), d(x2 )) + 1)
before the rule application

d(. . . )





d(. . . )
x2

x

b(. . . , . . . )

+1

b(. . . , . . . )
d(. . . )

b(. . . , . . . )






x1

&
x

w


d(. . . )



x2

Term b(x1 + 1, b(d(x1 ), d(x2 )) + 1)
after the rule application

Figure 5: Tree forms of the terms of Example 6. The calls in the active call stack are in ovals.
Based on the observations above, we use the following assumptions to construct the grammar models
for programs based on the call-by-name semantics.
1. A configuration can be considered as a tree of calls, and the active call stack — as a path in the
tree. We use a set of labels S with partial order / for denoting the positions of the function calls in
the tree.

A. Nepeivoda

145

2. Every call in the stack is modelled by a pair < NAME, LABEL >, where LABEL ∈ S.
3. Every configuration is represented as a word Γ$∆ consisting of the two parts separated by the
symbol $. The structure of the active stack is placed in Γ and is linearly ordered w.r.t. labels, the
function calls in the passive part of the configuration are placed in ∆.

3.2

Formalization

Let ϒ be a finite alphabet. Let S be a label set and / be a strict (non-reflexive) partial order relation over
S. We denote the labels from S by the letters s, t (maybe with subscripts). Let us say that s1 is a child of
s0 w.r.t. S0 ⊆ S (denoted by s1 = child(s0 )[S0 ]) if s0 / s1 , s0 ∈ S0 , s1 ∈ S0 and there is no such s2 ∈ S0 that
s0 / s2 and s2 / s1 . The inverse for the child relation is the parent relation. Given a set S0 ⊆ S and a label
t ∈ S \ S0 , we call t a fresh label w.r.t. S0 if S0 contains neither descendants nor ancestors of label t 7 .
Informally, the labels can be considered as nodes of trees with unbounded branching, then the child–
parent relation has its usual meaning.
Henceforth, the set of finite sequences of pairs {ha, si i|a ∈ ϒ & si ∈ S}∗ is denoted by LW(ϒ, S).
Elements of LW(ϒ, S) are called layered words, and are denoted by Greek capitals Γ, ∆, Φ, Ψ, Ξ, Θ. If
ha1 , s1 i . . . han , sn i is a layered word, the corresponding plain word is defined as a1 . . . an .
If Φ is a layered word, |Φ| stands for the number of the pairs in Φ and Φ[i] stands for the i-th pair.
For the sake of brevity, layered word ha1 , s0 i . . . han , s0 i can be also written as ha1 . . . an , s0 i (thus, ahs0 i
is an equivalent form for ha, s0 i).
Expression Φhs0 i denotes the maximal subsequence of Φ containing only the pairs labelled with s0 .
Expression Φhs0 i denotes the maximal subsequence of Φ not containing the pairs labelled with s0 . The
set of all labels in Φ is denoted by SΦ .
Example 7. Let Φ = ha1 , s1 iha2 , s1 iha3 , s2 iha4 , s4 iha5 , s1 iha6 , s3 iha7 , s4 i. Then Φhs1 i = ha1 a2 a5 , s1 i,
Φhs1 i = ha3 , s2 iha4 , s4 iha6 , s3 iha7 , s4 i.
If s1 / s2 / s3 , s1 / s4 (and s4 is fresh w.r.t. {s2 , s3 }, then the layered word Φ can be represented as the
following tree:
s1 : a1 a2 a5
s2 : a 3

v

(

s4 : a4 a7



s3 : a 6

The order of the letters in Φ does matter for the tree representation only if the letters have the same
label8 .
Given a label si and natural numbers K1 and K2 , we define a set of layer functions w.r.t. label si ,
FsKi 1 ,K2 : LW(ϒ, S) → LW(ϒ, S), as a minimal set of functions containing all compositions of K1 elementary
functions, which are:
1. Append Apps j [Ψ] (where s j ∈ S, Ψ ∈ ϒ∗ ): given a layered word Φ, Apps j [Ψ](Φ) is the word
ΦΨhs j i such that s j is a child of si w.r.t. SΦ ∪ {s j }, s j is fresh w.r.t. SΦ \ {si }, and |Ψ| ≤ K2 .
most cases, we assume that S0 is a set of all previously used labels, hence there is no need to write it in the square
brackets in expressions like child(s0 )[S0 ].
8 Hence, both the word Φ and, for example, word ha , s iha , s iha , s iha , s iha , s iha , s iha , s i are presented by the
3 2
1 1
4 4
7 4
2 1
6 3
5 1
same tree above.
7 In

146

Turchin’s Relation for Call-by-Name Computations
0
and s0 / s1 , then
For example, if Apps1 [g] ∈ Fs1,1

Apps1 [g](h f , s0 ihg, s1 i) = h f , s0 ihg, s1 ihg, s1 i
The appending operation, if considered as a tree transformation, appends some new letters to an
existing node (Figure 6).
...

...





si : Φi
sl : Φl

si : Φ i

%

y

sj : Φj

%

z

−→

s j : Φ jΨ

sl : Φl

Figure 6: Function Apps j [Ψ] as a tree operation
2. Insert Inss j [Ψhsk i] (where s j , sk ∈ S, Ψ ∈ ϒ∗ ): given Φ with a non-empty Φhs j i, where s j is a child
of si w.r.t. SΦ , Inss j [Ψhsk i](Φ) is the word ΦΨhsk i where |Ψ| ≤ K2 and sk is a child of si w.r.t.
SΦ ∪ {sk }, sk is fresh w.r.t. SΦ \ {si } and s j is a child of sk w.r.t. SΦ ∪ {sk }.
0 9
and s0 / s1 , then
For example, if Inss1 [g f hs2 i] ∈ Fs1,1

Inss1 [hg f , s2 i](h f , s0 ihg, s1 i) = h f , s0 ihg, s1 ihg f , s2 i
The insert operation differs from the append operation only by introduction of an unused child
label sk , which marks the newly appended word Ψ. In tree terms, this operation inserts a new node
between the nodes labelled by si and s j (Figure 7).
...

...





si : Φi
sl : Φl

y

si : Φi

%

sj : Φj

−→

z

sl : Φl

$

sk : Ψ



sj : Φj

Figure 7: Function Inss j [Ψhsk i] as a tree operation
3. Deleting Dels j (where s j ∈ S): given Φ with a non-empty Φhs j i, s j = child(si ) w.r.t. SΦ , Dels j
erases Φhs j i from Φ together with all Φhti for which s j / t.
0
For example, if Dels01 ∈ Fs1,1
and s0 / s01 , s02 is incomparable with s01 , then

Dels01 (hd, s01 ihd, s02 i) = hd, s02 i
In tree terms, this operation deletes the subtree, whose uppermost node is labelled by s j (Figure 8).
9 This

condition implies that s2 / s1 and s0 / s2 .

A. Nepeivoda

147
...



...

si : Φ i

'

y

sl : Φk

sj : Φj



−→

si : Φi





s j+1 : Φ j+1

sl : Φk

Figure 8: Function Dels j as a tree operation
4. Copying Copys j (where s j ∈ S): given Φ with a non-empty Φhs j i, s j = child(si ) w.r.t. SΦ , Copys j
appends Φhsk i to Φ, where sk is a child of si w.r.t. SΦ ∪ {s j }, s j is fresh w.r.t. SΦ \ {si }, and then
it appends all subsequences Φhsl i labelled by the children of s j and labels them by fresh children
of sl and so on until all the sequences Φhti, where s j / t, are copied exactly once.
0
For example, if Copys01 ∈ Fs1,1
and s0 / s01 , then

Copys01 (hd, s01 i) = hb, s0 ihd, s01 ihd, s02 i,
where s02 is incomparable with s01 .
In tree terms, this operation creates a copy of the subtree, whose uppermost node is labelled by s j
(Figure 9).
...

...





si : Φi
sl : Φl

y

'

si : Φi
sj : Φj



−→
sl : Φl

s j+1 : Φ j+1

x



sj : Φj



s j+1 : Φ j+1

(

sk : Φ j



sk+1 : Φ j+1

Figure 9: Function Copys j as a tree operation
Section 4 below shows how the elementary layer functions model the call stack transformations.
Definition 4. Let us consider a tuple G = hϒ, S, R, FvK1 ,K2 , Γ0 $∆0 i where Γ0 and ∆0 are layered words
over ϒ × S such that for every Γ0 [i] = hai , si i and Γ0 [ j] = ha j , s j i, if j > i then s j / si or s j = si , $ is a
special symbol, $ ∈
/ ϒ, and FvK1 ,K2 is a finite set of layer function forms where v runs over the label set S.
For every G-word Γ$∆, where Γ and ∆ are words in LW(ϒ, S), we call Γ the visible layer, and we call ∆
the invisible layer of Γ$∆.
Let all rewriting rules from R have one of the following forms:
• Simple rule:
Ξha, si iΘ$Ψ → ΦΘ$F si (Ψ),
where all the letters of Φ are labelled either by si or by fresh descendants of si , F si ∈ Fsi .

148

Turchin’s Relation for Call-by-Name Computations
• Pop rule: for Ψhs j i — the maximal subsequence of Ψ marked by some s j = child(si ) ∈ S,
Ξha, si iΘ$Ψ → Ψhs j iΦΘ$F si (Ψ),
where all the letters of Φ are labelled either by si or by fresh descendants of si , F si ∈ Fsi . In a pop
rule, we may specify s j , but there are no ways to specify Ψhs j i.

Such a grammar G is called a multi-layer prefix grammar. K2 is called the maximal rewrite depth, K1
is called the maximal replication index. A sequence of G-words starting at Γ0 $∆0 that are transformed
by the rules from R is called a trace of G.
If any rule of such a grammar changes only one letter of the visible layer (thus, Ξ = Λ), then the
multi-layer prefix grammar is alphabetic.
Definition 5. Let ΦΘ$∆i be the i-th G-word in a trace {Γk $∆k } generated by an alphabetic multi-layer
prefix grammar G. If Γ j $∆ j = ΨΘ$∆ j ( j > i) then we say that Ψ is a derivative prefix (or simply
a derivative) of Φ (denoted by deriv(Φ)).
Now we can prove some simple propositions about the multi-layer grammars.
Proposition 1. The following properties hold.
1. Given an alphabetic multi-layer prefix grammar G and a word Γ$∆ generated by G, for every
Γ[i] = hai , si i, Γ[ j] = ha j , s j i if i > j then either si = s j or si / s j .
2. Let an alphabetic multi-layer grammar G generate Γ$Ψ with the non-empty Ψhs1 i and Ψhs1 i such
that s1 and s2 are unequal and incomparable. Then derivatives of Ψhs1 i and Ψhs2 i cannot occur
in the visible part of the same word.
3. Let G generate a word Ξ = ha, si iΓhb, s j iΘ$Ψ. Given the trace containing Ξ, any occurrence of
deriv(ha, si i) in the visible layer of the word in the trace precedes all occurrences of deriv(hb, s j i).
Proof. 1. By the definition, the initial word Γ0 $∆0 satisfies the stated property. Given a word ha, si iΓ$∆
satisfying the stated property, a non-pop rule can only prepend descendants of ha, si i to Γ, and a pop rule
can only append descendants of ha, si i to Γ. Therefore, all the words generated from ha, si iΓ$∆ must
satisfy the stated property.
2. If s1 and s2 are incomparable then the labels of the derivatives of Ψhs1 i and Ψhs2 i are also
incomparable. And the stated property follows from the case 1.
3. Given a trace generated by G, deriv(hb, s j i) can be generated only after word hb, s j iΘ$Ψ0 occurring in the trace. Word hb, s j iΘ$Ψ0 can contain deriv(ha, si i) only in the invisible layer. All deriv(hb, s j i)
are appended to the end of the invisible layer (by the definitions of Appsk [Ψ], Inssk [Ψhsu i], Copysk ). They
are marked by the labels, which are not less (but may be incomparable) than the labels of deriv(ha, si i).
Hence, after applying the pop rules, deriv(hb, s j i) follows deriv(ha, si i) in the visible layer.
To specify the notion of a language generated by a multi-layer prefix grammar, we add one or several
[i]
halting rules R[Stop] to the set R. They are of the usual form, but halt the computation path.
Definition 6. A language generated by G is the set of all the words A ∈ ϒ∗ where A is a plain word
corresponding to the visible layer Γ of some layered word Γ$∆, such that:
• Γ$∆ is generated in a finite trace of multi-layer prefix grammar G;
• ∆ is the result of an application of a halting rule.

A. Nepeivoda

149
[i]

The rules R[Stop] can be considered as function definitions that cause the printing side effect. When
[i]

some R[Stop] is applied, we output the stack configuration where it happened.
Theorem 1. Every recursively enumerable set can be generated by a multi-layer prefix grammar.
The proof of Theorem 1 can be found in Appendix (proof 6.1). Every rule in the grammar constructed
in the proof changes the two first letters of the visible part of a G-word. In terms of computations, this
means that the two calls belonging to the active stack, which is modelled by the visible part, are evaluated
by a single action. Usually, only a single call from the top of the stack is evaluated, so the modelling
grammar is alphabetic. In the case of the plain prefix grammars, the class of the generating alphabetic
prefix grammars defines the regular languages as well as the class of all prefix grammars [2]. In the
case of the alphabetic multi-layer prefix grammars, the situation changes drastically. We can informally
compare their power to 1-state Turing machines, although the grammars modelling Turing machines use
only the insert layer functions, while the copy and append functions are left aside.
Proposition 2. Alphabetic multi-layer prefix grammars are strictly stronger10 than both context-free
grammars and one-state Turing machines.
The proof of Proposition 2 can be found in Appendix (proof 6.2).
Given a word w = w[1]w[2] . . . w[N], the inverse word of w is the word w[N] . . . w[2]w[1] (denoted by
inv(w)).
Proposition 3. There is no rule-set R such that any alphabetic multi-layer prefix grammar with the
rule-set R and the initial word from w ∈ {a, b}∗ can construct inv(w).
Proof. Let w be modelled by the initial word Φ0 hai , si iΦ1 hb j , s j i$Λ. The word inv(w) is modelled by
hb j ,t j i inv(Φ1 )hai ,ti i inv(Φ0 )$Λ. According to Proposition 1, because hb j ,t j i = deriv(hb j , s j i), hai ,ti i =
deriv(hai , si i), such a word cannot appear in any trace generated by any alphabetic multi-layer prefix
grammar.
This proof shows that the class of the alphabetic multi-layer prefix grammars does not coincide
with the classes of the tree automata grammars and linear indexed grammars [5]. Informally, this class
contains grammars that are able to generate very long words of a rather simple structure.

4

Modelling Call Stack Behaviour by Multi-Layer Grammars

We borrow the notions of f -function and g-function from [16] and use them in the following sense. An
f -function is a function whose definition consists of one rule with trivial patterns (e. g., if h1 is defined
as h1 (x1 , x2 ) = b(x2 , h2 (x1 + 1)) then h1 is an f -function). A g-function is a function with non-trivial
patterns in the definition (e. g., h2 (x + 1) = b(h2 (x), h2 (x)) is a definition of the g-function).
In order to get a grammar from a program, we treat every configuration generated by the unfolding
as a tree, whose nodes are named by function or constructor names and leaves contain no function calls.
First, we mark every function name in the tree by a superscript depending on the state of the function
call. If the call is ready to be evaluated without evaluation of other calls, the function name is marked as
“ready” (by + in the superscript). Otherwise, the function name is marked as “unready”. Hence, the call
10 They generate all the languages that can be generated by these models, and some languages that cannot be generated by
these two models.

150

Turchin’s Relation for Call-by-Name Computations

names of all f -functions are always marked as “ready”, while the call names of g-functions are marked
as “ready” if the patterns of the functions can be matched without evaluating another call11 .
Then we delete all the nodes containing static data12 . The remaining nodes are given the layer labels.
If some node T is a descendant of a node W , the label of T is greater than the label of W . Otherwise the
labels are incomparable.
Finally, we find all the nodes containing the unready call names with a single child. The child of
such a node is given the label of the node. And then, all the nodes with the same labels are merged: data
from the ancestor nodes are placed in the merged node after the data from their descendants.
The resulting tree is a tree form of the corresponding layered word.
Example 8. Given the term b(d(x1 ) + 1, b(x1 , d(d(x2 ))) + 1), we transform it to a layered word. All the
steps of the transformation are given in Figure 10.
First, we mark the calls as “ready”(with + in the superscript) and “unready”(with − in the superscript), and delete the nodes with the static data. The only function call in the configuration which is
ready to be evaluated without unfolding is the outermost call of b. The calls d(x1 ) and d(x2 ) require
unfolding (which generates restrictions on x1 and x2 ), but they do not require evaluation of other calls,
so they are also marked as ready. All the other calls are marked as unready.
Then we assign the layer labels in the resulting tree of the marked call names. The tree below shows
that s0 / s1 , s0 / s2 , s2 / s3 / s4 .
After that, we find all the nodes with a single child whose call name is marked as unready. The child
of such a node is given the layer label of its parent. Then we merge all the nodes having the same label
and prepend the data in the descendant nodes to the data in the ancestor nodes. In the second tree in
Figure 10, the two nodes will be given their ancestor’s layer label: the nodes labelled by s3 and by s4 .
Finally, the node containing the name of the call in the active stack is extracted. In Figure 10, the
node is s0 containing function name b. This name together with the node label take a place in the visible
part of the layered word; data from all the other nodes in the tree (namely, nodes s1 and s2 ) take a place
in the invisible part.
The layer functions used for defining the multi-layer grammars (see Section 3) describe one-step
actions transforming the passive parts of the function call stacks in language L (and the other call-byname programming languages).
1. Appending Apps j [Ψ] models adding an unready function call Ψ (or a sequence of such function
calls) to the passive part of the given configuration. None of the function calls from Ψ can be
evaluated immediately. E. g., as shown in Figure 11.
11 For programs in language L, we always can determine all the calls that are ready to be unfolded due to simplicity of the
patterns. In languages with complex pattern matching (e. g., Refal [19]), that can be done only if one knows the strategy of the
pattern matching applied in the interpreter.
12 In some cases, this action can transform the tree into a forest. For example, that can happen if the configuration is
cons(h1 (x), cons(h2 (x), Nil)). To avoid these cases, we always assume that the transformed tree has a root, but the root is
a “virtual” function call, which is always present in the G-word corresponding to the tree and is denoted by $.

A. Nepeivoda

151

+1

w



s1 : d +

+1





d(. . . )

b(. . . , . . . )





x1

y
s0 : b



s2

&

x1

Program

s0 : b+

b(. . . , . . . )

d(. . . )


d(. . . )



: b−
s1 : d



s3 : d −



s4

y


s2 : ddb

: d+

b(0, x2 ) = 1;
b(x1 , 0) = x1 ;
b(x1 + 1, x2 + 1) =
b(d(b(x1 , x2 + 1)),
x2 );
d(0) = 0;
d(x + 1) = d(x) + 1 + 1;

x2

(a)

(b)

(c)

Figure 10: Steps transforming the term b(d(x1 ) + 1, b(x1 , d(d(x2 ))) + 1) from a tree to layered word
hb, s0 i$hd, s01 ihddb, s02 i: (a) the initial term in the tree form; (b) the call names are marked, the static
data are deleted, the layer labels are assigned; (c) the layer labels are merged, the active part is extracted.
Program
f (0) = 0;
f (x + 1) =
f (g(x + 1)) + 1;

Configuration

Layered Word

f (h(g(x) + 1))
↓
f (g(g(x)) + 1)

hh, s0 ih f , s0 i$hg, s1 i
↓
h f , s0 i$hg, s1 ihg, s1 i = h f , s0 i$ Apps1 [g](hg, s1 i)

g(0) = 0;
g(x + 1) = h(x);
h(0) = 0;
h(x + 1) = g(x) + 1;

Figure 11: Sample model of the call-stack restructuring by using the function Apps j
2. Insert function Inss j [Ψhsk i] models adding a ready function call to the invisible layer. The ready
function call is a call whose pattern can be matched immediately. E. g., as shown in Figure 12 (the
program rules are the same as for Apps j ).
Configuration

Layered Word

f ( f (g(x) + 1))
↓
f ( f (g(g(x) + 1)) + 1)

h f , s0 ih f , s0 i$hg, s1 i
↓
h f , s0 i$hg, s1 ihg f , s2 i = h f , s0 i$ Inss1 [g f hs2 i](hg, s1 i)

Figure 12: Sample model of the call-stack restructuring by using the function Inss j [Ψhsk i]
3. Deleting Dels j corresponds to replacement of one argument of a function call by an expression
without function calls. E. g., as shown in Figure 13.
4. Copying Copys j corresponds to copying one argument of a function call into another. E. g., as

152

Turchin’s Relation for Call-by-Name Computations

Program

Configuration

Layered Word

b(b(0, d(x) + 1), d(x))
↓
b(1, d(x))

hb, s0 ihb, s0 i$hd, s01 ihd, s02 i
↓
hb, s0 i$hd, s02 i =
hb, s0 i$ Dels01 (hd, s01 ihd, s02 i)

b(0, x2 ) = 1;
b(x1 , 0) = x1 ;
b(x1 + 1, x2 + 1) =
b(d(b(x1 , x2 + 1)), x2 );
d(0) = 0;
d(x + 1) = d(x) + 1 + 1;

Figure 13: Sample model of the call-stack restructuring by using the function Dels j
shown in Figure 14 (the program rules are the same as for Dels j ). Since the semantics is call-byname, the transformation does not retain information about equality of the call and its copy.
Configuration

Layered Word

b(x1 + 1, d(x2 ) + 1)
↓
b(d(b(x1 , d(x2 ) + 1)), d(y))

hb, s0 i$hd, s01 i
↓
hbdb, s0 i$hd, s01 ihd, s02 i = hbdb, s0 i$ Copys01 (hd, s01 i)

Figure 14: Sample model of the call-stack restructuring by using the function Copys j

Because every function definition is finite, only a finite number of append, delete, copy and insert
functions can be applied in one step of the unfolding. That guarantees finiteness of the constants K1 and
K2 in the corresponding multi-layer grammars.

5

Turchin’s Relation and Multi-Layer Grammars

Definition 7. Let G be a multi-layer prefix grammar with the set of rules R such that every rule from R
rewrites at most N letters of a visible layer. Given a trace {Γk $∆k } and its segment [i, j], suffix Θ of Φi is
called a permanently stable suffix w.r.t. the segment [i, j] if all the words Γk $∆k , i ≤ k < j, are of the form
Φk Θ$∆k where Φk is a layered word with the length not less than N, and Γ j is of the form Φ j Θ, where
Φ j may be Λ 13 . If j is not bounded, Θ is called a permanently stable suffix w.r.t. i.
Informally, a permanently stable suffix is a suffix of the visible layer that is never changed in the trace
segment [i, j]. In terms of call stack behavior, a permanently stable suffix corresponds to an unchanged
context of the computation.
Example 9. Let a trace of some alphabetic multi-layer grammar be:

Φ0 : hh f , s0 i$hh, s1 i

/ Φ1 : h f , s0 i$hhg, s1 i

/ Φ2 : hg f , s0 i$hhg, s1 i

/ Φ3 : hhg, s1 ihg f , s0 i$Λ

Suffix h f , s0 i of Φi is permanently stable w.r.t. [2, 3], but is not permanently stable w.r.t. the position
0 (i. e., w.r.t. the whole trace) because in the word Φ1 it is preceded by the empty prefix in the visible
13 In

the case of alphabetic prefix grammars, when N = 1, the first condition implies the second.

A. Nepeivoda

153

layer14 . Suffix hg, s1 i of Φ1 is not permanently stable w.r.t. [1, 3], because in the words Φ1 , Φ2 it occurs
in the invisible layer.
Definition 8. Let G = hϒ, S, R, FvK1 ,K2 , Γ0 $∆0 i be a multi-layer prefix grammar. Given two G-words
Ξi = Γi $∆i , Ξ j = Γ j $∆ j in a trace {Γk $∆k }, we say that the words form a Turchin pair (denoted as
Ξi  Ξ j ) if Γi = ΦΘ0 , Γ j = Φ0 ΨΘ0 , Φ is equal to Φ0 as a plain word (up to the layer labels) and the
suffix Θ0 is permanently stable w.r.t. segment [i, j].
Thus, if we do not take into account the invisible layer and layer labels, then the definition of
the Turchin pair for the traces generated by the multi-layer prefix grammars repeats the definition for
the plain prefix grammars given in Section 2.
Theorem 2 (Strengthened Turchin’s Theorem). Let G = hϒ, S, R, FvK1 ,K2 , Γ0 $∆0 i be a multi-layer prefix
grammar. Every infinite trace generated by grammar G contains an infinite subsequence {Γk $∆k } such
that for every Γk1 $∆k1 , Γk2 $∆k2 , k1 < k2 implies Γk1  Γk2 .
Proof. The idea of the proof is borrowed from the original V. Turchin’s work [20].
Let N be the maximal number of the letters in the visible layer that can be changed by rewriting rules
from R. We consider the following two cases.
Let {Γi $∆i } be an infinite trace under the theorem conditions. If some word Γi $∆i contains a suffix
Θi that is permanently stable w.r.t. i in the trace, and for all j > i no word Γ j $∆ j contains a permanently
stable (w.r.t. j) suffix being longer than Θi , then there are infinitely many words Φ$Ψ in the trace such
that |Φ| ≤ |Θi | + N. Thus some word Φ repeats itself as a plain word in the visible parts infinitely
many times. The infinite subsequence of the words having Φ as the plain word in the visible part is a
subsequence of {Γi $∆i }, such that every two words of the subsequence form a Turchin pair.
Let {Γi $∆i } be an infinite trace with no upper bound on the permanently stable suffixes’ length. So
b in that
there is an infinite sequence of words {Γin $∆in } such that the visible part Γin contains the suffix Φ
is permanently stable w.r.t. in , but not w.r.t. in − 1. Namely, such words Γin $∆in are the words where
b in is generated in the visible part. The letter of Γin preceding Φ
b in does not belong to
the first letter of Φ
the permanently stable suffix, so it is erased somewhere further in the trace. The G-word in which it is
b in $∆i , |Ψin | ≤ N.
erased looks as Ψin Φ
k
b in $∆i }
Since |Ψin | is bounded, there exists at least one plain word Ψ such that the sequence {Ψin Φ
k
contains infinitely many G-words with the prefix Ψin equal to Ψ as a plain word. Let the subsequence of
b i , Γi = Ψi Φ
b i = Ψi ΞΦ
b i , the suffix Φ
b i is
such words be {Γil $∆il }. For every il1 < il2 , Γil1 = Ψil1 Φ
l1
l2
l2
l2
l2
l1
l1
unchanged in Γil2 , and Ψil1 and Ψil2 coincide as the plain words. Thus, the sequence {Γil $∆il } satisfies
the statement of the theorem.
Theorem 2 implies the following corollary.
Proposition 4. A composition of Turchin’s relation and an arbitrary well binary relation R is a well
binary relation with respect to the set of the traces generated by the multi-layer prefix grammars.
Proof. Every infinite trace generated by a multi-layer prefix grammar contains an infinite subsequence,
every two words of which form a Turchin pair. Due to the well-binariness of relation R, this subsequence
also contains two words Γ and ∆ such that Γ precedes ∆ and (Γ, ∆) ∈ R.
14 Thus,

the letter f in Φ1 is rewritten by some rule to g f in Φ2 .

154

Turchin’s Relation for Call-by-Name Computations

Example 10. We turn back to the program of Example 1. Example 2 shows that generalization w.r.t.
Turchin’s relation produces a better residual program than generalization w.r.t. the homeomorphic embedding. Let us consider the composition of these two relations. The result of the unfolding and the
generalization is shown in Figure 16 given in Appendix.
The residual program extracted from the graph after the generalization looks as follows.
Residual program generated by
the graph of Figure 16
f1 (0) = 0;
f1 (1) = 1;
f1 (2) = 1;
f1 (x + 1 + 1 + 1) = f1 (g1 (x) + 1);
g1 (0) = 0;
g1 (1) = 0;
g1 (x + 1 + 1) = g1 (x) + 1;
This residual program is more efficient than the two residual programs given in Example 2, and contains
less rules.
Why the composition helps to construct a good generalization in this case? Let us consider the
configurations in Turchin’s relation along the trace. The first two such configurations are f (g(g(x1 ) +
1)) + 1 and f (h(g(x1 ))) + 1. The innermost call of the first configuration does not appear the call-stack,
so from the point of view of Turchin’s relation these two configurations look as f (g(z1 )) and f (h(g(z2 )))
(and the call of f is not changed in the corresponding segment of the trace). So, if one uses only Turchin’s
relation, the two configurations are to be generalized. The homeomorphic embedding relation does not
ignore the passive parts of the configurations. But if we use only the homeomorphic embedding relation,
we will meet problems as described in Example 2. Thus, using the composition allows a supercompiler
to generalize configurations θ1 and θ2 only if both the call stacks of θ1 and θ2 are similar and the static
data in θ1 and θ2 are also similar, which results in more accurate generalizations.

6

Conclusion

Turchin’s relation for call-by-name computations is a strong and consistent branch termination criterion.
Every infinite trace generated by unfolding a program in the language with the call-by-name semantics
contains two elements, whose call-stack configurations form a Turchin pair. Neither the homeomorphic
embedding can replace Turchin’s relation nor Turchin’s relation can be considered as a simplification of
the homeomorphic embedding in the case of the normal-order reduction15 . Turchin’s relation can be used
together with the homeomorphic embedding relation without the loss of well-binariness, and can be used
not only for deciding when to terminate the computation path but also for deciding how to generalize the
configurations.
15 If all the configurations in the computation tree contained no branching (i.e., were consisting only of unary function calls
and constructors), Turchin’s relation could be considered as a “one-gap version” of the homeomorphic embedding for the callstacks, and could be replaced by an annotated version of the homeomorphic embedding as shown in [12]. However, for terms
having the tree structure (even with only one branching node), the “one-gap” (or even “n-gap”) relation is not well-binary
(that is also shown in [12]). So, considering the call-stack configurations as words is somewhat essential for making Turchin’s
relation well-binary.

A. Nepeivoda

155

The alphabetic multi-layer grammars, describing the function call stack behaviour, are able to generate languages with very long words, but it seems to us they are not able to generate languages with
words having a complex structure. It would be interesting to find some practical problems, which can
be solved with the power of Turchin’s relation (or homeomorphic embedding relation) on the call-stack
configurations for call-by-name computations.

Acknowledgements
I would like to thank A. P. Nemytykh for many fruitful advices and help in improving the paper, and the
anonymous referees for the useful feedback.

References
[1] E. Albert, J. Gallagher, M. Gomes-Zamalla & G. Puebla (2009): Type-based Homeomorphic Embedding for Online Termination. Journal of Information Processing Letters 109(15), pp. 879–886,
doi:10.1016/j.ipl.2009.04.016.
[2] D. Caucal (1992): On the regular structure of prefix rewriting. Theoretical Computer Science 106, pp. 61–86,
doi:10.1016/0304-3975(92)90278-N.
[3] S. Greibach (1965): A New Normal-Form Theorem for Context-Free Phrase Structure Grammars. Journal of
the ACM 12(1), doi:10.1145/321250.321254.
[4] G. W. Hamilton & N. D. Jones (2012): Distillation with labelled transition systems, pp. 15–24. IEEE Computer Society Press, doi:10.1145/2103746.2103753.
[5] J. E. Hopcroft & J. D. Ullman (1979): Introduction to Automata Theory, Languages, and Computation.
Addison-Wesley.
[6] A.K. Joshi, K.V. Shanker & D. Weir (1990): The Convergence of Mildly Context-Sensitive Grammar
Formalisms. Technical Report No. MS-CIS-90-01, University of Pennsylvania. Available at http:
//repository.upenn.edu/cis_reports/539.
[7] I. Klyuchnikov (2010): Inferring and Proving Properties of Functional Programs by Means of Supercompilation. Ph. D. Thesis (in Russian), Keldysh Institute of Applied Mathematics of RAS, Moscow. Available at
http://keldysh.ru/council/1/klyuchnikov-diss.pdf.
[8] J.B. Kruskal (1960): Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi’s Conjecture. Transactions of
the American Mathematical Society 95, pp. 210–225, doi:10.2307/1993287.
[9] M. Leuschel (2002): Homeomorphic Embedding for Online Termination of Symbolic Methods, pp. 379–403.
Lecture Notes in Computer Science 2566, IEEE Computer Society Press, doi:10.1007/3-540-36377-7 17.
[10] C. St. J. A. Nash-Williams (1965): On Well-quasi-ordering Infinite Trees. Proceedings of Cambridge Philosophical Society 61, pp. 697–720, doi:10.1017/s0305004100039062.
[11] A. P. Nemytykh (2007): The Supercompiler Scp4: General Structure. URSS, Moscow. (In Russian).
[12] A. Nepeivoda (2014): Turchin’s Relation and Subsequence Relation in Loop Approximation. In:
PSI 2014. Ershov Informatics Conference. Poster Session, 23, EPiC Series, EasyChair, pp. 30–
42. Available at http://www.easychair.org/publications/download/Turchin_s_Relation_and_
Subsequence_Relation_in_Loop_Approximation.
[13] L. Puel (1989): Using Unavoidable Set of Trees to Generalize Kruskal’s Theorem. Journal of Symbolic
Computation 8, pp. 335–382, doi:10.1016/s0747-7171(89)80035-5.
[14] Y. Saouter (1995): Halting Problem for One-State Turing Machines. Research Report RR-2577, INRIA.
Available at https://hal.inria.fr/inria-00074105.

156

Turchin’s Relation for Call-by-Name Computations

[15] M. H. Sørensen & R. Glück (1995): An Algorithm of Generalization in Positive Supercompilation. In: Proceedings of ILPS’95, the International Logic Programming Symposium, MIT Press, pp. 465–479. Available
at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.1869.
[16] M.H. Sørensen (1994): Turchin’s Supercompiler Revisited. Ms.Thesis, Department of Computer Science,
University of Copenhagen. Available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=
10.1.1.50.8214&rep=rep1&type=pdf.
[17] M.H. Sørensen, R. Glück & N. D. Jones (1996): A Positive Supercompiler. Journal of Functional Programming 6, pp. 811–838, doi:10.1017/s0956796800002008.
[18] V. F. Turchin (1986): The Concept of a Supercompiler. ACM Transactions on Programming Languages and
Systems 8(3), pp. 292–325, doi:10.1145/5956.5957.
[19] V. F. Turchin (1989): Refal-5, Programming Guide and Reference Manual. New England Publishing Co.,
Holyoke, Massachusetts. Electronic version:http://www.botik.ru/pub/local/scp/refal5/.
[20] V.F. Turchin (1988): The algorithm of generalization in the supercompiler. Partial Evaluation and Mixed
Computation, pp. 341–353.

Appendix
6.1

Proof of Theorem 1 (Subsection 3.2)

Proof. It is sufficient to prove that, given an input word, every Turing machine on the input can be
emulated by a multi-layer prefix grammar treating the input word as its initial word.
Consider an arbitrary Turing machine hQ, ϒA , b, σ , q0 , Fi, where Q is a finite state alphabet, ϒA is
a finite tape alphabet, b is the blank symbol, q0 ∈ Q is the initial state, F ⊂ Q is a set of the final
states, σ ⊂ Q × ϒA × Q × ϒA × {L, R} is a set of transition rules, and an input I ∈ ϒ∗A . Let us introduce
a multi-layer prefix grammar with the alphabet ϒ = ϒA ∪ QR ∪ QL ∪ {BlankL , BlankR , b}, where QR and
QL are the state alphabet Q marked by the superscripts meaning “a state after moving to the right cell”
and “a state after moving to the left cell” correspondingly. BlankR and BlankL are special “end-marks”
referring to the blanks on the tape after the rightmost and leftmost cells reached by the machine head
in the computation. All blanks on the tape between them are denoted in the model grammar by usual b
symbols.
Let us assume in this proof that all labels in the model grammar are of the form si , where i is a
rational number (i ∈ Q), and si / s j iff i < j (i, j ∈ Q).
The initial word in the model grammar is
Γ0 $∆0 = hqR0 , s0 iIhs0 ihBlankR , s0 i$hBlankL , s1 i
In order to emulate a rule (q1 , a1 ) → (q2 , a2 , R) ∈ σ , we use one of the following two rewrite schemes,
where x is a letter variable:
hqR1 , si iha1 , s j iΦ$Ψhx, sk i → hqR2 , s j iΦ$Ψhx, sk iha2 , s j+k i
2

ha1 , s j ihqL1 , si iΦ$Ψhx, sk i → hqR2 , si iΦ$Ψhx, sk iha2 , s i+k i
2

A. Nepeivoda

157

In order to emulate a rule (q1 , a1 ) → (q2 , a2 , L), we use one of the following two schemes (sk =
child(si )):
hqR1 , si iha1 , s j iΦ$Ψhx, sk i → hx, sk ihqL2 , s j iha2 , s j iΦ$Ψ
ha1 , s j ihqL1 , si iΦ$Ψhx, sk i → hx, sk ihqL2 , si iha2 , si iΦ$Ψ
If q2 ∈ F, we put the corresponding rule scheme into the set of the halting rules.
So we model the tape part to the right of the machine head by the visible layer, and the tape part
to the left of the machine head by the invisible layer. The letters from QR ∪ QL can only appear in the
visible layer, and what is more, any letter from QR may be only the first letter of the visible layer, and
any letter from QL — the second letter of the visible layer.

6.2

Proof of Proposition 2 (Subsection 3.2)

Proof. First, we prove that the described class of the multi-layer prefix grammars is not weaker than the
class of the context-free grammars and the class of the one-state Turing machines.
For the one-state Turing machines, the corresponding model is constructed in the proof of Theorem 1.
Given a context-free language, we consider its generating context-free grammar C in the Greibach
normal form [3]. Let the set of non-terminals of C be Q and the set of terminals be T . We construct
a multi-layer grammar with the alphabet ϒ = T ∪ Q ∪ {[Pop]}. The initial word is hS, s0 ih[Pop], s0 i$Λ
where S is the initial symbol of C.
For every rule q1 → uq2 q3 , qi ∈ Q, u ∈ T of the context-free grammar C, we construct the rewriting
rule
hq1 , s0 iΦ$Ψ → hq2 q3 , s0 iΦ$Ψhu, s1 i
For a rule q1 → Λ we construct the rule
hq1 , s0 iΦ$Ψ → Φ$Ψ
Finally, we add the halting rule R[Stop]
h[Pop], s0 iΦ$Ψ → Ψhs1 iΦ$Ψhs1 i
Because all invisible letters are labelled by s1 and [Pop] can only be generated in the initial word,
rule R[Stop] actually looks as h[Pop], s0 i$Ψhs1 i → Ψhs1 i$Λ.
Since the alphabetic multi-layer grammars generate all context-free languages and all languages
generated by one-state Turing machines, they are stronger than the one-state Turing machines (some
regular languages cannot be generated by such a machine [14]).
In order to prove that the alphabetic multi-layer prefix grammars are stronger than the context-free
n
grammars, it is sufficient to show that the language {b2 |n ∈ N} can be generated by such a grammar
(such a language cannot be generated by any context-free grammar [5]). We assume that sΓ / s∆ iff the
word Γ is a prefix of the word ∆. Otherwise, sΓ and s∆ are incomparable.

158

Turchin’s Relation for Call-by-Name Computations

Let the initial word of the grammar GExpLang be ha, s0 i$hbb, s01 i. The set of rewriting rules of
GExpLang is as follows.
R[1] : ha, s0 iΦ$Ψ → Ψhchild(s0 )iha, s0 iΦ$Ψhchild(s0 )i
R[2] : ha, s0 i$Ψ → Ψhchild(s0 )i$Ψhchild(s0 )i
R[3] : hb, si iΦ$Ψ → Φ$ Appsi1 [bb](Ψ)
Rule R[2] is the halting rule.
We consider the tree of the possible traces generated by grammar GExpLang (its fragment is shown in
Figure 6.2). All the letters in the invisible parts of the words in the trace have a single label. Thus, when
a pop rule is applied to a word in the trace, it pops all the letters from the invisible layer.

u

R[2]

ha, s0 i$hbb, s01 i

R[1]

hbb, s01 i$Λ

+

hbb, s01 iha, s0 i$Λ
[3]
R

hb, s01 iha, s0 i$hbb, s011 i
[3]
R

s

R[2]

ha, s0 i$hbbbb, s011 i
R[1]

. . .

hbbbb, s011 i$Λ



R[2]

... s

ha, s0 i$hb8 , s0111 i

R[1]

*. . .

Figure 15: A fragment of the tree of the possible traces generated by GExpLang

n

The resulting language {b2 |n ∈ N} is not even mildly context-sensitive16 [5].

16 The class of mildly context-sensitive grammars is a special subclass of context-sensitive grammars that includes not only
all context-free grammars, but also, e. g., tree adjoining grammars [6].

A. Nepeivoda

159

f (h(x))

Term:
Stack:

h h f , s0 i$Λ

Term:
Stack:

f (g(x1 ) + 1)
h f , s0 i$hg, s1 i



x=0

w
f (0)

x=x1 +1




f (g(g(x1 ) + 1)) + 1
hg f , s0 i$hg, s1 i

Term:
Stack:

0


Term:
Stack:

f (h(g(x1 ))) + 1
hg, s1 ihh f , s0 i$Λ

Term:
Stack:

f (h(h(x2 ))) + 1
hh, s1 ihh f , s0 i$Λ

x1 =0

t
f (h(0)) + 1




x2 =0

t

x1 =x2 +1

f (h(g(x3 ) + 1)) + 1

Term:

f (h(0)) + 1
Stack:

x2 =x3 +1

h h f , s0 i$hg, s2 i

Generalization of f (h(g(x3 ) + 1)) + 1 and f (h(x)) is built
Term:

f (h(x))

Stack:

h h f , s0 i$Λ

Term:
Stack:

f (g(x1 ) + 1)
h f , s0 i$hg, s1 i

x=0

f (0)

v

o

 x=x1 +1




Term:
Stack:

0

f (g(g(x1 ) + 1)) + 1
hg f , s0 i$hg, s1 i


f (h(g(x1 ))) + 1
hg, s1 ihh f , s0 i$Λ

Term:
Stack:

f (h(h(x2 ))) + 1
hh, s1 ihh f , s0 i$Λ

x1 =0

t
f (h(0)) + 1

f (h(0)) + 1

 x2 =x3 +1
let z = g(x3 ) + 1 in f (h(z)) + 1

u
g(x3 ) + 1
hg,t0 i$Λ

 x1 =x2 +1

x2 =0

t

Term:
Stack:

Term:
Stack:


Term:

f (h(z)) + 1

Stack:

h h f , s0 i$Λ

A fragment of the graph after the generalization
Figure 16: Generalization using the composition of Turchin’s relation and the homeomorphic embedding.
Example 10

