The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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.  In conclusion, theoretically it is possible but there could
be a situation where it is not a very good idea for programming
(constructive mathematics?).


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