From checking to inference via driving and dag grammars.
Abramov and Glck have recently introduced a technique called URA for inverting first order functional programs. Given some desired output value, URA computes a potentially infinite sequence of substitutions/restrictions corresponding to the relevant input values. In some cases this process does not terminate.In the present paper, we propose a new program analysis for inverting programs. The technique works by computing a finite grammar describing the set of all input that relate to a given output. During the production of the grammar, the original program is implicitly transformed using so-called driving steps. Whereas URA is sound and complete, but sometimes fails to terminate, our technique always terminates and is complete, but not sound. As an example, we demonstrate how to derive type inference from type checking.The idea of approximating functional programs by grammars is not new. For instance, the second author has developed a technique using tree grammars to approximate termination behaviour of deforestation. However, for the present purposes it has been necessary to invent a new type of grammar that extends tree grammars by permitting a notion of sharing in the productions. These dag grammars seem to be of independent interest.
INTRODUCTION
The program-transformation techniques collectively called
supercompilation have been shown to eectively handle problems
that partial evaluation and deforestation cannot han-
dle. The apparent strength of supercompilation stems from
driving the object programs, that is, speculatively unfolding
expressions containing variables, based on the possible executions
described by the program. As an example of driving,
consider the Haskell-like program
where, by convention, the main denition serves as the interface
to the program. It is not possible to execute this
program because of the variables v and vs in main v vs, but
we can drive the program, resulting in a process tree describing
all possible computations of the program. For the
above program, one possible process tree is
- append (Cons v vs) Nil
Cons v (append vs Nil)
- append vs Nil
let u=
- append Nil Nil
vs=Nil
append (Cons x xs) Nil -
vs=Cons x xs
Cons v u -
in
(1)
In general, the process tree is constructed as follows. The
root of the process tree is labelled with right-hand side of the
main denition. New leaves are added to the tree repeatedly
by inspecting the label of some leaf, and either
1. Unfolding an outermost call (-).
2. Instantiating a variable that hinders unfolding (-).
3. Generalising by creating two disjoint labels (-).
Whenever the label of a leaf is identical to the label of an
ancestor (up to renaming of variables), that leaf is not unfolded
further (-9 9 K-).
A new (slightly more e-cient) program can easily be extracted
from a process tree, namely
Our main interest in this paper is to transform a checker
into a description of the input that will satisfy the checker.
That is, given a program that answers true or false, we will
transform the program into a description of the input for
which the checker answers true.
The above activity is generally known as program inversion
when the description of the satisfying input is yet another
program. It is, however, a non-trivial task to perform program
inversion, as the following example shows.
Example 1. Consider a program that checks whether two
lists are identical.
The auxiliary functions isnil and iscons are needed because
we only allow pattern matching on one argument at a time.
The reason for having this restriction is that it associates
every pattern match with a particular function denition.
The result of inverting the above program w.r.t. true should
be another program that produces all pairs of identical lists.
However, it is unreasonable to assume that we can produce
such a program: Even though it is easy to imagine a program
that produces an innite stream of pairs of lists with identical
spines, where should the elements come from? Based on
their type, these elements could be enumerated, but such an
enumeration clearly leads to non-termination in the general
case. What is worse still, the imagined program will not
per se give us a good description of the input set; we can
merely get an indication of the input set by running it and
observing its ever-increasing output.
Instead of inverting a program, one might perform its computation
backwards. A general method to perform inverse
computation has been proposed by Abramov & Gluck [1],
namely the Universal Resolving Algorithm (URA). The URA
constructs a process tree for the object program, and produces
from the process tree a potentially innite set of constraints
on the uninstantiated input (variables xs and ys in
the above example). Each constraint describes a set of input
values by means of a substitution/restriction pair. The
produced constraints are pairwise disjoint, in the sense that
the sets they describe are pairwise disjoint. Variables can
appear several times in each constraint, indicating identical
values. For the above example, the URA would produce
something like
([xs 7! Nil; ys 7! Nil]; [])
([xs 7! Cons x1 Nil; ys 7! Cons x1 Nil]; [])
([xs 7! Cons x1 (Cons x2 Nil);
ys 7! Cons x1 (Cons x2 Nil)]; [])
(2)
Here the URA would never terminate. The merit of the
URA is that it is sound and complete, so if it terminates,
the result precisely captures the input set.
In this paper we will sacrice soundness to develop an approach
that always produces a nite description of the satisfying
input.
1.2

