A Scheme-Driven Approach to Learning
Programs from Input/Output Equations
Jochen Burghardt
jochen.burghardt alumni.tu-berlin.de
Feb 2018

arXiv:1802.01177v1 [cs.LO] 4 Feb 2018

Abstract
We describe an approach to learn, in a term-rewriting setting, function definitions
from input/output equations. By confining ourselves to structurally recursive definitions we obtain a fairly fast learning algorithm that often yields definitions close
to intuitive expectations. We provide a Prolog prototype implementation of our
approach, and indicate open issues of further investigation.
Key words: inductive functional programming

Contents
1

Introduction

2

2

The task of learning functions

3

3

Learning functions by anti-unification

4

4

Learning functions by structural recursion

5

5

Possible extensions

10

A

Example runs of our prototype implementation

15

References

19

1

1

Introduction

This paper describes an approach to learn function definitions from input/output equations. 1
In trivial cases, a definition is obtained by syntactical anti-unification of the given i/o equations.
In non-trivial cases, we assume a structurally recursive function definition, and transform the
given i/o equations into equations for the employed auxiliary functions. The latter are learned
from their i/o equations in turn, until a trivial case is reached.
We came up with this approach in 1994 but didn’t publish it until today. In this paper, we
explain it mainly along some learning examples, leaving a theoretical elaboration to be done.
Also, we indicate several issues of improvement that should be investigated further. However,
we provide at least a Prolog prototype implementation of our approach.
In the rest of this section, we introduce the term-rewriting setting our approach works in. In
Sect. 2, we define the task of function learning. In Sect. 3 and 4, we explain the base case and
the inductive case of our approach, that is, how to learn trivial functions, and how to reduce
learning sophisticated functions to learning easier functions, respectively. Section 5 sketches
some ideas for possible extensions to our approach; it also shows its limitations. Some runs of
our Prolog prototype are shown in Appendix A.
nat
list
tree
blist

1:
2:
3:
4:

::=
::=
::=
::=

0
nil
null
nl

|
s(nat)
|
nat::list
| nd(tree, nat, tree)
|
o(blist)
| i(blist)

natural numbers
lists of natural numbers
binary trees of natural numbers
list of binary digits

Figure 1. Employed sort definitions

We use a term-rewriting setting that is well-known from functional programming: A sort can
be defined recursively by giving its constructors. For example, sort definition 1, shown in
Fig. 1, defines the sort nat of all natural numbers in 0-s notation. In this example, we use 0
as a nullary, and s as a unary constructor.
5:
6:
7:
8:
9:
10:
11:

+
∗
lgth
app
size
dup
add

:
:
:
:
:
:
:

nat × nat
nat × nat
list
list × list
tree
nat
blist × blist

−→
−→
−→
−→
−→
−→
−→

nat
nat
nat
list
nat
nat
blist

addition of natural numbers
multiplication of natural numbers
number of elements of a list
concatenation of lists
number of elements of a binary tree
duplicating a natural number
addition of binary numbers (lists)

Figure 2. Employed function signatures

A sort is understood as representing a possibly infinite set of ground constructor terms, 2 e.g. the
1

We will use henceforth “i/o equations” for brevity. We avoid calling them “examples” as this could
cause confusion when we explain our approach along example sort definitions, example signatures, and
example functions.
2 i.e. terms without variables, built only from constructor symbols

2

12:
13:
14:
15:
16:
17:
18:
19:
20:
21:

x+0
x+s(y)
x∗0
x∗s(y)
lgth(nil)
lgth(x::y)
app(nil, z)
app(x::y, z)
size(null)
size(nd(x, y, z))

=
=
=
=
=
=
=
=
=
=

x
s(x+y)
0
x+x∗y
0
s(lgth(y))
z
x::app(y, z)
0
s(size(x)+size(z))

Figure 3. Example function definitions

sort nat represents the set {0, s(0), s(s(0)), s(s(s(0))), . . .}. A function has a fixed signature;
Fig. 2 gives some examples. The signature of a constructor can be inferred from the sort
definition it occurs in, e.g. 0 :−→ nat and s : nat −→ nat. We don’t allow non-trivial equations
between constructor terms, therefore, we have T1 = T2 iff T1 syntactically equals T2 , for all
ground constructor terms T1 , T2 .
A non-constructor function can be defined by giving a terminating ([DJ90, Sect.5.1, p.270])
term rewriting system for it such that its left-hand sides are sufficiently complete ([Gut77],
[Com86], [DJ90, Sect.3.2, p.264]). Examples for function definitions are shown in Fig. 3.
Given some functions f1 , . . . , fm defined by such a term rewriting system, for each i and each
ground constructor terms T1 , . . . , Tn we can find a unique ground constructor term T such that
fi (T1 , . . . , Tn ) = T . We then say that fi (T1 , . . . , Tn ) evaluates to T .
Given a term T , we denote by vars(T ) the set of variables occurring in T .

2

The task of learning functions

The problem our approach shall solve is the following. Given a set of sort definitions, a
non-constructor function symbol f , its signature, and a set of input/output equations
for f , construct a term rewriting system defining f such that it behaves as prescribed by the
i/o equations. We say that we want to learn a definition for f , or sloppily, that we want to
learn f , from the given i/o equations.
For example, given sort definition 1, signature 10, and the following input/output ground equations
22:
dup(0) = 0
23:
dup(s(0)) = s(s(0))
24:
dup(s(s(0))) = s(s(s(s(0))))
25:
dup(s(s(s(0)))) = s(s(s(s(s(s(0))))))
we are looking for a definition of dup such that equations
3

22, 23, 24,

and

25

hold.

One such

definition is
dup(0) = 0
dup(s(x)) = s(s(dup(x)))

26:
27:

We say that this definition covers the i/o equations
28:
29:

22, 23, 24,

and

25.

In contrast, a definition

dup(0) = 0
dup(s(x)) = s(s(x))

