5

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?

Gilles 'SO- stop being evil'
  • 2,667
  • 1
  • 27
  • 35
Polina
  • 51
  • 1

1 Answers1

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

Colin McQuillan
  • 3,546
  • 22
  • 29