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

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?

• Please add a tag for the prover you are using. Is it Coq? Commented Jul 1 at 15:44
• Wait, is this your own custom language? Commented Jul 1 at 15:45
• Now, this is Coq – but the question is not really tied to it, I guess, this is mostly about constructivism. Although the peculiarities of Coq's version of Prop come into account. Commented Jul 1 at 15:48
• It is Coq. @JasonRute Here is the code: github.com/KiJeong-Lim/LoL/blob/… Commented Jul 1 at 16:19
• I've done: github.com/KiJeong-Lim/LoL/blob/… Commented Jul 2 at 13:28

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