Program Extraction from Classical Proofs

Ulrich Berger and Helmut Schwichtenberg

Mathematisches Institut der Universität München, D–80333 München, Germany

Abstract. Different methods for extracting programs from a classical proofs are investigated. A direct method based on normalization and the wellknown negative translation combined with a realizability interpretation are compared and shown to yield equal results. Furthermore, the translation method is refined in order to obtain optimized programs. An analysis of the proof translation shows that in many cases only small parts of a classical proof need to be translated. Proofs extracted from such refined translations have simpler type and control structure. The effect of the refinements is demonstrated at two examples.

1 Introduction

It is well known that from a classical proof of ∀x∃ y B(x, y), B quantifier–free, one can extract a program t such that ∀x B(x, tx) holds. We discuss two possibilities to do this. 1. A direct method, which uses the classical proof and proof normalization directly as an algorithm. 2. A translation of the classical proof into an intuitionistic one from which via a realizability interpretation a program can be extracted. We show that both methods yield the same algorithm.

Furthermore we try to answer the question if “programs from classical proofs” is a useful device practically. We apply the proof translation to a simple but informative example: We prove classically that w.r.t. an unbounded function f: IN → IN such that f(0) = 0 each n has a root m, i.e., f(m) ≤ n < f(m + 1) holds. We translate the proof and extract a program root: IN → IN (depending on f) such that f(root(n)) ≤ n < f(root(n)+1) holds for all n. It’s interesting that the classical proof is extremely easy and short (even if fully formalized); considerably shorter than the intuitionistic proof one would give intuitively. However the extracted program is unnecessarily complicated. We take this as a motivation to study refinements of the proof translation yielding simpler programs.

Program extraction can be messy for mainly two reasons: 1. A completely formalized proof, using the basic axioms of arithmetic only, will in general be extremely long. This can be remidied by introducing additional global assumptions which are of such a form that they do not spoil the extraction. 2. When translating a classical derivation into an intuitionistic one, each atomic formula P is replaced by (P → A) → A, where A is the existential formula we want to prove. Thus existential formulas are spread all over the derivation and therefore each subderivation gets computational content. This means that the extracted program will be at least as long and complicated as the proof. Furthermore one has to pay for the additional assumptions introduced in 1., since their translations have to be proved. In general, these proofs use case splittings which later show up in the program.

In this paper we propose a refined proof translation which does not replace all atoms P by (P → A) → A. By a simple syntactical analysis of the assumptions used in the derivation one can determine a set of critical atoms which suffice to be replaced in order to make the translation work. Applying this refined translation to our root example simplifies the resulting program drastically. A second example, concerned with a search in binary trees, shows a similar effect.

It would be interesting to see if our refined method can be applied successfully to larger examples too. An candidate might be the classical proof of Higman’s Lemma [3], [6]. This proof has been translated and implemented in the Nuprl system by [5]. It is not known how the translated proof (which is extremely big) is related to the known constructive proofs of Higman’s Lemma [7], [1]. A refined translation might help answering this.

2 Preliminaries

Our basic logical calculus is the ∧→∀–fragment of minimal natural deduction for first order logic over simply typed lambda–terms. Classical and intuitionistic arithmetic and extensions thereof will be introduced via axioms.

Types are the ground types boole and nat, ρ × σ and ρ → σ.

Terms are the terms of Gödel’s system T, i.e. built from typed variables x^{ρ}, the constants true^{boole}, false^{boole}, 0^{nat}, S^{nat→nat}, R_{nat,ρ}^{ρ→(nat→ρ→ρ)→nat→ρ} (recursion), R_{boole,ρ}^{ρ→ρ→boole→ρ} (case analysis) by pairing ⟨r, s⟩^{ρ×σ}, projection π_{i}(r^{ρ_{0}×ρ_{1}})^{ρ_{i}}, abstraction (λx^{ρ}r^{σ})^{ρ→σ} and application (r^{ρ→σ}s^{ρ})^{σ}.

We have the usual conversions (writing t + 1 for St)

(λx r)s → r[s/x],
π_{i}⟨r_{0}, r_{1}⟩ → r_{i},
R_{nat,ρ}rs0 → r,
R_{nat,ρ}rs(t + 1) → st(R_{nat,ρ}rst),
R_{boole,ρ}rs true → r,
R_{boole,ρ}rs false → s.

It is well known that each term reduces to a unique normal form w.r.t. these conversions (cf. [10]). To simplify the calculus we will identify terms with the same normal form. We will write = for equality modulo normal forms and ≡ for syntactical identity.

Atomic formulas are ⊥ and P (t) where P is a predicate symbol and t is a list of terms. The types ρ_{i} of the terms t_{i} are specified by the arity (ρ) of P. We have at least one predicate symbol atom of arity (boole). The formula atom(t) will play the same role as usually t = 0 does. Frequently we will abreviate atom(t) by t. We assume that we have assigned to every predicate symbol P ≠ atom of arity (ρ) a closed term t_{P} of type ρ → boole defining the characteristic function of P. This means that we consider only decidable predicates.

Formulas are built from atomic formulas by conjunction A ∧ B, implication A → B and universal quantification ∀x^{ρ} A. Negation, disjunction and the existential quantifier are defined by

¬A :≡ A → ⊥,
A ∨ B :≡ ¬A ∧ ¬B → ⊥,
∃x A :≡ ¬∀x ¬A.

By ∀A we denote the universal closure of the formula A. A Π–formula is a formula of the form ∀x C, where C is quantifier–free.

Axioms are divided into two groups. Induction axioms:

Ind_{n,A}: ∀.A[0/n] → (∀n.A → A[n + 1/n]) → ∀n A,
Ind_{p,A}: ∀.A[true/p] → A[false/p] → ∀p A.

Π–axioms: All these axioms are closed Π-formulas.

T: atom(true),
¬F: ¬atom(false),

and for each predicate symbol P

Efq_{P}: ∀x.⊥ → P (x),
Stab_{P}: ∀x.¬¬P (x) → P (x),
Dec_{P,0}: ∀x.P (x) → atom(t_{P} x),
Dec_{P,1}: ∀x.atom(t_{P} x) → P (x).

Clearly there is a lot of redundance in these axioms. However, since the choice of the axioms in a particular proof influences the extracted program, it is important to have a rich axiom system.

Derivations d^{A} are built from assumptions u^{B} and axioms by the introduction and elimination rules for ∧, → and ∀:

(λu^{A} d^{B})^{A→B}, (d^{A→B}e^{A})^{B},
⟨d^{A}, e^{B}⟩^{A∧B}, π_{i}(d^{A_{0}∧A_{1}})^{A_{i}},
(λx^{ρ} d^{A})^{∀x^{ρ} A}, (d^{∀x^{ρ} A}t^{ρ})^{A[t/x^{ρ}]}

with the usual variable condition in the case of (λx d)^{∀x A}. We will write Γ ⊢ A if there is a derivation d^{A} with free assumptions among Γ. It’s easy to see that we can derive stability ¬¬A → A for all formulas A. Hence we have full classical arithmetic. Furthermore each quantifier–free formula A is decidable, i.e., there is a boolean term t_{A} such that ⊢ A ↔ atom(t_{A}). This can be used to do case splitting according to quantifier-free formulas A, i.e. for every formula B we can prove