would cover i/o equations 22 and 23, but neither 24 nor 25. We wouldn’t accept this definition,
since we are interested only in function definitions that cover all given i/o equations.
It is well-known that there isn’t a unique solution to our problem. In fact, given i/o equations
f (L1 ) = R1 , . . . , f (Ln ) = Rn and an arbitrary function g of appropriate domain and range, e.g.
the function defined by 3
f (x) = ( if x = L1 then R1 elif . . . elif x = Ln then Rn else g(x) fi )
trivially covers all i/o equations. Usually, the “simplest” function definitions are preferred,
with “simplicity” being some user-defined measure loosely corresponding to term size and/or
case-distinction count, like e.g. in [Bur05, p.8] and [Kit10, p.77]. However, the notion of
simplicity depends on the language of available basic operations. 4 In the end, the notion of
a “good” definition can hardly be defined more precisely than being one that meets common
human prejudice. From our prototype runs we got the feeling that our approach often yields
“good” definition in that sense.

3

Learning functions by anti-unification

One of the simplest ways to obtain a function definition is to syntactically anti-unify the given
i/o equations.
Given i/o equations

f (L11 , . . . ,Lm1 ) = R1
..
..
..
.
.
.
f (L1n , . . . ,Lmn ) = Rn ,

let

f ( L1 , . . . , Lm ) = R

be their least general generalization (lgg for short, see [Plo70,Plo71,Rey70]). If the variable
condition vars(R) ⊆ vars(L1 ) ∪ . . . ∪ vars(Lm ) holds, then the lgg will cover all n given i/o
equations.
3

We use common imperative notation here for sake of readability.
The “invariance theorem” in Kolmogorov complexity theory (e.g. [LV08, p.105, Thm.2.1.1]) implies
that ∀L1 , L2 ∃c ∀x : |CL1 (x) − CL2 (x)| 6 c, where the Li range over Turing-complete algorithm
description languages, c is a natural number, x ranges over i/o equation sets, and CL (x) denotes the
length of the shortest function definition, written in L, that covers x. This theorem is sometimes
misunderstood to enable a language-independent notion of simplicity; however, it does not, at least
for small i/o example sets.
4

4

For example, assume we are to generate a definition for a unary function called g2
from the i/o equations

32:

g2 (
0
) = s(s(
0
))
g2 ( s(s(0)) ) = s(s( s(s(0)) ))
g2 (s(s(s(s(0))))) = s(s(s(s(s(s(0)))))) .

33:

g2 (

30:
31:

We obtain the lgg

x024

) = s(s(

x024

))

As another example, we can generate a definition for a binary function called g4
from the i/o equations

36:

g4 (a, 0 ) = s( 0 )
g4 (a, s(0) ) = s( s(0) )
g4 (a,s(s(0))) = s(s(s(0))) .

37:

g4 (a, y012 ) = s( y012 )

34:
35:

We obtain the lgg
which satisfies the variable condition. 5
equations 36, 35, and 34.

Hence when g4 is defined by equation

37,

it covers i/o

As a counter-example, the lgg of the above
dup i/o equations

25

dup(
0
)
dup( s(0) )
dup( s(s(0)) )
dup(s(s(s(0))))

38:

dup( x0123

22
23
24

is computed as

=
0
=
s(s(0))
= s(s(s(s(0))))
= s(s(s(s(s(s(0))))))

)=

x0246

which violates the variable condition, and thus cannot be used to reduce a term dup(T ) to a
ground constructor term, i.e. to evaluate dup(T ).
The above anti-unification approach can be extended in several ways, they are sketched in
Sect. 5.1. However, in all but trivial cases, an lgg will violate the variable condition, and we
need another approach to learn a function definition.

4

Learning functions by structural recursion

For a function f that can’t be learned by Sect. 3, we assume a defining term rewriting system
that follows a structural recursion scheme obtained from f ’s signature and a guessed argument
position.
For example, for the function dup with the signature given in 10 and the only possible argument
position, 1, we obtain the schematic equations
39:
40:

dup(0) = g1
dup(s(x)) = g2 (dup(x))

5

Whenever applied to terms T1 , . . . , Tm that don’t start all with the same function symbol, Plotkin’s
lgg algorithm returns a variable that uniquely depends on T1 , . . . , Tm . We indicate the originating
terms by an index sequence; e.g. y012 was obtained as lgg(0, s(0), s(s(0))).

5

where g1 and g2 are fresh names of non-constructor functions.
If we could learn appropriate definitions for g1 and g2 , we could obtain a definition for dup just
by adding equations 39 and 40. The choice of g1 is obvious:
41:

22

39

0 = dup(0) = g1

In order to learn a definition for g2 , we need to obtain appropriate i/o examples for g2 from
those for dup. Joining equation 40 with dup’s relevant i/o equations yields three i/o equations
for g2 :
23

40

22

