10.6092/issn.1972-5787/2225
We revisit both the usual ``going-up'' induction principle and Manna and Waldinger's ``going-down'' induction principle for primitive recursion,`a la Goedel, and primitive iteration, `a la Church.  We use 'Kleene's trick' to show that primitive recursion and primitive iiteration are as expressive as the other, even in the presence of accumulators.  As a result, we can directly extract a variety of recursive and iterative functional programs of the kind usually written or optimized by hand.
application/pdf
1972-5787
2225
1
en
Olivier Danvy
Journal of Formalized Reasoning
A Proof-Theoretic Account  of Primitive Recursion and Primitive Iteration
Text.Serial.Journal
https://jfr.unibo.it/
4
Articles
2011-12-21
2011-06-24
2011-04-14
2016-01-29
85-109
JFR
Olivier Danvy
2011/12/21
10.6092/issn.1972-5787/2225
85
Aarhus University
1972-5787
1
en
109
A Proof-Theoretic Account  of Primitive Recursion and Primitive Iteration
https://jfr.unibo.it/article/download/2225/1762
4
A Proof-Theoretic Account
of Primitive Recursion and Primitive Iteration
LUCA CHIARABINI
Università degli Studi di Parma
Viale G.P.Usberti, 53/A - 43124 Parma , Italy
luca.chiarabini@unipr.it
and
OLIVIER DANVY
Department of Computer Science, Aarhus University
Aabogade 34, DK-8200 Aarhus N, Denmark
danvy@cs.au.dk


We revisit both the usual “going-up” induction principle and Manna and Waldinger’s “going-
down” induction principle for primitive recursion, à la Gödel, and primitive iteration, à la Church.
We use ‘Kleene’s trick’ to show that primitive recursion and primitive iteration are as expressive
as each other, even in the presence of accumulators. As a result, we can directly extract a variety
of recursive and iterative functional programs of the kind usually written or optimized by hand.




1.    INTRODUCTION
There is proof theory, and there is programming practice. In theory, correct pro-
grams are extracted from proofs, and in practice, the extracted programs need to
be optimized to run efficiently:
                                 proof

                       extraction
                                   
                               program _ _ _ _ _ _ _ _ _/ other
                                          optimization   program

For example, for one recursive definition of the factorial function, there is an array
of iterative versions, and the literature is replete with clever ways to go from the
recursive definition to one of the iterative versions [8, 10, 13].
   Our goal here is to give a proof-theoretic account of this cleverness so that the
programs that run are the programs that are extracted:
                                                          other
                             proof _ _ _ _ _ _ _ _ _ _ _/
                                                          proof

                   extraction                                          extraction
                                                                     
                                                                 other
                           program
                                                                 program

     We focus on primitive recursion, à la Gödel, and primitive iteration, à la Church.
                                         Journal of Formalized Reasoning Vol. 4, No. 1, 2011 Pages 85–109.
86      ·     Chiarabini and Danvy

Recursion over N                          Recursion over L(ρ)
RσN : σ → (N → σ → σ) → N → σ             RσL(σ
                                             2
                                                1)
                                                   : σ2 → (σ1 → L(σ1 ) → σ2 → σ2 ) → L(σ1 ) → σ2
                                            σ1
RσN b f 0 7−→ b                           RL(σ2 ) b f nil 7−→ b
RσN b f (Succ n) 7−→ f n (RσN b f n)      RσL(ρ) b f (a :: l) 7−→ f a (RσL(ρ) b f l)

Recursion over B                          Projections            Application
RσB : σ → σ → B → σ                       π0 (r, s) −→ r        (λx.r)s −→ r[x := s]
(RσB r s)tt 7−→ r                         π1 (r, s) −→ s
(RσB r s)ff 7−→ s


                      Fig. 1.   Conversion rules for Gödel’s System T

   Overview. We first make a short excursus about extracting programs from proofs
(Section 2) with Minlog,1 the proof assistant we used to develop all the proofs
presented through the paper. We then review primitive up/down recursion and
iteration (Section 3) and we study their expressive power (Section 4). Next, we
turn to their accumulator-based counterparts (Section 5). Our running example,
in Section 3, Section 4, and Section 5, is the factorial function. In Section 6, we
extract three iterative versions of this function with an accumulator.

2.    MODIFIED REALIZABILITY FOR FIRST-ORDER MINIMAL LOGIC
2.1    Gödel’s System T
Types are built from base types and from compound types. Base types are natural
numbers (N) and booleans (B). Compound types are lists with elements of some
type (L(σ)), functions (→), and pairs (×). The terms of Gödel’s System T [4]
are the terms of the simply typed λ-calculus with pairs, projections, and constants
(constructors and recursive operators over natural numbers, booleans, and lists):


        Type ∋ σ, σ1 , σ2 ::= N | B | L(σ) | σ1 → σ2 | σ1 × σ2
             Const ∋ c ::= 0 | Succ | tt | ff | nil | cons | RσN | RσB | RσL(σ
                                                                            2
                                                                               1)

     Terms ∋ t, t0 , t1 , t2 ::= c | x σ | (λx σ1 .tσ2 )σ1 →σ2 | (t0 σ1 →σ2 t1 σ1 )σ2 |
                                                 σ ×σ
                                 (t1 σ1 , t2 σ2 ) 1 2 | (π1 tσ1 ×σ2 )σ1 | (π2 tσ1 ×σ2 )σ2
As an abbreviation, t0 :: · · · :: tn :: nil represents a list with n + 1 elements.
  We equip this calculus with the usual conversion rules for the recursive operators,
applications and projections (Figure 1).

2.2    Heyting Arithmetic
We define Heyting Arithmetic HAω [10, Page 240] for our language based on Gödel’s
System T, which is finitely typed. We define negation ¬ϕ by ϕ → ⊥.

Formulas: Atomic formulas (P~tρ~ ) (P a predicate symbol, ~t, ρ
                                                              ~ lists of terms and
types), ϕ → ψ, ∀xρ ϕ, ∃xρ ϕ, ϕ ∧ ψ.

1 http://www.minlog-system.de



Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration                         ·   87



               Derivations                            Terms                  Open assumptions


                         (ass)                            uϕ                       {u}
                 ϕ

          |M            |N
           ϕ             ψ                       (hM ϕ , N ψ iϕ∧ψ )          OA(M ) ∪ OA(N )
                               (∧+ )
               ϕ∧ψ

                |M
               ϕ∧ψ                                  (M ϕ∧ψ 0)ϕ                   OA(M )
                          (∧−
                            0 )
                 ϕ

                |M
               ϕ∧ψ                                  (N ϕ∧ψ 1)ψ                   OA(N )
                          (∧−
                            1 )
                 ψ

              [u : ϕ]
                |M
                                                  (λuϕ M ψ )ϕ→ψ                OA(M )\{u}
               ψ
                          (→+
                            u)
              ϕ→ψ

         |M               |N
        ϕ→ψ                ϕ                      (M ϕ→ψ N ϕ )ψ              OA(M ) ∪ OA(N )
                                  (→− )
            ψ

       |M
                                                                    ρ
        ϕ               with Var. cond.           (λxρ M ϕ )∀x          ϕ        OA(M )
               (∀+ )
      ∀xρ ϕ

          |M
                                                          ρ
        ∀xρ ϕ(x)             tρ        −
                                                  (M ∀x       ϕ(x) tρ )ϕ         OA(M )
                                   (∀ )
              ϕ(t)

     |M
                          with Var. cond.                          nc xρ ϕ
      ϕ                                         (λnc xρ M ϕ )∀                   OA(M )
              (∀nc+ )     and x 6∈ [[M ]]
   ∀nc xρ ϕ

          |M
       nc ρ                                              nc xρ ϕ ρ ϕ
      ∀ x ϕ(x)               tρ                   (M ∀          t )              OA(M )
                                   (∀nc− )
           ϕ(t)
    “with Var. cond.” stands for “provided xρ 6∈ FV(ϕ), for any uϕ ∈OA(M )”

                     Fig. 2.      Derivation terms for ∀, ∀nc , → and ∧


                                              Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
