The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Arnaud,

> I've only have a quick glimpse at the proof. Let me try to summarise my understanding of it:

> you prove to each total recursive function (in the sense that its graph is a total functional relation)

> then there corresponds a normalisable lambda-term (in the sense of the accessibility predicate)

> and then you define a function by recursion over this accessibility predicate.

>

> Is that correct?

This is indeed roughly the idea but let me point out a detail
of critical importance, which you might have noticed but I point
it out anyway.  

"Normalisable" is typically a *reachability predicate* (there
is a path which leads to a normal form/maximal element)
whereas "strongly normalisable" is an *accessibility predicate*
(every path leads to a normal form).

It is typically not possible to define a function over Type or Set
by induction over a reachability predicate because the
path information is not available at the computational
level. On the other hand, I did not even think of representing
all total recursive functions by strongly normalisable
lambda terms (I not sure that this is impossible anymore
as Coq itself should have the SN property right ?).

But one trick here is to remark that "normalisable" and
"strongly normalisable" are equivalent predicates for
deterministic (ie functional) relations.

And lambda calculus has deterministic and complete
reduction strategies for beta reduction, for instance
leftmost reduction.

So the recursion is not over beta-reachability of a
normal form but over accessibility for leftmost
beta reduction (actually the converse of that relation).

Of course to show that leftmost reduction
is complete, the way it is done in Krivine's book is
to use intersection type system Domega (which are

useful for head reduction as well ...)

> This makes use of the singleton-elimination of accessibility.

> A subtle point in Coq (in particular since it's hard to reconcile

> with judgemental proof irrelevance, and this is an extension of

> Coq which has been mooted a number of times). For instance,

> you mention that if totality of the recursive function is proved

> with axioms, then a Coq function still emerges. This would be

> right, but I'd expect the function to block on some natural numbers

> as it would need to match on the axioms.

Actually the remark about axioms is made in a comment inside
the code ... so welcome inside the code ;-)

This is a point I would like to discuss more deeply. Let me
first insist on what I understand as "singleton-elimination".
Practically, this means performing a destruct on an hypothesis
in Prop while your conclusion lies in Type or Set. This is generally
not accepted unless the predicate is a singleton, ie it only
has one constructor (and the constructor does not contain
computational information).

And indeed, the default way to define a function by induction over
an accessibility predicate is to first perform a destruct on that
predicate (see the code acc_rect_* below).

But there is *another way to proceed* by induction over an
accessibility predicate that does not use singleton elimination.
Actually, this is the way Fix_F is defined in the Standard
Library of Coq. In that case, there is also a destruct but
it occurs later while building a Prop (see the code of
acc_rect_alt_* below).

In general, functions defined by induction over an accessibility
predicate have a behavior that does not depend on the proof
of that predicate and it is removed by the extraction mechanism
(this is the case for any predicate in Prop due to proof irrelevance

of extraction). The predicate is just a guarantee that the reduction

terminates.

But if you use the second method (acc_rect_alt), it seems to
me that there would be no need to advance in the computation
of the accessibility proof while reducing a term defined by
induction on that predicate, even within Coq internal evaluation
strategies. I am not sufficiently aware of Coq's internal evaluation
mechanism to be certain of that but I do not think that added
axioms would block the evaluation because the proof of
accessibility is never needed to reduce the term. It might
however saturate the memory if it is never reduced ...

Of course, the way the lambda terms are build might also

saturate the memory ...
 
Maybe you know more on that point (Eval compute, etc ...) but

I am pretty convinced that singleton elimination is not needed.

Dominique

As a complement, here are the two ways to proceed by recursion

over an accessibility predicate

Section acc.

  Variable (X : Type) (R : X -> X -> Prop).

  Unset Elimination Schemes.

  Inductive acc (x : X) : Prop :=
    | acc_intro : (forall y, R y x -> acc y) -> acc x.

  Set Elimination Schemes.

  Variable (P : X -> Type) (f : forall x, (forall y, R y x -> P y) -> P x).

  (** This is the recursion principle that USES singleton elimination
   ** It is the one that is automatically generated by Coq when
   ** elimination schemes are set
   **)

  (* First in proving style *)

  Fixpoint acc_rect_proof x (Hx : acc x) : P x.
  Proof.
    destruct Hx as [ Hx ].  (* the destruct occurs in Type context *)
    apply f.
    intros y Hy.
    apply acc_rect_proof, Hx, Hy.
  Qed.

  (* Then in programming style *)

  Fixpoint acc_rect_prog x (Hx : acc x) : P x :=
    match Hx with
      | acc_intro _ H => f _ (fun y Hy => acc_rect_prog _ (H _ Hy))
    end.

  (** This is the recursion principle that DOES NOT USE singleton elimination
   ** It is for instance what is used in the Wf library to program the Fix_F
   ** operator
   **)

  Fixpoint acc_rect_alt_proof x (Hx : acc x) : P x.
  Proof.
    apply f.
    intros y Hy.
    apply acc_rect_alt_proof.
    destruct Hx as [ Hx ].   (* the destruct occurs in Prop context *)
    apply Hx, Hy.
  Qed.

  (* Then in programming style *)

  Fixpoint acc_rect_alt x (Hx : acc x) : P x :=
    f x (fun y Hy => acc_rect_alt _
                        match Hx with
                          | acc_intro _ H => H _ Hy
                        end).

End acc.