<p>The usual definition of partial recursive functions using Turing machines and classical logic (with a few novelties) has been implemented in Coq: see </p>

<p>Zammit, Vincent (1997) <a href="http://kar.kent.ac.uk/21524/" rel="nofollow">A Proof of the S-m-n theorem in Coq</a>. Technical report. University of Kent, The University of Kent, Canterbury, Kent, UK</p>

CC BY-SA 3.0
2012-11-10T11:06:09.980Z
2012-11-10T11:06:09.980Z
Colin McQuillan
<p>Would the set of all computable functions be just the set of all maps of the form </p>

<pre><code>f : forall n : nat, P n -&gt; nat
</code></pre>

<p>where <code>P : nat -&gt; Prop</code>, and <code>(P n)</code> has a proof whenever <code>(f n)</code> is defined - so, <code>n</code> is in the domain of <code>f</code>. Is this some smaller set of maps actually computable by Coq, or is this what I want?</p>

<p>If not, is there an existing formalization? Using lambda calculus, or combinators K and S, or some basic concept of an algorithm?</p>

<p>Perhaps along with a proof of the Snm theorem - that says this set is enumerable?</p>

CC BY-SA 3.0
2012-11-10T11:08:18.147Z
Related: http://cstheory.stackexchange.com/questions/4302/is-there-a-reasonable-automated-proof-system-for-tcs-theorems
Colin McQuillan
<computability><coq><recursive>
How to describe the set of "all computable functions" using Coq?
Polina
# How to describe the set of "all computable functions" using Coq?

(Asked by: username_0 on 2012-11-09)

Would the set of all computable functions be just the set of all maps of the form 
f : forall n : nat, P n -> nat

where P : nat -> Prop, and (P n) has a proof whenever (f n) is defined - so, n is in the domain of f. Is this some smaller set of maps actually computable by Coq, or is this what I want?
If not, is there an existing formalization? Using lambda calculus, or combinators K and S, or some basic concept of an algorithm?
Perhaps along with a proof of the Snm theorem - that says this set is enumerable?

**Tags:** computability, coq, recursive

> **Comments:**
> **username_1**: Related: http://cstheory.stackexchange.com/questions/4302/is-there-a-reasonable-automated-proof-system-for-tcs-theorems  

---

## 1 answers

### Answer by username_1 on 2012-11-10. Score: 2

The usual definition of partial recursive functions using Turing machines and classical logic (with a few novelties) has been implemented in Coq: see

Zammit, Vincent (1997) [A Proof of the S-m-n theorem in Coq](http://kar.kent.ac.uk/21524/). Technical report. University of Kent, The University of Kent, Canterbury, Kent, UK


---

