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?


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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