88     ·     Chiarabini and Danvy

  Derivations: By the Curry-Howard correspondence [10] it is convenient to write
derivations as terms: we define λ-terms M ϕ for natural deduction proofs of formulas
ϕ together with the set OA(M ) of open assumptions in M (see Figure 2). Usually
we will omit type and formula indices in derivations if they are uniquely determined
by the context or if they are not relevant.
  We will use two special quantifiers ∀nc /∃nc (introduction and elimination rules
in Figure 2) to indicate that there should be no computational content [11]. The
logical meaning of the universal quantifiers is unchanged. However, we have to
observe a special variable condition for ∀nc+ : the variable to be abstracted should
not be a computational variable in the given proof, i.e., the extracted program of
this proof should not depend on x.
  We use ∃ and ∨ in our logic, if we allow appropriate axioms as constant derivation
terms:
                    ∃+         ρ       ρ
                     xρ ,ϕ : ∀x (ϕ → ∃x ϕ)
                  ∃−           ρ       ρ
                   xρ ,ϕ,ψ : ∃x ϕ → (∀x ϕ → ψ) → ψ with x 6∈ F V (ψ)

We can define ∨ from ∃ via:
                          ϕ ∨ ψ := ∃pB (p → ϕ) ∧ ((p → ⊥) → ψ)
  We use the following axioms to perform proofs by induction over naturals (N),
booleans (B) and lists of elements of type ρ (L(ρ)):
               Indn,A : A[n 7→ 0] → ∀n(A → A[n 7→ Sn]) → ∀nN A,
               Indp,A : A[p 7→ tt] → A[p 7→ ff] → ∀pB A,
                Indl,A : A[l 7→ nil] → (∀x, l.A → A[l 7→ x :: l]) → ∀lL(α) A
Finally we use the constant derivation term (IFϕ ),
                           IFϕ : ∀pB (p → ϕ) → ((p → ⊥) → ϕ) → ϕ
to perform case distinction on boolean terms w.r.t. a goal formula ϕ.

2.3   Short Excursus in Program Extraction from Proofs
By definition, existence proofs have computational content: we can exhibit a wit-
ness, which thus contributes to the extracted program. Realizability extends this
idea to other formulas; it can be seen as an incarnation of the Brouwer-Heyting-
Kolmogorov interpretation [12] of proofs.
   2.3.1 Type of a Formula. We note τ (ϕ) the type of the term (or “program”) to
be extracted from a proof of ϕ. More precisely, to every formula ϕ it is possible
to assign an object of type τ (ϕ) (a type or the “nulltype” symbol ε). In case
τ (ϕ) = ε proofs of ϕ have no computational content; such formulas ϕ are called
Harrop formulas. (See Appendix A.1.)
   2.3.2 Extraction Map. From every derivation M of a computationally meaning-
ful formula ϕ (that is, τ (ϕ) 6= ε), it is possible to define its extracted program [[M ]]
of type τ (ϕ) [1, 7, 9, 10]. If τ (ϕ) = ε then [[M ]] = ε: the notational overlap does not
hurt, as those programs are dropped out anyway. (See Appendix A.2.)


Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
        A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration         ·     89

  2.3.3 Realization of a formula. The correctness of the extracted programs is
guaranteed by the notion of modified realizability. Intuitively, if t is the extracted
program from the derivation M of the formula ∀x∃y.P (x, y) (ϕ), then for each x
the formula P (x, t(x)) is provably correct (Soundness), i.e., t realizes ϕ (according
to modified realizability), written (t mr ϕ). (See Appendix A.3.)
   Theorem (Soundness). Let M be a derivation of a formula ϕ from assump-
tions ui : ϕi . Then we can find a derivation of the formula ([[M ]] mr ϕ) from
assumptions ūi : xui mr ϕi .
     Proof. By structural induction on M .
In the following, for readability, all the extracted programs will be displayed in a
the syntax of Standard ML.

3.    UP AND DOWN INDUCTION PRINCIPLES OVER NATURAL NUMBERS
We successively review primitive recursion, i.e., ‘rec’ in Gödel’s System T (Sec-
tion 3.1) and then primitive iteration, i.e., Church numerals (Section 3.2). We then
turn to symmetric analogues that correspond to Manna and Waldinger’s “going
down” recursion (Section 3.3) and induction (Section 3.4). In reference to Manna
and Waldinger’s pioneering work [8], we refer to these induction principles as ‘up’
and ‘down.’
3.1    Up primitive recursive induction
Here is the proof principle for primitive recursion:
                         |Z                   |S
                        P (0)      ∀n(P (n) → P (n + 1))
                                                         (up-prim-rec)
                                    ∀nP (n)
   Manna and Waldinger refer to it as ‘going up’ since P (n) is needed to deduce
P (n + 1). The corresponding synthesized functional Up.prim rec is displayed in
Figure 3. There, z is extracted from [[Z]] and s from [[S]]. The computation is driven
by the natural number denoted by the input variable n: computing the result for n
requires the result for n − 1 to be computed, until the base case n = 0 is reached in
a trail of nested applications of the function denoted by s. The computation then
proceeds going up from 0 to the given natural number.
   The traditional definition of the factorial function is a straightforward example
of primitive recursion. It is obtained as an instance of Up.prim rec where z is
instantiated with the neutral element for multiplication (1) and s with the (curried)
multiplication function (fn i => fn c => (i + 1) * c):
fun fact n
    = Up.prim_rec (1, fn i => fn c => (i + 1) * c) n
The extracted program reads as follows:
fun up_prim_rec_fact n
    = let fun visit m
              = if m = 0 then 1 else m * (visit (m - 1))
      in visit n
      end
                                             Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
90      ·    Chiarabini and Danvy


structure Up
= struct
    (* prim_rec : ’a * (int -> ’a -> ’a) -> int -> ’a *)
    fun prim_rec (z, s) n
        = let fun visit m
                  = if m = 0 then z else s (m - 1) (visit (m - 1))
          in visit n
          end

       (* prim_iter : ’a * (’a -> ’a) -> int -> ’a *)
       fun prim_iter (z, s) n
           = let fun visit m
                     = if m = 0 then z else s (visit (m - 1))
             in visit n
             end
     end



                         Fig. 3.   Synthesized functionals for up induction

3.2    Up primitive iterative induction
Here is the proof principle for primitive iteration:
                           |Z                    |S
                                       nc
                         P (0)        ∀ n(P (n) → P (n + 1))
                                                             (up-prim-iter)
                                        ∀nP (n)
The difference between primitive and iterative induction is that in the iterative
case, we quantify non computationally over n in the inductive step. One can then
synthesize the functional for up primitive iteration Up.prim rec in Figure 3. Again,
there, z is extracted from [[Z]] and s from [[S]].
  To define the factorial function as an instance of Up.prim iter, we must generalize
