2
$\begingroup$

I am having trouble finding out what a primitive subset of the lambda calculus would look like. I reference primitive recursion as shown here: "https://en.wikipedia.org/wiki/Primitive_recursive_function".

These are the three base axioms:

  • Constant function: The 0-ary constant function 0 is primitive recursive.
  • Successor function: The 1-ary successor function S, which returns the successor of its argument (see Peano postulates), is primitive recursive. That is, S(k) = k + 1.
  • Projection function: For every n≥1 and each i with 1≤i≤n, the n-ary projection function Pin, which returns its i-th argument, is primitive recursive.

Here is my confusion. In the LC zero is represented as (λfx. x). Next the successor functions is defined as (λnfx. f (n f x)). Because they are both axioms both of these functions can be classified as primitive. But when I apply the function suc to zero I get the encoding of the number one. Which is represented as the function (λf.(λx.(f x))). Now this number is neither zero or the suc function but the result of application. As such I do not see how this result function (value of 1) fits into the rule set. But very clearly a program with the number 1 in it is still primitive recursive. What am I not understanding here? While 1 is the suc to zero, once suc is applied it is neither suc, nor zero.

|cite|improve this question
$\endgroup$
  • $\begingroup$ There are also "derivation rule", namely composition and recursion. $\endgroup$ – Yuval Filmus Jan 23 '16 at 13:44
  • $\begingroup$ Of course @YuvalFilmus but as far as I could tell those did not affect the problem. Unless I have misunderstood in which case how do they help? $\endgroup$ – 44701 Jan 23 '16 at 13:46
2
$\begingroup$

As you mention, $1$ is primitive recursive according to the following proof:

  • $0$ is primitive recursive (axiom)
  • $\operatorname{suc}$ is primitive recursive (axiom)
  • $1=\operatorname{suc}(0)$ is primitive recursive (composition)

Using this you can show that $1$ is admissible, that is if you add $1$ as an axiom, the resulting set of functions is still the primitive recursive functions.

Note that lambda calculus has absolutely nothing to do with the answer.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ So just to clarify if I apply suc to zero, then the function that is the result is also primitive recursive? It will then not be possible for that function to introduce Turing complete behavior? $\endgroup$ – 44701 Jan 23 '16 at 13:54
  • $\begingroup$ That's right – you can use composition and primitive recursion in defining primitive recursive functions. It says so clearly in the definition. Even using these rules, you can't obtain all computable functions. $\endgroup$ – Yuval Filmus Jan 23 '16 at 13:57

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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