Cases_{A,B}: (A → B) → (¬A → B) → B.

The derivation Cases_{A,B} is given by

λu_{1}, u_{2}.Ind x(λu_{3}λu_{4}.u_{3}T)(λu_{5}λu_{6}.u_{6}¬F)t_{A}(λu_{7}.u_{1}(d_{0}u_{7}))(λu_{8}.u_{2}(d_{1}u_{8}))

where d_{0}^{atom(t_{A})→A}, and d_{1}^{¬atom(t_{A})→¬A} are derivations which exist according to the decidability of A and the axioms and assumption variables with indices are (writing t for atom(t))

Ind_{p,(p→B)→(¬p→B)→B},

u_{1}^{A→B}, u_{2}^{¬A→B}, u_{3}^{true→B}, u_{4}^{¬true→B}, u_{5}^{false→B}, u_{6}^{¬false→B}, u_{7}^{t_{A}} and u_{8}^{¬t_{A}}. Conversion for derivations is defined similary as for terms in the usual way.

π_{i}(⟨d_{0}, d_{1}⟩) → d_{i},
(λu d)^{A→B}e → d[e/u],
(λx d)^{∀x A}t → d[t/x],
Ind_{n,A}rde0 → d,
Ind_{n,A}rde(t + 1) → et(Ind_{n,A}rdet)
Ind_{p,A}rde true → d,
Ind_{p,A}rde false → e.

Again it can be shown by standard methods — just as for Gödel’s T — that any derivation term in arithmetic has a unique normal form w.r.t. these conversions.

Intuitionistic arithmetic is obtained by extending the calculus above by a constructive or strong existential quantifier written ∃^{∗} (as opposed to ∃ defined by ¬∀¬). We add axioms corresponding to the usual introduction and elimination rules for ∃^{∗}.

∃_{x,A}^{∗+}: ∀∀x.A → ∃^{∗}x A,
∃_{x,A,B}^{∗−}: ∀.(∃^{∗}x^{ρ} A) → (∀x^{ρ}.A → B) → B.

Of course, in general, stability is underivable for formulas containing ∃^{∗}. Constructive disjunction ∨^{∗} can be defined by

A ∨^{∗} B :≡ ∃^{∗}p.(p = true → A) ∧ (p = false → B).

Program extraction from derivations with ∃^{∗} is done via a modified realizability interpretation due to Kreisel (cf. [4]). First we associate with each formula A (possibly containing ∃^{∗}) a list of types τ(A) as follows.

τ(R(t)) :≡ ε,

where ε denotes the empty list, and if τ(A) = ρ and τ(B) = σ_{1}, …, σ_{n} we let

τ(A → B) :≡ ρ → σ_{1}, …, ρ → σ_{n},
τ(A ∧ B) :≡ ρ, σ,
τ(∀x^{ρ} B) :≡ ρ → σ_{1}, …, ρ → σ_{n},
τ(∃^{∗}x^{ρ} B) :≡ ρ, σ.

Instead of ρ → σ_{1}, …, ρ → σ_{n} we will sometimes write ρ → σ. To give some examples, let n, m, k be of type nat. Then

τ(∀n∃^{∗}m R(n, m)) ≡ nat → nat,
τ(∀n∃^{∗}m∃^{∗}k R(n, m, k)) ≡ (nat → nat), (nat → nat),
τ(∀n∃^{∗}m R(n, m) → ∃^{∗}k Q(k)) ≡ (nat → nat) → nat.

For every formula A (possibly containing ∃^{∗}) and every list r of type τ(A) we define a formula r mr A without ∃^{∗}, to be read r modified realizes A.

ε mr R(t) :≡ R(t),
r_{1}, …, r_{n} mr (A → B) :≡ ∀x.x mr A → r_{1}x, …, r_{n}x mr B,
r, s mr (A ∧ B) :≡ r mr A ∧ s mr B,
r_{1}, …, r_{n} mr ∀x^{ρ} B :≡ ∀x^{ρ} r_{1}x, …, r_{n}x mr B,
r, s mr ∃^{∗}x^{ρ} B :≡ s mr B[r/x].

Note that if A does not contain ∃^{∗} then τ(A) ≡ ε and ε mr A ≡ A .

Definition. Assume that to any assumption variable u^{B} we have assigned a list x_{u}^{τ(B)} = x_{u_{1}}^{ρ_{1}}, …, x_{u_{n}}^{ρ_{n}} of distinct variables, where ρ_{1}, …, ρ_{n} = τ(B). Relative to this assignment we define for any derivation d^{A} its extracted terms ets(d^{A}), by induction on d^{A}. If τ(A) = σ_{1}, …, σ_{k}, then ets(d^{A}) will be a list r_{1}^{σ_{1}}, …, r_{k}^{σ_{k}}.

ets(Ind_{n,A}) :≡ λxR_{nat,τ(A)},
ets(Ind_{p,A}) :≡ λxR_{boole,τ(A)},
ets(Π–axiom) :≡ ε,
ets(u^{A}) :≡ x_{u}^{τ(A)},
ets(λu^{A} d^{B}) :≡ λx_{u}^{τ(A)} ets(d),
ets(d^{A→B}e^{A}) :≡ ets(d)ets(e),
ets(⟨d^{A}, e^{B}⟩) :≡ ets(d^{A}), ets(e^{B}),
ets(π_{0}(d^{A∧B})) :≡ the head of ets(d^{A∧B}) of same length as τ(A),
ets(π_{1}(d^{A∧B})) :≡ the tail of ets(d^{A∧B}) of same length as τ(B),
ets(λx^{ρ} d^{A}) :≡ λx^{ρ} ets(d),
ets(d^{∀x^{ρ} A}t^{ρ}) :≡ ets(d)t,
ets(∃_{x,A}^{∗+}) :≡ λxλxλy.x, y,
ets(∃_{x,A,B}^{∗−}) :≡ λxλxλyλz_{1} … λz_{n}.z_{1}xy, …, z_{n}xy.

To be precise, for the extracted terms of the induction axioms we need simultaneous recursion operators in case τ(A) has length > 1. These can be defined easily. Furthermore note that if ets(d) = r_{1}, …, r_{k} and ets(e) = s, then ets(d)ets(e) = r_{1}s, …, r_{k}s and λx ets(d) = λx r_{1}, …, λx r_{k}. In the last clause the (omitted) types are

x^{ρ}, (y)^{τ(A)} and z_{j}^{ρ→τ(A)→σ_{j}},

where τ(B) = σ_{1}, …, σ_{n}.

The following can be proved easily.

Lemma. FV(ets(d)) ⊆ FV(d) ∪ {x_{u}^{τ(A)} : u^{A} ∈ FA(d)}.

Lemma. We have ets(d[t/x]) = ets(d)[t/x] and ets(d[e/u]) = ets(d)[ets(e)/x_{u}], and if d and e have the same normal form then ets(d) and ets(e) have the same normal form too.

