Logic languages based on the theory of rational, possibly infinite,
trees have much appeal in that rational trees allow for faster
unification (due to the omission of the occurs-check) and increased
expressivity. Note that cyclic terms can provide a very efficient
representation of grammars and other useful objects. Unfortunately,
the use of infinite rational trees has problems. For instance, many
of the built-in and library predicates are ill-defined for such trees
and need to be supplemented by run-time checks whose cost may be
significant. Moreover, some widely-used program analysis and
manipulation techniques are only correct for those parts of programs
working over finite trees. It is thus important to obtain,
automatically, a knowledge of those program variables (the finite
variables) that, at the program points of interest, will always be
bound to finite terms. For these reasons, we propose here a new
data-flow analysis that captures such information. We present a
parametric domain where a simple component for recording finite
variables is coupled with a generic domain (the parameter of the
construction) providing sharing information. The sharing domain is
abstractly specified so as to guarantee the correctness of the
combined domain and the generality of the approach.
