5
$\begingroup$

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?

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
2
$\begingroup$

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. Technical report. University of Kent, The University of Kent, Canterbury, Kent, UK

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.