Soundness Theorem. Assume that to any assumption variable u^{A} we have assigned a list x_{u}^{τ(A)} and a new assumption variable ũ: x_{u}^{τ(A)} mr A. Relative to this assignment we can find for any derivation d: A with FA(d) = {u_{1}: A_{1}, …, u_{n}: A_{n}} a derivation

μ(d): ets(d) mr A

with FA(μ(d)) ⊆ {ũ_{1}: x_{1} mr A_{1}, …, ũ_{n}: x_{n} mr A_{n}}.

Proof. Induction on d.

As an example we compute the extracted terms of the derivation Cases_{A,B} for case splitting.

ets(Cases_{A,B}) = λy, z.ift_{A}yz

where if :≡ R(λy_{1}, z_{1}.y_{1})(λy_{1}, z_{1}.z_{1}) and y, z, y_{1}, z_{1} are lists of variables of types ρ :≡ τ(B). Clearly

if true rs = r, if false rs = s.

For better readability we use for ift_{A}rs the notation

if A then r else s fi.

3 Proof translation and the direct method

As is well known a proof of a ∀∃–theorem with a quantifier–free kernel — where ∃ is viewed as defined by ¬∀¬ — can be used as a program. We describe a “direct method” to use such a proof as a program (cf. [8]), and compare it with Gödel’s negative translation followed by Harvey Friedman’s A–translation (cf. [2]) and the program extraction described above.

3.1 The direct method

Assume we have a classical derivation d: ∀x∃y B[x, y], B quantifier–free, from closed Π–assumptions FA(d) = {v_{1}: ∀x_{1} C_{1}, …, v_{n}: ∀x_{n} C_{n}}. We describe an algorithm which, applied to closed terms r, returns terms s such that B[r, s] holds provided the assumptions v_{1}, …, v_{n} are true. The algorithm proceeds in three steps.

1. Instanciate d to r. We get dr: ∃y B[r, y], i.e.,

dr: (∀y.B[r, y] → ⊥) → ⊥.

2. Apply dr to a fresh assumption variable u: ∀y.B[r, y] → ⊥. We get

dru: ⊥.

3. Normalize dru: ⊥. From its normal form (dru)↓ read off the first instance

s :≡ |(dru)↓|.

Below we describe how the first instance |(dru)↓| is obtained.

Clearly we may assume that the Π–assumptions v_{i}: ∀x_{i} C_{i} do not contain ∧ and that the formula B[r, y] is of the form ⋀ ⋀_{i} B_{i}[y] where the B_{i} do not contain ∧. Therefore the fresh assumption u: ∀y.B[r, y] → ⊥ in step 2. may assumed to be u: ∀y.B_{1}[y] → … → B_{m}[y] → ⊥. Finally we may assume that d contains no free object variables. If it does, substitute arbitrary closed terms for them.

Let d: ⊥ (corresponding to (dru)↓: ⊥ above) be a normal derivation with FV(d) = ∅ of ⊥ from assumptions

u: ∀y.B_{1}[y] → … → B_{m}[y] → ⊥,
v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}

where ∀y.B_{1}[y] → … → B_{m}[y] → ⊥ is a false and ∀C_{1}, …, ∀C_{n} are true closed Π–formulas. We define a list |d| of closed terms, called the first instance of d, such that B_{1}[|d|], …, B_{m}[|d|] are true. |d| is defined by induction on d. Since d is normal and FV(d) = ∅ it does not contain axioms (exept the truth axiom, which is a closed Π–formulas and hence may be assumed to be among the Π– assumptions ∀C_{i}). To see this recall that the normal form of any closed term of type nat is of the form S(S(S … (S0) …)) and of any closed term of type boole is either true or false; hence all induction axioms unfold. Therefore d is of the form

wsd_{1} … d_{k},

where s are closed terms and d_{1}, …, d_{k} are derivations of closed quantifier–free formulas. We distinguish two cases.

1. d_{1}, …, d_{k} derive only true formulas (which can be decided, since the formulas are quantifier–free and closed). Then w cannot be one of the v_{i} since all ∀C_{i} are true. Hence d = usd_{1} … d_{k} and the d_{i} derive B_{i}[s]. So let |d| :≡ s.

2. There is a minimal i such that d_{i} derives a false formula, A_{1} → ⋯ → A_{n_{i}} → ⊥ say. Then A_{1} …, A_{n_{i}} are true. Without loss of generality we may assume that d_{i} = λw_{1}^{A_{1}} … λw_{n_{i}}^{A_{n_{i}}} e where e: ⊥ contains assumptions among

u: ∀y.B_{1}[y] → … → B_{m}[y] → ⊥,
v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n},
w_{1}: A_{1}, …, w_{n_{i}}: A_{n_{i}}.

Therefore we can recursively define |d| :≡ |e|.

3.2 Proof translation

Now we describe the more traditional way to obtain program from a classical proof of a formula ∃y B, B quantifier free, from (not necessarily closed) Π– assumptions. First, stability axioms are removed by applying Gödel’s negative translation. We obtain an intuitionistic proof of ∃x B. Since intuitionistically ¬∀x¬B is equivalent to ¬¬∃^{∗}x B we can use the fact that intuitionistic arithmetic is closed under Markov’s rule and obtain an intuitionistic proof of ∃^{∗}x B. For the latter step we use Friedman’s A–translation from [2].

In principle the negative translation is not necessary since we could prove stability for all atomic formulas by case splitting. However, these proofs would introduce characteristic functions t_{P} which might lead to inefficient programs.

The negative translation replaces each atomic formula P by (P → ⊥) → ⊥ and the A–translation in turn replaces P by P ∨^{∗}A, where A :≡ ∃^{∗}x B. So, at the end, P is replaced by ((P ∨^{∗} A) → A) → A which is intuitionistically equivalent to (P → A) → A. Hence we merge the two steps and define the A–translation B^{A} of a formula B to be obtained by replacing any atomic subformula P of B by (P → A) → A (including P = ⊥; this is, of course, not optimal but convenient for comparison with the direct method). A similar translation for first order logic is described in [9], 2.3., page 63, Theorem 3.16 (i).

Note that any derivation d of some formula B from assumptions C_{1}, …, C_{n} becomes after the A–translation a derivation of B^{A} from C_{1}^{A}, , …, C_{n}^{A}. To see this recall that our logical rules are those of minimal logic and hence give no extra treatment to falsity. Also the axiom schemes (exept the truth axiom, the falsity axiom and Efq_{atom}, which will be viewed as Π–assumptions) remain instances of the same axiom scheme after the A–translation. E.g. boolean induction

B[true/p] → B[false/p] → ∀p B

is translated into

B^{A}[true/p] → B^{A}[false/p] → ∀p B^{A},

which again is an instance of boolean induction.

Let us look at what happens with Π–assumptions under the A–translation. Again we may assume that all formulas considered do not contain ∧.

Lemma 1 For any quantifier–free formula C there is a derivation d: C → C^{A}.

Proof. Induction on C. Let C ≡ B_{1} → … → B_{m} → R with an atom R. We must derive

