Proof search and induction choices in AF_{2} system

D. Galmiche and O. Hermann

CRIN-CNRS & INRIA-Lorraine Campus Scientifique - B.P. 239 54506 Vandœuvre-lès-Nancy Cedex France. e-mail : galmiche{ohermann}@loria.fr

Abstract

We consider, in this paper, the AF_{2} system with the aim to automatize the proof search process considering the possibilities to synthesize programs but also to prove some properties of the programs. In our work, we consider an analysis of program specifications to take in charge the problem of induction choice and we propose adequate induction schemas to instantiate the induction step in the proof search process. In a certain way, our analysis allows to generate a proof strategy based on a specific proof form (including an adequate induction) for different kinds of function specifications. Thus we describe a proof search procedure based on induction choices following a classification of function specifications in AF_{2} w.r.t. the failure cases of given induction schemas.

1 Introduction

A lot of type-systems have been proposed since several years with a main purpose that is program extraction via the Curry-Howard isomorphism establishing a correspondence between proofs of specifications and programs. Here we consider one of these systems, namely AF_{2} (second order functional arithmetic) [5, 7] such that algorithmic specifications are equations and having a programming method that ensures the correctness of programs extracted form proofs of function totality. But what about construction of proofs and programs and also efficiency of these programs ? It appears clearly that there exists a link between the choice of data types definition, and then of induction schema during the proof search, in this logical system and the efficiency of extracted programs [8]. To get the efficiency that one might expect some works have introduced new types in AF_{2} as inductives types [9] or coinductive types [10] preserving the correctness of the programming method. Another point consists in trying to propose some procedures for inductive proof search that could generate efficient programs with a maximal mechanization of the proof search process. In our work, that is the continuation of previous work on automated proof search in AF_{2} based on tactics and proof plans [2, 3], we consider the initial logical system (without extensions or restrictions) as an appropriate sequent calculus and we try to automate the proof search process considering the possibilities to synthesize programs or to prove some program properties. In previous work, in a restriction of AF_{2} with recursive types, [6] has proposed, for two fixed induction schemas, specific proof strategies based on specific proof forms. These strategies are correct and complete but the choice of the induction schema is made a priori by the user. Let us recall that most inductive theorem provers rely upon the user intervention with the need for some eureka steps such as this induction schema selection [1, 4]. Moreover, expressing the properties in a second order logical framework allows the generation of new induction schemas based on specific second order substitutions. In this paper, we consider an analysis of program specifications to take in charge this problem of induction choice and then propose adequate induction schemas to instantiate the induction step in the proof search process. In a certain way, our analysis allows to generate a proof strategy based on a specific proof form (including an adequate induction) for different kinds of function specifications. Thus, we describe here a procedure of induction choice with an original approach based on a classification of function specifications in AF_{2} w.r.t. the failure cases of proof search with given induction schemas. It defines and classifies the induction positions and variables inside the specification and thus selects an induction schema for each induction position. This proposal is based on a taxonomy of function specifications w.r.t. induction choices failure cases. Compared to other works [6, 9], we do not restrict the use of some data types and then keep in this automated proof search the possibility to synthesis some efficient programs. But with this global approach we do not have directly proof forms and proof strategies that are complete w.r.t. to provability of certain specifications forms. Here the choice of the induction schema is not made a priori by the user but proposed by a procedure. Therefore we have a general proof form with four main parts that are specification analysis that leads to possible induction choices, induction, rewriting and resolution. If we fix some induction choices and some specifications forms, we can recover refined proof forms that are complete as in [6] and a further work would consists to start from our results and to refine them to propose new proof forms that would be complete for given specifications. In this way, we could have a powerful tool for interactive and automated proof search in AF_{2} and their programming applications. We will illustrate the interest of this procedure (and of the underlying second order intuitionistic logic) for efficient and successful proof search leading to efficient programs and also avoiding some eureka steps during properties proof search.

2 The logical framework

In this paper, we consider a second-order constructive framework, named AF_{2} [7]. It is a secondorder typed lambda-calculus, that is a natural deduction system for our logic with extraction of λ-terms (considered as programs) from constructive proofs.

2.1 A second order constructive logic

The formulae (or types) are constructed using the connective →, the quantifier ∀, individual (or first order) variables x, y, z,..., predicate (or second-order) variables X, Y, Z,..., individual and function constants. The individual terms are constructed from individual and function constants. Notice that the other logical symbols are definable from → and ∀. The expressions of the language are in the form a : A with either one of these interpretations: a is an element of type A, or a is a proof of the proposition A. Here, we consider the second one where formulas are regarded as types and deductions as λ-terms. The construction of deductions uses the following inference rules (A, B denote formulae while Γ represents contexts, i.e., sequences of formulae and F V (Γ) the set of free variables in the context Γ):

R1. Axiom. x : A ⊢ x : A R2. Abstraction rule. If Γ, x : A ⊢ t : B then Γ ⊢ λx.t : A → B R3. Application rule. If Γ ⊢ t : A → B, and Γ ⊢ u : A then Γ ⊢ (t,u) : B R4. Generalization rule 1. If Γ ⊢ t : A with x ∉ FV(Γ) then Γ ⊢ t: ∀x A R5. Specialization rule 1. If Γ ⊢ t : ∀x A, with b individual term then Γ ⊢ t : A[b/x] R6. Generalization rule 2. If Γ ⊢ t : A with X ∉ FV(Γ) then Γ ⊢ t : ∀ X A R7. Specialization rule 2. If Γ ⊢ t : ∀ X A with b a formula then Γ ⊢ t : A[b/ X] R8. Equivalence rule. If Γ ⊢ t : A then Δ ⊢ t : A if Δ is obtained from Γ by permutation, extension or contraction. R9. Equality rule. If Γ ⊢ t : A and u = v then Γ ⊢ t : A[v/u] .

