The greatest common divisor: a case study for program extraction from classical proofs

U. Berger  H. Schwichtenberg

September 25, 2000

Yiannis Moschovakis suggested the following example of a classical existence proof with a quantifier–free kernel which does not obviously contain an algorithm: the gcd of two natural numbers a_{1} and a_{2} is a linear combination of the two. Here we treat that example as a case study for program extraction from classical proofs. We apply H. Friedman’s A– translation [3] followed by a modified realizability interpretation to extract a program from this proof. However, to obtain a reasonable program it is essential to use a refinement of the A–translation introduced in Berger/Schwichtenberg [2, 1]. This refinement makes it possible that not all atoms in the proof are A–translated, but only those with a “critical” relation symbol. In our example only the divisibility relation ·|· will be critical.

Let a, b, c, i, j, k, ℓ, m, n, q, r denote natural numbers. Our language is determined by the constants 0, 1, +, ∗, function symbols for the quotient and the remainder denoted by q(a, c) and r(a, c), a 4–ary function denoted by abs(k_{1}a_{1}−k_{2}a_{2}) whose intended meaning is clear from the notation and an auxiliary 5–ary function f which will be defined later. We will express the intended meaning of these function symbols by stating some properties (lemmata) v_{1}, …, v_{6} of them; these will be formulated as we need them.

Theorem.

∀a_{1}, a_{2}(0 < a_{2} → ∃k_{1}, k_{2}(abs(k_{1}a_{1} − k_{2}a_{2})|a_{1} ∧ abs(k_{1}a_{1} − k_{2}a_{2})|a_{2} ∧ 0 < abs(k_{1}a_{1} − k_{2}a_{2}))).

Proof. Let a_{1}, a_{2} be given and assume 0 < a_{2}. The ideal (a_{1}, a_{2}) generated from a_{1}, a_{2} has a least positive element c, since 0 < a_{2}. This element has a representation c = abs(k_{1}a_{1} −k_{2}a_{2}) with k_{1}, k_{2} ∈ N. It is a common divisor of a_{1} and a_{2} since otherwise the remainder r(a_{i}, c) would be a smaller positive element of the ideal.

The number c ∈ (a_{1}, a_{2}) dividing a_{1} and a_{2} is the greatest common divisor since any common divisor of a_{1} and a_{2} must also be a divisor of c.

The least element principle and <-induction.

In order to formally write out the proof above we need to make explicit the instance of the induction scheme used implicitly in the least element principle. The least element principle w.r.t. a measure μ says

∃k⃗ M(k⃗) → ∃k⃗ (M(k⃗) ∧ ∀ℓ⃗[μ(ℓ⃗) < μ(k⃗) → M(ℓ⃗) → ⊥])

(in our example M(k_{1}, k_{2}) ≡ 0 < abs(k_{1}a_{1} −k_{2}a_{2}) and μ(k_{1}, k_{2}) ≡ abs(k_{1}a_{1} −k_{2}a_{2})). In order to reduce this to the induction scheme we use the fact that the formula above is classically equivalent to

∀k⃗ (M(k⃗) → ∀ℓ⃗[μ(ℓ⃗) < μ(k⃗) → M(ℓ⃗) → ⊥] → ⊥) → ∀k⃗(M(k⃗) → ⊥)

which nothing but the principle of <–induction for the complement of M, N(k⃗) := M(k⃗) → ⊥. We can write this as

Prog(N) → ∀k⃗ N(k⃗),

where

Prog(N) := ∀k⃗(∀ℓ⃗[μ(ℓ⃗) < μ(k⃗) → N(ℓ⃗)] → N(k⃗)).

In the formal treatment of our example it will be more convenient to use the least element principle in the form of <–induction.

To prove <–induction we assume that N is progressive,

w_{1}: Prog(N),

and prove ∀k⃗ N(k⃗). This is achieved by proving ∀nB(n), where

B(n) := ∀k⃗(μ(k⃗) < n → N(k⃗)),

and using B(n) with n := μ(k⃗) + 1. We prove ∀nB(n) by (zero–successor) induction. Base. B(0) follows easily from the lemma

v_{1}: ∀m(m < 0 → ⊥)

and Efq: ⊥ → N(k⃗). Efq is not needed if (as in our example) N is a negation.