(B → R) → B^{A} → (R → A) → A.

So assume

ũ : B → R,
ṽ_{i} : B_{i}^{A},
w : R → A.

We must show A.

Case u_{i}^{−}: ¬B_{i} for some i. Let B_{i} ≡ Ci → P_{i} with atoms P_{i}. Then

ṽ_{i}: Ci^{A} → (P_{i} → A) → A

and we have

e_{ij}[u_{i}^{−}]: ≡ Stab_{C_{ij}}λv^{¬C_{ij}}.u_{i}^{−}λuCi.Efq_{P_{i}}(vu_{j}): C_{ij},
e_{i}[u_{i}^{−}]: ≡ λw_{i}^{P_{i}}.u_{i}^{−}λuCiw_{i}: ¬P_{i}.

By IH we have d_{C_{ij}}: C_{ij} → C_{ij}^{A}. Hence

ṽ_{i}(d_{C_{i1}}e_{i1}) … (d_{C_{in_{i}}} e_{in_{i}})(λw_{i}^{P_{i}}.Efq_{A}(e_{i}w_{i})): A.

Case u_{i}^{+}: B_{i} for all i. Then

w(ũu_{1}^{+} … u_{m}^{+}): A

The extracted terms for this derivation are

d^{ets} ≡ λx_{1}, …, x_{m}, z. if ¬B_{1} then x_{1}d_{C_{11}}^{ets} … d_{C_{1n_{1}}}^{ets} 0 else
…
if ¬B_{m} then x_{m}d_{C_{m1}}^{ets} … d_{C_{mnm}}^{ets} 0 else
z fi … fi,

where x_{i}, z are the lists of variables associated with ṽ_{i}: B_{i}^{A}, w.

Here we have used case splitting formulas B_{i}.

Up to now, the formula A could have been arbitrarily chosen. If we want to use the A–translation to extract the computational content from a classical proof we have to choose a particular A involving the strong existential quantifier.

Lemma 2 Let B_{i}[x, y] be quantifier–free formulas without ∧, and

A[x] :≡ ∃^{∗}y ⋀ ⋀_{i} B_{i}[x, y].

Then we can find a derivation of (∀y.B_{1}[x, y] → … → B_{m}[x, y] → ⊥)^{A[x]}.

Proof. Let y be given and assume ṽ_{i}: B_{i}^{A} and w: ⊥ → A. We must show A. Case u_{i}^{−}: ¬B_{i} for some i. Let B_{i} ≡ Ci → P_{i} with atoms P_{i}. Then

ṽ_{i}: Ci^{A} → (P_{i} → A) → A

and we have

e_{ij}[u_{i}^{−}]: ≡ Stab_{C_{ij}}λv^{¬C_{ij}}.u_{i}^{−}λuCi.Efq_{P_{i}}(vu_{j}): C_{ij},
e_{i}[u_{i}^{−}]: ≡ λw_{i}^{P_{i}}.u_{i}^{−}λuCiw_{i}: ¬P_{i}.

Using d_{C_{ij}}: C_{ij} → C_{ij}^{A} from Lemma 1 we obtain

ṽ_{i}(d_{C_{i1}}e_{i1}) … (d_{C_{in_{i}}} e_{in_{i}})(λw_{i}^{P_{i}}.Efq_{A}(e_{i}w_{i})): A.

Case u_{i}^{+}: B_{i} for all i. Then

∃^{+}y⟨u_{1}^{+}, …, u_{m}^{+}⟩: A

Note that the assumption w: ⊥ → A[x] has not been used. The extracted terms for this derivation are

d^{ets} ≡ λy, x_{1}, …, x_{m}, z. if ¬B_{1} then x_{1}d_{C_{11}}^{ets} … d_{C_{1n_{1}}}^{ets} 0 else
…

if ¬B_{m} then x_{m}d_{C_{m1}}^{ets} … d_{C_{mnm}}^{ets} 0 else

y fi … fi,

where x_{i}, z are the lists of variables associated with ṽ_{i}: B_{i}^{A}, w.

Theorem (Friedman). For any derivation

d[u: ∀y.B_{1}[x, y] → … → B_{m}[x, y] → ⊥, v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}]: ⊥

with B_{i}, C_{j} quantifier–free and without ∧ we can find a derivation

d^{tr}[v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}]: ∃^{∗}y ⋀ ⋀_{i} B_{i}[x, y].

Proof. Let A[x] :≡ ∃^{∗}y ⋀ ⋀_{i} B_{i}[x, y] and consider the A[x]–translation

d^{A[x]}[u′, v′_{1}]: (⊥ → A[x]) → A[x]

where

[u′: (∀y.B_{1}[x, y] → … → B_{m}[x, y] → ⊥)^{A[x]},
v′_{1}: (∀C_{1})^{A[x]}, … v′_{n}: (∀C_{n})^{A[x]}]

of d, obtained by just changing some formulas. By Lemma 1 we have

d_{v_{i}}[v_{i}: ∀C_{i}]: (∀C_{i})^{A[x]}.

By Lemma 2 (now using the particular choice of A[x]) the A[x]–translation of the assumption u is provable without assumptions:

d_{u}: (∀y.B_{1}[x, y] → … → B_{m}[x, y] → ⊥)^{A[x]}

Substituting d_{v_{i}}[v_{i}: ∀C_{i}] for v′_{i} and d_{u} for u′ we obtain

d^{tr}[v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}]: ∃^{∗}y ⋀ ⋀_{i} B_{i}[x, y],

where

d^{tr} ≡ d^{A[x]}[d_{u}, d_{v_{1}}, …, d_{v_{n}}]Efq_{A[x]}.

Having obtained a proof d^{tr} of an existential formula ∃^{∗}y ⋀ ⋀_{i} B_{i}[x, y] we can then apply the general method of extracting terms to this proof. It yields

(d^{tr})^{ets} ≡ (d^{A[x]})^{ets}[d_{u}^{ets}, d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0,  (1)

3.3 Comparison

We now prove that the value of the extracted terms when instanciated with a list r of closed terms is in fact the same as the result of the direct method.

So consider again the situation of Friedman’s Theorem, i.e. a derivation

d[u: ∀y.B_{1}[x, y] → … → B_{m}[x, y] → ⊥, v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}]: ⊥

with B_{i}, C_{j} quantifier–free and without ∧. We just observed that the program (d^{tr})^{ets} extracted from the translated derivation has the form (1) above. Let us try to understand how this program works. First, (d^{A[x]})^{ets} closely follows the structure of d. The reason is that d^{A[x]} differs from d only with respect to the formulas affixed, and when forming the extracted terms this affects only the types and the arities of the lists of object variables associated with assumption variables.

In order to comprehend d_{v_{i}}^{ets} and d_{u}^{ets} let us have a second look at the proofs of Lemma 1 and 2. First note that d_{v_{i}}[v_{i}: ∀C_{i}]: (∀C_{i})^{A[x]} is obtained from d_{i}: C_{i} → C_{i}^{A[x]} constructed in the proof of Lemma 1 by

d_{v_{i}} ≡ λy_{i}.d_{i}(v_{i}y_{i}).

