The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Stefan Karrmann wrote:
> Hello,
>
> as a newbie to coq I have some questions. As I'm used to functional
> programs I tried to start with function definitions and extraction.
>
> How can I switch from coq's nat to Haskell's Integer type? The former
> uses much more memory.
>
> How can I define recursive functions, e.g. the Ackermann function?
> I found a definition which uses streams, but my try to define it
> directly failed. Where can I find some hints? Is well-foundmess (Wf)
> the right starting point?

You can use also a primitive recursive polymorphic scheme


Fixpoint iterate (A:Set)(f:A->A)(n:nat)(x:A){struct n} : A :=
  match n with
  | O => x
  | S p => f (iterate A f p x)
  end.


Definition ackermann (n:nat) : nat->nat :=
  iterate (nat->nat)
          (fun (f:nat->nat)(p:nat) => iterate nat f (S p) 1)
          n
          S.


It  also possible to use a well founded order on pairs of natural 
numbers (using Coq standard library) and define ackerman of type
nat * nat -> nat (or Z * Z -> Z)

Pierre





> ------------------------------------------------------------------------------
> Module Ackermann.
>
> (*
> ackermann 0 n = n+1
> ackermann m 0 = ackermann (m-1) 1
> ackermann m n = ackermann (m-1) (ackermann m (n-1))
> *)
>
> Require Import Arith.
>
> Section Ackermann1.
>
> Require Import Streams.
>
> CoFixpoint nats_from (n:nat) : Stream nat :=
>    Cons n (nats_from (n+1)).
>
> CoFixpoint col_from (n : nat)(x:Stream nat) : Stream nat :=
>    let v := Str_nth n x
>    in Cons v (col_from v x).
>
> CoFixpoint ack_from (c:Stream nat) : Stream (Stream nat) :=
>    Cons c (ack_from (col_from 1 c)).
>
> Definition ack_tab : Stream (Stream nat) :=
>    ack_from (nats_from 1).
>
> Definition ack (m n : nat) : nat :=
>    Str_nth n (Str_nth m ack_tab).
>
> (* Eval compute in ack 2 2.  *)
>
> End Ackermann1.
>
> (*
> Extraction "ackermann" ack.
> Extraction Language Haskell.
> Extraction "ackermann" ack.
> *)
>
> Section Ackermann2.
>
> Require Import Wf.
>
> Definition A : Set := prod nat nat.
>
> Definition P (A:Set) : Type := nat.
>
> Definition R (x y : A) : Prop :=
>    ((fst x) < (fst y))
>    \/ ((fst x = fst y)
>       /\ (snd x < snd y) ).
>
> Definition F (x:A) (f: A -> nat) : nat :=
>    match x with
>    | (0,n) => n+1
>    | (m,0) => f (m-1,1)
>    | (m,n) => f (m-1,f (m,n-1))
>    end.
>
> (*
> This fails:
> *)
>
> Fixpoint ack' (x:A) : nat :=
>    F x ack'.
>
> Definition ack2 (m n:nat):nat :=
>    ack' (m,n).
>
> End Ackermann2.
>
> End Ackermann.
> ------------------------------------------------------------------------------
>
> Sincerly,



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran