DFKI Research Report-96-01 |
Induction on Non-Freely Generated Data Types
188 Pages
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 -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 -relation. Moreover, usually both terms possess a common subterm. Hence, the proof obligations are of the form:
In order to prove this obligation, it is split by the Estimation Calculus into a chain of estimations with respect to the -relation. Furthermore, each single estimation is based on certain properties of the underlying formal specification:
To show that the objects which are denoted by the two terms are within the strict -relation, for each single estimation a formula is synthesized which is sufficient for the -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.
This document is available as Postscript.
The next abstract is here, and the previous abstract is here.
Note: This page was written to look best with CSS stylesheet support Level 1 or higher. Since you can see this, your browser obviously doesn't support CSS, or you have turned it off. We highly recommend you use a browser that supports and uses CSS, and review this page once you do. However, don't fear, we've tried to write this page to still work and be readable without CSS.