The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Fri, May 19, 2023 at 6:45 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Thanks Yannick and Mario! I was somehow under a (flawed) assumption
that functions that computes fuel were alway primitive recursive, but
it may or may not be the case. So my understanding is: theoretically
it is possible to turn an non-primitive recursive function into a
primitive recursive function (Kleene's normal form theorem) by means
of using nat as a fuel, but computing the fuel may be as complicated
as computing the original function, i.e., it may not be primitive
recursive.  I also came up with a counterexample for my flawed
assumption: I can write a division function on natural numbers using
the subtraction function (I know it is not a great way to write
division function):

Theorem nat_div :  nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    cut (Acc lt a);
    [revert a |].
    +
      refine(fix nat_div a (acc : Acc lt a) {struct acc} :
        forall b : nat, 0 < b -> nat * nat :=
        match acc with
        | Acc_intro _ f => fun b Ha =>
          match (lt_eq_lt_dec a b) with
          | inleft Hb =>
            match Hb with
            | left Hc => (0, a)
            | right Hc => (1, 0)
            end
          | inright Hb =>
            match nat_div (a - b) _ b Ha with
            | (q, r) => (S q, r)
            end
          end
        end).
      assert (Hc : (a - b) < a).
      abstract nia.
      exact (f (a - b) Hc).
    +
      eapply lt_wf.
  Defined.

But if I want to turn this into a primitive recursive function by
means of fuel, then computing fuel itself requires a division
function. 

Not in this case.  You  can always over-approximate how much fuel you need.  In this case taking "a" as the fuel should suffice. 

 

In conclusion, theoretically it is possible but there could
be a situation where it is not a very good idea for programming
(constructive mathematics?).

Both for programming and for mathematics, I'd rather use well-founded recursion than nat-valued fuel.  Think of well-founded recursion as recursing on a fuel that is a proof of accessibility in an order of your choice.  This gives more flexibility than recursing on silly Peano natural numbers.  In particular, because you can choose the order, proving accessibility is generally easier than proving the existence of a large enough nat-valued fuel.

For what it's worth...

- Xavier Leroy

 

Best,
Mukesh



On Thu, May 18, 2023 at 7:12 PM Yannick Forster <yannick AT yforster.de> wrote:
>
> Sure, computing the fuel is not going to be primitive recursive because the fuel is large. But given a defined Coq (or any other constructive type theory) function f : nat -> nat it can be turned into a primitive recursive function f' : nat -> nat -> nat such that f' n x = S v, then for all n' >= n, f' n x = S v and forall x, exists n, f' n x = S (f x).
>
> Here, f' is a primitive recursive function expecting fuel n and an argument x, and then computes f for large enough fuel (and else returns 0). The n might, as you say, have to be very large, but constructing f' is always possible.
>
>
> On 18 May 2023 20:04:06 Mario Carneiro <di.gama AT gmail.com> wrote:
>>
>> This doesn't sound quite correct. While Kleene's T tells you that for any terminating computation there is *some* bound for the fuel you need to compute the value, the bound itself might be quite large, and so you are reduced to computing very fast growing functions, to compute the initial fuel value you use to power the rest of the computation. These functions need just as much "power" from the theory as the original recursion did. There are functions which are not primitive recursive, like the ackermann function, and if you rewrite them to use a fuel variable you will need to supply a function which grows about as fast as the ackermann function to get the initial fuel value, and that function is also not primitive recursive.
>>
>> Now, Ackermann's function is computable in Coq because it has higher order functions and hence goes beyond the traditional conception of primitive recursive function, but I think you might still need more than just N-indexed inductions to get the full power of Coq terminating functions. There are inductive types with a much larger rank than N around, and I don't think you can get epsilon_0 induction simply by composing inductions of rank omega.
>>
>> On Thu, May 18, 2023 at 1:48 PM Yannick Forster <yannick AT yforster.de> wrote:
>>>
>>> Hi Mukesh,
>>>
>>> in computability theory this intuition is behind Kleene's normal form theorem: https://en.m.wikipedia.org/wiki/Kleene%27s_T_predicate
>>>
>>> You can prove the normal form theorem for computable functions in Coq when defining them using some model of computation. But since given any concrete Coq function (over natural numbers or some suitable datatype isomorphic to numbers) you could have implemented it as a function in a model of computation provided enough time and endurance, this means you can re-write any definable Coq function as a fueled primitive recursive function, yes.
>>>
>>> Best
>>> Yannick
>>>
>>> On 18 May 2023 19:35:56 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
>>>
>>>> Hi everyone,
>>>>
>>>> Is it always possible to turn a non-primitive (terminating) recursive
>>>> function into a primitive recursive function by passing a natural
>>>> number as a fuel? If so, is there any formal underpinning for this,
>>>> i.e., turning a non-primitive (terminating) recursive function into a
>>>> primitive recursive function by passing a natural number, or is it
>>>> just obvious? My intuition says it's true but I am very keen to see
>>>> some formal reasoning.
>>>>
>>>> For example, I can write a function that computes a byte list from a
>>>> (binary) natural number like this [1] (I call it non-primitive
>>>> (terminating) recursive function but I may not be correct with my
>>>> terminology):
>>>>
>>>> Definition length_byte_list_without_guard : N -> list byte.
>>>>  Proof.
>>>>     intro np.
>>>>     cut (Acc lt (N.to_nat np));
>>>>     [revert np |].
>>>>     +
>>>>       refine(fix length_byte_list_without_guard np (acc : Acc lt (N.to_nat np))
>>>>         {struct acc} :=
>>>>       match acc with
>>>>       | Acc_intro _ f =>
>>>>         match (np <? 256) as npp
>>>>           return _ = npp -> _
>>>>         with
>>>>         | true => fun Ha => List.cons (np_total np Ha) List.nil
>>>>         | false => fun Ha =>
>>>>             let r := N.modulo np 256 in
>>>>             let t := N.div np 256 in
>>>>             List.cons (np_total r _) (length_byte_list_without_guard t _)
>>>>         end eq_refl
>>>>       end).
>>>>       ++
>>>>         apply N.ltb_lt, (nmod_256 np).
>>>>       ++
>>>>         apply N.ltb_ge in Ha.
>>>>         assert (Hc : (N.to_nat t < N.to_nat np)%nat).
>>>>         unfold t. rewrite N2Nat.inj_div.
>>>>         eapply Nat.div_lt; try abstract nia.
>>>>         exact (f (N.to_nat t) Hc).
>>>>     +
>>>>       apply lt_wf.
>>>>  Defined.
>>>>
>>>> But I can also write the same function by passing a natural number [2]
>>>> (from top level,
>>>> I just need to ensure the right amount of fuel):
>>>>
>>>> Fixpoint byte_list_from_N_fuel (n : nat) (up : N) : list byte :=
>>>>   match n with
>>>>   | 0%nat => [np_total (N.modulo up 256) (nmod_256_dec up)]
>>>>   | S n' =>
>>>>     let r := N.modulo up 256 in
>>>>     let t := N.div up 256 in
>>>>     List.cons (np_total r (nmod_256_dec up)) (byte_list_from_N_fuel n' t)
>>>>   end.
>>>>
>>>> Best,
>>>> Mukesh
>>>>
>>>> [1] https://github.com/mukeshtiwari/Coq-automation/blob/master/Opaque.v#L75
>>>> [2] https://github.com/mukeshtiwari/Formally_Verified_Verifiable_Group_Generator/blob/main/src/Sha256.v#L239
>>>
>>>
>