Publikation
Induction on Non-Freely Generated Data Types
Claus Sengler
DFKI, DFKI Research Reports (RR), Vol. 96-01, 1996.
Zusammenfassung
The induction principle is based on well-founded orderings, i.e., orderings without infinite descending chains. Therefore, in order to automate inductive proofs, it is essential to automate the proofs for an ordering to be well-founded, which is closely related to a termination proof.
The general idea to achieve these proofs is to use the < N-relation on natural numbers and to map each data type object into a natural number by use of a measure function. For an automation typically a single measure function is used, for instance, the size of an object. In case of freely generated data types, that is for data types whose objects possess a unique syntactic structure, like, for instance, natural numbers, finite lists, and finite trees, the size of an object corresponds to the number of reflexive constructor functions that are necessary to represent the object. Here, the axiomatization of a function to compute the size of an object can be easily encoded in a first-order logic. Thus, together with an axiomatization of the natural numbers the occurring proof obligations can be proved quite easily.
Besides freely generated data types there are non-freely generated data types which frequently occur in practical applications. These data types include, for example, finite sets and arrays. They are characterized by having objects with different syntactic representations. The size of such an object corresponds to the minimal number of reflexive constructor functions that are necessary to represent the object. Compared to freely generated data types, the size of a non-freely generated data type object can only be axiomatized within a first-order logic in a complicated and inconstructive way, which leads to substantially more difficult proofs.
Yet, for the proof obligations that occur during the proofs of an ordering to be well-founded it is not necessary to compute the size of an object explicitly. Instead it is sufficient to estimate how two objects relate to each other with respect to their size. This idea is incorporated into a specific calculus, the Estimation Calculus, which was originally designed by Walther for termination proofs over freely generated data types.
In this report we present a generalization of this calculus that allows to efficiently derive estimations for non-freely generated data type objects with respect to their size, too.
For the resulting proof obligations when proving an ordering to be well-founded, the Estimation Calculus decides whether under a condition φ the sizes of two objects, which are denoted by terms, are within the < N-relation. Moreover, usually both terms possess a common subterm. Hence, the proof obligations are of the form:
φ → |f(t)| < N |g(t)|.
In order to prove this obligation, it is split by the Estimation Calculus into a chain of estimations with respect to the ≤ N-relation. Furthermore, each single estimation is based on certain properties of the underlying formal specification:
φ → |f(t)| ≤ N |t| and
φ → |t| ≤ N |g(t)|.
These single estimations together with the transitivity of the ≤ N-relation-Relation guarantee
φ → |f(t)| ≤ N |g(t)|.
To show that the objects which are denoted by the two terms are within the strict < N-relation, for each single estimation a formula is synthesized which is sufficient for the < N-relation. Then, an additional proof that the disjunction of these formulas follows from the condition φ guarantees the original proof obligation.
For the single estimations within the Estimation Calculus certain properties of the involved functions are used. Defined functions are analyzed whether they are argument-bounded, i.e., whether the size of one of their arguments denotes an upper bound for the size of an application of the function. And for constructor functions it is determined, whether the size of each argument is a lower bound for the size of an application of the function.
Whereas the first property can be proved within the Estimation Calculus itself, the second property is more difficult to show. To do that an implementation of the non-freely generated data type as a freely generated data type has to be used. This allows one to axiomatize a function that computes the size of an object explicitly, however, in general, in an inconstructive way. Together with an axiomatization of the natural numbers, the second property can be encoded in a first-order logic, and, thus, be proved.
Hence, for a data type specification certain properties of the involved functions are proved in advance, in order to allow the use of these properties later on for proofs of orderings being well-founded. Thereby, this approach together with the generalized Estimation Calculus enables an efficient automation of the proofs for an ordering to be well-founded.
For a demonstration of how our method works in practice, DFKI Research Report RR-96-06 contains many examples of data types together with various function and predicate specifications, as well as the resulting proof obligations during the proofs for orderings to be well-founded.