Programming in this framework consists in giving first a formal specification (a logical proposition and some equations stating the behaviors of the intended function), constructing a proof of the given formula and then extracting code systematically from this proof with the realizability notion. Programs obtained this way have the essential properties of correctness and termination. This framework naturally contains induction through the data type definitions. For example, it is possible to define integers following an iterative or recursive way . The iterative definition for integers is expressed by the following second-order formula: Nx ≡ ∀X [∀y [Xy → Xs(y)] → [X0 → Xx]] where X design a second-order variable and x, y first-order variables. The recursive definition is expressed by the following formula: Nx ≡ ∀X [∀y [Ny → Xy → Xs(y)] → [X0 → Xx]].

2.2 How to express specifications and properties

In this framework, a function f is specified by a formal specification Spec composed of some equations stating the behaviors of the intended function and of a formula F stating that the function is well typed. Then a n-ary function f : T_{1} × ... × T_{n} → T is defined by:

- p equations of the form: f(t_{11}, ..., t_{1n}) = u_{1}, ...... f(t_{p1}, ..., t_{pn}) = u_{p}.

- a formula that expresses its type information: ∀z_{1} T_{1}z_{1} → .... → ∀z_{n}T_{n}z_{n} → T f(z_{1}, ..., z_{n}).

In fact, a data type is defined by a name T and a set of constructors composed by

- basic constructors: c_{1}, .., c_{p} with c_{i} of type T,