s(s(0))
= dup(s(0)) = g2 (dup(0)) =
g2 (0)
24
40
23
s(s(s(s(0)))) = dup(s(s(0))) = g2 (dup(s(0))) = g2 (s(s(0)))
25
40
24
s(s(s(s(s(s(0)))))) = dup(s(s(s(0)))) = g2 (dup(s(s(0)))) = g2 (s(s(s(s(0))))

30
31
32

A definition for g2 covering its i/o examples 30, 31, and 32 has already been derived by antiunification in Sect. 3 as
33
g2 (x024 ) = s(s(x024 )) .
Altogether, we obtain the rewriting system
dup(0)
dup(s(x))
g1
g2 (x024 )

39
40
41
33

=
g1
= g2 (dup(x))
=
0
= s(s(x024 ))

as a definition for dup that covers its i/o equations 22, 23, 24, and 25. Subsequently, this system
may be simplified, by inlining, to
dup(0) =
0
dup(s(x)) = s(s(dup(x)))

39
40

which is the usual definition of the dup function.
Returning to the computation of i/o equations for g2 from those for dup, note that g2 ’s derived
i/o equations 30, 31, and 32 were necessary in the sense that they must be satisfied by each
possible definition of g2 that leads to dup covering its i/o equations (23, 24, and 25). Conversely,
g2 ’s i/o equations were also sufficient in the sense that each possible definition of g2 covering
them ensures that dup covers 23, 24, and 25, provided it covers 22:
Proof of
Proof of
Proof of

23:
24:
25:

40

22

30

dup(s(0)) = g2 (dup(0)) =
g2 (0)
=
s(s(0))
40
23
31
dup(s(s(0))) = g2 (dup(s(0))) = g2 (s(s(0))) = s(s(s(s(0))))
40
24
32
dup(s(s(s(0)))) = g2 (dup(s(s(0)))) = g2 (s(s(s(s(0))))) = s(s(s(s(s(s(0))))))

Observe that the above proofs are based just on permutations of the equation chains from 30,
31, and 32.
Moreover, note that the coverage proof for dup(s(T )) relies on the coverage for
dup(T ) already being proven. That is, the coverage proofs follow the employed structural
recursion scheme. As for the base case, g1 ’s coverage of 41 is of course necessary and sufficient
for dup’s coverage of 22.
6

4.1

Non-ground i/o equations

As an example that uses i/o equations containing variables, consider the function lgth, with the
signature given in 7. Usually, i/o equations for this functions are given in a way that indicates
that the particular values of the list elements don’t matter. For example, an i/o equation like
lgth(a::b::nil) = s(s(0)) is seen much more often than lgth(s(0)::0::nil) = s(s(0)). Our approach
allows for variables in i/o equations, and treats them as universally quantified. That is, a
non-ground i/o equation is covered by a function definition iff all its ground instances are.
Assume for example we are given the i/o equations
lgth(nil)
lgth(a::nil)
lgth(a::b::nil)
lgth(a::b::c::nil)

42:
43:
44:
45:

=
=
=
=

0
.
s(0)
s(s(0))
s(s(s(0)))

Given the signature of lgth (see 7) and argument position 1, we obtain a structural recursion
scheme
46:
lgth(nil) = g3
47:
lgth(x::y) = g4 (x, lgth(y)) .
Similar to the dup example, we get
48:

42

46

0 = lgth(nil) = g3 ,

and we can obtain i/o equations for g4 from those for lgth: 6
34
35
36

43

47

42

s(0) = lgth(a::nil) = g4 (a, lgth(nil)) = g4 (a, 0)
44
47
43
s(s(0)) = lgth(a::b::nil) = g4 (a, lgth(b::nil)) = g4 (a, s(0))
45
47
44
s(s(s(0))) = lgth(a::b::c::nil) = g4 (a, lgth(b::c::nil)) = g4 (a, s(s(0)))

Again, a function definition covering these i/o equation happens to have been derived by antiunification in Sect. 3:
37
g4 (a, y012 ) = s(y012 )
Altogether, equations 46, 47, 48, and 37 build a rewriting system for lgth that covers all its
given i/o equations. By subsequently inlining g3 ’s and g4 ’s definition, we obtain a simplified
definition for lgth:
49:
lgth(nil) = 0
50:
lgth(x::y) = s(lgth(y))
which agrees with the usual one found in textbooks.
Similar to the ground case, g4 ’s derived i/o equations
6

34, 35,

and

36

were necessary for lgth

In the rightmost equation of each line, we employ a renaming substitution. For example, we apply
{a 7→ b, b 7→ c} to i/o equation 44 in line 36. For this reason, our approach wouldn’t work if a, b, c
were considered non-constructor constants rather than universally quantified variables.

7

covering its i/o equations. And as in the ground case, they are also sufficient:
Proof of
Proof of
Proof of

43:
44:
45:

47

42

Again, renaming substitutions were used in the application of

4.2

34

lgth(a::nil) = g4 (a, lgth(nil)) =
g4 (a, 0)
= s(0)
47
43
35
lgth(a::b::nil) = g4 (a, lgth(b::nil)) = g4 (a, s(0)) = s(s(0))
47
44
36
lgth(a::b::c::nil) = g4 (a, lgth(b::c::nil)) = g4 (a, s(s(0)))) = s(s(s(0)))
43

and

44.

Functions of higher arity

For functions with more than one argument, we have several choices of the argument on which
to do the recursion. In these cases, we currently systematically try all argument positions 7
in succession. This is feasible since
• our approach is quite simple, and hence fast to compute, and
• we have a sharp and easy to compute criterion (viz. coverage 8 of all i/o examples) to decide
whether recursion on a given argument was successful.
For the function +, with the signature given in 5, and argument position 2, we obtain the
structural recursion scheme
51:
52:

x+0 = g5 (x)
x+s(y) = g6 (x, x+y) .

Appendix A.1 shows a run of our Prolog prototype implementation that obtains a definition
for +. In Sect. 5.2, we discuss possible extensions of the structural recursion scheme, like
simultaneous recursion.

4.3

Constructors with more than one recursion argument

When computing a structural recursion scheme, we may encounter a sort s with a constructor
that takes more than one argument of sort s. A common example is the sort of all binary trees
(of natural numbers), as given in 3. The function size, with the signature given in 9, computes
the size of such a tree, i.e. the total number of nd nodes. A recursion scheme for the size and
argument position 1 looks like:
53:
54:

size(null) = g9
size(nd(x, y, z)) = g10 (y, size(x), size(z))

7

In particular, the recursive argument’s sort and the function’s result sort needn’t be related in any
way, as the lgth example above demonstrates.
8 Checking if an i/o equation is covered by a definition requires executing the latter on the lhs arguments of the former. Our structural recursion approach ensures the termination of such computations,
and establishes an upper bound for the number of rewrite steps. For example, g2 and g4 , defined in 33
and 37, respectively, need one such step, while their callers dup and lgth, defined in 39,40 and 46,47,
respectively, need a linear amount of steps. An upper-bound expression for learned functions’ time
complexity remains to be defined and proven.

8

In App. A.2, we show a prototype run to obtain a definition for size.

4.4

General approach

In the previous sections, we have introduced our approach using particular examples. In this
section, we sketch a more abstract and algorithmic description.
Given a function and its signature f : s1 × . . . × sn −→ s, and given one of its argument
positions 1 6 i 6 n, we can easily obtain a term rewriting system to define f by structural
recursion on its ith argument. Assume in the definition of f ’s ith domain sort si we have an
alternative
si ::= . . . | c(s01 , . . . , s0l ) | . . . ,
assume {s0ν(1) , . . . , s0ν(m) } 63 si is the set of non-recursive arguments of the constructor c, and
s0ρ(1) = . . . = s0ρ(k) = si are the recursive arguments of c. Let g be a new function symbol. We
build an equation
f (x1 , . . . , xi−1 , c(y1 , . . . , yl ), xi+1 , . . . , xn )
=
g(x1 , . . . , xi−1 , xi+1 , . . . , xn , yν(1) , . . . , yν(m) ,
f (x1 , . . . , xi−1 , yρ(1) , xi+1 , . . . , xn )
...
f (x1 , . . . , xi−1 , yρ(k) , xi+1 , . . . , xn )
)
In a somewhat simplified presentation, we build the equation
f (. . . , c(y1 , . . . , yl ), . . .) = g(. . . , f (..., yρ(1) , ...), . . . , f (..., yρ(k) , ...)).

