primitive recursion in the lambda calculus

Question

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.

• Yuval Filmus: There are also "derivation rule", namely composition and recursion.
• 44701: 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?

Answer 1

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.

• 44701: 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?
• Yuval Filmus: 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.