Step. Let n be given and assume w_{2}: B(n). To show B(n + 1) let k⃗ be given and assume w_{3}: μ(k⃗) < n + 1. We will derive N(k⃗) by using the progressiveness of N, w_{1}, at k⃗. Hence we have to prove

∀ℓ⃗(μ(ℓ⃗) < μ(k⃗) → N(ℓ⃗)).

So, let ℓ⃗ be given and assume further w_{4}: μ(ℓ⃗) < μ(k⃗). ¿From w_{4} and w_{3}: μ(k⃗) < n + 1 we infer μ(ℓ⃗) < n (using an arithmetical lemma). Hence, by induction hypothesis w_{2}: B(n) at ℓ⃗ we get N(ℓ⃗).

Detailed proof of the theorem.

Now we repeat the proof of the theorem in some more detail using <–induction. As always in classical logic, we may view the proof as an indirect one, deriving a contradiction from the assumption that the claim is false. So let a_{1}, a_{2} be given and assume v_{0}: 0 < a_{2} and

u: ∀k_{1}, k_{2}(abs(k_{1}a_{1} − k_{2}a_{2})|a_{1} → abs(k_{1}a_{1} − k_{2}a_{2})|a_{2} → 0 < abs(k_{1}a_{1} − k_{2}a_{2}) → ⊥).

We have to prove ⊥ which will be achieved by proving ∀k_{1}, k_{2}(0 < abs(k_{1}a_{1} − k_{2}a_{2}) → ⊥) by <–induction and then specializing this formula to k_{1}, k_{2} = 0, 1 and using the assumption v_{0}: 0 < a_{2}(= abs(0a_{1} − 1a_{2})).

The principle of <-induction is used with

N(k_{1}, k_{2}) := 0 < abs(k_{1}a_{1} − k_{2}a_{2}) → ⊥ and μ(k_{1}, k_{2}) := abs(k_{1}a_{1} − k_{2}a_{2}).

We have to show that N is progressive. To this end let k_{1}, k_{2} be given and assume

u_{1}: ∀ℓ_{1}, ℓ_{2}(μ(ℓ_{1}, ℓ_{2}) < μ(k_{1}, k_{2}) → N(ℓ_{1}, ℓ_{2})).

We have to prove N(k_{1}, k_{2}). So, assume u_{2}: 0 < μ(k_{1}, k_{2}). We have to show ⊥. This will be achieved by using the (false) assumption u at k_{1}, k_{2}. We have to prove μ(k_{1}, k_{2})|a_{1} and μ(k_{1}, k_{2})|a_{2}. Informally, one would argue “if, say, μ(k_{1}, k_{2}) |̸a_{1} then the remainder r_{1} := r(a_{1}, μ(k_{1}, k_{2})) is positive and less than μ(k_{1}, k_{2}). Furthermore we can find ℓ_{1}, ℓ_{2} such that r_{1} = μ(ℓ_{1}, ℓ_{2}). Altogether this contradicts the assumption u_{1}”. More formally, to prove μ(k_{1}, k_{2})|a_{1} we use the lemma

v_{2}: ∀a, q, c, r(a = qc + r → (0 < r → ⊥) → c|a)

at a_{1}, q_{1} := q(a_{1}, μ(k_{1}, k_{2})) (the quotient), μ(k_{1}, k_{2}) and r_{1}. We have to prove the premises

a_{1} = q_{1}μ(k_{1}, k_{2}) + r_{1} and 0 < r_{1} → ⊥

of the instantiated lemma v_{2}. Here we need the lemmata

\begin{matrix}v_{3}: ∀a, c(0 < c → a = q(a, c)c + r(a, c)), \\ v_{4}: ∀a, c(0 < c → r(a, c) < c) \end{matrix}

specifying the functions quotient and remainder. Now the first premise follows immediately from lemma v_{3} and u_{2}: 0 < μ(k_{1}, k_{2}). To prove the second premise, 0 < r_{1} → ⊥, we assume u_{3}: 0 < r_{1} and show ⊥. First we compute ℓ_{1}, ℓ_{2} such that r_{1} = μ(ℓ_{1}, ℓ_{2}). This is done by some auxiliary function f, defined by