Kleene’s trick to compute the predecessor function over Church numerals [6]. We
instantiate z with (1, 1) and s with fn (i, c) => (i + 1, i * c) in Up.prim iter:
fun fact n
    = let val (i, c) = Up.prim_iter ((1, 1), fn (i, c) => (i + 1, i * c)) n
      in c
      end
The extracted program reads as follows:
fun up_prim_iter_fact n
    = let fun visit m
          = if m = 0 then (1, 1) else let val (i, c) = visit (m - 1)
                                      in (i + 1, i * c)
                                      end
      in let val (i, c) = visit n in c end
      end


Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
      A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration         ·     91

3.3   Down primitive recursive induction
Manna and Waldlinger also present a ‘going down’ version of primitive recursion:
                      |Z                   |S
                     Q(n)       ∀m(Q(m + 1) → Q(m))
                                                    (down-prim-rec)
                                   Q(0)
where n could be a free variable in Q. They refer to it as ‘going down’ since Q(n+1)
is needed to deduce Q(n).
   The idea is that the property ∀nP (n) is proved using a predicate Q(m) such
that Q(0) reduces to P (n). This induction principle is then applied to Q(0). The
challenging point here is that a kind of eureka step is required in order to find
a satisfactory predicate Q. So, given the proof of Q(0) in terms of Z Q(n) and
S ∀m(Q(m+1)→Q(m)) , we prove ∀nP (n) by
                                  |R
                                                  ..
                                P (n)              .
                                           →+
                             Q(0) → P (n)        Q(0)
                                                            →−
                                       P (n)
                                              ∀+
                                      ∀nP (n)
Here we require the normalization of the code extracted from the proof term
λuQ(0) RP (n) to be equal to the identity function. This is because we assume Q(z)
to be a predicate that, when instantiated with 0, can be rewritten into P (n) in a
finite number of steps, using an opportune set of rewriting rules. This process of
simplification is performed using the following, and only the following, axiom:
                  Eq-Compat : ∀x1 , x2 (x1 ; x2 → P (x1 ) → P (x2 ))
where ; denotes a binary relation and P a generic predicate symbol. This axiom
says that, if we know that a given term (bounded by x1 ) is in relation with another
term (bounded by x2 ) – for example the equality relation – and we know that
P (x1 ) holds, then we can conclude that P (x2 ) holds. Letting the computational
content of the Eq-compat axiom be the identity function, it is clear that the program
extracted from nested applications of Eq-compact, once normalized, will correspond
to the identity function. Since the derivation above is a detour, we rewrite it in the
following way:
                                          ..
                                           .
                                         Q(0)
                                           |R
                                        P (n)
                                               ∀+
                                       ∀nP (n)

which can be read as the replacement of each open assumption uQ(0) in R by the
proof of Q(0). The program extracted from the complete proof of ∀nP (n) is the
functional Down.prim rec in Figure 4, where z could depend on n (hence the order
of the parameters).

                                           Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
92      ·    Chiarabini and Danvy


structure Down
= struct
    (* prim_rec : int -> ’a * (int -> ’a -> ’a) -> ’a *)
    fun prim_rec n (z, s)
        = let fun visit m
                  = if m = n then z else s m (visit (m + 1))
          in visit 0
          end

       (* prim_iter : int -> ’a * (’a -> ’a) -> ’a *)
       fun prim_iter n (z, s)
           = let fun visit m
                     = if m = n then z else s (visit (m + 1))
             in visit 0
             end
     end



                       Fig. 4.   Synthesized functionals for down induction

     We now return to the factorial function over natural numbers:
                                 
                                    1                 if n = 0
                       fact(n) =
                                    n × fact(n − 1) if n > 0
Let us prove that ∀n∃m(m = fact(n)) by going-down primitive recursion. We
assume n. In order to prove ∃m(m = fact(n)), we design the new goal ∃m(fact(0) ×
m = fact(n)). Applying the going-down primitive recursive induction principle to
this formula requires us to prove the following two subgoals:
—∃m(fact(n) × m = fact(n)): It is sufficient to set m = 1.
—Now assume y and ih : ∃m(fact(y +1)×m = fact(n)). We prove ∃m(fact(y)×m =
 fact(n)). By ih, we know that there does exist an m′ such that fact(y + 1) × m′ =
 fact(n). Considering that fact(y + 1) = (y + 1) × fact(y), the thesis is proved for
 m = (y + 1) × m′ .
The program extracted from this proof reads as follows:
fun down_prim_rec_fact n
    = let fun visit m
              = if m = n then 1 else (m + 1) * (visit (m + 1))
      in visit 0
      end

This residual program was obtained as an instance of Down.prim rec where z is
instantiated with the neutral element for multiplication and s with the (curried)
multiplication function – the same instantiation as in Section 3.1:
fun fact n
    = Down.prim_rec n (1, fn i => fn c => (i + 1) * c)



Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
       A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration                   ·   93

3.4   Down primitive iterative induction
Here is the proof principle for primitive iteration:
                           |Z                     |S
                                         nc
                     Q(n)               ∀ m(Q(m + 1) → Q(m))
                                                             (down-prim-iter)
                                            Q(0)
Again, the difference between primitive and iterative induction is that in the itera-
tive case, we quantify non computationally over m in the inductive step. One can
then synthesize the functional for down primitive iteration in Figure 4, where n, in
the local definition of visit, is free.
   Again, to define the factorial function as an instance of Down.prim iter, we use
Kleene’s trick. As in Section 3.2, we instantiate z with (1, 1) and s with fn (i,
c) => (i + 1, i * c) in Down.prim iter:
fun fact n
    = let val (i, c) = Down.prim_iter n ((1, 1),
                                         fn (i, c) => (i + 1, i * c))
      in c
      end
The extracted program reads as follows:
fun down_prim_iter_fact n
    = let fun visit m
          = if m = n then (1, 1) else let val (i, c) = visit (m + 1)
                                      in (i + 1, i * c)
                                      end
      in let val (i, c) = visit 0 in c end
      end

4.    EXPRESSIVE POWER OF THE UP AND DOWN INDUCTION PRINCIPLES
In this section we show that the induction principles (and the associate synthesized
functionals) reviewed in Section 3 share the same expressive power.


                                    o          Section 4.3
                Up.prim-rec                                            / Down.prim-rec
                            O                                                  O
                                               Section 4.4

         Section 4.1            Section 4.2                  Section 4.6           Section 4.5

                                              Section 4.8         /           
                Up.prim-iter o                                         Down.prim-iter
                                               Section 4.7

   In the picture above each arrow A −→ B states the existence of a proof to
simulate the induction principle B in terms of the induction principle A. At the
level of programs, this corresponds to adapting the functional associated with the
principle A in order to simulate the execution of the functional associated with the

                                                   Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
94      ·    Chiarabini and Danvy

principle B. The binary relation −→ is not transitive, and the missing arrows in
the diagram are left as an exercise.
  To the knowledge of the authors, the proofs presented in this section and in
Section 5 are new. They are available in the first author’s home page.2 By the
Curry-Howard correspondence, we manipulated proofs of programs – and not di-
rectly their code. This made it possible for us to supply a complete set of tactics to
transform the proof of each induction principle into a certified version of the others.
4.1    Up primitive iteration in terms of up primitive recursion
To simulate up primitive iteration in terms of up primitive recursion, we instantiate
the base and step of Up.prim rec respectively with z and with fn i => fn c => s
c, where z and s are the base and step of up prim iter:
fun up_prim_iter (z, s) n
    = let fun visit m
              = if m = 0 then z else s (visit (m - 1))
      in visit n
      end