Overview

In Section 2, we present a formalisation of a certain kind of
context-free grammars, namely dag grammars. For instance,
the above checker can be described by the grammar> > <
Nil Nil
Cons
x
Cons
The grammar consists of two productions, each formed as
an acyclic directed graph (also known as a dag). The rst
says that an S can be rewritten into a dag consisting of two
single nodes labelled Nil. The second says that an S can
be rewritten into a more complex dag with two roots. The
two productions can be viewed as a nite representation of
(2). Such dag grammars can precisely express the data and
control
ow of a program, something which is not possible
with standard tree grammars.
In Section 4, we present an automatic method to extract a
dag grammar from a program. Conceptually, the extraction
works in two steps: First we drive the object program to
produce a process tree, second we extract a grammar from
this process tree. A precursor for driving the program is
a precise formulation of the semantics of our programming
language, which we present in Section 3. The extracted dag
grammars are approximations of the input set, and in Section
6, we consider various ways to improve the precision of
our method.
As an application, we will in Section 5 show that, given a
type checker and a -term, it is possible to derive a type
scheme for the -term.
2. DAG GRAMMARS
We denote by fs0 the set containing s0
we
g. For a binary relation *  S  T ,
we denote by D* the domain S of *. The set of deterministic
binary relations (i.e., partial functions) from S to
T is denoted by S - T , and such partial functions can be
g. By S $ T we denote the
set of bijections between S and T .
Denition 1. Given a set S, a graph G over S consists
of a label function lab 2 N - S and a connected-by relation
means that node i's
kth successor is node j and j's 'th predecessor is i. The
relation should satisfy the properties that there is a label
to each node, and that the successors and predecessors are
numbered consecutively from 0. Formally,
When the order of successors and predecessors is immaterial,
we simply use - as a binary relation and write i - j
whenever 9k ' 2 N [i k ' - j].
In the following, we will use subscripts like lab G or -
G
when it is otherwise not obvious which graph we refer to.
By - we denote the transitive closure of - . In general,
we will superscript any binary relation with + to denote its
transitive closure, and we will superscript with  to denote
its re
exive closure.
Denition 2. A graph G is a dag when it contains no
cycles (i.e., @i 2 N [i i]). For dags, it is natural to talk
of roots and leaves:
roots G
G i]
leaves G
G j]