- functional constructors: cf_{1}, .., cf_{k} with cf_{i} of type A_{i1} × ... × A_{is_{i}} × T × ... × T → T with A_{ij} soon defined. Moreover, the iterative definition of type T is given by the expression T z ≡ ∀X(ϕ_{1} → .... → ϕ_{k} → Xc_{1}... → Xc_{p} → Xz with ϕ_{i} ≡ ∀a_{i1}A_{i1}a_{i1} → ... → a_{is_{i}}A_{is_{i}}a_{is_{i}} → y_{i1}X_{i1}y_{i1} → y_{it_{i}}X_{it_{i}}y_{it_{i}} → Xcf_{i}(a_{i1}, ..y_{it_{i}}).

Example 2.1 We define the addition function with the following specification (1) plus(0, y) = y,

(2) plus(s(x), y) = s(plus(x, y)),
(3) ∀z (Nz → (∀z_{1}(Nz_{1} → Nplus(z, z_{1})))).

Moreover, the iterative definition of integer data type is given by the following expression Nz ≡ ∀X(∀y(Xy → Xs(y)) → (X0 → Xz)).

If we prove (3) in G_{AF 2}, the λ-term extracted from the proof will be a program of addition. Even, we can naturally use the proof of the type formula to synthesize programs, we will consider here another formulas that express properties or conjectures on functions expressed in this calculus. Such properties have here the following general form: ∀z_{1} T_{1}z_{1} → .... → ∀z_{n}T_{n}z_{n} → (f(g_{1}(z_{11}, ... z_{1r_{1}}), ...g_{n}(z_{n1}, ..., z_{nr_{n}})) = h(z_{11}, ...z_{nr_{n}}) with f, h, g_{1}, ...g_{n} are specified in the logical framework.

Example 2.2 We can express properties as the associativity of the addition function by ∀z (Nz → ∀z_{1} (Nz_{1} → ∀z_{2} Nz_{2} → (plus(z, plus(z_{1}, z_{2})) = plus(plus(z, z_{1}), z_{2})))).

3 Proof search in AF_{2}

There are some works devoted to AF_{2} as programming with proofs language. From the proof search point of view, a main work concerns a restriction of AF_{2} with recursive types [6] with, for two induction schemas, a specific proof strategy based on a specific proof form. These two strategies are correct and complete but the choice of the induction schema is made a priori by the user. Here we want to consider the initial logical system and to try to automatize such inductions choices.

3.1 A sequent calculus for AF_{2}

The previous system was formulated under a natural deduction formalism. Thus, a first step towards proof search methods consists in proposing an equivalent sequent calculus, denoted here G_{AF_{2}} that will be more adapted for automated proof search.

- Axiom:

- → rules:

\frac{Γ, x : A ⊢ T : B}{Γ ⊢ λx.T : A → B} (→_{r})∗  \frac{Γ ⊢ M : A Γ, y : B ⊢ N : C}{Γ, x : A → B ⊢ N[y := (xM)] : C} (→_{l}) ∗ ∗

- ∀_{1} rules

\frac{Γ, t : ∀x A, t_{1} : A[y/x] ⊢ M : C}{Γ, t : ∀x A ⊢ M[t_{1} := t] : C} (∀_{1}_{l})∗  \frac{Γ ⊢ M : A}{Γ ⊢ M : ∀x A} (∀_{1}_{r}) ∗ ∗

- ∀_{2} rules

\frac{Γ, t : ∀X A, t_{1} : A[F/X] ⊢ M : C}{Γ, t : ∀X A ⊢ M[t_{1} := t] : C} (∀_{2}_{l})∗  \frac{Γ ⊢ M : A}{Γ ⊢ M : ∀X A} (∀_{2}_{r}) ∗ ∗

currence in Γ

- Equality rules ^{1}

\frac{Γ ⊢ M : A[v/u]}{Γ ⊢ M : A} (=_{r})  \frac{Γ, t : A[v/u] ⊢ N : C}{Γ, t : A ⊢ N : C} (=_{l})

\overline{Γ, x : A ⊢ x : A} (ax)

(*) where x has no occurrence in Γ and (**) where y has no occurrence in Γ.

(*) where t_{1} has no occurrence in Γ and t_{1} ≠ t, (**) if the first order variable x has no free occurrence in Γ.

(*) with t_{1} ≠ t and t_{1} has no occurrence in Γ, (**) if the second order variable X has no free ocif u = v is an instance of an equation.

1In these rules we use the notation A[v/u] to represent the substitution in the formula A of the first order term u by the first order term v

- Equivalence rules

\frac{Γ ⊢ M : A}{Γ ⊢ M : B} (eq_{r})  \frac{Γ, t : A ⊢ N : C}{Γ, t : B ⊢ N : C} (eq_{l})

if A ≡ B.

- Cut rule

\frac{Γ ⊢ M : A Γ, y : A ⊢ N : C}{Γ ⊢ N[y := M] : C} (cut)

where y has no occurrence in Γ.

- Structural rules

\frac{Γ, t : A, t_{1} : A ⊢ N : C}{Γ, t : A ⊢ N[t_{1} := t] : C} (cont)

where t_{1} ≠ t and t_{1} has no occurrence in Γ.

\frac{Γ, t : A ⊢ N : C}{Γ, t : A, t_{1} : A ⊢ N : C} (weak)  \frac{Γ, t : A ⊢ N : C}{t : A, Γ ⊢ N : C} (exch)

This sequent calculus is equivalent to the initial logical system, i.e.,

Theorem 3.1 Γ ⊢_{AF 2} M : A if and only if Γ ⊢_{G_{AF 2}} M : A

Let us remark that we can naturally define, from this calculus, the notions of tactic and proof plan dedicated to this framework and thus proposed some plans to search proofs and extract programs from them [2, 3].

3.2 How to guide inductive proofs in G_{AF 2}

When we want to develop inductive proofs in such a framework, some problems arise as: how to find at what place to apply induction ? on which variables to apply it ? and which induction schemas to apply ? In fact, we will restrict the form of equations such that we can find and order the places where induction is applied only with a study of the left-hand side members of the equations. Finally, it is not a significant restriction because we express the classical algorithms and functions with such a form. In this case, the first two mentioned problems have direct solutions and we will focus on the third one by looking for induction schemas to apply and for proof search strategies that can be associated to them.

3.2.1 Preliminary definitions

Definition 3.1 Let t = f(t_{1}, ..., t_{n}) be a term and u a subterm of t, the place of u in t is defined by pl(u, t) = i if there exists i such that u = t_{i}, pl(u, t) = i.pl(u, t_{i}) if u has an occurrence in t_{i}.

Definition 3.2 The subterm u of term t in place q is inductively defined by s term(t, 0) = t, s term(f(t_{1}, ..., t_{n}), i.q) = s term(t_{i}, q).

Definition 3.3 The substitution of z by t in f(t_{1}, .., t_{n}) at place q, denoted f(t_{1}, .., t_{n})[t/z]_{q}, is defined by f(t_{1}, .., t_{n})[t/z]_{q} = f(t_{1}, ..t_{i−1}, t, t_{i+1}, ..., t_{n}), if q = i and s term(f(t_{1}, ..t_{n}), i) = z, = f(t_{1}, ..., t_{n}), if q = i and s term(f(t_{1}, ..t_{n}), i) ≠ z, = f(t_{1}, ..t_{i−1}, t[t/z]_{q′}, t_{i+1}, ..., t_{n}), if q = i.q′.

We naturally extend this definition to the substitution of z by t in a formula F (F [t/z]_{q}).

3.2.2 Induction positions and induction variables

We consider here as specification a set of equations that have a restricted form and that are called acceptable. We do not give here formal definitions knowing that all classical functions and algorithms can be represented in such a system. In fact, an important result to notice is that the choice of places and variables to apply induction is direct in this case. Moreover, this form ensures the sufficient completeness of the function definition.

Definition 3.4 Let us consider two places q_{1} and q_{2} in a term t, we have q_{1} ≤_{a} q_{2} if q_{2} = q_{1}.k

Definition 3.5 A place q is an induction position in a term t if

1. s term(t, q) = c_{T} (t_{1}, ...t_{n}) with T data type,

2. for any i, c_{T} (t_{1}, ...t_{n}) has no occurrence in t_{i},

3. q = inf{p / s term(t, p) = c_{T} (t_{1}, ..., t_{n})}.

Definition 3.6 Let S be an acceptable specification of f (g_{i} = d_{i}, 1 ≤ i ≤ p), the set of induction positions of the equation g_{i} = d_{i} is P os_{i}(f) = {q, q induction position of g_{i}}. The set of induction positions of S is P os(f) = ∪_{i=1}^{p}P os_{i}(f).

Definition 3.7 Let f a function with type formula ∀z_{1}T z_{1} → ......∀z_{n}T z_{n} → T f(z_{1}, ...z_{n}) with P os(f) = {q_{1}, ..q_{p}}, the set of induction variables (denoted V ar(f)) is {v_{1}, ...v_{p}} with v_{i} = z_{i} for 1 ≤ q_{i} ≤ r and v_{i} =?var (meta-variable) in the other cases.

Thus, having a specification in AF_{2} with the type formula F, we are able to determinate the list of the induction positions pos list = [q_{1}, q_{2}, ..., q_{n}] and the list of the induction variables v list = [v_{1}, v_{2}, .., v_{n}] with an algorithm that analyses the specification. Now we can focus our attention on the following question: which induction schemas to apply ?

3.2.3 Second order substitution

An essential feature of AF_{2} is the second-order specialization rule which allows us to substitute a second-order variable (i.e., predicate variable) by either a predicate or a formula. This choice corresponds exactly to induction choice. Let us start to illustrate with the addition example the importance of second order substitution and its effect on proof search success. If we want to prove (3) by using the iterative definition of integer data type we have Nz ≡ ∀X(∀y(Xy → Xs(y)) → (X0 → Xz))(≡ F). To prove ⊢ ∀z (Nz → (∀z_{1}(Nz_{1} → Nplus(z, z_{1})))), we can apply all the possible right rules and then we have to prove v : Nz, v_{1} : Nz_{1} ⊢ ∀X(∀y(Xy → Xs(y)) → (X0 → Xplus(z, z_{1}))). Therefore, we have v : Nz, v_{1} : Nz_{1}, f : ∀y(Xy → Xs(y)), a : X0(≡ Γ) ⊢ Xplus(z, z_{1}). We can start with Γ ⊢ v_{1} : Nz_{1} and then develop Nz_{1} to obtain Γ ⊢ v_{1} : ∀X_{1}(∀y_{1}(X_{1}y_{1} → X_{1}s(y_{1})) → (X_{1}0 → X_{1}z_{1}))(≡ F_{1}). Having to prove Γ ⊢ Xplus(z, z_{1}), we apply to F_{1} the following second order substitution F_{1}[Xplus(z, x)/X_{1}x]. In fact, we substitute a predicate Xplus(z, ) to the second order variable X_{1} and obtain Γ ⊢ v_{1} : ∀y_{1}(Xplus(z, y_{1}) → Xplus(z, s(y_{1})) → (Xplus(z, 0) → Xplus(z, z_{1}). It leads to an induction schema and prove, by induction on z_{1}, the basis case Xplus(z, 0) and the induction case ∀y_{1}(Xplus(z, y_{1}) → Xplus(z, s(y_{1}))). Finally, the proof search is successful.

The choice of the second order substitution is essential and can lead to a success or a failure during the proof search process. For example, the substitution F_{1}[Xplus(x, z_{1})/X_{1}x] is not usable and the substitution F [Xplus(x, z_{1})/X_{1}x] leads to an induction schema that can be successful only if we have supplementary equations in the specification as plus(x, 0) = x and plus(x, s(y)) = s(plus(x, y)). Another substitution in the previous proof [∀z(Nz → Nplus(z, z_{1}))/X_{1}x]F_{1} leads to a new proof of the initial formula.

3.3 Induction schemas and proof search

The application of induction consists principally in the use of the second order substitution rule and the different forms of induction are derived from different substitutions. A first one consists of the maximum breakdown of the formula to prove (application of right rules) to obtain an atomic formula and is called predicate induction because it involves the substitution of a predicate to a second order variable. At the opposite, a second one consists of a minimum breakdown of the formula to prove and is called formula induction because it involves the substitution of a second order formula to a second order variable. Here we only present the rules corresponding to iteration and do not treat the recursion rules.

Definition 3.8 Predicate iteration. A predicate iteration on the variable z at the q place consists of the application of the (∀_{2} l) rule of G_{AF 2} with the following schema:

\frac{Γ, M : T z, M : F [F_{1}/X_{1}x] ⊢ N : Xf(t_{1}, ⋯, t_{n})}{Γ, M : T z, M : F ⊢ N : Xf(t_{1}, ⋯, t_{n})} (∀_{2} l)

with X second order variable, T z ≡ ∀X_{1}(Φ_{T} → (X_{1}b_{T} → X_{1}z)), x new variable, z has a unique occurrence in f(t_{1}, ⋯, t_{n}) at the q place and F_{1} ≡ Xf(t_{1}, ⋯, t_{n})[x/z]_{q}.

If we consider the previous example, we have applied, in the first case, the predicate iteration with the following instantiation

\frac{Γ, v_{1} : T z, v_{1} : F [Xplus(z, x)/X_{1}x] ⊢ t : Xplus(z, z_{1})}{Γ, v_{1} : T z, v_{1} : F ⊢ t : Xplus(z, z_{1})} (∀_{2} l)

with F ≡ ∀X_{1}(∀y_{1}(X_{1}y_{1} → X_{1}s(y_{1})) → (X_{1}0 → X_{1}z_{1})).

Definition 3.9 Formula iteration A formula iteration on the variable z at the q place consists of the application of the (∀_{2} l) rule of G_{AF 2} with the following schema:

\frac{Γ, M : T z, M : F [F_{1}/X_{1}x] ⊢ N : F_{2}}{Γ, M : T z, M : F ⊢ N : F_{2}} (∀_{2} l)

with T z ≡ ∀X_{1}(Φ_{T} → (X_{1}b_{T} → X_{1}z)), x new variable, F_{2} = ... → Df(t_{1}, ⋯, t_{n}), z has a unique occurrence in f(t_{1}, ⋯, t_{n}) at the q place and F_{1} ≡ F_{2}[x/z]_{q}

If we consider the previous example, we have applied, in the second case, the formula iteration with the following instantiation

\frac{Γ, v_{1} : T z, v_{1} : F [F_{1}/X_{1}x] ⊢ t : F orm}{Γ, v_{1} : T z, v_{1} : F ⊢ t : F orm} (∀_{2} l)

with F ≡ ∀X_{1}(∀y_{1}(X_{1}y_{1} → X_{1}s(y_{1})) → (X_{1}0 → X_{1}z_{1})), F_{1} ≡ ∀z(Nz → Nplus(z, z_{1})) and F orm ≡ ∀z(Nz → Nplus(z, z_{1}).

3.4 Inductive proof search strategies

Considering the previous induction schemas, we can define for each one a proof search strategy. Let us illustrate this point with the predicate iteration

Definition 3.10 Let f be a function specified in AF_{2} with F its type formula and such that pos list = [q_{1}, q_{2}, .., q_{n}] and v list = [v_{1}, v_{2}, ..., v_{n}], the predicate iteration proof strategy consists in proving F with an initial decomposition phase, n applications of predicate iteration on the variables v_{1}, ..., v_{n} at places q_{1}, ..., q_{n}, followed by applications of right and left rules of the sequent calculus G_{AF 2}.

In fact, the predicate iteration is successful for the addition specification. It fails for the predecessor specification for which we have pos list = [1] and v list = [z]. But if we consider a recursive definition of integers we obtain a success. The formula iteration fails also for the same reasons. In the case of Ackermann specification we have pos list = [1, 2] and v list = [z, z_{1}] and the predicate iteration proof strategy fails, even if we consider a recursive definition of integers. But we can show that the formula iteration proof leads to a success with iterative data type definition. In the case of Fibonacci specification the predicate iteration proof strategy fails, even with a recursive definition of integers. We have the same result for the formula iteration proof.

4 Failure cases for proof search strategies

The previous simple examples are only instances of specific specifications forms for which some proof strategies fail. In this section, we define various classes of function specifications such that a given proof strategy fails.

4.1 Functions with out-variables

Definition 4.1 A variable y is a possibly out-variable in the term t if y has an occurrence in a subterm of t having the form c_{T} (a_{1}, ⋯, a_{r}, y_{1}, ⋯ y_{s}) with c_{T} : A_{1} × ⋯ A_{r} × T ⋯ × T → T, c_{T} being a functional constructor associated to type T.

Definition 4.2 The variable y is a variable independent of f in term t if there exists a place q such that s_term(t,q) = y and ∀q′ ≥_{a} q, s term(t, q′) ≠ f(⋯).

Definition 4.3 Let f be a function defined with a system of p equations and the formula ∀z_{1} T_{1}z_{1} → ⋯ → ∀z_{n} T_{n}z_{n} → f(z_{1}, ⋯, z_{n}), z_{i} is a out-variable for the equation e_{m} : f(t_{1}, ⋯, t_{n}) = d_{m} if there exists y such that the following three conditions are verified: 1) y is a variable independent of f in d_{m}, 2) y is a possible out-variable of t_{i}, 3) the position of i is an induction position.

The set of out-variables of the equation e_{m} for f will be denoted V S_{m}(f) and the set of out-variables for f : ∪_{i=1}^{p}V S_{m}(f) is denoted V S(f).

In the case of the predecessor, in the second equation, the possible out-variable y is independent of p and thus V S(p) = {z}. If we consider the Ackermann specification, the first equation has no possible out-variable (no function constructor) and there is no independent variable of ack in the others and then V S(ack) = ∅.

Theorem 4.1 Let f be a n-ary function such that pos list = [1, 2, .., p] and V S(f) ≠ ∅, let F be its type formula, if the data type definition is iterative then the proof search strategy by predicate iteration or by formula iteration applied to F fails.

Proof 4.1 see appendix A

This result confirms that the predicate strategy fails for the predecessor.

4.2 Special recursive functions

Definition 4.4 Let f be a function such that pos list = [1, 2, ⋯, p], it is transverse-recursive if an equation of its specification is transverse, i.e, has one of the following forms :

(1) f(c_{1}(⋯), ⋯, c_{j}(⋯), b_{j+1}, z_{j+2}, ⋯, z_{n}) = f(c_{1}(⋯), ⋯, c_{j−1}(⋯), y_{j_{i}}, b_{j+1}, z_{j+2}, ⋯, h(⋯, z_{k}, ⋯), ⋯, z_{n}) or f(c_{1}(⋯), ⋯, c_{j−1}(⋯), y_{j_{i}}, h(⋯, b_{j+1}, ⋯), z_{j+2}, ⋯, z_{n}).

(2) f(c_{1}(⋯), ⋯, c_{p}(⋯), z_{p+1}, ⋯, z_{n}) = f(c_{1}(⋯), ⋯, c_{p−1}(⋯), y_{p_{i}}, z_{p+1}, ⋯, h(⋯, z_{k}, ⋯), ⋯, z_{n}) with h function soon defined.

Definition 4.5 An equation of f is p-decreasing with p ≥ 1 if it has one of the following forms: f(c_{1}(⋯), ⋯, c_{j}(⋯), u_{j+1}, z_{j+2}, ⋯, z_{n}) = g(⋯, f(v_{1}, ⋯, v_{j−1}, y_{j_{m}}, u_{j+1}, z_{j+2}, ⋯, z_{n}), ⋯) or f(c_{1}(⋯), ⋯, c_{j}(⋯), u_{j+1}, z_{j+2}, ⋯, z_{n}) = f(v_{1}, ⋯, v_{j−1}, y_{j_{m}}, u_{j+1}, z_{j+2}, ⋯, z_{n}) with for any i from 1 to j -1, v_{i} = c_{i}(⋯) or y_{i_{k}}, g defined function and p the number of v_{i} such that v_{i} = y_{i_{k}}. A function f is a multi-decreasing function if an equation of its specification is p-decreasing with p ≥ 1.

The decreasing set of the equation e_{m} for f will be denoted MD_{m}(f) = {z_{k}/l + 1 ≤ k ≤ j} and the decreasing set of f is ∪_{i=1}^{p}MD_{m}(f) is denoted MD(f).

Theorem 4.2 Let f be a n-ary function such that pos list = [1, 2, .., p] and MD(f) ≠ ∅ and let F ≡ ∀z_{1} T_{1}z_{1} → ....∀z_{n} T_{n}z_{n} → T f(z_{1}, ...z_{n}) be its type formula, the proof search strategy by formula iteration applied to F fails

Definition 4.6 An induction variable is recursive if it is an out-variable or if it belongs to MD(f). The set of recursive variables for f is Rec(f) = V S(f) ∪ MD(f).

Theorem 4.3 Let f be a n-ary function such that pos list = [1, 2, .., p] and Rec(f) ≠ ∅ and let F ≡ ∀z_{1} T_{1}z_{1} → ....∀z_{n} T_{n}z_{n} → T f(z_{1}, ...z_{n}) be its type formula, the proof search strategy by formula iteration applied to F fails

Definition 4.7 A function f is a multi-recursive function if an equation of its specification has one of the following forms: f(c_{1}(⋯), ⋯, c_{j}(⋯), u_{j+1}, z_{j+2}, ⋯, z_{n}) = g(⋯, f(t_{1}, ⋯, t_{n}), ⋯) or f(c_{1}(⋯), ⋯, c_{j}(⋯), u_{j+1}, z_{j+2}, ⋯, z_{n}) = f(t_{1}, ⋯, t_{n}) with f having at least an occurrence in a term t_{i} and g defined function.

Definition 4.8 A function f is a special recursive function if it is transverse-recursive or multidecreasing or multi-recursive.

The Ackermann function is multi-recursive because of the equation ack(s(x), s(y)) = ack(x, ack(s(x), y)) and thus it is special recursive.

Theorem 4.4 Let f be a n-ary function multi-recursive such that pos list = [1, 2, .., p] and v list = [z_{1}, z_{2}, .., z_{p}] and let F ≡ ∀z_{1} T_{1}z_{1} → ....∀z_{n} T_{n}z_{n} → T f(z_{1}, ...z_{n}) be its type formula, the proof search strategy by predicate iteration applied to F fails.

4.3 Complex recursive functions

Definition 4.9 A function f is a complex recursive function of level 2 at position q.i if there are two base cases for a same induction position, i.e., three equations of the forms : f(t_{1}, ⋯, t_{q−1}, b_{D}, t_{q+1}, ⋯, t_{n}) = G, f(t_{1}, ⋯, t_{q−1}, c_{D}(a_{1}, ⋯, a_{r}, y_{1}, ⋯, y_{i−1}, b_{D}, y_{i+1}, ⋯, y_{s}), t_{q+1}, ⋯, t_{n}) = H, f(u_{1}, ⋯, u_{q−1}, c_{D}(a_{1}, ⋯, a_{r}, y_{1}, ⋯, y_{i−1}, c_{D}(a′_{1}, ⋯, a′_{r}, y′_{1}, ⋯, y′_{s}), y_{i+1}, ⋯, y_{s}) u_{q+1}, ⋯, u_{n}) = I, with at most an index j such that u_{j} ≠ t_{j}.

Definition 4.10 The set of complex positions of f is defined by Comp(f) = { q.i such that q ∈ pos_list and et f is complex recursive of level 2 at the position q.i }

The fibonacci function is complex recursive at the position 1.1

Theorem 4.5 Let f be a n-ary function, complex recursive at level 2 at the position q.i, such that pos list = [1, 2, .., p] and v list = [z_{1}, z_{2}, ..., z_{p}] and let F ≡ ∀z_{1} T_{1}z_{1} → ....∀z_{n} T_{n}z_{n} → T f(z_{1}, ...z_{n}) be its type formula, the proof search strategy by predicate iteration or by formula iteration applied to F fails

5 Other induction schemas

In the example of the predecessor, we have a failure of the predicate iteration strategy (with iterative data types) because we have no derivation of the judgement Γ, Xp(y) ⊢ Xy. But when we consider the recursive definition of integers, the type information about the out-variable y involved in the hypothesis Ny can lead to a success in the proof search. It leads to another induction schema, called predicate recursion, that corresponds to the definition of predicate iteration only modified with F_{1} ≡ Xf(t_{1}, .., t_{n})[x/z]_{q} ∧ Xx. We can prove, as in the previous section, that a proof strategy based on predicate recursion fails in the both cases of special recursive and complex recursive functions. Thus we can apply it to the predecessor but it does not solve the other examples. With the same approach, we can propose another induction schema, called formula recursion, that corresponds to the definition of formula iteration only modified with F_{1} ≡ F orm[x/z]_{q} ∧Dx. With a proof strategy based on this induction schema, we can solve the addition, predecessor and Ackermann examples. But it cannot solve the failure concerning the complex recursive functions because of the impossibility to use the given equations to find a correspondence between the conclusion and the induction hypothesis. Some work have considered this problem and proposed some methods to sove it [4]. But in our work we want to consider the potentialities of the second order substitution to solve this problem and consequently we propose new induction schemas corresponding to case induction or recursion. If we consider that a function can be at the same time complex recursive and/or special recursive and/or can have out variables we thus can propose four new induction schemas that are case predicate or formula / iteration or recursion. If we apply a proof strategy based on the induction schema named case predicate iteration, we obtain a successful proof search for the fibonacci function.

6 A procedure for efficient inductive proof search

Starting from the previous results on induction, we propose here a procedure for choice of induction that take in charge some choices about finding and ordering induction positions and variables and about choosing the induction mode for each induction position. With such a procedure we have a main goal that is to avoid the failure cases we have found, that means: to avoid predicate induction for special recursive function, to avoid iteration for a out-variable when data types are iteratively defined, to avoid formula and predicate induction for a complex induction position. In fact, we can also propose heuristics for the choices among the possible induction, if we focus on the problem on the efficiency of the extracted programs.

6.1 Principles of the procedure

The aim of this procedure is to fix some choices concerning the induction schemas. In fact, it takes the specification and gives as results the instantiations of the four following lists:

- pos list: list of the induction positions,

- v list: list of the induction variables,

- f list: list of the formula inductions to apply,

- p list: list of the predicate inductions to apply.

It corresponds to two main phases, i.e., (1) the choice and ordering of induction positions and variables, (2) the choice of the adequate induction form for each induction variable. Let us illustrate these phases with the example of the addition. The procedure of selecting and ordering the induction positions and variables leads to pos list = [2] and v list = [z_{1}]. To instantiate f list and p list, we analyze the criteria studied in the previous section as

- special recursive function or not,

- recursive variables or not (Rec(f) empty or not),

- complex induction positions (Comp(f) empty or not),

- definition of the data types (iterative or recursive). We obtain, with these four ordered criteria, sixteen cases to instantiate the two induction lists. For example, if f is special recursive, we reject the predicate induction and thus p list = []. Moreover, in this case, if there are no out variables, if there are complex induction positions and if the data definition is iterative, we have f list = [r_{1}, ..., r_{p}] where r_{i} = iteration if P os.j ∉ Comp(f) and r_{i} = case rec(j) if P os.j ∈ Comp(f) The complete procedure, including all the analysis case will be given in the full paper. In the case of our example, plus is not a special recursive function and Rec(f) = Comp(f) = ∅ and thus we have f list = [] and p list = [iteration] for any data type definition.

6.2 Application of the procedure

It is possible to illustrate the interest of the procedure to determinate the adequate induction schemas for program synthesis in AF_{2} but also for proving program property, we consider the proof search of a given conjecture or property that involves the definition of the addition, the multiplication and a particular function f and such that automated proof search with other methods involves eureka steps and failure cases. Let us consider at first the specification of the addition on integers. Moreover, we assume that the two following properties have been proved : ∀z (Nz → ∀z_{1} (Nz_{1} → ∀z_{2} Nz_{2} → (plus(z, plus(z_{1}, z_{2})) = plus(plus(z, z_{1}), z_{2})))), i.e., the addition function is associative and ∀z (Nz → plus(z, 0)) = z. We consider also the multiplication specification: mult(0, y) = 0, mult(s(x), y) = plus(y, mult(x, y)) and ∀z (Nz → (∀z_{1}(Nz_{1} → Nmult(z, z_{1})))) Starting from the previous definition, we define the function f as follows f(0, y, z) = z, f(s(x), y, z) = f(x, y, add(y, z))and ∀z (Nz → (∀z_{1}(Nz_{1} → ∀z_{2}(Nz_{2} → Nf(z, z_{1}, z_{2}))))). We consider now the following conjecture to prove: f(z, z_{1}, z_{2}) = plus(z_{2}, mult(z, z_{1})). It means that in our logical framework we have to prove

∀z (Nz → ∀z_{1}(Nz_{1} → ∀z_{2}(Nz_{2} → (f(z, z_{1}, z_{2}) = plus(z_{2}, mult(z, z_{1}))))))

We apply the induction choice procedure to the three functions plus, mult and f and obtain the following proposal:

- for the function plus, it suggests to perform predicate iteration on the first variable i.e. z since this function is not a special recursive one nor a complex recursive one and has no out variables.

- for the function mult, it suggests to perform predicate iteration on the first variable i.e. z for the same reason.

- for the last one f, it suggests to perform formula iteration on the first variable i.e. z since f is a special recursive function.

Taking into account the result of the induction choice procedure for the three functions occurring in this conjecture and the order over the induction schemes, it proposes to prove it by formula iteration on the first variable i.e. z. This involves a given proof form and also a proof search strategy, including this induction choice, that leads to a successful automated proof. The complete proof will be given in the full paper.

7 Concluding remarks

In a restriction of AF_{2} with recursive types, [6] has proposed for two induction schemas a specific proof strategy based on a specific proof form that is correct and complete but the choice of the induction schema is made a priori by the user. In our work, we propose an analysis of the specification to take in charge this problem of induction choice and thus we propose an adequate induction schema to instantiate the induction step in the proof search process. In a certain way, our analysis allows to generate a proof strategy based on a specific proof form (including an adequate induction) for different kinds of function specifications. An important further work could be to refine our method by fixing a priori proof strategy and specification forms and thus to prove the completeness of the former w.r.t of the latter. Most theorem provers rely upon user interaction to identify and patch failures. Our work attempts to automatize this process following an original approach. The method depends on theoretical results of failure of induction in a second order logical framework and allows to select the induction rule in order to avoid these failure cases. In such a framework we have established a taxonomy of recursively defined functions w.r.t induction schemas failures. Our study initially dedicated to program synthesis in AF_{2} appears as a nice method to prune the proof search tree in inductive proof and the use of second order substitution allows to avoid some eureka steps that appears when we develop similar proof in first order framework. To extend these results to another conjecture forms we need also to deal with failures due to the lack of some lemmas. This problem has already been tackled in other works and would be necessarily considered in our global approach.

References

[1] A. Bundy, F. Van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7(3):303–324, 1991.

[2] D. Galmiche and O. Hermann. Automated proof and program development, volume 35 of IMA Conference Series, pages 397–410. Oxford University Press, 1992.

[3] D. Galmiche and O. Hermann. SKIL: A system for programming with proofs. In LPAR’93, International Conference on Logic Programming and Automated Reasoning, LNAI 698, pages 348–350, St. Petersburg, Russia, July 1993.

[4] D. Hutter. Guiding induction proofs. In 10th Conference on Automated DEduction, LNAI 449, pages 132–146, 1990.

[5] D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51–68, 1986.

[6] P. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science, 135(2):319–343, 1994.

[7] M. Parigot. Programming with proofs : a second order type theory. In European Symposium On Programming 88, LNCS 300, pages 145–159, Nancy, France, March 1988. Springer Verlag.

[8] M. Parigot. On the representation of data in lambda-calculus. In CSL ’89, LNCS 440, pages 309–321, Kaiserslautern, FRG, October 1989.

[9] M. Parigot. Recursive programming with proofs. Theoretical Computer Science, 94(2):335– 356, March 1992.

[10] C. Raffali. Data types, infinity and equality in system AF2. In 7th Workshop CSL’93, LNCS 832, pages 280–294, Swansea, UK, september 1994.

A Proof of theorem 4.1.

Theorem A.1 Let f be a n-ary function such that pos list = [1, 2, .., p] and V S(f) ≠ ∅, let F be its type formula, if the data type definition is iterative then the proof search strategy by predicate iteration or by formula iteration applied to F fails.

Proof A.1 Let z_{i} ∈ V S(f). 1- Let us consider the equation e_{m} having the form : f(c_{1}(⋯), ⋯, c_{i}(a_{i1}, ⋯, a_{ir_{i}}, y_{i1}, ⋯, y_{is_{i}}), ⋯, c_{m−1}(⋯), b_{m}, z_{m+1}, ⋯, z_{n}) = y_{ij} We can prove that after the steps of initial decomposition and of p applications of predicate iteration a leaf of the proof tree has the form: Γ_{m} ⊢ Xf(c_{1}(⋯), ⋯, c_{m−1}(⋯), b_{m}, z_{m+1}, ⋯, z_{n}) reduced by application of the (= r) (rewriting phase) to Γ_{m} ⊢ Xy_{ij}. The proof of this sequent fails because:

- no right-rule is applicable,

- there is no hypothesis of the form Xy_{ij} and thus the leaf is not an axiom,

- there is no hypothesis of the form Θ = ∀z F with F ≡ ... → Xz and thus the rule (∀_{1} l) cannot be applied,

- there is no hypothesis of the form Dy_{ij} with D data types and thus (eq l) cannot be applied. The failure reasons are the same if the equation e_{p} has the form : f(c_{1}(⋯), ⋯, c_{p}(a_{p1}, ⋯, a_{pr_{p}}, y_{p1}, ⋯, y_{ps_{p}}), z_{p+1}, ⋯, z_{n}) = y_{pj}.

2- Let us assume that the equation e_{m} has the form: f(c_{1}(⋯), ⋯, c_{i}(a_{i1}, ⋯, a_{ir_{i}}, y_{i1}, ⋯, y_{is_{i}}), ⋯, c_{m−1}(⋯), b_{m}, z_{m+1}, ⋯, z_{n}) = g(t_{1}, ⋯, t_{l}) with pl(y_{ij}, g(t_{1}, ⋯, t_{l})) = q. We can easily prove that there exists a derivation of ⊢ F such that one of the leaves is: Γ_{m} ⊢ Xf(c_{1}(⋯), ⋯, c_{m−1}(⋯), b_{m}, z_{m+1}, ⋯, z_{n}) that is reduced, by application of the (= r) rule (rewriting phase), to Γ_{m} ⊢ Xg(t_{1}, ⋯, t_{l}) We can only apply the (cut) rule that produces the leaves Γ_{m} ⊢ Xt_{i} pour i de 1 à l. Let us consider two cases : q = i (y_{ij} has an occurrence at depth 1) or q = i.k (y_{ij} has an occurrence at depth greater than 1). In the first case, there is no complete extension of Γ_{m} ⊢ Xy_{ij} as in 1). Let us assume that the proof fails if y_{ij} has an occurrence at deep t − 1, and show that the proof fails if y_{ij} is a subterm of g(t_{1}, ⋯, t_{l}) at depth 1. If y_{ij} is a subterm of g(t_{1}, ⋯, t_{l}) at depth t then y_{ij} is a subterm of t_{i} at depth t − 1 and by induction hypothesis the proof of Γ_{m} ⊢ Xt_{i} fails. The failure reasons are the same if the equation e_{p} has the form f(c_{1}(⋯), ⋯, c_{p}(⋯), z_{p+1}, ⋯, z_{n}) = g(t_{1}, ⋯, t_{l}) with y_{ij} variable independent of f in g(t_{1}, ⋯, t_{l}).