(* = Up.prim_rec (z, fn i => fn c => s c) n *)

Proof interpretation:
     Proposition 4.1. Given the proof
                          |M                     |N
                         P (0)       ∀nc n(P (n) → P (n + 1))
                                                              (up-prim-iter)
                                        ∀nP (n)
then there exist M ′ , N ′ such that:
                           |M ′                  |N ′
                          P (0)       ∀n(P (n) → P (n + 1))
                                                            (up-prim-rec)
                                        ∀nP (n)
with computational content equal to up prim iter.
     Proof. ciao

                                      |N
                           nc
                          ∀ n(P (n) → P (n + 1))      n
                                                          ∀−
                               P (n) → P (n + 1)               [u : P (n)]
                                                                              →−
                                                P (n + 1)       +
                                                             →u
               |M                          P (n) → P (n + 1)
                                                                ∀+
              P (0)                      ∀n(P (n) → P (n + 1))
                                                                (up-prim-rec)
                                   ∀nP (n)




2 http://cmt.math.unipr.it/luca/MinlogCode/




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
      A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration           ·     95

4.2   Up primitive recursion in terms of up primitive iteration
To simulate up primitive recursion in terms of up primitive iteration, we use
Kleene’s trick: we instantiate the base and step of Up.prim iter respectively with
(0, z) and fn (j, c) => (j + 1, s’ j c), where z and s are the base and step of
up prim rec:
fun up_prim_rec (z, s) n
    = let fun visit m
              = if m = 0 then (0, z) else let val (i, c) = visit (m - 1)
                                          in (i + 1, s i c)
                                          end
      in let val (i, c) = visit n in c end
      end
(* = #2 (Up.prim_iter ((0, z), fn (i, c) => (i + 1, s’ i c)) n) *)

Proof interpretation:
  Proposition 4.2. Given the proof
                        |M                   |N
                        P (0)     ∀n(P (n) → P (n + 1))
                                                        (up-prim-rec)
                                    ∀nP (n)
then there exist M ′ , N ′ , R such that:

        |M ′                                      |N ′
 ∃y(y = 0) ∧ P (0)      ∀nc n(∃y(y = n) ∧ P (n) → ∃y(y = n + 1) ∧ P (n + 1))
                                                                             (up-prim-iter)
                             ∀n(∃y(y = n) ∧ P (n))
                                      |R
                                   ∀nP (n)
and from which it is possible to extract up-prim-rec.
  Proof. See Figure 5.

4.3   Up primitive recursion in terms of down primitive recursion
To simulate up primitive recursion in terms of down primitive recursion, again we
use Kleene’s trick: we instantiate the base and step of Down.prim rec respectively
with (0, z) and fn m => fn (i, c) => (i + 1, s i c), where z and s are the base
and step of up prim rec’:
fun up_prim_rec’ (z, s) n
    = let fun visit m
          = if m = n then (0, z) else let val (i, c) = visit (m + 1)
                                      in (i + 1, s i c)
                                      end
      in let val (i, c) = visit 0 in c end
      end
(* = #2 (Down.prim_rec n ((0, z), fn m => fn (i, c) => (i + 1, s i c)))                       *)



                                             Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
96        ·    Chiarabini and Danvy




                                                                         |N
                                                          ∀n(P (n) → P (n + 1))                       y
                                                                                                           ∀−
                Eq-Compat           [u : y = n]                     P (y) → P (y + 1)
                                                                                                  −
                                                                                              →
                                        P (n) → P (n + 1)


                                                             [r : ∃y(y = n) ∧ P (n)]
                                                                                                  ∧−
                                                                                                   1
                                                                             P (n)
                                                                                         −
                                                                                     →
                                          P (n + 1)
                                                                →+
                                                                 u
                                    y = n → P (n + 1)
                                                                    ∀+
                                  ∀y(y = n → P (n + 1))


                                   [r : ∃y(y = n) ∧ P (n)]
                                                                    ∧−
                                                                     0
                        ∃−                ∃y(y = n)
                                                                                             ∃−
                                               P (n + 1)


                                                                                [u : y = n]
                                                   ∃+ (y + 1)                 y+1=n+1
                                                                                                      ∃+
                                                                ∃y(y = n + 1)
                                                                                             →+
                                                                                              u
              [r : ∃y(y = n) ∧ P (n)]                     y = n → ∃y(y = n + 1)
                                         ∧−                                                    +
                                          0                                                       ∀
     ∃−             ∃y(y = n)                        ∀y(y = n → ∃y(y = n + 1))
                                                                                                  ∃−
                                  ∃y(y = n + 1)                                                                 )
                                                                                          ∧+
                                                      ∃y(y = n + 1) ∧ P (n + 1)
                                                                                        →+
                                                                                         r
                                      (∃y(y = n) ∧ P (n)) → (∃y(y = n + 1) ∧ P (n + 1))
                                   nc                                                      ∀nc+
                                  ∀ n((∃y(y = n) ∧ P (n)) → (∃y(y = n + 1) ∧ P (n + 1)))


                        ∃+ 1 (1 = 0)                 |M
                                          ∃+
                          ∃y(y = 0)                 P (0)
                                                             ∧+
                                ∃y(y = 0) ∧ P (0)
                                                                                (up-prim-iter)
                                 ∀n(∃y(y = n) ∧ P (n))                   n
                                                                              ∀−
                                         ∃y(y = n) ∧ P (n)
                                                                    ∧−
                                                                     1
                                                  P (n)
                                                                +
                                                            ∀
                                               ∀nP (n)


The variable n does not occur in the content of the proof of the formula (∃y(y = n) ∧ P (n)) →
(∃y(y = n + 1) ∧ P (n + 1)), thus the (∀nc+ ) inference yields a result that is correct w.r.t. the
definition given in Figure 2.

                     Fig. 5.    Simulation of up-prim-rec in term of up-prim-iter




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
       A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration          ·         97

Proof interpretation:
  Proposition 4.3. Given the proof
                         |M                  |N
                        P (0)      ∀n(P (n) → P (n + 1))
                                                             (up-prim-rec)
                                     ∀nP (n)
then there exist M ′ , N ′ such that:
                                                            |N ′
                |M ′                 ∀y((∃z(z = n − (y + 1)) ∧ P (n − (y + 1))) →
      ∃z(z = n − n) ∧ P (n − n)              (∃z(z = n − y) ∧ P (n − y)))
                                                                                (down-prim-rec)
                           ∃z(z = n − 0) ∧ P (n − 0) −
                                                     ∧1
                                    P (n)
                                               +
                                             ∀
                                   ∀nP (n)
and from which it is possible to extract the procedure up-prim-rec’.
  Proof. See Figure 6. [Note that the derivation (∗) in Figure 6 is not true for
general z, n and y in N. In order to make (∗) correct we can replace the end formula
on which we apply the (down-prim-rec) principle with ∃z(z = n − 0) ∧ P (n − 0) ∧ (n ≥
0). By this replacement, from the assumption u : z = n − (y + 1) and n ≥ (y + 1)
we correctly derive z + 1 = n − y.]
4.4   Down primitive recursion in terms of up primitive recursion
To simulate down primitive recursion in terms of up primitive recursion, we in-
stantiate the base and step of Up.prim rec respectively with (n, z) (for some input
parameter n) and fn m => fn (i, c) => (i - 1, s (i - 1) c), where z and s are
the base and step of down prim rec:
fun down_prim_rec (z, s) n
    = let fun visit m
              = if m = 0 then (n, z) else let val (i, c) = visit (m - 1)
                                          in (i - 1, s (i - 1) c)
                                          end
      in let val (i, c) = visit n in c end
      end
(* = #2 (Up.prim_rec ((n, z),
                       fn m => fn (i, c) => (i - 1, s (i - 1) c)) n) *)
