The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

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