The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

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