From the i/o equations for f , we often 9 can construct i/o equations for g: If we have an
i/o equation that matches the above equation’s left-hand side, and we have all i/o equations
needed to evaluate the recursive calls to f on its right-hand side, we can build an i/o equation
equation for g.
This way, we can reduce the problem of synthesizing a definition for f that reproduces the given
i/o equations to the problem of synthesizing a definition for g from its i/o equations. As a base
case for this process, we may synthesize non-recursive function definitions by anti-unification
of the i/o equations.
It should be possible to prove that f covers all its i/o equations iff g covers its, under some
appropriate conditions. We expect that a sufficient condition is that all recursive calls to f
could be evaluated. At least, we could demonstrate this in the above dup and lgth example.

9

Our construction isn’t successful in all cases.

We give a counter-example in Sect. 5.3

9

Fct Eqn Lf Rg Fct Eqn Lf Rg
22
23

dup

24
25

2
3
4
5

1 g1
3
5 g2
7

41
30
31
32

1
2
4
6

1
3
5
7

Figure 4. Left- and right-hand term sizes of i/o equations for dup and g2

4.5

Termination

In order to establish the termination of our approach, it is necessary to define a criterion by
which g is easier to learn from it i/o equations than f is from its. Term size or height cannot
be used in a termination ordering; when proceeding from f to g they may remain equal, or may
even increase, as shown in Fig. 4 for the dup vs. g2 example.
However, the number of i/o equations decreases in this example, and in all other ones we dealt
with. A sufficient criterion for this is that f ’s i/o equations don’t all have the same left-hand
side top-most constructor. However, the same criterion would have to be ensured in turn for
g, and it is not obvious how to achieve this.
In any case, by construction of g’s i/o example from f ’s, no new terms can arise. 10 Even
more, each term appearing in an i/o example for g originates from a right-hand side of an i/o
example for f . Therefore, our approach can’t continue generating new auxiliary functions
forever, without eventually repeating the set of i/o equations. Our prototype implementation
doesn’t check for such repetitions, however.

5

Possible extensions

In this section, we briefly sketch some possible extensions of our approach. Their investigation
in detail still remains to be done.

5.1

Extension of anti-unification

In Sect. 3 we used syntactical anti-unification to obtain a function definition, as a base case of
our approach. Several way to extend this technique can be thought of.

Set anti-unification It can be tried to split the set of i/o equations into disjoint subsets
such that from each one an lgg satisfying the variable condition is obtained. This results in
several defining equations. An additional constraint might be that each subset corresponds to
another constructor symbol, observed at some given fixed position in the left-hand side terms.
10

except for the fresh left-hand side top function symbols

10

sq(
0
)
sq( s(0) )
sq( s(s(0)) )
sq(s(s(s(0))))
sq( x0123 )

56:
57:
58:
59:
60:

=
0
=
s(0)
= s(s(s(s(0))))
=
s9 (0)
= x0123 ∗x0123

Figure 5. Application of E-anti-unification to learn squaring

Anti-unification modulo equational theory Another extension consists in considering an
equational background theory E in anti-unification; it wasn’t readily investigated in 1994. See
[Hei94b,Hei94a,Hei95] for the earliest publications, and [Bur05,Bur17] for the latest.
As of today, the main application of E-anti-unification turned out to be the synthesis of nonrecursive function definitions from input/ output equations [Bur17, p.3]. To sketch an example,
let E consist just of definitions 12, 13, 14, and 15.
Assume the signature
55:

sq : nat −→ nat

and the i/o equations 56, 57, 58, and 59 of the squaring function. Applying syntactical antiunification to the left-hand sides yields a variable x0123 , and four corresponding substitutions.
Applying constrained E-generalization [Bur05, p.5, Def.2] to the right-hand sides yields a term
set that contains x0123 ∗x0123 as a minimal-size member, see Fig. 5.

Depth-bounded anti-unification In many cases, defining equations obtained by syntactical
anti-unification appear to be too particular. For example, s4 (0) and s9 (0) are generalized to
s4 (x05 ), while being by 4 greater than something wouldn’t be the first choice for a common
property of both numbers for most humans. As a possible remedy, a maximal depth d may be
introduced for the anti-unification algorithm. Beyond this depth, terms are generalized by a
variable even if all their root function symbols agree. Denoting by lgg d (t1 , t2 ) the result of an
appropriately modified algorithm, it should be easy to prove that lgg d (t1 , t2 ) can be instantiated
to both t1 and t2 , and is the most special term with that property among all terms of depth up
to d. If d is chosen as ∞, lgg d and lgg coincide.
In our prototype implementation, we meanwhile built in such a depth boundary. Figure 6
compares the learned function definitions for size for d = 2, 3, 4 (top to bottom). For example,
for d = 2, the —nonsensical— equation size(x) = 0 is learned, while for d > 3 the respective
equation reads size(null) = 0. Not surprisingly, for d = 2 only one of the given 9 i/o equations
is covered. For d 6 1, the attempt to learn defining equations for size fails.
For d = 4, the learned equations agree with those for d = ∞, and hence also with those for
all intermediate depths. The prototype run for d = ∞ is shown in App. A.2. Note that the
prototype simplifies equations by removing irrelevant function arguments. For this reason,
f12 there has only two arguments, while the corresponding function f1 in Fig. 6 has three.
11