Since v_{i} has type ∀C_{i}, which is a Harrop formula, we have d_{v_{i}}^{ets} ≡ λy_{i} d_{i}^{ets}. Now from the proof of Lemma 1 we obtain

d_{i}^{ets} ≡ λx_{1}, …, x_{m}, z. if ¬B_{1} then x_{1}d_{C_{11}}^{ets} … d_{C_{1n_{1}}}^{ets} 0 else
…
if ¬B_{m} then x_{m}d_{C_{m1}}^{ets} … d_{C_{mnm}}^{ets} 0 else
z fi … fi, (2)

where C_{i} ≡ B_{1} → … → B_{m} → R with B_{i} ≡ C_{i} → P_{i} and x_{i}, z are the lists of variables associated with ṽ_{i}, w. Furthermore, d_{C_{ij}}^{ets} are the extracted terms of derivations d_{C_{ij}}: C_{ij} → C_{ij}^{A[x]} constructed by previous applications of Lemma 1. Similarly

d_{u}^{ets} ≡ λy, x_{1}, …, x_{m}, z. if ¬B_{1} then x_{1}d_{C_{11}}^{ets} … d_{C_{1n_{1}}}^{ets} 0 else
…
if ¬B_{m} then x_{m}d_{C_{m1}}^{ets} … d_{C_{mnm}}^{ets} 0 else
y fi … fi, (3)

where B_{i} ≡ C_{i} → P_{i} and x_{i}, z are the lists of variables associated with ṽ_{i}, w. Furthermore, d_{C_{ij}}^{ets} are the extracted terms of derivations d_{C_{ij}}: C_{ij} → C_{ij}^{A[x]} constructed by previous applications of Lemma 1.

This analysis makes it possible to prove that the value of the extracted terms when instanciated with a list r of closed terms is in fact the same as the result of the direct method to read off the first instance provided by the instanciated derivation

d̄[ū: ∀y.B_{1}[r, y] → … → B_{m}[r, y] → ⊥, v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}]: ⊥

Below we will show the following

Claim. For any normal derivation

e[ū: ∀y.B_{1}[r, y] → … → B_{m}[r, y] → ⊥, v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n}]: ⊥

with FV(e) = ∅ we have