f(a_{1}, a_{2}, k_{1}, k_{2}, q) := \{ \begin{matrix}qk_{1} − 1, & if k_{2}a_{2} < k_{1}a_{1} and 0 < q; \\ qk_{1} + 1, & otherwise. \end{matrix}

f satisfies the lemma

v_{5}: ∀a_{1}, a_{2}, k_{1}, k_{2}, q, r(a_{1} = q · μ(k_{1}, k_{2}) + r → r = μ(f(a_{1}, a_{2}, k_{1}, k_{2}, q), qk_{2})).

Hence we let ℓ_{1} := f(a_{1}, a_{2}, k_{1}, k_{2}, q_{1}) and ℓ_{2} := q_{1}k_{2}. Now we have μ(ℓ_{1}, ℓ_{2}) = r_{1} < μ(k_{1}, k_{2}) by v_{5}, u_{2} and v_{4}, as well as 0 < r_{1} = μ(ℓ_{1}, ℓ_{2}) by u_{3} and v_{5}. Therefore, we get ⊥ by u_{1} at ℓ_{1}, ℓ_{2} (using some equality lemmata). This completes the proof of μ(k_{1}, k_{2})|a_{1}. μ(k_{1}, k_{2})|a_{2} is proved similarly using the lemma

v_{6}: ∀a_{1}, a_{2}, k_{1}, k_{2}, q, r(a_{2} = q · μ(k_{1}, k_{2}) + r → r = μ(qk_{1}, f(a_{2}, a_{1}, k_{2}, k_{1}, q))).

The refined A–translation.

The proof of the principle of <–induction and the proof of the theorem were given in such a detail that it is now easy to formalize them completely. Only some arguments concerning < and = were left implicit. We will now briefly recall the term extraction process described in [2, 1] in general, and will see that we don’t need to worry about these omissions.

Let ∀x⃗_{1}C_{1}, …, ∀x⃗_{ℓ}C_{ℓ} be Π–formulas (i.e. C_{i} quantifier free) and A_{1}, …, A_{m} quantifier free formulas (in our example C_{1} ≡ 0 < a_{2} (x⃗_{1} is empty), A_{1} ≡ abs(a_{1}k_{1} − a_{2}k_{2})|a_{1}, A_{2} ≡ abs(a_{1}k_{1} − a_{2}k_{2})|a_{2}, A_{3} ≡ 0 < abs(a_{1}k_{1} − a_{2}k_{2})). Assume we have a classical proof of

∀a⃗(∀x⃗_{1}C_{1} → … → ∀x⃗_{ℓ}C_{ℓ} → ∃k⃗(A_{1}∧, …, ∧A_{m})),

i.e., a deduction

d[u: ∀k⃗(A_{1} → … → A_{m} → ⊥), v_{1}: ∀x⃗_{1}C_{1}, …, v_{ℓ}: ∀x⃗_{ℓ}C_{ℓ},]: ⊥.

To keep the derivation short we allow auxiliary lemmata v_{ℓ+1}: ∀x⃗_{ℓ+1}C_{ℓ+1}, …, v_{n}: ∀x⃗_{n}C_{n} asserting true Π–formulas. So, in fact, we have

d[u, v_{1}, …, v_{n}]: ⊥.

We sketch the main steps leading from this derivation to an intuitionistic proof of

A := ∃^{∗}k⃗(A_{1} ∧ … ∧ A_{m})

(∃^{∗} is the constructive existential quantifier) and hence to terms computing a witness k⃗.

1. Let L := {A_{1} → … → A_{m} → ⊥, C_{1}, …, C_{n}}. Determine inductively the L–critical relation symbols as follows: If (D⃗_{1} → P_{1}) → … → (D⃗_{m} → P_{m}) → R(t⃗) is a positive subformula of a formula in L, and for some i, P_{i} ≡ ⊥ or P_{i} ≡ Q(s⃗) where Q is L–critical, then R is L–critical too.

2. For each formula F let its A–translation F^{A} be the formula obtained from F by replacing ⊥ by A and each subformula R(s⃗), where R is L–critical, by (R(s⃗) → A) → A. Find derivations

d_{u}: ∀k⃗(A_{1} → … → A_{m} → ⊥)^{A}, and d_{v_{i}}[v_{i}: ∀x⃗_{i}C_{i}]: ∀x⃗_{i}C_{i}^{A}

following the recipe given in [1].

3. Replace in d[u, v_{1}, …, v_{n}]: ⊥ each formula by its A–translation. We obtain a derivation

d_{A}[u_{A}, v_{1A}, …, v_{nA}]: A,

where u_{A}: ∀k⃗(A_{1}^{A} → … → A_{m}^{A} → A) and v_{iA}: ∀x⃗_{i}C_{i}^{A} (induction axioms are replaced by new induction axioms for the A–translated formulas). Furthermore replace in the derivation above the free assumptions by the derivations constructed in step 2. We get the translated derivation

d^{tr}[v_{1}, …, v_{n}] := d_{A}[d_{u}, d_{v_{1}}, …, d_{v_{n}}]: A.

4. Apply Kreisel’s modified realizability interpretation [4] to extract a finite list of terms

r⃗ := (d^{tr})^{ets}

such that A_{1}[r⃗/k⃗] ∧ … ∧ A_{m}[r⃗/k⃗] is provable from v_{1}, …, v_{6}.

Comments.

– Term extraction commutes with the logical rules, e.g. (d_{1}d_{2})^{ets} = d_{1}^{ets}d_{2}^{ets}, and substitution, i.e.

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

By the latter we may first extract terms from the derivations d_{A}, d_{v_{1}}, …, d_{v_{n}} and also from the proof of <–induction separately, and then substitute these terms into the terms extracted from d_{A}[u_{A}, v_{1A}, …, v_{nA}]: A.

– Assume that we have fixed some system of lemmata ∀x⃗_{1}C_{1}, …, ∀x⃗_{n}C_{n} and computed the L-critical relation symbols according to step 1. Then it’s clear that we may use any other true → ∀–formula D as a further lemma, provided D does neither contain ⊥ nor any L–critical relation symbol. The simple reason is, that in this case D^{A} ≡ D. In the sequel we will call such formulas D harmless.

Computing the L–critical relation symbols.

Now we come back to our example. Let us repeat the main lemmata used in the proofs of the principle of <–induction and the theorem.

v_{0}: 0 < a_{2},
v_{1}: ∀m(m < 0 → ⊥),
v_{2}: ∀a, q, c, r(a = qc + r → (0 < r → ⊥) → c|a),
v_{3}: ∀a, c(0 < c → a = q(a, c)c + r(a, c)),
v_{4}: ∀a, c(0 < c → r(a, c) < c),
v_{5}: ∀a_{1}, a_{2}, k_{1}, k_{2}, q, r(a_{1} = q · μ(k_{1}, k_{2}) + r → r = μ(f(a_{1}, a_{2}, k_{1}, k_{2}, q), qk_{2})),
v_{6}: ∀a_{1}, a_{2}, k_{1}, k_{2}, q, r(a_{2} = q · μ(k_{1}, k_{2}) + r → r = μ(qk_{1}, f(a_{2}, a_{1}, k_{2}, k_{1}, q))).

The only critical relation symbol w.r.t. v_{0}, …, v_{6} is ·|·. Since the parts of our proofs which were left implicit concerned neither ·|· nor ⊥, they may be viewed as applications of harmless lemmata (in the sense of the second comment) and hence won’t cause problems.

Formal derivations.

We now spell out the derivation term d[u, v_{0}, v_{1}, …, v_{6}]: ⊥ formalizing the proof of the theorem. We use the following abbreviations.

μ(k⃗) := abs(k_{1}a_{1} − k_{2}a_{2}),
q_{i}(k⃗) := q(a_{i}, μ(k⃗)),
r_{i}(k⃗) := r(a_{i}, μ(k⃗)),
ℓ⃗_{1}(k⃗) := f(a_{1}, a_{2}, k_{1}, k_{2}, q_{1}(k⃗)), q_{1}(k⃗)k_{2},
ℓ⃗_{2}(k⃗) := q_{2}(k⃗)k_{1}, f(a_{2}, a_{1}, k_{2}, k_{1}, q_{2}(k⃗)),
N(k⃗) := 0 < μ(k⃗) → ⊥,
Prog := ∀k⃗(∀ℓ⃗[μ(ℓ⃗) < μ(k⃗) → N(ℓ⃗)] → N(k⃗)),
B(n) := ∀k⃗(μ(k⃗) < n → N(k⃗)).

Recall that, using the abbreviations above, u denotes the assumption

u: ∀k⃗(μ(k⃗)|a_{1} → μ(k⃗)|a_{2} → N(k⃗)).

The derivations below are given in a natural deduction calculus and are written as typed λ–terms according to the well–known Curry–Howard correspondence. By e we will denote (different) subderivations of d which derive a harmless formula from harmless assumptions.

There is no need to make them explicit since they will disappear in the term extraction process. The derivation of the theorem is given by

d ≡ d_{<−ind}^{Prog→∀k⃗ N(k⃗)}d_{prog}^{Prog}01(e^{0<μ(0,1)}[v_{0}]),

where

d_{<−ind} ≡ λw_{1}^{Prog}λk⃗.Ind_{n,B(n)}d_{base}d_{step}(μ(k⃗) + 1)k⃗e^{μ(k⃗)<μ(k⃗)+1},
d_{base} ≡ λk⃗, w_{0}^{μ(k⃗)<0}, w̃_{0}^{0<μ(k⃗)}.v_{1}μ(k⃗)w_{0},
d_{step} ≡ λn, w_{2}^{B(n)}, k⃗, w_{3}^{μ(k⃗)<n+1}.w_{1}k⃗(λℓ⃗, w_{4}^{μ(ℓ⃗)<μ(k⃗)}.w_{2}ℓ⃗(e^{μ(ℓ⃗)<n}[w_{4}, w_{3}])),

d_{prog} ≡ λk⃗, u_{1}^{∀ℓ⃗(μ(ℓ⃗)<μ(k⃗)→N(ℓ⃗))}, u_{2}^{0<μ(k⃗)}.uk⃗d_{div_{1}}^{μ(k⃗)|a_{1}}d_{div_{2}}^{μ(k⃗)|a_{2}}u_{2},
d_{div_{i}} ≡ v_{2}a_{i}q_{i}(k⃗)μ(k⃗)r_{i}(k⃗)(e^{a_{i}=q_{i}(k⃗)μ(k⃗)+r_{i}(k⃗)}[v_{3}, u_{2}])d_{≮_{i}}^{0<r_{i}(k⃗)→⊥},
d_{≮_{i}} ≡ λu_{3,i}^{0<r_{i}(k⃗)}.u_{1}ℓ⃗_{i}(k⃗)(e^{μ(ℓ⃗_{i}(k⃗))<μ(k⃗)}[v_{5}, u_{2}, v_{4}])(e^{0<μ(ℓ⃗_{i}(k⃗))}[u_{3,i}, v_{5}]).

A–translation and term extraction.

Preparation. We let

A := ∃^{∗}k⃗(μ(k⃗)|a_{1} ∧ μ(k⃗)|a_{2} ∧ 0 < μ(k⃗)),

where k⃗ ≡ k_{1}, k_{2}. In the modified realizability interpretation every formula F is mapped to a finite list τ(F) of finite types over nat, such that if d derives F then d^{ets} has type τ(F). For instance τ(A) = n⃗at := (nat, nat). Using some obvious abbreviations to denote finite sequences of types — for instance nat → n⃗at → n⃗at abbreviates (ρ, ρ), where ρ ≡ nat → nat → nat → nat — we compute the types of some further formulas.

τ(N(k⃗)^{A}) = τ(⊥^{A}) = τ(A) = n⃗at,
τ(Prog^{A}) = n⃗at → (n⃗at → n⃗at) → n⃗at,
τ(B(n)^{A}) = τ(a|c^{A}) = n⃗at → n⃗at.

If F neither contains ⊥ nor ·|· then τ(F^{A}) = τ(F) = () and hence the sequence of extracted terms of a derivation of F is empty too. Furthermore note that (Ind_{n,B(n)^{A}})^{ets} ≡ R⃗ where R⃗ ≡ (R_{1}, R_{2}) are simultaneous primitive recursion operators of type

R⃗: (n⃗at → n⃗at) → (nat → (n⃗at → n⃗at) → (n⃗at → n⃗at)) → nat → (n⃗at → n⃗at)

with

\begin{matrix}R_{i}y⃗f⃗0 = y_{i}, \\ R_{i}y⃗f⃗(z + 1) = f_{i}z(R_{1}y⃗f⃗z)(R_{2}y⃗f⃗z). \end{matrix}

Now we are prepared to compute the extracted terms. To make the relation between the derivations and their extracted terms as clear as possible we denote the finite list of object– (or function–) variables corresponding to the assumption w_{i} by w⃗_{i} etc. According to step 3 and step 4 and the comment the extracted terms are given by

(d^{tr})^{ets} ≡ (d_{<−ind}^{tr})^{ets}(d_{prog}^{tr})^{ets}01

where

(d_{<−ind}^{tr})^{ets} ≡ λw_{1}^{n⃗at→(n⃗at→n⃗at)→n⃗at}λk⃗.R⃗(d_{base}^{tr})^{ets}(d_{step}^{tr})^{ets}(μ(k⃗) + 1)k⃗,
(d_{base}^{tr})^{ets} ≡ λk⃗.d_{v_{1}}^{ets}μ(k⃗),
(d_{step}^{tr})^{ets} ≡ λn, w_{2}^{n⃗at→n⃗at}, k⃗.w⃗_{1}k⃗(λℓ⃗.w⃗_{2}ℓ⃗),
(d_{prog}^{tr})^{ets} ≡ λk⃗, u_{1}^{n⃗at→n⃗at}.d_{u}^{ets}k⃗(d_{div_{1}}^{tr})^{ets}(d_{div_{2}}^{tr})^{ets},
(d_{div_{i}}^{tr})^{ets} ≡ d_{v_{2}}^{ets}a_{i}q_{i}(k⃗)μ(k⃗)r_{i}(k⃗)(u⃗_{1}ℓ⃗_{i}(k⃗)).

It remains to compute d_{u}^{ets}, d_{v_{1}}^{ets} and d_{v_{2}}^{ets}.

d_{u}: ∀k⃗(((μ(k⃗)|a_{1} → A) → A) → ((μ(k⃗)|a_{2} → A) → A) → 0 < μ(k⃗) → A),

d_{u} ≡ λk⃗, u_{4}^{((μ(k⃗)|a_{1}→A)→A)}, u_{5}^{((μ(k⃗)|a_{2}→A)→A)}, u_{6}^{0<μ(k⃗)}.u_{5}(λu_{8}^{μ(k⃗)|a_{2}}.u_{4}(λu_{7}^{μ(k⃗)|a_{1}}.∃_{A}^{∗+}k⃗u_{7}u_{8}u_{6})).

Here we used the ∃^{∗}–introduction axiom

∃_{A}^{∗+}: ∀k⃗(μ(k⃗)|a_{1} → μ(k⃗)|a_{2} → 0 < μ(k⃗) → A)

with (∃_{A}^{∗+})^{ets} ≡ λk⃗.k⃗. We obtain

d_{u}^{ets} ≡ λk⃗, u_{4}^{n⃗at→n⃗at}, u_{5}^{n⃗at→n⃗at}.u⃗_{5}(u⃗_{4}k⃗).

The computation of d_{v_{1}}^{ets} is easy:

d_{v_{1}}: ∀m(m < 0 → A),
d_{v_{1}} ≡ λm, u_{9}^{m<0}.Efq_{A}(v_{1}mu_{9}),
d_{v_{1}}^{ets} ≡ λm0

(instead of 0 any terms of type n⃗at would do). The control structure of the extracted program is introduced by d_{v_{2}}^{ets}:

d_{v_{2}}: ∀a, q, c, r(a = qc + r → (0 < r → A) → (c|a → A) → A),
d_{v_{2}} ≡ λa, q, c, r, u_{10}^{a=qc+r}, u_{11}^{0<r→A}, u_{12}^{c|a→A}.g_{0<r}u_{11}(λu_{13}^{0<r→⊥}.u_{12}(v_{2}aqcru_{10}u_{13})),

where

g_{0<r}: (0 < r → A) → ((0 < r → ⊥) → A) → A

is a derivation with extracted terms

g_{0<r}^{ets} ≡ λx⃗, y⃗.if 0 < r then xn⃗at else yn⃗at fi.

Hence

d_{v_{2}}^{ets} ≡ λa, q, c, r, un⃗at ; 11, un⃗at ; 12.if 0 < r then u⃗_{11} else u⃗_{12} fi.

The final program.

If we plug d_{u}^{ets}, d_{v_{1}}^{ets} and d_{v_{2}}^{ets} into the program pieces we obtain

(d^{tr})^{ets} ≡ (d_{<−ind}^{tr})^{ets}(d_{prog}^{tr})^{ets}01

where

(d_{<−ind}^{tr})^{ets} =_{αβη} λw_{1}^{n⃗at→(n⃗at→n⃗at)→n⃗at}λk⃗′.R⃗(λk⃗.0)(λn, w_{2}^{n⃗at→n⃗at}, k⃗.w⃗_{1}k⃗w⃗_{2})(μ(k⃗′) + 1)k⃗′,
(d_{prog}^{tr})^{ets} =_{β} λk⃗, u_{1}^{n⃗at→n⃗at}.(d_{div_{2}}^{tr})^{ets}((d_{div_{1}}^{tr})^{ets}k⃗),
(d_{div_{i}}^{tr})^{ets} =_{β} λun⃗at ; 12.if 0 < r⃗_{i}(k⃗) then u⃗_{1}ℓ⃗_{i}(k⃗) else u⃗_{12} fi

and hence

(d_{prog}^{tr})^{ets} =_{β} λk⃗, u_{1}^{n⃗at→n⃗at}. if 0 < r_{2}(k⃗) then u⃗_{1}ℓ⃗_{2}(k⃗) else
if 0 < r_{1}(k⃗) then u⃗_{1}ℓ⃗_{1}(k⃗) else
k⃗ fifi.

Therefore we get, using the fact that μ(0, 1) = a_{2},

(d^{tr})^{ets} =_{β} R⃗(λk⃗.0)
(λn, w_{2}^{n⃗at→n⃗at}, k⃗. if 0 < r_{2}(k⃗) then w⃗_{2}ℓ⃗_{2}(k⃗) else
if 0 < r_{1}(k⃗) then w⃗_{2}ℓ⃗_{1}(k⃗) else
k⃗ fifi)
(a_{2} + 1)01

To make this algorithm more readable we may write it in the form (d^{tr})^{ets} = h⃗(a_{2} + 1, 0, 1), where

h⃗(0, k⃗) := 0,
h⃗(n + 1, k⃗) := if 0 < r_{2}(k⃗) then h⃗(n, ℓ⃗_{2}(k⃗)) else
if 0 < r_{1}(k⃗) then h⃗(n, ℓ⃗_{1}(k⃗)) else
k⃗ fifi.

As an example let us try out the extracted algorithm to compute coefficients k_{1}, k_{2} such that gcd(66, 27) = |k_{1} · 66 − k_{2} · 27|.

h⃗(28, 0, 1)  μ(0, 1) = 27

0 < r_{1} = 12 q_{1} = 2

\underbrace{q_{1}k_{1}}_{0} ±1, \underbrace{q_{1}k_{2}}_{2} −1, if k_{2}a_{2} < \underbrace{k_{1}a_{1}}_{0} No

1, 2

h⃗(27, 1, 2)  μ(1, 2) = 12

0 < r_{1} = 6 q_{1} = 5

\underbrace{q_{1}k_{1}}_{5·1} ±1, \underbrace{q_{1}k_{2}}_{5·2} −1, if \underbrace{k_{2}a_{2}}_{2·27} < \underbrace{k_{1}a_{1}}_{1·66} Yes

4, 10

h⃗(26, 4, 10)  μ(4, 10) = |4 · 66 − 10 · 27| = |264 − 270| = 6

6|66 0 < r_{2} = 3 q_{2} = 4

\underbrace{q_{2}k_{1}}_{4·4}, \underbrace{q_{2}k_{2}}_{4·10} ±1 − 1, if \underbrace{k_{1}a_{1}}_{4·66=264} < \underbrace{k_{2}a_{2}}_{10·27=270} Yes

16, 39

h⃗(25, 16, 39)  μ(16, 39) = |16 · 66 − 39 · 27| = |1056 − 1053| = 3

3|66 3|27 Result: 16, 39

Note that, although 3 = |16 · 66 − 39 · 27| is the least positive element of the ideal (66, 27), the coefficients 16, 39 are not minimal. The minimal coefficients are 2, 5.

Remarks.

– As one sees from this example the recursion parameter n is not really used in the computation but just serves as a counter or more precisely as an upper bound for the number of steps until both remainders are zero. This will always happen if the induction principle is used only in the form of the least element principle (or, equivalently, <– induction) and the relation symbol < is not critical. Because then in the extracted terms of <–induction, the step (d_{step}^{tr})^{ets} ≡ λn, w_{2}^{n⃗at→n⃗at}, k⃗.w⃗_{1}k⃗(λℓ⃗.w⃗_{2}ℓ⃗) has in its kernel no free occurrence of n.

– If one removes n according to the previous remark it becomes clear that our gcd algorithm is similar to Euklid’s. The only difference lies in the fact that we have kept a_{1}, a_{2} fixed in our proof whereas Euklid changes a_{1} to a_{2} and a_{2} to r(a_{1}, a_{2}) provided r(a_{1}, a_{2}) > 0 (using the fact that this doesn’t change the ideal).

– There is an interesting phenomenon which may occur if we extract a program from a classical proof which uses the least element principle. Consider as a simple example the wellfoundedness of <,

∀g^{nat→nat}∃k(g(k + 1) < g(k) → ⊥).

If one formalizes the classical proof “choose k such that g(k) is minimal” and extracts a program one might expect that it computes a k such that g(k) is minimal. But this is impossible! In fact the program computes the least k such that g(k + 1) < g(k) → ⊥ instead. This discrepancy between the classical proof and the extracted program didn’t show up in our gcd example since there was only one c = μ(k) > 0 such that c divides a_{1} and a_{2}, whereas in the example above there may be different c = g(k) such that g(k + 1) < g(k) → ⊥.

Implementation.

The gcd example has been implemented in the interactive proof system MINLOG. We show the term which was extracted automatically from a derivation of the theorem.

(lambda (a1)
(lambda (a2)
((((((nat-rec-at '(arrow nat (arrow nat (star nat nat))))
  (lambda (k1) (lambda (k2) (cons n000 n000))))
 (lambda (n)
  (lambda (w)
   (lambda (k1)
    (lambda (k2)
     ((((if-at '(star nat nat))
        ((<-strict-nat 0) r2))
       ((w l21) l22))
       ((((if-at '(star nat nat))
         ((<-strict-nat 0) r1))
         ((w l11) l12))
        (cons k1 k2))))))))
((plus-nat a2) 1))
0)
1)))

Here we have manually introduced r1, r2, l11, l12, l21, l22 for somewhat lengthy terms corresponding to our abbreviations r_{i}, ℓ⃗_{i}. The unbound variable n000 appearing in the base case is a dummy variable used by the system when it is asked to produce a realizing term for the instance ⊥ → ∃kA(k) of ex–falso–quodlibet. In our case, when the existential quantifier is of type nat one might as well pick the constant 0 (as we did in the text).

Acknowledgements. We would like to thank Monika Seisenberger and Felix Joachimski for implementing the refined A–translation and doing the gcd example in the MINLOG system.

References

[1] Ulrich Berger and Helmut Schwichtenberg. Program extraction from classical proofs. In D. Leivant, editor, Logic and Computational Complexity, International Workshop LCC ’94, Indianapolis, IN, USA, October 1994, volume 960 of Lecture Notes in Computer Science, pages 77–97. Springer Verlag, Berlin, Heidelberg, New York, 1995.

[2] Ulrich Berger and Helmut Schwichtenberg. The greatest common divisor: a case study for program extraction from classical proofs. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs. International Workshop TYPES ’95, Torino, Italy, June 1995. Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 36–46. Springer Verlag, Berlin, Heidelberg, New York, 1996.

[3] Harvey Friedman. Classically and intuitionistically provably recursive functions. In D.S. Scott and G.H. Müller, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21–28. Springer Verlag, Berlin, Heidelberg, New York, 1978.

[4] Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101–128. North– Holland, Amsterdam, 1959.