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.

Improve this question
$\endgroup$
2
  • $\begingroup$ There are also "derivation rule", namely composition and recursion. $\endgroup$ Commented Jan 23, 2016 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$ Commented Jan 23, 2016 at 13:46

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
2
  • $\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$ Commented Jan 23, 2016 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$ Commented Jan 23, 2016 at 13:57

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.