|e| = [[(e^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0]].

We then obtain that the instanciation of the extracted terms (1) with r for x, i.e.

(d^{A[x]})^{ets}[d_{u}^{ets}, d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0[r/x] ≡ (d[r/x]^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0

has as its value the list of closed terms which is the first instance of the instanciated derivation d[r/x], i.e. |d[r/x]↓|. For by the claim we have

|d[r/x]↓| = [[((d[r/x]↓)^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0]]
= [[((d[r/x]^{A[r]})^{ets})↓[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0]]
= [[(d[r/x]^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0]],

since normalization commutes with A[r]–translation and the formation of extracted terms.

It remains to prove the claim. We use induction on e. Since e is normal, it must be of the form e = wse_{1} … e_{k} with w ∈ {ū, v_{1}, …, v_{n}}.

Case 1. e_{1}, …, e_{k} derive only true formulas. Then w = ū, k = m and the e_{i} derive B_{i}[r, s]. By definition |e| :≡ s. Furthermore

(e^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0
= d_{u}^{ets}[r/x]s(e_{1}^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …] … (e_{m}^{A[r]})^{ets}[d_{u}^{ets}[r/x], d_{v_{1}}^{ets}, …]0
= s

by the form (3) of d_{u}^{ets}, since all B_{i}[r, s] = (Bi → P_{i})[r, s] are true.

Case 2. There is a minimal i such that e_{i} derives a false formula, D_{i1}[s] → ⋯ → D_{in_{i}}[s] → ⊥ say. Then D_{i1}[s], …, D_{in_{i}}[s] are true. Without loss of generality we may assume that e_{i} = λw_{1}^{D_{i1}[s]} … λw_{m}^{D_{in_{i}} [s]} f where f: ⊥ contains assumptions among

ū: ∀y.B_{1}[r, y] → … → B_{m}[r, y] → ⊥,
v_{1}: ∀C_{1}, …, v_{n}: ∀C_{n},
w_{1}: D_{i1}, …, w_{m}: D_{in_{i}}.

Therefore by definition |e| ≡ |f|. Furthermore, using the notation d_{w_{j}}[w_{j}]: D_{ij}^{A[r]} for the derivation obtained by applying Lemma 1 to D_{ij}, we have

(e^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]0
= \{ \begin{matrix}d_{u}^{ets}[r]s (e_{1}^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …] … (e_{k}^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …]0 & if w = ū \\ d_{v_{i}}^{ets}s (e_{1}^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …] … (e_{k}^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …]0 & if w = v_{i} \end{matrix}
= (e_{i}^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}]d_{w_{1}}^{ets} … d_{w_{n_{i}}}^{ets} 0 by (3) and (2), respectively
= (f^{A[r]})^{ets}[d_{u}^{ets}[r], d_{v_{1}}^{ets}, …, d_{v_{n}}^{ets}, d_{w_{1}}^{ets}, …, d_{w_{n_{i}}}^{ets} ]0,

so the claim follows from the IH.

4 Refinements

In applications it will be important to produce extracted terms with as few as possible case distinctions, and also that the case distinctions should be over as simple as possible boolean terms. The following example will show that such improvements are indeed necessary.

4.1 The root example

Let f: nat → nat be an unbounded function with f(0) = 0. Then we can prove

∀n∃m.f(m) ≤ n < f(m + 1).

If e.g. f(m) = m^{2}, then this formula expresses the existence of an integer square root m := [\sqrt{n}] for any n. More formally we can prove

∀n∃m.¬n < f(m) ∧ n < f(m + 1)  (1)

from the assumptions

v_{1}: ∀n ¬n < f(0), v_{2}: ∀n n < f(g(n)).

Here <^{nat→nat→boole} is the characteristic function of the natural ordering of the natural numbers and r < s denotes atom(<rs). We expressed f(m) ≤ n by ¬n < f(m) and f(0) = 0 by ∀n ¬n < f(0) to keep the formal proof as simple as possible. In order to have Π–assumptions we had to express the unboundedness of f by a witnessing function g.

Now let us prove (1). Let n be given and assume

u: ∀m.¬n < f(m) → n < f(m + 1) → ⊥.

We have to show ⊥. From v_{1} and u we inductively get ∀m ¬n < f(m). For m := g(n) this yields a contradiction to v_{2}.

The derivation term corresponding to this proof is

d :≡ Ind_{m,¬n<f(m)}n(v_{1}n)u(g(n))(v_{2}n): ⊥.

Now let

A :≡ ∃^{∗}m.¬n < f(m) ∧ n < f(m + 1).

The program extracted from d is

(d^{tr})^{ets} ≡ (d^{A})^{ets}[d_{u}^{ets}, d_{v_{1}}^{ets}, d_{v_{2}}^{ets}]0: nat.

(d^{A})^{ets} is the same as d exept that Ind_{m,¬n<f(m)} has to be replaced by

λn R_{nat,(nat→nat)→nat→nat}

(since τ((¬n < f(m))^{A}) = τ(((n < f(m) → A) → A) → (⊥ → A) → A) = (nat → nat) → nat → nat), and the assumption variables u, v_{1}, v_{2} in d have to be replaced by (unary lists of) object variables

x_{u}: nat → [(nat → nat) → nat → nat] → (nat → nat) → nat → nat,
x_{v_{1}}: nat → (nat → nat) → nat → nat,
x_{v_{2}}: nat → nat → nat.

The subprograms d_{u}^{ets}, d_{v_{1}}^{ets}, d_{v_{2}}^{ets} (of the same types as x_{u}, x_{v_{1}}, x_{v_{2}}) are given by

d_{u}^{ets} ≡ λm, x_{1}, x_{2}, k. if n < f(m) then x_{1}id0 else
if ¬n < f(m + 1) then x_{2}0 else
m fifi,
d_{v_{1}}^{ets} ≡ λn, x_{1}, k. if ¬n < f(0) then x_{1}0 else
k fi,
d_{v_{2}}^{ets} ≡ λn, k k.

Hence the normal form of (d^{tr})^{ets} is

R (λx_{1}, k.if ¬n < f(0) then x_{1}0 else k fi)

(λm, w_{1}, w_{2}, k.

if n < f(m) then w_{1}id0 else
if ¬n < f(m + 1) then w_{2}0 else
m fifi)

(g(n)) (λk k) 0

Informally, (d^{tr})^{ets} = H(g(n), λk k, 0) where H: nat → (nat → nat) → nat → nat is such that

H(0, x_{1}, k) = if ¬n < f(0) then x_{1}0 else k fi
H(m + 1, x_{1}, k) = if n < f(m) then H(m, id, 0) else
if ¬n < f(m + 1) then x_{1}0 else
m fifi

This program is correct, but it is unnecessarily complicated. We will now describe a refined A–translation which will simplify the type of the auxiliary function H as well as its if–then–else structure. The type reduction will be achieved by not replacing all atoms P by (P → A) → A.

4.2 The refined translation

Let L be a set of formulas. In our applications L will consist of the quantifier–free kernels of the lemmata ∀C_{i}, and in addition of the formula B_{1}[x, y] → … → B_{m}[x, y] → ⊥, if our goal formula is ∀x∃y ⋀ ⋀_{i} B_{i}[x, y].

The set of L–critical relation symbols is the smallest set satisfying the following condition.

If (C_{1} → P_{1}) → … → (C_{m} → P_{m}) → R(t) is a positive subformula of an L–formula, and if for some i P_{i} ≡ ⊥ or P_{i} ≡ Q(s) for some L–critical relation symbol Q, then R is L–critical.

We now define an A–translation relative to L:

R(t)^{A} :≡ \{ \begin{matrix}(R(t) → A) → A, & if R is L–critical \\ R(t), & otherwise \end{matrix}
⊥^{A} :≡ A
(B → C)^{A} :≡ B^{A} → C^{A}.

We will write P ∈ C_{L} if the atom P is of the form R(t) for some L–critical R or P ≡ ⊥.

A quantifier–free formula B_{1} → … → B_{m} → R will be called L–relevant if R ∈ C_{L}.

Lemma 1^{∗} For any B ∈ Neg(L) and any C ∈ Pos(L) we can find the following derivations.

(i) d_{C}: C → C^{A}. Let C ≡ B → R. Then in case R ∈ C_{L} we need g_{B_{i}} for B_{i} L–relevant and f_{B_{j}} for B_{j} L–irrelevant, and in case R ∉ C_{L} we need fB.

(ii) e_{C,D}: ((C → D) → A) → C^{A} for C L–relevant. Let C ≡ B → R. Then we need Cases_{R} if R ≢ ⊥, and also g_{B_{i}} or f_{B_{i}} depending on whether B_{i} is L–relevant or not.

(iii) f_{B}: B^{A} → B for B L–irrelevant. Let B ≡ C → R. Then we need dC. (iv) g_{B}: B^{A} → (B → A) → A for B L–relevant. Let B ≡ C → R. Then we need

some e_{C_{i},D} for C_{i} L–relevant, and Cases_{C_{j}} and also d_{C_{j}} for C_{j} L–irrelevant.

Proof. Simultaneously by induction on the subformulas of L–formulas. In each case we will also calculate the axtracted terms, i.e., we define by simultaneous structural recursion the terms d_{C}^{ets}, e_{C,D}^{ets}, f_{B}^{ets} and g_{B}^{ets}.

(i) Let C ≡ B → R. Case R ∈ C_{L}, R ≢ ⊥. We must derive

(B → R) → B^{A} → (R → A) → A.

So assume u: B → R, v_{i}: B_{i}^{A} and w: R → A. We must show A.

Let B_{i} for i ∈ {1, …, k} be relevant and B_{j} for j ∈ {k + 1, …, m} be irrelevant. Assume u_{i}: B_{i} and note that f_{j}v_{j}: B_{j}. Then from u: B_{1} → … → B_{k} → B_{k+1} → … → B_{m} → R and w: R → A we get A. Now cancel u_{k}: B_{k}, yielding B_{k} → A. Using the IH g_{B_{k}}: B_{k}^{A} → (B_{k} → A) → A and the assumption B_{k}^{A} we get A. Repeating this procedure we finally cancel u_{1}: B_{1}, yielding B_{1} → A. Using the IH g_{B_{1}}: B_{1}^{A} → (B_{1} → A) → A and the assumption B_{1}^{A} we get A, as required. The derivation term is

d_{C} ≡ λu, v_{1}, …, v_{m}, w.
g_{B_{1}}v_{1}λu_{1}^{B_{1}}. · · · g_{B_{k}}v_{k}λu_{k}^{B_{k}}.w (uu_{1} … u_{k}(f_{B_{k+1}}v_{k+1}) … (f_{B_{m}}v_{m}))

and we get

d_{C}^{ets} ≡ λx_{1}, …, x_{k}, z. g_{B_{1}}^{ets}x_{1}(g_{B_{2}}^{ets}x_{2} … (g_{B_{k}}^{ets}x_{k}z) …)

where x_{i}, z are the lists of variables associated with v_{i}, w.

Case R ≡ ⊥. Similarly, using Efq_{A} instead of w: R → A. Then in d_{C}^{ets} we leave out λz.

Case R ∉ C_{L}. Then all B_{i} are irrelevant. We must derive

(B → R) → B^{A} → R.

So assume u: B → R and B^{A}. Using the IH f_{B_{i}}: B_{i}^{A} → B_{i} we obtain B and hence R. In this case d_{C}^{ets} ≡ ε.

(ii) Case R with R ∈ C_{L}, R ≢ ⊥. Then R^{A} ≡ (R → A) → A, and we must derive

((R → D) → A) → (R → A) → A.

So assume u: (R → D) → A and v: R → A. Then clearly A can be derived, using Cases_{R} and Efq_{D}. The derivation term is

e_{R,D} ≡ λu, v.Cases_{R}vλu_{1}^{¬R}.uλu_{2}^{R}.Efq_{D}(uu_{1})

and we get

e_{R,D}^{ets} ≡ λx, y. if R then y else x fi.

Case R with R ≡ ⊥. Then R^{A} ≡ A, and we must derive

((⊥ → D) → A) → A.

But this clearly can be done using Efq_{D}, and we have e_{⊥,D}^{ets} ≡ λx x. Case B → C. We must derive

[((B → C) → D) → A] → B^{A} → C^{A}

So assume u: ((B → C) → D) → A and v: B^{A}. We must show C^{A}. First note that we can derive (C → D) → A from our assumptions, using the fact that by IH we can derive B^{A} → (B → A) → A (with g_{B} or f_{B}, depending on whether B is relevant or not). But then the claim follows, since by IH

e_{C,D}: ((C → D) → A) → C^{A}.

(iii) Let B ≡ C → R. Since B is irrelevant we have R ∉ C_{L}. Then (C → R)^{A} ≡ C^{A} → R. We must derive

(C^{A} → R) → C → R.

But this is easy, using the IH d_{C_{i}}: C_{i} → C_{i}^{A}. Clearly f_{B}^{ets} ≡ ε.

(iv) Case R with R ∈ C_{L}, R ≢ ⊥. Then R^{A} ≡ (R → A) → A, and we must derive

((R → A) → A) → (R → A) → A,

which is trivial. We have g_{R}^{ets} ≡ λx x.

Case R with R ≡ ⊥. Then R^{A} ≡ A, and we must derive

A → (⊥ → A) → A,

which again is trivial. We have g_{⊥}^{ets} ≡ λx, y . x.

Case C → B. By assumption B is relevant. We must derive

(C^{A} → B^{A}) → ((C → B) → A) → A.

So assume u: C^{A} → B^{A} and v: (C → B) → A.

We first consider the case where C is relevant. Then we have e_{C,B}: ((C → B) → A) → C^{A} by IH(ii), hence B^{A} (using v and u). By IH(iv) for the shorter formula B we know g_{B}: B^{A} → (B → A) → A and hence (B → A) → A. But B → A can easily be derived from our hypothesis v: (C → B) → A and hence we obtain A, as required. The derivation term is

g_{C→B} ≡ λu, v.g_{B}(u(e_{C,B}v))λu_{1}^{B}.vλu_{2}^{C}u_{1}

and we get

g_{C→B}^{ets} ≡ λx, y.g_{B}^{ets}(x(e_{C,B}^{ets}y))y.

We finally consider the case where C is irrelevant. The derivation now uses Cases_{C}; so it suffices to first derive (1) under the additional hypothesis C, and then derive (1) under the additional hypothesis ¬C.

So assume u^{+}: C. Since by IH(i) d_{C}: C → C^{A} we obtain C^{A} and hence B^{A} (using u: C^{A} → B^{A}). By IH(iv) for the shorter formula B we know g_{B}: B^{A} → (B → A) → A and hence (B → A) → A. But B → A can easily be derived from our hypothesis v: (C → B) → A and hence we obtain A, as required.

Now assume u^{−}: ¬C. Then by ex–falso–quodlibet we obtain C → B and hence A, using our hypothesis v: (C → B) → A.

The derivation term is

g_{C→B} ≡ λu, v.Cases_{C}(λu^{+}.g_{B}(u(d_{C}u^{+}))λu_{1}^{B}.vλu_{2}^{C}u_{1})(λu^{−}.vλu_{3}^{C}.Efq_{B}(u^{−}u_{3}))

and we get

g_{C→B}^{ets} ≡ λx, y. if C then g_{B}^{ets}(xd_{C}^{ets})y else y fi.

Lemma 2^{∗} Let B_{i} be quantifier–free formulas and A :≡ ∃^{∗}y ⋀ ⋀_{i} B_{i}. Then we can find a derivation of

∀y.B_{1}^{A} → … → B_{m}^{A} → A

involving Cases_{B_{i}} and d_{C_{ij}}: C_{ij} → C_{ij}^{A} for relevant B_{i} ≡ C_{i} → P_{i} and f_{B_{j}}: B_{j}^{A} → B_{j} for irrelevant B_{j}.

Proof. Let y be given and assume v_{1}: B_{1}^{A}, …, v_{m}: B_{m}^{A}. We must show A. We may assume that B_{i} for i ∈ {1, …, k} be relevant and B_{j} for j ∈ {k + 1, …, m} be irrelevant

Case u_{i}^{−}: ¬B_{i} for some i ∈ {1, …, k}. Let B_{i} ≡ Ci → P_{i} with atoms P_{i}. Then

v_{i}: Ci^{A} → (P_{i} → A) → A

in case P_{i} ≢ ⊥ and

v_{i}: Ci^{A} → A

in case P_{i} ≡ ⊥. We have

e_{ij}[u_{i}^{−}]: ≡ Stab_{C_{ij}}λv^{¬C_{ij}}.u_{i}^{−}λuCi.Efq_{P_{i}}(vu_{j}): C_{ij},
e_{i}[u_{i}^{−}]: ≡ λw_{i}^{P_{i}}.u_{i}^{−}λuCiw_{i}: ¬P_{i}.

Using d_{C_{ij}}: C_{ij} → C_{ij}^{A} from Lemma 1^{∗} we obtain in case P_{i} ≢ ⊥

v_{i}(d_{C_{i1}}e_{i1}) … (d_{C_{in_{i}}} e_{in_{i}})(λw_{i}^{P_{i}}.Efq_{A}(e_{i}w_{i})): A

and in case P_{i} ≡ ⊥

v_{i}(d_{C_{i1}}e_{i1}) … (d_{C_{in_{i}}} e_{in_{i}}): A.

Case u_{i}^{+}: B_{i} for all i ∈ {1, …, k}. Then

∃^{+}y⟨u_{1}^{+}, …, u_{k}^{+}, f_{B_{k+1}}v_{k+1}, …, f_{B_{m}}v_{m}⟩: A

The extracted terms for this derivation are

d^{ets} ≡ λy, x_{1}, …, x_{m}. if ¬B_{1} then x_{1}d_{C_{11}}^{ets} … d_{C_{1n_{1}}}^{ets} 0 else
…
if ¬B_{k} then x_{k}d_{C_{k1}}^{ets} … d_{C_{kn_{k}}}^{ets} 0 else
y fi … fi,

where x_{i} is the list of variables associated with v_{i}: B_{i}^{A}.

This A–translation relative to L simplifies the extracted terms a lot. First the derivations of C → C^{A} are necessary only for those lemmata ∀C where C involves L–critical relation symbols (for otherwise we have C^{A} ≡ C). For the other lemmata a derivation of C → C^{A} provided by Lemma 1^{∗} involves in most cases only very few case distinctions. Finally, in the derivation given by Lemma 2^{∗} of the A–translation of our false assumption ⋀ ⋀_{i} B_{i}^{A} → A direct case distinctions are only necessary for the relevant B_{i}; for the other B_{j} we have a derivation of B_{j}^{A} → B_{i} by Lemma 1^{∗}.

4.3 Examples refined

Let us now come back to our initial example and study the effect of our refinements there. We can relativize the A–translation to the set L of formulas consisting of

n < f(0) → ⊥,
n < f(g(n)),
(n < f(m) → ⊥) → n < f(m + 1) → ⊥.

Since no positive subformula of an L–formula is an implication with a <–atom as its conclusion there are no L–critical relation symbols. Hence only negations B → ⊥ are L–relevant.

We now repeat our treatment of the root example, based on the A–translation relative to L and the refined Lemmas 1^{∗} and 2^{∗}. The derivation term corresponding to the informal proof is

d :≡ Ind_{m,¬n<f(m)}n(v_{1}n)u(g(n))(v_{2}n): ⊥.

Now let

A :≡ ∃^{∗}m.¬n < f(m) ∧ n < f(m + 1).

The program extracted from d is

(d^{tr})^{ets} ≡ (d^{A})^{ets}[d_{u}^{ets}, d_{v_{1}}^{ets}, d_{v_{2}}^{ets}]: nat.

(d^{A})^{ets} is the same as d exept that Ind_{m,¬n<f(m)} has to be replaced by

λn R_{nat,nat}

(since τ((n < f(m) → ⊥)^{A}) = τ(n < f(m) → A) = nat), and the assumption variables u, v_{1} in d have to be replaced by (unary lists of) object variables

x_{u}: nat → nat → nat,
x_{v_{1}}: nat → nat,

whereas v_{2} has to be replaced by the empty list. The subprograms d_{u}^{ets}, d_{v_{1}}^{ets} (of the same types as x_{u}, x_{v_{1}}) are given by (cf. Lemmata 2^{∗} and 1^{∗})

d_{u}^{ets} ≡ λm, x. if n < f(m) then x else m fi,
d_{v_{1}}^{ets} ≡ λn 0.

Hence the normal form of (d^{tr})^{ets} is

R0(λm, x. if n < f(m) then x else m fi)(g(n)).

Informally, (d^{tr})^{ets} = h(g(n)) where h: nat → nat is such that

h(0) = 0,
h(m + 1) = if n < f(m) then h(m) else m fi.

We conclude with a further example which is still simple but exploits the general results of section 4.2 more seriously.

Let p be a decidable property of finite binary trees. We consider the problem of computing from a tree x_{0} with px_{0} another tree y_{0} with py_{0} but minimal, i.e., for no proper subtree of y_{0} property p holds. Let p̃x mean that p holds for no proper subtree of x. p̃ can be defined inductively by

v_{1}: p̃ε, v_{2}: ∀x, y.¬px → ¬py → p̃x → p̃y → p̃⟨x, y⟩

where ε denotes the empty tree and ⟨x, y⟩ denotes the tree with immediate subtrees x and y. We assume further

v_{3}: px_{0}

and try to prove ∃y.p̃y ∧ py, i.e., under the additional assumption

u: ∀y.p̃y → py → ⊥

we have to prove ⊥. Of course, in the proof we may use induction on trees, i.e., for any formula B(x) the axiom

Ind_{B(x)}: B(ε) → (∀x, y . B(x) → B(y) → B(⟨x, y⟩)) → ∀x B(x).

Informally, from u and v_{2} we get ∀x, y . p̃x → p̃y → p̃⟨x, y⟩ and hence, by induction, using v_{1}, ∀x p̃x. This clearly contradicts u and v_{3}.

¿From the proof term

d = ux_{0}(Indp̃v_{1}(λx, y, w_{1}^{p̃x}w_{2}^{p̃y}. v_{2}xy(uxw_{1})(uyw_{2})w_{1}w_{2})x_{0})v_{3}

we obtain the program

(d^{tr})^{ets} = d_{u}^{ets}x_{0}(Rd_{v_{1}}^{ets}(λx, y, w_{1}w_{2}. d_{v_{2}}^{ets}xy(d_{u}^{ets}xw_{1})(d_{u}^{ets}yw_{2})w_{1}w_{2})x_{0})d_{v_{3}}^{ets} where d_{u}^{ets} and the d_{v_{i}}^{ets} still have to be calculated. Looking at our assumptions u and v_{i} it is clear that only p̃ is relevant. Hence, using the recipe given in the proof of Lemma 2^{∗}, we obtain

d_{u}^{ets} = λx, w . wx and d_{v_{1}}^{ets} = d_{v_{3}}^{ets} = id.

The calculation of d_{v_{2}}^{ets} is a little bit more involved. We have

d_{v_{2}}^{ets} = λz_{1}, z_{2}, w_{1}, z.g_{¬px}^{ets}z_{1}(g_{¬py}^{ets}z_{2}(g_{p̃x}^{ets}w_{1}(g_{p̃y}^{ets}w_{2}z)))

and

g_{¬px}^{ets} = λz_{1}, z_{2} . if px then z_{1} else z_{2} fi
g_{¬py}^{ets} = λz_{1}, z_{2} . if py then z_{1} else z_{2} fi
g_{p̃x}^{ets} = g_{p̃y}^{ets} = id.

Hence

d_{v_{2}}^{ets} = λz_{1}, z_{2}, w_{1}, w_{2}, z .
if px then z_{1} else if py then z_{2} else w_{1}(w_{2}z) fifi.

Therefore we get

(d^{tr})^{ets} = R id
(λx, y, w_{1}w_{2}, z.
if px then w_{1}x else
if py then w_{2}y else w_{1}(w_{2}z) fifi)
x_{0}
x_{0}.

This means (d^{tr})^{ets}(x_{0}) = g(x_{0}, x_{0}) where

g(ε, z) = z,
g(⟨x, y⟩, z) = if px then g(x, x) else
if py then g(y, y) else g(x, g(y, z)) fifi.

References

1. Coquand, T.: A proof of Higman’s lemma by structural induction. Manuscript (1993)

2. Friedman, H.: Classically and intuitionistically provably recursive functions. In: Higher Set Theory, SLNCS 699 (1978) 21–28

3. Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2 (1952) 236–366

4. Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Constructivity in Mathematics, North–Holland, (1959) 101–128

5. Murthy, C.: Extracting Constructive Content from Classical Proofs. PhD thesis. Technical Report, Nr. 90–1151, Dep. of Comp. Science, Cornell Univ, Ithaca, New York (1990)

6. Nash-Williams, C.: On well–quasi–ordering finite trees. Proc. Cambridge Phil. Soc. 59 (1963) 833–835

7. Schütte, K., Simpson, S.G: Ein in der reinen Zahlentheorie unbeweisbarer Satz über endliche Folgen natürlicher Zahlen. Arch. Math. Logik 25 (1985) 75–89

8. Schwichtenberg, H.: Proofs as programs. In: Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, Cambridge University Press (1992) 81–113

9. Troelstra, A. S., van Dalen, D.: Constructivism in Mathematics Vol. 1. An Introduction. In: Studies in Logic and the Foundations of Mathematics, North–Holland 121 (1988)

10. Troelstra, A. S.: Metamathematical Investigations of Intuitionistic Arithmetic and Analysis. SLNM 344 (1973)

This article was processed using the LaTEX macro package with LLNCS style