Proof interpretation:
  Proposition 4.4. Given
                        |M                   |N
                       Q(n)      ∀m(Q(m + 1) → Q(m))
                                                             (down-prim-rec)
                                    Q(0)
                                        |R
                                    P (n)
                                              ∀+
                                   ∀nP (n)

                                             Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
98     ·     Chiarabini and Danvy




                                [r : ∃z(z = n − (y + 1)) ∧ P (n − (y + 1))]
                                                                               ∧−
                                                                                1
                                              P (n − (y + 1))

                                                              |N
                                                  ∀n(P (n) → P (n + 1))             z
                                                                                            ∀−
       Eq-Compat [u : z = n − (y + 1)]                    P (z) → P (z + 1)
                                                                              →−
                          P (n − (y + 1)) → P (n − y)
                                                                                                        →−
                                                          P (n − y)
                                                                                    →+
                                                                                     u
                                              (z = n − (y + 1)) → P (n − y)
                                                                                      +
                                                                                        ∀
                                            ∀z((z = n − (y + 1)) → P (n − y))


                          [r : ∃z((z = n − (y + 1)) ∧ P (n − (y + 1)))]
                                                                              ∧−
                                                                               0
               ∃−                        ∃z(z = n − (y + 1))
                                                                                                  ∃−
                                                 P (n − y)


                                                     [u : z = n − (y + 1)]
                                                                              (∗)
                                   ∃+ (n − y)             z+1=n−y
                                                                           ∃+
                                              ∃z(z = y − n)
                                                                           →+u
                                   (z = n − (y + 1)) → ∃z(z = n + 1)
                                                                              ∀+
                                 ∀z((z = n − (y + 1)) → ∃z(z = n − y))


                              [r : ∃z(z = n − (y + 1)) ∧ P (n − (y + 1))]
                                                                              ∧−
                                                                               1
                ∃−                       ∃z(z = n − (y + 1))
                                                                                                 ∃−
                                              ∃z(z = n − y)


                                                                                                       ∧+
                                       ∃z(z = n − y) ∧ P (n − y)
                                                                                 →+
                                                                                  r
                               (∃z(z = n − (y + 1)) ∧ P (n − (y + 1))) →
                                       ∃z(z = n − y) ∧ P (n − y)
                                                                                    ∀+
                              ∀y((∃z(z = n − (y + 1)) ∧ P (n − (y + 1))) →
                                       ∃z(z = n − y) ∧ P (n − y))


                 ∃+ 0 (0 = n − n)                    |M
                                         ∃+
                    ∃z(z = n − n)                 P (n − n)
                                                                ∧+
                         ∃z(z = n − n) ∧ P (n − n)
                                                                              (down-prim-rec)
                                      ∃z(z = n − 0) ∧ P (n − 0)
                                                                      ∧−
                                                                       1
                                                 P (n)
                                                          ∀+
                                                ∀nP (n)


                    Fig. 6.     Simulation of up-prim-rec in term of down-prim-rec




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
        A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration              ·    99

