A $\mu$-recursive function converges at an input, how to find the output?

Question

Summary: I want to implement an interpreter for $\mu$-recursive functions which, for any $\mu$-recursive function $f$ and input $\mathbf{x}$, returns $f \left( \mathbf{x} \right)$ if it is defined.

Let's define MuRec : nat -> Set represent the syntax of $\mu$-recursive functions by:

Inductive MuRec : nat -> Set :=
  | MR_succ : MuRec 1
  | MR_zero : MuRec 0
  | MR_proj {n : nat} (i : Fin.t n) : MuRec n
  | MR_compose {n : nat} {m : nat} (g : MuRecs n m) (h : MuRec m) : MuRec n
  | MR_primRec {n : nat} (g : MuRec n) (h : MuRec (S (S n))) : MuRec (S n)
  | MR_mu {n : nat} (g : MuRec (S n)) : MuRec n
with MuRecs : nat -> nat -> Set :=
  | MRs_nil {n : nat} : MuRecs n 0
  | MRs_cons {n : nat} {m : nat} (f : MuRec n) (fs : MuRecs n m) : MuRecs n (S m).

and define the semantics of $\mu$-recursive functions by:

Inductive MuRecSpec : forall n : nat, MuRec n -> Vector.t Value n -> Value -> Prop :=
  | MR_succ_spec x
    : MuRecSpec 1 (MR_succ) [x] (S x)
  | MR_zero_spec
    : MuRecSpec 0 (MR_zero) [] 0
  | MR_proj_spec n xs i
    : MuRecSpec n (MR_proj i) xs (xs [@ i ])
  | MR_compose_spec n m g h xs ys z
    (g_spec : MuRecsSpec n m g xs ys)
    (h_spec : MuRecSpec m h ys z)
    : MuRecSpec n (MR_compose g h) xs z
  | MR_primRec_spec_O n g h xs z
    (g_spec : MuRecSpec n g xs z)
    : MuRecSpec (S n) (MR_primRec g h) (0 :: xs) z
  | MR_primRec_spec_S n g h xs z a acc
    (ACC : MuRecSpec (S n) (MR_primRec g h) (a :: xs) acc)
    (h_spec : MuRecSpec (S (S n)) h (a :: acc :: xs) z)
    : MuRecSpec (S n) (MR_primRec g h) (S a :: xs) z
  | MR_mu_spec n g xs z
    (g_spec : MuRecSpec (S n) g (z :: xs) 0)
    (MIN : forall y, y < z -> exists p, p > 0 /\ MuRecSpec (S n) g (y :: xs) p)
    : MuRecSpec n (MR_mu g) xs z
with MuRecsSpec : forall n : nat, forall m : nat, MuRecs n m -> Vector.t Value n -> Vector.t Value m -> Prop :=
  | MRs_nil_spec n xs
    : MuRecsSpec n 0 MRs_nil xs []
  | MRs_cons_spec n m xs y ys f fs
    (f_spec : MuRecSpec n f xs y)
    (fs_spec : MuRecsSpec n m fs xs ys)
    : MuRecsSpec n (S m) (MRs_cons f fs) xs (y :: ys).

We say $f \left( \mathbf{x} \right)$ is defined as $z$ if $\mathtt{MuRecSpec} \, n \, f \, \mathbf{x} \, z$ holds for $n$-ary $\mu$-recursive function $f$ and input $\mathbf{x}$ and denote by $$ f \left( \mathbf{x} \right) = z . $$

Now let $f : \mathtt{Murec} \, n$ with $n \in \mathbb{N}$.

Question: Given $\mathbf{x} \in \mathbb{N}^n$, if there exists $z \in \mathbb{N}$ s.t. $f \left( \mathbf{x} \right) = z$ holds, then can we find such $z$?

---

I know we could assume the following axiom:

ConstructiveIndefiniteDescription := forall A : Type, forall P : A -> Prop, (exists x, P x) -> { x : A | P x }.

But I want to prove

Theorem MuRecInterpreter (n : nat) (f : MuRec n) (xs : Vector.t nat n)
  (CONVERGE : exists z, MuRecSpec n f xs z)
  : { z : nat | MuRecSpec n f xs z }.

without axioms. Is it possible?

Answer 1

You are lucky: this should be provable, entirely axiom-free! Albeit with some sweat.

The core idea is that while the general axiom of constructive indefinite description you mention is not provable in Coq, a variant for decidable propositions over natural numbers (or, more generally, enumerable types) is. This is in the standard library as

constructive_indefinite_ground_description_nat :
forall P : nat -> Prop,
(forall n : nat, {P n} + {~ P n}) -> (exists n : nat, P n) -> {n : nat | P n}

in file ConstructiveEpsilon. The idea is roughly that we can use the abstract proof of existence of a number to fuel a search for a explicit natural number. The files in the standard library are quite richly commented if you want to know more about how this happens.

In regard of that, one could hope that it would be possible to show decidability of MuRecSpec, and be done with it. Things, however, are not so simple: to decide MuRecSpec 0 (MR_mu g) [] 1, one would need to decide whether there exist p such that MuRecSpec 1 g [0] p. For an arbitrary g, this is basically the halting problem…

At a high level, the issue is that knowing the return value of a recursive function is not enough: you need to know "how long" the computation was, with some sort of fuel.

However, this idea of the fuel should give you what you want, roughly as follows:

1. define a variant MuRecFuel : forall n : nat, MuRec n -> Vector.t Value n -> Value -> Fuel -> Prop where MuRecFuel n g xs v f means "the function g gives value v on inputs xs after f steps" – in particular MuRecFuel n g xs v 0 is always false; there is some latitude in how exactly you decrease fuel, the important thing is that
2. this predicate should be decidable, because you can now rely on the fuel to serve as a proof of termination for your decider
3. next, show that MuRecSpec n g xs v <-> exists f, MuRecFuel n g xs f v
4. use constructive_indefinite_ground_description_nat to obtain a proper fuel out of a mere existence
5. implement a fueled interpreter interp : (n : nat) (g : MuRec n) (xs : Vector.t nat n) (f : Fuel) : Value, by induction on the fuel for termination
6. show that interp n g xs f = v iff MuRecFuel n g xs f v

Answer 2

Short Answer to your question:

If you want to compute your function within Coq, then you will need to partially compute with the termination proof, which means that it should be transparent, or else use folklore Acc based fuel trick, but it is parameterized by a nat much like the nat based fuel technique.

Long Answer (containing external references):

Well I did spend quite some time working with µ-recursive algorithms in Coq, either as a model of computation in the Coq library of Undecidability Proofs or to show that they can be extracted as is (in OCaml) from Coq code.

Initially at ITP 2017, I did use ConstructiveEpsilon to show that they can be represented as partial Coq fuinctions, but last year at ITP 2023 with JF Monin, we did explain how to moreover get perfect OCaml extraction for µ-recursive algorithms.

Btw in those ITP papers, your mutual inductive MuRecs _ _ type is represented as a nested type, ie we use MuRecs := Vector.t MuRec.

You might want to look at the latest source code there https://github.com/DmxLarchey/Murec_Extraction