The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Sun, 13 Jun 2004, 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.

Well, for the moment, nothing fully automatic exists to replace nat by
Integer (or Ocaml equivalent). It could be done, but would not be so
simple:

- In the case where you have only a type domain and a few operations, e.g:
Parameter my_nat : Set.
Parameter my_zero : my_nat.
Parameter my_plus : my_nat -> my_nat -> my_nat.
Then it is trivial to replace these axioms by efficient implementations
when extracting:
Extract Constant my_nat => "Integer"
Extract Constant my_zero => "0"
Extract Constant my_plus => "(+)"

- But Coq nat is more than a type with a few operations: it has an
inductive structure (data Nat = O | S Nat) and you can do matching on a
nat value. So you need to translate this matching to Haskell Integer.
Of course this can be done, but if you do it systematically, you loose all
the interest of a translation to Integer. For example, plus in nat is
defined by matching, and you would then obtain a linear-time plus in
Haskell instead of the quasi-constant-time (+).

- So a good solution to your question would involve identifying as many
critical fonctions and possible like plus, mult, etc, and at the same time
keeping the inductive structure of nat. I haven't coded that yet.

- Instead of using an axiomatic my_nat like above (really painful since
you start with __no__ library results), a not-so-bad trade-off is to use
Coq binary numbers instead of Peano unary numbers. The currently available
types are:
  positive (integers > 0)
  N  (integers >= 0)
  Z  (any integers)
Then, in all extraction examples that contains arithmetic computations, I
add two manual functions for encoding the program input and decoding the
output before printing it, e.g:
 I2Z :: Integer -> Z
 Z2I :: Z -> Integer
Of course, computations using positive or Z cannot compare with hardware
integer, but they are already quite usable (fibonacci(10000) in a few
seconds, see user's contribution Bordeaux/Additions).


>
> 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?
>

- "usual" recursive functions (i.e. those with a structurally decreasing
argument) can be defined directly via the Fixpoint construction.
- "tricky" ones (i.e. based on a clever termination proof) can always
be defined by using the Well-Foundedness functions.
- In your particular case of ackermann, you can in fact use a (classical)
trick to define it via two nested fixpoints, since there is always at
least one of the two arguments that strictly decreases:

Fixpoint ack (m:nat) : nat -> nat :=
   match m with
     | 0 =>  fun n => S n
     | S m => fix ack' (n:nat) : nat :=
                       match n with
                         | 0 => ack m 1
                         | S n => ack m (ack' n)
                       end
   end.

The same trick is used for example in the "merge" function over two sorted
lists.

Pierre Letouzey