we can find the opportune M ′ , N ′ such that if the proof of Q(0) is substituted by
                                                  |N ′
            |M ′              ∀y(((∃z(z = n − y) ∧ Q(n − y)) →
      ∃z(z = n) ∧ Q(n)     (∃z(z = n − (y + 1)) ∧ Q(n − (y + 1))))
                                                                             (up-prim-rec)
                     ∀y(∃z(z = n − y) ∧ Q(n − y))                                            n
                                                                                                 ∀−
                                           ∃z(z = 0) ∧ Q(0) −
                                                              ∧1
                                                  Q(0)
then the computational content of the resulting proof corresponds to down prim rec.
  Proof. We propose only a sketch because the structure of the proof is the same
as the one displayed in Figure 6. The idea is to prove the lemma
                              ∀y(∃z(z = n − y) ∧ Q(n − y))
by up primitive recursion:
    Base y = 0. We must prove ∃z(z = n) ∧ Q(n). The left conjunct is proved by
introducing n for z. The right conjunct is given by M .
    Step y + 1. Let us assume y and z ′ such that z ′ = n − y and Q(n − y). We must
prove ∃z(z = n − (y + 1)) ∧ Q(n − (y + 1)). The left conjunct is proved introducing
z ′ − 1 for z. The right conjunct is proved by instantiating N on z ′ − 1, from which
we deduce Q(z ′ ) → Q(z ′ − 1) that can be rewritten as Q(n − y) → Q(n − y − 1)
by the induction hypothesis z ′ = n − y. We finally instantiate this formula with
Q(n − y).



4.5     Down primitive iteration in terms of down primitive recursion
To simulate down primitive iteration in terms of down primitive recursion, we
instantiate the base and step of Down.prim rec respectively with z and fn i => fn
c => s c, where z and s are the base and step of down prim iter:
fun down_prim_iter n (z, s)
    = let fun visit m
              = if m = n then z else s (visit (m + 1))
      in visit 0
      end
(* = Down.prim_rec n (z, fn i => fn c => s c) *)

Proof interpretation:
  Proposition 4.5. Given
                       |M                        |N
                                  nc
                      Q(n)      ∀ m(Q(m + 1) → Q(m))
                                                                  (down-prim-iter)
                                   Q(0)
                                         |R
                                        P (n)
                                                  ∀+
                                       ∀nP (n)

                                                 Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
100     ·      Chiarabini and Danvy

we can find the opportune M ′ , N ′ such that if the proof of Q(0) is replaced by
                            |M ′                   |N ′
                        Q(n)        ∀m(Q(m + 1) → Q(m))
                                                          (down-prim-rec)
                                       Q(0)
then the computational content of the transformed proof is equal to down prim iter.
  Proof. The structure of the proof is similar to that of Proposition 4.1. We
                                                             nc
simply set N ′ to be equal to the proof term λm, uQ(m+1) (N ∀ m(Q(m+1)→Q(m)) m u)
and M ′ to be equal to M .

4.6   Down primitive recursion in terms of down primitive iteration
To simulate down primitive recursion in terms of down primitive iteration, we
instantiate the base and step of Down.prim iter respectively with (n, z) (for some
given n) and fn (i, c) => (i - 1, s (i - 1) c), where z and s are the base and
step of down prim rec’:
fun down_prim_rec’ n (z, s)
    = let fun visit m
              = if m = n then (n, z) else let val (i, c) = visit (m + 1)
                                          in (i - 1, s (i - 1) c)
                                          end
      in let val (i, c) = visit 0 in c end
      end
(* = #2 (Down.prim_iter n ((n, z), fn (i, c) => (i - 1, s (i - 1) c))) *)
Proof interpretation:
  Proposition 4.6. Given the proof

                        |M                         |N
                       Q(n)        ∀m(Q(m + 1) → Q(m))
                                                          (down-prim-rec)
                                      Q(0)
                                           |R
                                          P (n)
                                                    ∀+
                                         ∀nP (n)
find M ′ , N ′ and an appropriate Q′ such that
                       |M ′                        |N ′
                        ′           nc
                      Q (n)        ∀ m(Q (m + 1) → Q′ (m))
                                             ′
                                                             (down-prim-iter)
                                          Q′ (0)
                                            |R
                                          P (n)
                                                     ∀+
                                         ∀nP (n)
and from which it is possible to extract down prim rec’.



Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
      A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration         ·     101

  Proof. We propose only a sketch because the structure of the proof is the same
as the one displayed in Figure 5. The idea is to set
                                Q′ (0) ≡ ∃y(y = 0) ∧ Q(0)
and prove Q′ (0) by up primitive iteration:
    Case n. We have to prove ∃y(y = n) ∧ Q(n), which follows directly by n = n and
M Q(n) .
    Case m + 1 → m. Assume m (which we quantify non-computationally) and y ′
such that y ′ = m + 1 and Q(m + 1). We prove ∃y(y = m) ∧ Q(m). For the left
conjunct, it is enough to introduce y ′ − 1 for y. For the right conjunct, we need
to instantiate N with (y ′ − 1), obtaining Q(y ′ ) → Q(y ′ − 1). By the assumption
y ′ = m + 1, we have Q(m + 1) → Q(m) and instantiating it with Q(m + 1) we
obtain the thesis.



4.7   Up primitive iteration in terms of down primitive iteration
To simulate up primitive iteration in terms of down primitive iteration, we instan-
tiate the base and step of Down.prim iter respectively with (0, z) and fn (i, c)
=> (i + 1, s c), where z and s are the base and step of up prim iter’:
fun up_prim_iter’ (z, s) n
      = let fun visit m
            = if m = n then (0, z) else let val (i, c) = visit (m + 1)
                                        in (i + 1, s c)
                                        end
        in let val (i, c) = visit 0 in c end
        end
(* = #2 (Down.prim_iter n ((0, z), fn (i, c) => (i + 1, s c))) *)
This case is treated as the one in Section 4.4.

4.8   Down primitive iteration in terms up primitive iteration
To simulate down primitive iteration in terms of up primitive iteration, we use
Kleene’s trick: we instantiate the base and step of Up.prim iter respectively with
(n, z) and fn (i, c) => (i - 1, s c), where z and s are the base and step of
down prim iter’:
fun down_prim_iter’ n (z, s)
    = let fun visit m
              = if m = 0 then (n, z) else let val (i, c) = visit (m - 1)
                                          in (i - 1, s c)
                                          end
      in let val (i, c) = visit n in c end
      end
(* = #2 (Up.prim_iter ((n, z), fn (i, c) => (i - 1, s c)) n) *)
This case is treated as the one in Section 4.3.


                                            Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
102     ·      Chiarabini and Danvy

5.    PRIMITIVE RECURSION AND ITERATION WITH ACCUMULATORS
Here we present the proof-theoretical analogue of fold-left from functional program-
ming with lists, where the result is accumulated at call time instead of at return
time. We consider in turn the accumulator-based versions of each of the induction
principles reviewed in Section 3.

5.1    Up primitive recursion with accumulator
Here the problem is how to transform the following up primitive recursive induction
principle,
                          |M                  |N
                         P (0)       ∀n(P (n) → P (n + 1))
                                                             (up-prim-rec)
                                       ∀nP (n)
into another proof (of the same formula ∀nP (n)) but with a computational content
that is the accumulator-based version of up primitive recursion:
fun up_prim_rec_acc (z, s) n
    = let fun visit m i a
              = if m = 0 then a else visit (m - 1) (i + 1) (s i a)
      in visit n 0 z
      end
In these definitions, we use and manipulate two accumulators: i, to count from 0
to n, and a, to store the partial result at step i. Obviously, for i = n we have
a = s (n − 1)(. . . (s 0 z) . . .).
  So, given a proof of ∀nP (n), by the up primitive recursive induction principle in
terms of z : M P (0) and s : N ∀n(P (n)→P (n+1)) , we can build a new proof of ∀nP (n)
with content up prim rec acc through the following two steps:
(1) We prove the lemma ∀n∀m(P (m) → P (n + m)) by up primitive recursive
    induction:
    Case n = 0. We have to prove
                                         ∀m(P (m) → P (m))
      which is trivially proved by (λm, u.u).
      Case n + 1. Let us assume n, the recursive call p : ∀m(P (m) → P (n + m)), m
      and the accumulator y : P (m). We have to prove
                                            P (n + m + 1)
    We apply s to m and y, obtaining (s m y) : P (m + 1). Then we apply p to
    (m + 1) and s m y.
(2) Finally we derive the initial formula ∀nP (n) by assuming n and instantiating
    the formula proved in the first step on n, 0 and z : M P (0) .
5.2    Up primitive iteration with accumulator
We follow the same schema as in Section 5.1. The only difference is that in the
intermediate lemma (point 1), we have to quantify non computationally over m. In

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
      A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration         ·     103

other words, we have to prove the modified intermediate lemma:
                              ∀n∀nc m(P (m) → P (n + m))
The synthesized program embodies the up primitive iterative induction principle
with accumulator:
fun up_prim_iter_acc (z, s) n
    = let fun visit m a
              = if m = 0 then a else visit (m - 1) (s a)
      in visit n z
      end

5.3   Down primitive recursion with accumulator
Here the problem is how to transform the following down primitive recursive in-
duction principle,
                        |M                 |N
                       Q(n)       ∀y(Q(y + 1) → Q(y))
                                                          (down-prim-rec)
                                     Q(0)
into another proof, still of the formula Q(0), but with a computational content that
is the accumulator-based version of down primitive recursion:
fun down_prim_rec_acc n (z, s)
    = let fun visit m i a
              = if m = n then a else visit (m + 1) (i - 1) (s (i - 1) a)
      in visit 0 n z
      end
We propose an approach similar to the one in Section 5.1. We equip the function
down prim rec acc with two accumulators, denoted by i and a. The first one is
initialized with n at the beginning of the computation and decremented at each
iteration. The second one is initialized with z, of type P (n), and is dedicated to store
the partial results. The proof from which it is possible to synthesize up prim rec acc
is based on the following two steps:
(1) We prove the intermediate lemma ∀i(Q(i) → Q((i + 0) − n)) by down primitive
    recursive induction:
    Case y = n. We have to prove ∀i(Q(i) → Q(i)) that is given, by construction,
    by the following proof term λi, uQ(i) u.
    Case y + 1 → y. Given y, the induction hypothesis visit : ∀i(Q(i) → Q((i + y +
    1) − n)), i and u : Q(i), we prove Q((i + y) − n) by constructing the following
    proof term: (visit (i − 1) (N ∀y(Q(y+1)→Q(y)) (i − 1) u))Q((i+y)−n) .
(2) We instantiate the proof of the formula ∀i(Q(i) → Q((i + 0) − n)) on n and on
    z Q(n) , obtaining Q(0).
5.4   Down primitive iteration with accumulator
We follow the same schema as in Section 5.3. The only difference is that in the
intermediate lemma (point 1), we have to quantify non computationally over i. In
other words, we have to prove the modified intermediate lemma:
                              ∀nc i(Q(i) → P ((i + 0) − n))
                                            Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
104     ·      Chiarabini and Danvy

The procedure extracted from this new proof is the following down primitive iter-
ation principle with accumulator:
fun down_prim_iter_acc’ n (z, s)
    = let fun visit m a
              = if m = n then a else visit (m + 1) (s a)
      in visit 0 z
      end

6.    CASE STUDY: THE FACTORIAL FUNCTION
In this section we put into practice what we have seen so far, by revisiting the
factorial function:
                               
                                 1               if n = 0
                     fact(n) =
                                 n × fact(n − 1) if n > 0
We prove ∀n∃y(y = fact (n)) by up primitive induction over natural numbers:

                                                                         [u : y = fact(n)]
                                                                    (n + 1) × y = fact(n + 1)
                                                                                               ∃+
                                                                       ∃y(y = fact(n + 1))
                                                                                              →+
                                                                                               u
                                                                         (y = fact(n)) →
                                                                       ∃y(y = fact(n + 1))
                                                                                              ∀+
                                                                        ∀y(y = fact(n) →
                                   ∃−    [v : ∃y(y = fact(n))]         ∃y(y = fact(n + 1)))
                                                                                              ∃−
                                                       ∃y(y = fact(n + 1))
                                                                                     →+
      ∃+       1 = fact(0)                 ∃y(y = fact(n)) → ∃y(y = fact(n + 1))      v

                             ∃+                                                         +
                                                                                        ∀
        ∃y(y = fact(0))                  ∀n(∃y(y = fact(n)) → ∃y(y = fact(n + 1)))
                                                                                        up-prim-rec
                                     ∀n∃y(y = fact(n))

  Let us name this proof Proof fact1. The program extracted from Proof fact1
reads as follows:
fun fact1 n
    = if n = 0 then 1 else n * (fact1 (n - 1))
   In Proof fact1 we name B the proof of base and S the proof of step. We have
already seen in Section 4.2 how to express at the level of programs, via Kleene’s
trick, up primitive recursion in terms of up primitive iteration. In the same section,
we have seen how to do it also at the level of proofs. So replacing M with B, N
with S, and P (n) with fact(n) in Figure 5, we obtain a new proof, that we name
Proof fact2, with the following computational content:
fun fact2 n
    = let fun visit m
              = if m = 0 then (0, 1) else let val (i, c) = visit (m - 1)
                                          in (i + 1, (i + 1) * c)
                                          end
      in let val (i, c) = visit n in c end
      end




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
     A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration                     ·      105

  Proof fact2 is a proof with the following shape:
                                                                   |S
               |B                             ∀n(∃y(y = fact(n)) → ∃y(y = fact(n)))
         ∃y(y = fact(0))                                           |J
               |K                            ∀nc n((∃y(y = n) ∧ ∃y(y = fact(n))) →
   ∃y(y = 0) ∧ ∃y(y = fact(0))                     (∃y(y = n + 1) ∧ ∃y(y = fact(n + 1)))
                                                                                             (up-prim-iter)
                           ∀n(∃y(y = n) ∧ ∃y(y = fact(n)))              n
                                                                            ∀−
                                   ∃y(y = n) ∧ ∃y(y = fact(n))
                                                                   ∧−
                                                                    1
                                         ∃y(y = fact(n))
                                                               +
                                                           ∀
                                       ∀n∃y(y = fact(n))

  Where |K and |J can be deduced from Figure 5. Now, in Section 5.2, we have
seen how to transform an up primitive iterative proof of the form
                            |M                      |N
                           P (0)        ∀nc n(P (n) → P (n + 1))
                                                                            (up-prim-iter)
                                           ∀nP (n)
into another proof with an accumulator-based extracted program. Now replacing
M with K[B], N with J[S], and P (n) with ∃y(y = n)∧fact(n) in the above schema,
and then applying the proof transformation described in Section 5.2 to the proof
so instantiated, we obtain a new proof of the formula ∀n(∃y(y = n) ∧ fact(n)), that
we name Proof fact3. Thus, from the derivation
                                       Proof fact3
                             ∀n(∃y(y = n) ∧ ∃y(y = fact(n)))                     n
                                                                                     ∀−
                                  ∃y(y = n) ∧ ∃y(y = fact(n))
                                                                             ∧−
                                                                              1
                                        ∃y(y = fact(n))
                                                          ∀+
                                       ∀n∃y(y = fact(n))
we extract the following iterative and accumulator-based version of the factorial
function:
fun fact3 n
    = let fun visit m (i, c)
              = if m = 0 then (i, c) else visit (m - 1) (i + 1, (i + 1) * c)
      in let val (i, c) = visit n (0, 1) in c end
      end
   We would like to point out once more that, even if the program obtained after
the application of the above transformation is not particularly complicated, our
transformation is completely mechanical and acts at the level of proofs. The proof
itself constitutes a certificate of the correctness of the extracted program.




                                                    Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
106     ·      Chiarabini and Danvy

7.    CONCLUSIONS
We have presented a set of mechanical methods to transform the proof of an in-
duction principle that corresponds to a certain recursion principle into a proof of
another induction principle that corresponds to another recursion principle. In
this work, we considered the well-known up/down primitive and up/down iterative
recursion principles and their corresponding proofs. Because each of these transfor-
mations was done at the level of proofs, we did not transform programs but proofs
of programs: the extracted programs are thus not only correct, but also unadul-
terated. There is thus no need for adultery to make them run more efficiently.
Following the same pattern, we have then transformed each recursive principle into
an equivalent one that uses an accumulator. Again, each of the transformations
was done at the level of proofs. The extracted programs are tail recursive.
   In this article, we have concentrated on the factorial function as our running ex-
ample, but the up and down induction principles, of course, apply to any program
whose number of iterations is bounded by a natural number, as in, e.g., the Eu-
clidean algorithm [3]. To our knowledge, all the proofs here presented are new, and
are not treated in the literature. The aim of this work is theoretical, but as illus-
trated in Section 6, the mechanical methods presented here could find applications
in the formal development of programs using proof assistants.

Acknowledgments
This work was carried out in the winter of 2008–2009 while the first author was
visiting the second in the Department of Computer Science at Aarhus University [2,
Chapter 8]. Thanks are due to the anonymous referees for their comments. The first
author is also grateful to Helmut Schwichtenberg for his feedback on a preliminary
version of this manuscript, and the second to Mayer Goldberg for introducing him
to the generalization of Kleene’s trick we have pervasively used here [5].

A.    BASICS FOR PROGRAM EXTRACTION FROM CONSTRUCTIVE PROOFS
This appendix contains the material informally presented in Sections 2.3.1, 2.3.2,
and 2.3.3.
A.1    Type of a Formula
                      
                        αP If P is a predicate variable with assigned type αP
         τ (P (~x)) =
                        ε Otherwise
                      
               ρ        ρ         If τ (ϕ) = ε
         τ (∃x ϕ) =
                        ρ × τ (ϕ) Otherwise
                      
               ρ        ε          If τ (ϕ) = ε
         τ (∀x ϕ) =
                        ρ → τ (ϕ) Otherwise
       τ (∃nc xρ ϕ) = τ (ϕ)
       τ (∀nc xρ ϕ) = τ (ϕ)
                      
                       τ (ϕ)          If τ (ψ) = ε
         τ (ϕ ∧ ψ) =     τ (ψ)         If τ (ϕ) = ε
                         τ (ϕ) × τ (ψ) Otherwise
                      

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
      A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration                 ·     107
                   
                    τ (ψ)         If τ (ϕ) = ε
       τ (ϕ → ψ) =   ε             If τ (ψ) = ε
                     τ (ϕ) → τ (ψ) Otherwise
                   

A.2   Extraction map
                                                   τ (ϕ)
                            [[uϕ ]] = xuτ (ϕ) (xu          uniquely associated with ϕ)
                                          [[M   ]]          If τ (ϕ) = ε
                                      
                        [[λuϕ M ]] =           τ (ϕ)
                                          λxu [[M ]] Otherwise
                                      
                                          [[M ]]       If τ (ϕ) = ε
                 [[M ϕ→ψ N ϕ ]] =
                                          [[M ]][[N ]] Otherwise
                                      
                                       [[N ]]               If τ (ϕ) = ε
                  [[hM ϕ , N ψ i]] =       [[M ]]            If τ (ψ) = ε
                                           h[[M ]], [[N ]]i Otherwise
                                      
                                      
                                          [[M ]] If τ (ϕ) = ε or τ (ψ) = ε
                      [[M ϕ∧ψ i]] =
                                          πi [[M ]] Otherwise
               [[(λxρ M )∀xϕ ]] = λxρ [[M ]]
                    [[M ∀xϕ t]] = [[M ]]t
                           nc xϕ
             [[(λxρ M )∀           ]] = [[M ]]
                         ∀nc xϕ
                   [[M            t]] = [[M ]]
Content of the proof constants:

                                    λxρ f ρ→τ (ψ) .f x
                                
                                                                              If τ (ϕ) = ε
             [[∃−
                xρ ,ϕ,ψ ]] =        λxρ×τ (ϕ) f ρ→τ (ϕ)→τ (ψ) .f (π0 x)(π1 x) Otherwise
                                    λxρ x
                                
                                                        If τ (ϕ) = ε
                [[∃+
                   xρ ,ϕ ]] =
                                    λxρ y τ (ϕ) .hx, yi Otherwise
                                    λxτ (ψ) .x
                                
                                                               If τ (ϕ) = ε
         [[(∃nc )−
                 xρ ,ϕ,ψ ]] =       λxτ (ϕ) f τ (ϕ)→τ (ψ) .f x Otherwise
           [[(∃nc )+
                   xρ ,ϕ ]] = λx
                                 τ (ϕ)
                                       x
                  [[IFϕ ]] = λbB , lτ (ϕ) , rτ (ϕ) .(if b l r) If τ (ϕ) 6= ε
           [[Indn,ϕ(n) ]] = RσN
                               σ
             [[Indl,ϕ(l) ]] = RL(ρ)
            [[Indt,ϕ(t) ]] = RσB

A.3   Modified Realizability

               r mr P (~t) = P (~t)
                             
                                ε mrϕ[x/r]        If τ (ϕ) = ε
             r mr (∃x.ϕ) =
                                π1 r mr ϕ[x/π0 r] Otherwise
                             
                                ∀x.ε mr ϕ If τ (ϕ) = ε
             r mr (∀x.ϕ) =
                                ∀x.r mr ϕ Otherwise

                                                    Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
108     ·      Chiarabini and Danvy

                                     ∃nc x.ε mrϕ
                                 
                    nc                                 If τ (ϕ) = ε
            r mr (∃ x.ϕ) =
                                     ∃nc x.r mr ϕ      Otherwise
                                     ∀nc x.ε mr ϕ
                                 
                      nc                               If τ (ϕ) = ε
            r mr (∀x .ϕ) =
                                     ∀nc x.r mr ϕ      Otherwise
                            
                             ε mr ϕ → r mr ψ                     if τ (ϕ) = ε
            r mr (ϕ → ψ) =    ∀x.x mr ϕ → ε mr ψ                  If τ (ϕ) 6= ε = τ (ψ)
                              ∀x.x mr ϕ → rx mr ψ                 Otherwise
                            
                            
                             ε mr ϕ ∧ r mr ψ                     If τ (ϕ) = ε
             r mr (ϕ ∧ ψ) =   r mr ϕ → ε mr ψ                     If τ (ψ) = ε
                              π0 r mr ϕ → π1 r mr ψ               Otherwise
                            

B.    ON THE ORDER OF MULTIPLICATIONS IN EXTRACTED PROGRAMS
The computation associated to the factorial function can be syntactically charac-
terized with the following data type:
datatype residual = LIT of int
                  | TIMES of int * residual
For example, the computation associated to the factorial function of Section 3.1
can be visualized by making it map an integer to a syntactic witness of the trail of
multiplications it entails:
(* fact_gen : int -> residual *)
fun fact_gen n
    = Up.prim_rec (LIT 1, fn i => fn c => TIMES (i + 1, c)) n

Applying fact gen to 5, for example, yields the following residual trail:
TIMES (5, TIMES (4, TIMES (3, TIMES (2, TIMES (1, LIT 1)))))
The same residual trail is obtained for the factorial functions defined in Section 3.2
and in Section 6.
   Likewise, the computation associated to the factorial function of Section 3.3 can
also be visualized by making it map an integer to a syntactic witness of the trail of
multiplications it entails:
fun fact_gen n
    = down_prim_rec (LIT 1, fn i => fn c => TIMES (i + 1, c)) n

Applying fact gen to 5, for example, yields the following residual trail:
TIMES (1, TIMES (2, TIMES (3, TIMES (4, TIMES (5, LIT 1)))))

The same residual trail is obtained for the factorial function defined in Section 3.4.
  As can be readily seen, the order of the multiplications is not the same. It
does not matter for the factorial function since multiplication is associative and
commutative, but it would for other functions, e.g., to process lists.




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
    A Proof-Theoretic Accountof Primitive Recursion and Primitive Iteration         ·     109

References
 [1] Andrea Asperti and Enrico Tassi. Modified realizability and inductive types.
     Technical report, Dipartimento di Scienze dell’Informazione, Università degli
     Studi di Bologna, 2006.
 [2] Luca Chiarabini. Program Development by Proof Transformation. PhD the-
     sis, Fakultät für Mathematik, Informatik und Statistik, Ludwig Maximilians
     Universität, München, Germany, 2009.
 [3] Olivier Danvy and Mayer Goldberg. Partial evaluation of the Euclidean algo-
     rithm. Lisp and Symbolic Computation, 10(2):101–111, 1997.
 [4] Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten
     Standpunkts. Dialectica, 12:280–287, 1958.
 [5] Mayer Goldberg. Recursive Application Survival in the λ-Calculus. PhD the-
     sis, Computer Science Department, Indiana University, Bloomington, Indiana,
     May 1996.
 [6] Stephen C. Kleene. Origins of recursive function theory. Annals of the History
     of Computing, 3(1):52–67, January 1981.
 [7] Georg Kreisel. Interpretation of Analysis by means of Functionals of Finite
     Type. In Arend Heyting, editor, Constructivity in Mathematics, 1959.
 [8] Zohar Manna and Richard J. Waldinger. Towards automatic program synthe-
     sis. Communications of the ACM, 14(3), 1971.
 [9] Iman Poernomo, John N. Crossley, and Martin Wirsing. Adapting Proofs-as-
     Programs : The Curry-Howard Protocol. Springer, 2005.
[10] Morten Heine B. Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard
     Isomorphism. Elsevier, 1998.
[11] Helmut Schwichtenberg.          Minimal logic for computable functionals.
     http://www.mathematik.uni-muenchen.de/~chiarabi/mlcf.pdf, February
     2008.
[12] Anne S. Troelstra. Constructivism and proof theory, 2003.
[13] Dirk van Dalen. Logic and Structure. Springer, 2008.




                                          Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