Two dags D and E are equivalent, denoted D  E, when D
and E can be transformed into one another by renumbering
the nodes, that is,
The set of dags over S is denoted DS .
Example 2. Each of the two structures (3) depicts an equivalence
class of dags over fS Nil Cons xg | in the sense that
the structure describes a family of equivalent dags | because
the node set ( N) is left unspecied; the order of
successors and predecessors, however, is specied by adopting
the convention that heads and tails of arcs are ordered
from left to right. A concretisation of the right dag is, for
example,
and we have that leaves = f3 4g and roots = f0g.
Denition 3. Given a set , a dag grammar over  is
a set of nite dags over . The set of dag grammars over
is denoted G.
Example 3. The two dags (3) comprise a dag grammar
over fS x Nil Consg.
A dag grammar describes a dag language, in which every dag
has been generated by a number of rewrites on an initial
dag. Before we give the formal denition of rewrites and
languages, an example is in order.
Example 4. The dag
can be rewritten by the dag
grammar (3) as
Nil Nil
Cons
x
Cons
Cons
x Nil
Cons
Cons
x Cons
x
Cons
Cons
The symbol  is here used to maintain an order between an
otherwise unordered set of roots.
Below you will nd the formal denition of graph grammar
rewrites. The example above hopefully illustrates how such
rewrites work. Informally, a dag can be rewritten if it has a
leaf node i that matches a root node j in a dag in the graph
grammar. By matches, we mean that i and j have the same
label, and that the number of predecessors of i matches the
number of successors of j. The result of the rewrite is that
the leaf i and root j dissolve, as it were, and the predecessors
of i become the predecessors of the successors of j, in the
right order, as illustrated below.6 6k1    kn
6 6 6k1    kn
denitions generalise the above notion of rewriting
to several leaves We will
need this generality in Section 4.
Denition 4. We denote by S P the set of all nite sequences
over set S. Both sequences and tuples are denoted
by angles h   i.
Denition 5. Given dags D and E, we dene
match
ng
(lab
and
maxmatch
Denition 6. Given sets S and T , if S and T are disjoint,
we write S  T , and in that case the disjoint union S ]
T is dened (and undened, otherwise). Given a relation
*  S  T and a set S 0 , we dene the removal of S 0 from
* as * nS 0
. The disjoint
union of two binary relations is dened if their domains are
disjoint.
In the following, we carefully pay attention to the exact set
of nodes ( N) that each particular dag comprises. To avoid
node clashes when we rewrite graphs, we use the fact that,
given a nite dag G 0 , there are innitely many equivalent
dags G.
Denition 7. Given a dag grammar 2 G , the one-
step-rewrite relation !  D  D is dened by
9 hI Ji 2 maxmatch D G6 6 6
I
Denition 8. Given a dag grammar and an initial dag
I, the dag language LI is the set of normal forms: LI
We now have a grammar framework that can readily express
sets of input. The next step is to show how a dag grammar
can be extracted from a program. We start by dening
the semantics of the object language, and, on top of the
semantics, we then build the machinery that calculates the
desired grammars.
3. OBJECT LANGUAGE
Our object language is a rst-order functional language with
pattern matching and operators for term equality and boolean
and.
Denition 9. Given a set of variables X, function names
F , pattern-function names G, and constructors C (including
the constants true and false), we dene
d
G. As
usual, we require that no variable occurs more than once in
the left-hand side of a function denition (left-linear), and
that all variables in the right-hand side of a function definition
is a subset of those in the left-hand side (closed).
Finally we require that the patterns dened for each g-function
are pairwise distinct modulo variable names (non-
overlapping); in particular, a g-function can have at most
one \catch-all" pattern.
In concrete programs we use a Haskell-like syntax, including
data-type denitions. The above syntax can be viewed
as the intermediate language obtained after type checking,
which rules out terms like Nil & Nil and Nil  true.
Denition 10. Given a term t, we denote by V t
the variables of t, collected from left to right. Term t is
Example 5.
(Triple x y
Denition 11. A function  2 X - T can be regarded
as a substitution T - T in the usual way, and, for t 2
T , we will write t for the result of such a substitution.
Given program p, writing, say, g (c
means that in p there is a function denition identical to
t, up to variable naming.
We will now give the normal-order semantics of the object
language by dening a small-step relation that takes redexes
into their contracta. We can separate redexes from their
contexts by the following syntactic classes.
if
if
true

Figure

1: Normal-order semantics
Denition 12.
e
O 3
By d([t]) we denote the result of replacing ([ ]) in d with term
t.
Any ground term t is either a value or can be uniquely decomposed
into a context and a redex (i.e.,
decomposition property allows us to dene the semantics as
below. The semantics imposes left-to-right evaluation, except
for the equality operator, which evaluates both its arguments
until two outermost constructors can be compared.
Denition 13. Given a program p, the small-step semantics
of p is dened by the smallest relation !  RT
on closed terms as dened by Fig. 1. In the following we will
use subscripts like ! p when it is otherwise not obvious which
program we refer to.
To get the full semantics of the language, we simply need
to close the !-relation under all contexts. The semantics is
deterministic:
Lemma 1.
Proof sketch. By induction and case analysis of the
syntactic structure of terms: Each term either cannot be
decomposed into a context and a redex, or it can be uniquely
decomposed, in which case the redex has at most one small-step
derivation.
4. EXPLICITATION
The previous section aloows us to deal with execution of
ground terms. To be able to drive a program, however, we
need to handle terms containing variables. We use the following
syntactic class, in combination with the previously
dened ones, to describe all terms that cannot be decomposed
into contexts and redexes.
Denition 14.
As for the variables of a let-term, V (let
The use of let-terms will be described below. As in the previous
section, we obtain a unique-decomposition property:
Any term t is either a value, can be uniquely decomposed
into a context and a redex, or can be uniquely decomposed
into a context and a speculative (i.e., d([s])). The extra
syntactic class s enables us to identify terms that need to
be driven (i.e., instantiated).
In supercompilation, driving is used to obtain a process tree
from the object program. The process tree serves two orthogonal
purposes: It keeps track of data and control
ow
(essentially variable instantiations and recursive calls), and
it provides a convenient way to monitor the driving process
and perform the generalisations needed to ensure a -
nite process tree. When a generalisation is needed for a
t, t is replaced by a term \let " such that
. The point of making such a generalisation
is to be able to treat t1 and t2 independently. For an exam-
ple, you might want to revisit (1) in the introduction. For a
thorough introduction to these techniques, see Srensen &
Gluck [13].
In our approach to program inversion, called explicitation,
we will assume that the generalisations necessary to ensure
termination have been computed in advance by an o-line
generalisation analysis. To be more specic, we assume that
some terms have been replaced by terms of the form let
t1 in t2 in the program of interest. With respect to the data
and control
ow of the program, the
ow can be expressed
by dag grammars, which we will elaborate on later in this
section.
Since we have thus eliminated the need for a process tree, we
will, to keep things simple, drive the object program without
constructing the actual process tree. The construction of
a process tree, although important in practice, is not the
essence in our approach.
Remark 1. We should note here that the existence of an
o-line generalisation analysis is not essential: The explicitation
process described in the following could incorporate
well-known non-termination detection and perform the necessary
generalisations. 1 But because such an incorporation
would induce unnecessary clutter in our presentation, we
will concentrate on the description of how to extract a dag-
grammar by driving.
From a bird's-eye view, the explicitation process of a single
branch of speculative execution works as follows. Starting
with the main term of the object program, a dag grammar
is gradually built up by driving the term: each time a
speculative (cf. Def. 14) hinders normal reduction, we perform
an instantiation to both the term and the dag gram-
mar, such that reduction of the term can proceed and the
re
ects the structure of the input variables. In
fact, each driving step of a term results in a new production
in the grammar, such that every term we meet while driving
the program has its own production. When we meet a
term which we have seen before, a loop is introduced into
the grammar, and driving of the term stops. A term t that
cannot be driven any further is compared to the output we
desired, namely non-false output: If t is false, then the result
is an empty grammar; otherwise it is the accumulated
grammar . In general, we parameterise the explicitation
process over a discrimination function h. For our purpose,
In the above fashion, we can produce a grammar for every
speculative execution of the program: Each possible instantiation
of a term gives rise to a slightly dierent term and
grammar. The nal grammar is then the union of the grammars
produced for all executions.
As an example of an instantiation on a dag grammar, consider
the dags
same xs ys
6 6 6xs ys
Cons
iscons ys x xs7 7
same xs ys
Cons
iscons ys x xs7
D represents a call to same where the arguments are un-
known. E represents the body of same: a pattern match on
the variable xs and a call to iscons with three arguments (cf.
Example 1). The order of the arrows is important, since it
have presented a method for preventing
non-termination and performing generalisations of dangerous
terms, as it were, based on certain quasi-orders. With
a few extensions, this method can be applied to our lan-
guage. We can prove that such an extended method will indeed
guarantee termination of the explicitation, if we apply
the general framework for proving termination of program
transformers presented by the second author [14].
denes the data
ow. If we view fEg as a dag grammar, D
can be rewritten into D 0 by means of fEg, as shown above.
Formally,
Denition 15. Given dags D and E, the dag substitution
fEgD is dened as (cf. Def. 5)
D; otherwise.
Substitutions are extended to grammars in the obvious way:
To construct dags from terms, we use the following shorthands

Denition 16. Given a term t,
and ? t
The full explicitation process will be explained in detail be-
low. Formally, it is summed up in the following denition.
Denition 17. Given a program p and a function h 2
the explicitation of p is a
dag grammar Eh [[p]], as described in Fig. 2.
The following explanation of the explicitation process carries
a number of references that hopefully will guide the
understanding of Fig. 2.
Explicitation starts with the main term t of the program,
an empty dag grammar , and an empty set of previously
seen
terms
In each step, we inspect the structure of the
current term t, and either stop, or add a production for t to
and make a new step with t added to the seen-before set.
If t has been seen before, a production for t is already
present in the grammar , so we return the accumulated
unchanged. - If a renaming of t has been seen before
(captured by a bijection ), we introduce recursion in the
grammar by adding a production that connects t to the (pre-
viously seen) t, respecting the number of variables.
- If a redex can be unfolded using the standard semantics
(cf. Defs. 12 & 13), a production linking t to its unfolding is
added to , and the process continues with the unfolding.
- If a generalised term hinders unfolding, that is
t1 in t2 ]), d([t 2 ]) and t1 are processed independently. There-
fore, a production is added to the grammar such that t is
linked to both d([t 2 ]) and t1 . This production will have some
dangling roots 2 (namely x and V t1 \ V t2 ) which re
ect that
the data
ow is approximated. Because the traces of t1 will
tell us nothing about the output of t, the function h (cf. (4))
Unmatched roots are allowed in dag rewrites, cf. Def. 7.
Eh
let
[ ftg in
- if tthen
then [<

@> <
c
AC
A
@> <
r
x y
AC
A
and t
and
x
c
and t

x
true
#)
and t

x
false
#)

Figure

2: Explicitation by driving
that is supposed to discriminate between various output is
replaced by the function xy:y which does not discriminate:
It always returns the accumulated grammar.
- For a pattern matching function, the process is continued
for all dened patterns. For each pattern q, we substitute the
arguments into the matching body, and put it back into the
context, which in turn receives the instantiation fx 7! qg,
and we add to the grammar a production re
ecting this
instantiation.
For comparisons, there are three cases. - The rst simply
makes sure that variables are on the left side of the com-
parison. That settled, - if the right-hand side is another
variable, two possibilities are explored: Either the comparison
will fail, and hence we replace the speculative with false;
or the comparison will succeed, and we replace the speculative
with true and update the grammar and the context to
re
ect that both sides must be identical. In the grammar,
the equal variables are coalesced by means of a special symbol
r, which is needed to maintain the invariant that the
in/out degree of terms correspond to the number of distinct
variables. - If the right-hand side is an n-ary constructor,
either the comparison will fail (as above), or it will succeed,
in which case we will propagate that the variable must have a
particular outermost constructor, of which the children must
be tested for equality with the children of the constructor.
- If a boolean expression depends on a variable, then the
variable will evaluate to either true or false, and this information
is propagated to each branch.
- Terms that cannot be driven any further (i.e., t 2 V ) are
fed to the function h, which in turn decides what to do with
the accumulated grammar.
Example 6. Let p be the program from Example 1 and h
dened as (4). The explicitation Eh is depicted in Fig. 3.
The grammar produced is fA B D F I Jg.
The derived grammars are sub-optimal: Most of the productions
are intermediate, in the sense that they can be directly
unfolded, or in-lined as it were. We say that a grammar is
normalised if it contains no intermediate productions, and
we can easily normalise a grammar.
Denition 18. A dag grammar can be normalised, denoted
b , as follows.
roots G  leaves G
Example 7. If we normalise the grammar from Example 6,
we almost get the grammar we promised in the introduction:4
same xs ys
same xs ys
Cons Cons
r same xs ys
In this particular grammar, the bookkeeping symbol r can
be eliminated by yet another normalisation process, if so
desired.
Given that the object program contains the necessary gen-
eralisations, the lemma below is not surprising. However,
if we incorporated a standard on-line termination strategy
into the explication process, as explained in Remark 1, the
following lemma would still hold.
Lemma 2. Any explicitation produces a nite grammar.
Proof. The process tree of the program is nite (since
the program contains the necessary generalisations), and
thus a nite number of dags will be produced, assuming
the h function is to be total and computable.
More interestingly, the explicitation returns a dag grammar
that contains all solutions. To express such a completeness
theorem, we need a precise formulation of the set of
terms generated by a dag grammar, as given below. Infor-
mally, a term is extracted from a dag simply by following
the edges from left to right, collecting the labels | except
when the label is a variable or the bookkeeping symbol r:
Every variable is given a distinct name, and r is treated as
an indirection and left out in the term.
Denition 19. Given a dag grammar , a label S with
arity n, and a set of variables g, the term
language T n
S is the set of tuples of terms that can be
extracted from the underlying dag language:
I =4
0:
S5
=> <
and fhi 0 '0
We can now relate all possible executions of the program to
the set of terms generated by its explicitation.
Eh [[same xs ys
fsame xs ysg
Eh
f(same xs ys) (isnil ys)g
Eh
f(same xs ys) (isnil ys)g
Eh [[iscons ys x xs
fsame xs ysg
Eh
f(same xs ys) (iscons ys x xs)g
f(same xs ys) (iscons ys x xs)g
f:::(if (xy) (same xs ys) false)g
f:::(if (xy) (same xs ys) false) (if false (same xs ys)
f:::(if (xy) (same xs ys) false)g
f(same xs ys):::
6 6same xs ys
Nil
6 6isnil ys
Cons
iscons ys x xs
Nil x xs7G 2
(same xs ys)(false)
x y if false
(same xs ys)(false)7 7
if
(same xs ys)(false)
r
x
if true
(same xs ys)
isnil ys
same xs ys
Cons
iscons ys x xs7 7 75
26 6 6
6 6iscons ys x xs
Cons
if
6 6if false
(same xs ys)
xs ys7
6 6if true
(same xs ys)
same xs ys7
Figure

3: Explicitation of the same-program
Theorem 1. Given a program p where main
holds that
5. APPLICATION: TYPE INFERENCE
We now show that a type checking algorithm can be transformed
into a type inference algorithm by explicitation. Specif-
ically, we check that a -calculus expression has a given type
in a given environment, using the standard relation
As an example, consider the expression
meaning \what is the type of x:y:z:(xz)(yz) in the empty
environment?". We would expect the answer to be something
like
We will now perform explicitation of the above expression.
The type checker below takes an encoding of a proof tree P ,
an expression M , and an environment , and returns true
if P is indeed a valid proof of the type of M in . In this
encoding, 3 x:y:z:(xz)(yz) becomes
and ? becomes Empty. If we want to explicitate the above
expression, we can add the denition
main
to the implementation of the type checker (which we then
refer to as the specialised typechecker):
data
3 | Abs Int Term
4 data
5 data Proof = Infer Premise Type
6 data
7 | Intro Proof
9 expchk (Var x) y z
match z x y
14 elimchk (Elim x y) z v w
3 The implementation assumes a primitive integer type Int.
19 arrowcheck v x y z w
match (Bind x y z) v
22 if (v == x) (w == y) (match z v w)
match x y
arrowcheck (Ar x y) z v w
26 y == conclusion z
28 conclusion (Infer x
29 if false x
Explicitation of the specialised typechecker gives a term language
that consists of a single pair
<(Ar (Ar x (Ar y z)) (Ar (Ar x y) (Ar x z)))
(.)>
The rst element is indeed the encoding of type (5), and the
second is the proof tree, which we have left out.
6. IMPROVING SOUNDNESS
Any automatic method for inversion of Turing-complete programs
will have to make a compromise with respect to com-
pleteness, soundness and termination. We have made a compromise
that will result in possibly unsound results: The explicitation
of a program can produce a grammar that generates
too many terms. From a practical point of view,
we feel that this is the right compromise: It is better to
obtain an approximation than not obtaining an answer at
all. Moreover, explicitation can produce grammars that precisely
identies the input set, as seen from the two examples
is previous sections, which indicates that explicitation
is tight enough for at least some practical problems.
However, it still remains to identify exactly what causes loss
of soundness in the general case. Our method is inherently
imprecise for three reasons.
Generalisations cause terms to be split up in separate
parts (by means of let-terms). This prevents instantiations
in the left branch of the process tree to aect
the right branch, and vice versa.
Negative information is not taken in to account while
driving. For example, driving the speculative term
x  y will not propagate the fact that x 6= y to the
right branch of the process tree (although the fact that
propagated to the left branch, by means of
a substitution). Moreover, the dag grammars cannot
represent negative information.
Occur check is not performed on speculative terms like
that is, a situations where
for some i  n is not discovered. Obviously, such
an equality would never imply that
Similarly, the symmetric property that x  x never
implies x 6= x is not used either.
The occur check and its counterpart can easily be incorporated
into rules - and -, respectively, in Fig. 2. Interest-
ingly, explicitation of the type checker (specialised to a -
would be sound, had these checks been incorporated.
As for negative information, we have described how to handle
and propagate such information in another paper [11].
Incorporating negative information as proposed in that paper
would be a simple task. Incorporating negative information
into the dag grammars, however, would destroy their
simplicity and thus severely cripple their usability.
Hence, generalisation and the inability of dag grammars to
represent negative information are the true culprits. One
could therefore imagine a variant of the explicitation algorithm
| lets call it EXP | where one has incorporated
the extensions we have suggested above. To improve soundness
of EXP, one should target the way generalisations are
carried out.
We are now in a position to conjecture the following roundabout
relationship between EXP and the URA [1] described
in the introduction: Given a program p without generalisa-
tions, EXP terminates on p whenever URA terminates on p.
Moreover, if the result of URA contains no restrictions (neg-
ative information), the resulting grammar of EXP is sound.
7. RELATED WORK
Program inversion
In the literature, most program inversion is carried out by
hand. One exception is Romanenko [9], who describes a
pseudo algorithm for inverting a small class of programs
written in Refal. In a later paper, Romanenko [10] extends
the Refal language with non-deterministic construct, akin
to those seen in logic programming, to facilitate exhaustive
search. He also considers inverting a program with respect
to a subset of its parameters, so-called partial inversion. We
would like to extend our method to handle partial inversion,
but as of this writing it is unclear how this should be done.
The only fully automated program inversion method we
know of, is the one presented by Abramov & Gluck [1].
Their method constructs a process tree from the object pro-
gram, and solutions are extracted from the leaves of the
tree in form of substitution/restriction pairs. The process
trees are perfect (Gluck & Klimov [3]) in the sense that no
information is lost in any branch (completeness), and every
branching node divides the information in disjoint sets
(soundness). Unfortunately, soundness together with completeness
implies non-termination for all but a small class
of programs. The method we have presented here sacrices
soundness for termination.
What is common to both ours and the above methods is that
they all build upon the ground breaking work of Turchin and
co-workers. The rst English paper that contains examples
of program inversion by driving seems to be [15]. For more
references, see Srensen & Gluck [4].
Grammars
The idea of approximating functional programs by grammars
is not new. For instance, Jones [5] presents a
ow
analysis for non-strict languages by means of tree gram-
mars. Based on this work, the second author has developed
a technique using tree grammars to approximate termination
behaviour of deforestation [12]. Tree grammars, how-
ever, cannot capture the precise data and control
ow: By
denition, branches in a tree grammar are developed inde-
pendent, which renders impossible the kind of synchronisation
we need between variable and function calls. The dag
grammars we have presented, precisely capture the data and
control
ow for any single speculative computation trace;
synchronisation can only be lost when several alternative
recursive productions exist in the grammar.
It seems possible to devise a more precise
ow analysis based
on dag grammars, which could be used along the lines of [12].
Indeed, the way we use dag grammars to trace data and
control
ow, turns out to have striking similarities with the
use of size-change graphs, presented by Lee, Jones & Ben-
Amram [7]. Size-change graphs approximate the data
ow
from one function to another, by capturing size-changes of
parameters.
The dag-rewrite mechanism we have presented turns out to
have a lot in common with the fan-in/fan-out rewrites presented
by Lamping [6], in the quest for optimal reduction
in the -calculus. The fan-in/fan-outs represent a complex
way of synchronising dierent parts of a -graph, whereas
our dag rewrites only perform a simple use-once synchroni-
sation. The rewriting mechanism is also akin to graph substitution
in hyper-graph grammars (see Bauderon & Courcelle
[2] for a non-category-theory formulation), except that we
allow any number of leaves to be rewritten and do not allow
inner nodes to be rewritten. Strength-wise, hyper-graph
grammars are apparently equivalent to attribute grammars.
At present, we are not sure of the generative power of dag
grammars.
8. CONCLUSION AND FUTURE WORK
We have developed a method for inverting a given program
with respect to a given output. The result of the inversion
is a nite dag grammar that gives a complete description of
the input: \Running" the dag grammar produces a (possibly
innite) set of terms that will contain all tuples of terms that
result in the given output.
The method seems to be particularly useful when the object
program is a checker, that is, one that returns either true or
false. We have exemplied this by deriving a type scheme
from a type checker and a given -term, thus eectively
synthesising a type inference algorithm. Following this line,
one could imagine a program that checks whether a document
is valid XML. Inverting this program would result in
a dag grammar, which could then be compared to a speci-
cation for valid XML, as a means of verifying the program.
Inverting the program when specialised to a particular doc-
ument, would result in a Document Type Denition. One
could even imagine inverting a proof-carrying-code verier
[8] with respect to a particular program, thus obtaining a
proof skeleton for the correctness of the code.
Further experiments with the above kinds of applications
should be carried out to establish the strength and usability
of our method.
9.



--R


Graph expressions and graph rewritings.


Flow analysis of lazy higher-order functional programs
An algorithm for optimal lambda calculus reduction.
The size-change principle for program termination
Compiling with Proofs.
The generation of inverse functions in Refal.
Inversion and metacomputation.




de
--TR
An algorithm for optimal lambda calculus reduction
Inversion and metacomputation
Convergence of program transformers in the metric space of trees
The size-change principle for program termination
Introduction to Supercompilation
On Perfect Supercompilation
Occam''s Razor in Metacompuation
A Roadmap to Metacomputation by Supercompilation
Semantic definitions in REFAL and the automatic production of compilers
The Universal Resolving Algorithm
Grammar-Based Data-Flow Analysis to Stop Deforestation
Compiling with proofs

--CTR
Siau-Cheng Khoo , Kun Shi, Output-constraint specialization, Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation, p.106-116, September 12-14, 2002, Aizu, Japan
Aaron Tomb , Cormac Flanagan, Automatic type inference via partial evaluation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.106-116, July 11-13, 2005, Lisbon, Portugal
Siau-Cheng Khoo , Kun Shi, Program Adaptation via Output-Constraint Specialization, Higher-Order and Symbolic Computation, v.17 n.1-2, p.93-128, March-June 2004
Morten Heine Srensen , Jens Peter Secher, From type inference to configuration, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
Principles of inverse computation and the Universal resolving algorithm, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
supercompilation;program inversion;inference