The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Hello all,
 I was thinking on the problem of fixpoint reduction when the argument
 is a singleton.

First point, we can put the computation outside of the "match with"
with the singleton type:

> Goal forall A (P:A->A->Prop) (a:A) (x:Acc P a) (T:Type)
>  (h:(forall b, P b a -> Acc P b) -> T),
>  match x with Acc_intro f => h f end =
>  h (match x with Acc_intro f => f end).
> Proof.
>  intros.
>  destruct x.
>  split.
> Qed.

For example:

> Fixpoint mult (m n:nat) (acc:Acc (fun m n => m<n) m) {struct acc}:
>  nat := match acc with
>   | Acc_intro f =>
>    match m as m0
>    return (forall x, x < m0 -> Acc (fun m n => m<n) x) -> nat with
>    | O => fun _ => O
>    | S m' => fun f => n + (mult m' n (f m' (le_n (S m'))))
>    end f
>  end.

can be changed into:

> Definition mult_aux mult_ n α
> : (forall b, b<α -> Acc (fun m n => m<n) b) -> nat :=
>    match α as m0
>    return (forall x, x < m0 -> Acc (fun m n => m<n) x) -> nat with
>    | O => fun _ => O
>    | S m' => fun f => n + (mult_ m' n (f m' (le_n (S m'))))
>    end
> . 
> Fixpoint mult2 (m n:nat) (acc:Acc (fun m n => m<n) m) {struct acc}:
> nat :=
>  (mult_aux mult2 n m)
>  match acc with
>  | Acc_intro f => f
>  end
> .

that way, we shouldn't be blocked by the pattern matching on acc, since
it is not at head place.

For instance "mult2 (S m) n [x]" could be reduced in
"n + mult2 m n (match [x] with Acc_intro f => f m (le_n m) end)"
instead of
"match [x] with Acc_intro f => n + mult2 m n (f m (le_n m)) end"
which would still stuck as its head is a match on an opaque term.

In fact it is not the case since iota reduction can be triggered only
if the structural argument is an application to a constructor, as far
as I understand the system.

So I was wondering if there could be some relaxed restriction which
could allow such a reduction.

I understand you cannot wildly reduce any term, since it could give non
terminating reductions, and unification would become harder
(undecidable?).

But in some case (for example when arguments are closed, that is you
don't have any free variable in them), there shouldn't be problems I
think.

In the same idea, does "fix" really require to be part of head normal
forms?

That is "(fix f x := T[f,x]) a" cannot be reduced if a is not an
application to a constructor. But at first glance we could change it
into "(fun f x => T[(fix f x := T[f,x]),x]) a" and then β reduce it.
My point is that you cannot encounter a fully applied occurence of f
wich is not inside a branch of a "match with" (a "fun x => f (g x)" is
of course not considered fully applied). So allowing unfolding of fix
in head position wouldn't lead to a non terminating reduction.
I am not sure what I have written is right, but if there is some way to
reduce these fixpoints without requiring to inspect the structural term
(so that we could make it opaque), but require it to guarantee
termination, I think that it would help a lot of people.