x
)=0
null
null
size( nd(x, y, z) ) = f1 ( y, size(x), size(z))
size(

y
f1 (x, 0 ,
0
f1 (x, s(y) ,

z

) = s(

z

)

z

) = f2 ( x, z, f1 (x, y, z))

y
z
z
f2 (x, 0 , s(z) ) = s( s(z) )
0
s(0)
s(0)
y
z
z
f2 (x, s(y) , s(z) ) = s( s(z) )
s(y) s(s(z))
s(s(z))
Figure 6. Learned tree size definition for anti-unification depth 2, 3, and 4

5.2

Extension of structural recursion

Some functions are best defined by simultaneous recursion on several arguments. As an
example, consider the sort definition 4 with nl, o, and i denoting an empty list, a 0 digit, and
a 1 digit, respectively. For technical reasons, such a list is interpreted in reversed order, e.g.
o(i(i(nl))) denotes the number 6. The sum function add, its signature shown in 11, may then
be defined by the following rewrite system:

61:
62:
63:
64:
65:
66:

add( x , nl )
add( nl , y )
add(o(x),o(y))
add(o(x), i(y) )
add( i(x) ,o(y))
add( i(x) , i(y) )

=
=
=
=
=
=

x
y
o(add(x, y))
i(add(x, y))
i(add(x, y))
o(inc(add(x, y)))

where
67:

inc : blist −→ blist

is a function to increment a binary digit list.
mentation, with inc being used for the carry.

This corresponds to the usual hardware imple-

It is obvious that this definition cannot be obtained from our simple structural recursion scheme
from Sect. 4, neither by recurring over argument position 1 nor over 2. Instead, we would need
12

recursion over both positions simultaneously, i.e. a scheme like
68:
69:
70:
71:
72:
73:
74:
75:
76:

add( nl , nl )
add( nl ,o(y))
add( nl , i(y) )
add(o(x), nl )
add(o(x),o(y))
add(o(x), i(y) )
add( i(x) , nl )
add( i(x) ,o(y))
add( i(x) , i(y) )

=
=
=
=
=
=
=
=
=

g15
g16 (y)
g17 (y)
g18 (x)
g19 (add(x, y))
g20 (add(x, y))
g21 (x)
g22 (add(x, y))
g23 (add(x, y))

An extension of our approach could provide such a scheme, additionally to the simple structural
recursion scheme.
If we could prove that each function definition obtainable by the simple recursion scheme can
also be obtained by a simultaneous recursion scheme, we needed only to employ the latter. This
way, we would no longer need to guess an appropriate argument position to recur over; instead
we could always recur simultaneously over all arguments of a given sort. Unfortunately, simultaneous recursion is not stronger than simple structural recursion. For example, the function
app to concatenate two given lists can be obtained by simple recursion over the first argument
(see 18,19 in Fig. 3), but not by simultaneous recursion: app(w::x, y::z) = g24 (w, y, app(x, z))
doesn’t lead to a sensible definition, for any choice of g24 .
One possible remedy is to try simple structural recursion first, on any appropriate argument
position, and simultaneous recursion next, on any appropriate set of argument positions. Alternatively, user commands may be required about which recursion to try on which argument
position(s).
Another possibility might be to employ a fully general structural recursion scheme, like
77:

and

78:

app(w::x, y::z) = g24 (w, y, app(w::x, z) , app(x, y::z) , app(x, z) )
add(o(x), o(y)) =
g25 ( add(o(x), y) , add(x, o(y)) , add(x, y) ) .

In this scheme, calls for simple recursion over each position are provided, as well as for simultaneous recursion over each position set. A new symbol Ω, intended to denote an undefined
term, could be added to the term language. When e.g. i/o equations are missing to compute add(o(x), y) for some particular instance, the first argument of g25 would be set to Ω in
the respective i/o equation. In syntactical anti-unification and coverage test, Ω needed to be
handled appropriately. This way, only one recursion scheme would be needed, and no choice of
appropriate argument position(s) would be necessary. However, arities of auxiliary functions
might grow exponentially.

5.3

Limitations of our approach

In this section, we demonstrate an example where our approach fails. Consider again the
squaring function, its signature shown in 55, and consider again its i/o equations 56, 57, 58,
13

and

59.

Since syntactical anti-unification as in Sect. 3 (i.e. not considering an equational background
theory E) doesn’t lead to a valid function definition, we build a structural recursion scheme as
in Sect. 4:
79:
sq(0) = g11
80:
sq(s(x)) = g12 (sq(x))
We get g11 = 0, and the following i/o equations for g12 :
57

80

56

s(0)
= sq(s(0)) = g12 (sq(0)) =
g12 (0)
58
80
57
s(s(s(s(0)))) = sq(s(s(0))) = g12 (sq(s(0))) =
g12 (s(0))
59
80
58
9
s (0)
= sq(s(s(s(0)))) = g12 (sq(s(s(0)))) = g12 (s(s(s(s(0)))))

81:
82:
83:

Observe that we are able to obtain i/o equations for g12 only on square numbers. For example,
there is no obvious way to determine the value of g12 (s(s(s(0)))).
Syntactically anti-unifying g12 ’s i/o equation still doesn’t yield a valid function definition. So
we set up a recursion scheme for g12 , in turn:
84:
85:

g12 (0) = g13
g12 (s(x)) = g14 (g12 (x))

Again, g13 = s(0) is obvious. Trying to obtain i/o equations for g14 , we get stuck, since we
don’t know how g12 should behave on non-square numbers:
86:
87:
88:
89:

s(s(s(s(0))))
??
??
9
s (0)

82

=
g12 (s(0))
??
= g12 (s(s(0)))
??
= g12 (s(s(s(0))))
83
= g12 (s(s(s(s(0)))))

As an alternative, by applying
90:

85

85

=
g14 (g12 (0))
85
= g14 (g12 (s(0)))
85
= g14 (g12 (s(s(0))))
85
= g14 (g12 (s(s(s(0)))))

81

=
g14 (s(0))
= g14 (s(s(s(s(0)))))
??
=
g14 (??)
??
=
g14 (??)

82

sufficiently often rather than just once, we can obtain:

83

s9 (0) =
g12 (s(s(s(s(0)))))
85
= g14 (g12 (s(s(s(0)))))
85
= g14 (g14 (g12 (s(s(0)))))
85
82
= g14 (g14 (g14 (g12 (s(0))))) = g14 (g14 (g14 (s(s(s(s(0)))))))

However, no approach is known to learn g14 from an extended i/o equation like 90, which
determines g14 ◦ g14 ◦ g14 rather than g14 itself. In such cases, we resort to the excuse that the
original function, sq isn’t definable by structural recursion.
A precise criterion for the class that our approach can handle is still to be found. It is not
even clear that such a criterion can be computable. If not, it should still be possible to give
computable necessary and sufficient approximations.

14

A

A.1

Example runs of our prototype implementation

Addition of 0-s numbers

?- SgI = [ + signature [nat,nat] --> nat],
|
SD = [ nat sortdef 0 ! s(nat)],
|
ExI = [ 0
+ 0
= 0,
|
s(0)
+ 0
= s(0),
|
0
+ s(0)
= s(0),
|
0
+ s(s(0))
= s(s(0)),
|
s(0)
+ s(0)
= s(s(0)),
|
s(0)
+ s(s(0))
= s(s(s(0))),
|
s(s(0)) + s(0)
= s(s(s(0))),
|
s(s(0)) + 0
= s(s(0))],
|
run(+,SgI,SD,ExI).
+++++ Examples input check:
+++++ Example 1:
+++++ Example 2:
+++++ Example 3:
+++++ Example 4:
+++++ Example 5:
+++++ Example 6:
+++++ Example 7:
+++++ Example 8:
+++++ Examples input check done
induce(+)
. trying argument position:
1
. inducePos(+,1,0)
. . matching examples: [0+0=0,0+s(0)=s(0),0+s(s(0))=s(s(0))]
. . anti-unifier:
0+v3 = v3
. inducePos(+,1,0)
. inducePos(+,1,s(nat))
. . matching examples: [s(0)+0=s(0),s(0)+s(0)=s(s(0)),s(0)+s(s(0))=s(s(s(0))),s(s(0))+s(0)=s(s(s(0))),s(s(0))+0=s(s(0))]
. . new recursion scheme:
s(v9)+v8 = f10(v8,v9+v8)
. . derive new equation:
s(0) = s(0)+0 = f10(0,0)
. . derive new equation:
s(s(0)) = s(0)+s(0) = f10(s(0),s(0))
. . derive new equation:
s(s(s(0))) = s(0)+s(s(0)) = f10(s(s(0)),s(s(0)))
. . derive new equation:
s(s(s(0))) = s(s(0))+s(0) = f10(s(0),s(s(0)))
. . derive new equation:
s(s(0)) = s(s(0))+0 = f10(0,s(0))
. . induce(f10)
. . . trying argument position: 1
. . . inducePos(f10,1,0)
. . . . matching examples:
[f10(0,0)=s(0),f10(0,s(0))=s(s(0))]
. . . . anti-unifier:
f10(0,v13) = s(v13)
. . . inducePos(f10,1,0)
. . . inducePos(f10,1,s(nat))
. . . . matching examples:
[f10(s(0),s(0))=s(s(0)),f10(s(0),s(s(0)))=s(s(s(0))),f10(s(s(0)),s(s(0)))=s(s(s(0)))]
. . . . anti-unifier:
f10(s(v15),s(v16)) = s(s(v16))
. . . inducePos(f10,1,s(nat))
. . . all examples covered
. . induce(f10)
. inducePos(+,1,s(nat))
. all examples covered
induce(+)
+++++ Examples output check:
+++++ Examples output check done
FUNCTION SIGNATURES:
f10 signature [nat,nat]-->nat
(+)signature[nat,nat]-->nat
FUNCTION EXAMPLES:
0+0=0
s(0)+0=s(0)
0+s(0)=s(0)
0+s(s(0))=s(s(0))
s(0)+s(0)=s(s(0))
s(0)+s(s(0))=s(s(s(0)))
s(s(0))+s(0)=s(s(s(0)))
s(s(0))+0=s(s(0))
FUNCTION DEFINITIONS:
0+v17=v17
s(v18)+v19=f10(v19,v18+v19)
f10(0,v20)=s(v20)
f10(s(v21),s(v22))=s(s(v22))
?-

A.2

Size of a tree

?- SgI = [ size signature [tree] --> nat],
|
SD = [ tree sortdef nl ! nd(tree,nat,tree),
|
nat sortdef 0 ! s(nat)],
|
ExI = [ size(nl)

= 0,

15

|
size(nd(nl,va,nl))
= s(0),
|
size(nd(nd(nl,va,nl),vb,nl))
= s(s(0)),
|
size(nd(nl,va,nd(nl,vb,nl)))
= s(s(0)),
|
size(nd(nd(nl,va,nl),vb,nd(nl,vc,nl))) = s(s(s(0))),
|
size(nd(nl,va,nd(nd(nl,vb,nl),vc,nl))) = s(s(s(0))),
|
size(nd(nl,va,nd(nl,vb,nd(nl,vc,nl)))) = s(s(s(0))),
|
size(nd(nd(nl,va,nl),vb,nd(nd(nl,vc,nl),vd,nl)))
= s(s(s(s(0)))),
|
size(nd(nd(nd(nl,va,nl),vb,nl),vc,nd(nl,vd,nl)))
= s(s(s(s(0))))
|
],
|
run(size,SgI,SD,ExI).
+++++ Examples input check:
+++++ Example 1:
+++++ Example 2:
+++++ Example 3:
+++++ Example 4:
+++++ Example 5:
+++++ Example 6:
+++++ Example 7:
+++++ Example 8:
+++++ Example 9:
Variable sorts:
[vd:nat,vc:nat,vb:nat,va:nat]
+++++ Examples input check done
induce(size)
. trying argument position:
1
. inducePos(size,1,nl)
. . matching examples: [size(nl)=0]
. . anti-unifier:
size(nl) = 0
. inducePos(size,1,nl)
. inducePos(size,1,nd(tree,nat,tree))
. . matching examples: [size(nd(nl,va,nl))=s(0),size(nd(nd(nl,va,nl),vb,nl))=s(s(0)),size(nd(nl,va,nd(nl,vb,nl)))=s(s(0)),size(nd(nd(nl,va,nl),vb,n...
. . new recursion scheme:
size(nd(v10,v9,v11)) = f12(v9,size(v10),size(v11))
. . derive new equation:
s(0) = size(nd(nl,va,nl)) = f12(va,0,0)
. . derive new equation:
s(s(0)) = size(nd(nd(nl,va,nl),vb,nl)) = f12(vb,s(0),0)
. . derive new equation:
s(s(0)) = size(nd(nl,va,nd(nl,vb,nl))) = f12(va,0,s(0))
. . derive new equation:
s(s(s(0))) = size(nd(nd(nl,va,nl),vb,nd(nl,vc,nl))) = f12(vb,s(0),s(0))
. . derive new equation:
s(s(s(0))) = size(nd(nl,va,nd(nd(nl,vb,nl),vc,nl))) = f12(va,0,s(s(0)))
. . derive new equation:
s(s(s(0))) = size(nd(nl,va,nd(nl,vb,nd(nl,vc,nl)))) = f12(va,0,s(s(0)))
. . derive new equation:
s(s(s(s(0)))) = size(nd(nd(nl,va,nl),vb,nd(nd(nl,vc,nl),vd,nl))) = f12(vb,s(0),s(s(0)))
. . derive new equation:
s(s(s(s(0)))) = size(nd(nd(nd(nl,va,nl),vb,nl),vc,nd(nl,vd,nl))) = f12(vc,s(s(0)),s(0))
. . induce(f12)
. . . trying argument position: 1
. . . inducePos(f12,1,0)
. . . . matching examples:
[]
. . . . no examples
. . . inducePos(f12,1,0)
. . . inducePos(f12,1,s(nat))
. . . . matching examples:
[]
. . . . no examples
. . . inducePos(f12,1,s(nat))
. . . uncovered examples:
[f12(va,0,0)=s(0),f12(va,0,s(0))=s(s(0)),f12(va,0,s(s(0)))=s(s(s(0))),f12(vb,s(0),0)=s(s(0)),f12(vb,s(0),s(0))=s(s(s...
. . . trying argument position: 2
. . . inducePos(f12,2,0)
. . . . matching examples:
[f12(va,0,0)=s(0),f12(va,0,s(0))=s(s(0)),f12(va,0,s(s(0)))=s(s(s(0)))]
. . . . anti-unifier:
f12(va,0,v37) = s(v37)
. . . inducePos(f12,2,0)
. . . inducePos(f12,2,s(nat))
. . . . matching examples:
[f12(vb,s(0),0)=s(s(0)),f12(vb,s(0),s(0))=s(s(s(0))),f12(vb,s(0),s(s(0)))=s(s(s(s(0)))),f12(vc,s(s(0)),s(0))=s(s(s(s...
. . . . new recursion scheme:
f12(v43,s(v45),v44) = f46(v43,v44,f12(v43,v45,v44))
. . . . derive new equation:
s(s(0)) = f12(vb,s(0),0) = f46(vb,0,s(0))
. . . . derive new equation:
s(s(s(0))) = f12(vb,s(0),s(0)) = f46(vb,s(0),s(s(0)))
. . . . derive new equation:
s(s(s(s(0)))) = f12(vb,s(0),s(s(0))) = f46(vb,s(s(0)),s(s(s(0))))
. . . . derive new equation:
s(s(s(s(0)))) = f12(vc,s(s(0)),s(0)) = f46(vc,s(0),s(s(s(0))))
. . . . induce(f46)
. . . . . trying argument position:
1
. . . . . inducePos(f46,1,0)
. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f46,1,0)
. . . . . inducePos(f46,1,s(nat))
. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f46,1,s(nat))
. . . . . uncovered examples:
[f46(vb,0,s(0))=s(s(0)),f46(vb,s(0),s(s(0)))=s(s(s(0))),f46(vb,s(s(0)),s(s(s(0))))=s(s(s(s(0)))),f46(vc,s(0),s(s(s(0...
. . . . . trying argument position:
2
. . . . . inducePos(f46,2,0)
. . . . . . matching examples: [f46(vb,0,s(0))=s(s(0))]
. . . . . . anti-unifier:
f46(vb,0,s(0)) = s(s(0))
. . . . . inducePos(f46,2,0)
. . . . . inducePos(f46,2,s(nat))
. . . . . . matching examples: [f46(vb,s(0),s(s(0)))=s(s(s(0))),f46(vb,s(s(0)),s(s(s(0))))=s(s(s(s(0)))),f46(vc,s(0),s(s(s(0))))=s(s(s(s(0))))]
. . . . . . anti-unifier:
f46(v63,s(v64),s(s(v65))) = s(s(s(v65)))
. . . . . inducePos(f46,2,s(nat))
. . . . . all examples covered
. . . . induce(f46)
. . . inducePos(f12,2,s(nat))
. . . all examples covered
. . induce(f12)
. inducePos(size,1,nd(tree,nat,tree))
. all examples covered
induce(size)
+++++ Examples output check:
+++++ Examples output check done
FUNCTION SIGNATURES:
f46 signature [nat,nat,nat]-->nat
f12 signature [nat,nat,nat]-->nat
size signature [tree]-->nat
FUNCTION EXAMPLES:
size(nl)=0
size(nd(nl,va,nl))=s(0)

16

size(nd(nd(nl,va,nl),vb,nl))=s(s(0))
size(nd(nl,va,nd(nl,vb,nl)))=s(s(0))
size(nd(nd(nl,va,nl),vb,nd(nl,vc,nl)))=s(s(s(0)))
size(nd(nl,va,nd(nd(nl,vb,nl),vc,nl)))=s(s(s(0)))
size(nd(nl,va,nd(nl,vb,nd(nl,vc,nl))))=s(s(s(0)))
size(nd(nd(nl,va,nl),vb,nd(nd(nl,vc,nl),vd,nl)))=s(s(s(s(0))))
size(nd(nd(nd(nl,va,nl),vb,nl),vc,nd(nl,vd,nl)))=s(s(s(s(0))))
FUNCTION DEFINITIONS:
size(nl)=0
size(nd(v66,v67,v68))=f12(size(v66),size(v68))
f12(0,v69)=s(v69)
f12(s(v70),v71)=f46(v71,f12(v70,v71))
f46(0,s(0))=s(s(0))
f46(s(v72),s(s(v73)))=s(s(s(v73)))
?-

A.3

Reversing a list

?- SgI = [rev signature [list] --> list],
|
SD = [ list sortdef [] ! [nat|list],
|
nat sortdef 0 ! s(nat)],
|
ExI = [ rev([])
= [],
|
rev([va])
= [va],
|
rev([vb,va])
= [va,vb],
|
rev([vc,vb,va]) = [va,vb,vc]],
|
run(rev,SgI,SD,ExI).
+++++ Examples input check:
+++++ Example 1:
+++++ Example 2:
+++++ Example 3:
+++++ Example 4:
Variable sorts:
[vc:nat,vb:nat,va:nat]
+++++ Examples input check done
induce(rev)
. trying argument position:
1
. inducePos(rev,1,[])
. . matching examples: [rev([])=[]]
. . anti-unifier:
rev([]) = []
. inducePos(rev,1,[])
. inducePos(rev,1,[nat|list])
. . matching examples: [rev([va])=[va],rev([vb,va])=[va,vb],rev([vc,vb,va])=[va,vb,vc]]
. . new recursion scheme:
rev([v7|v8]) = f9(v7,rev(v8))
. . derive new equation:
[va] = rev([va]) = f9(va,[])
. . derive new equation:
[va,vb] = rev([vb,va]) = f9(vb,[va])
. . derive new equation:
[va,vb,vc] = rev([vc,vb,va]) = f9(vc,[va,vb])
. . induce(f9)
. . . trying argument position: 1
. . . inducePos(f9,1,0)
. . . . matching examples:
[]
. . . . no examples
. . . inducePos(f9,1,0)
. . . inducePos(f9,1,s(nat))
. . . . matching examples:
[]
. . . . no examples
. . . inducePos(f9,1,s(nat))
. . . uncovered examples:
[f9(va,[])=[va],f9(vb,[va])=[va,vb],f9(vc,[va,vb])=[va,vb,vc]]
. . . trying argument position: 2
. . . inducePos(f9,2,[])
. . . . matching examples:
[f9(va,[])=[va]]
. . . . anti-unifier:
f9(va,[]) = [va]
. . . inducePos(f9,2,[])
. . . inducePos(f9,2,[nat|list])
. . . . matching examples:
[f9(vb,[va])=[va,vb],f9(vc,[va,vb])=[va,vb,vc]]
. . . . new recursion scheme:
f9(v22,[v23|v24]) = f25(v22,v23,f9(v22,v24))
. . . . derive new equation:
[va,vb] = f9(vb,[va]) = f25(vb,va,[vb])
. . . . derive new equation:
[va,vb,vc] = f9(vc,[va,vb]) = f25(vc,va,[vb,vc])
. . . . induce(f25)
. . . . . trying argument position:
1
. . . . . inducePos(f25,1,0)
. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f25,1,0)
. . . . . inducePos(f25,1,s(nat))
. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f25,1,s(nat))
. . . . . uncovered examples:
[f25(vb,va,[vb])=[va,vb],f25(vc,va,[vb,vc])=[va,vb,vc]]
. . . . . trying argument position:
2
. . . . . inducePos(f25,2,0)
. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f25,2,0)
. . . . . inducePos(f25,2,s(nat))
. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f25,2,s(nat))
. . . . . uncovered examples:
[f25(vb,va,[vb])=[va,vb],f25(vc,va,[vb,vc])=[va,vb,vc]]
. . . . . trying argument position:
3
. . . . . inducePos(f25,3,[])

17

. . . . . . matching examples: []
. . . . . . no examples
. . . . . inducePos(f25,3,[])
. . . . . inducePos(f25,3,[nat|list])
. . . . . . matching examples: [f25(vb,va,[vb])=[va,vb],f25(vc,va,[vb,vc])=[va,vb,vc]]
. . . . . . anti-unifier:
f25(v37,va,[vb|v38]) = [va,vb|v38]
. . . . . inducePos(f25,3,[nat|list])
. . . . . all examples covered
. . . . induce(f25)
. . . inducePos(f9,2,[nat|list])
. . . all examples covered
. . induce(f9)
. inducePos(rev,1,[nat|list])
. all examples covered
induce(rev)
+++++ Examples output check:
+++++ Examples output check done
FUNCTION SIGNATURES:
f25 signature [nat,nat,list]-->list
f9 signature [nat,list]-->list
rev signature [list]-->list
FUNCTION EXAMPLES:
rev([])=[]
rev([va])=[va]
rev([vb,va])=[va,vb]
rev([vc,vb,va])=[va,vb,vc]
FUNCTION DEFINITIONS:
rev([])=[]
rev([v39|v40])=f9(v39,rev(v40))
f9(v41,[])=[v41]
f9(v42,[v43|v44])=f25(v43,f9(v42,v44))
f25(v41,[v45|v46])=[v41,v45|v46]
?-

18

References

[Bur05] Jochen Burghardt.
165(1):1–35, 2005.

E-generalization using grammars.

Artificial Intelligence Journal,

[Bur17] Jochen Burghardt. An improved algorithm for E-generalization. Technical report, Berlin,
Sep 2017.
[Com86] Hubert Comon. Sufficient completeness, term rewriting systems and “anti-unification”. In
Proc. 8th International Conference on Automated Deduction, volume 230 of LNCS, pages
128–140. Springer, 1986.
[DJ90]

N. Dershowitz and J.-P. Jouannaud. Rewrite Systems, volume B of Handbook of Theoretical
Computer Science, pages 243–320. Elsevier, 1990.

[Gut77] John V. Guttag.
Abstract data types and the development of data structures.
Communications of the ACM, 20(6):396–404, Jun 1977.
[Hei94a] Birgit Heinz. Anti-unification and its application to lemma discovery, 1994. Workshop Talk
given in CADE-12.
[Hei94b] Birgit Heinz. Lemma discovery by anti-unification of regular sorts. Technical Report 94–21,
TU Berlin, 1994.
[Hei95] Birgit Heinz.
Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur
Lemmagenerierung. PhD thesis, TU Berlin, Dec 1995.
[Kit10] Emanuel Kitzelmann. A Combined Analytical and Search-Based Approach to the Inductive
Synthesis of Functional Programs. PhD thesis, Univ. Bamberg, May 2010.
[LV08]

Ming Li and Paul Vitányi. An Introduction to Kolmogorov Complexity and Its Applications.
texts in computer science. Springer, New York, 3rd edition, 2008.

[Plo70] Gordon D. Plotkin. A note on inductive generalization. Machine Intelligence, 5:153–163,
1970.
[Plo71] Gordon D. Plotkin. A further note on inductive generalization. Machine Intelligence, 6:101–
124, 1971.
[Rey70] John C. Reynolds. Transformational systems and the algebraic structure of atomic formulas.
Machine Intelligence, 5:135–151, 1970.

19

