1
$\begingroup$

I am trying to write a program to recognize if a given lambda calculus expression is primitive recursive. I believe that a general algorithm to do this does not exist, but I am interested in the most general algorithm. This is a subset of the primitive recursive functions in the LC.

Primitive recursion is built up from the following rules: "http://safalra.com/lambda-calculus/partial-recursive-functions"

To outline some of these rules

  • (λfx. x) is zero
  • (λnfx. f (n f x)) is successor
  • etc...

Now in my program I can just recognize these axioms directly. My confusion is what happens when I get to things derived from them. Take the number 5 for example encoded as (λs.(λz.(s (s (s (s (s z))))))). This is the result of applying the the successor function to zero 5 times. But the above expression is not one of the axioms. I believe that the rule set says that the result of primitive recursive functions are also primitive recursive, but I do not see how given one of these results the result can be shown primitive recursive.

What I mean is that given just the encoding of the number 5 how can I show that it is primitive recursive? That is without brute force search building up from the axioms. Also is my method of representing the primitive recursion axioms correct (for suc and zero) or are the axioms not that literal? Thanks!

$\endgroup$
  • 2
    $\begingroup$ How is this different from your previous question cs.stackexchange.com/questions/52176/…? (Other than using 5 as an example rather than 1.) $\endgroup$ – Yuval Filmus Jan 25 '16 at 5:59
  • $\begingroup$ Are you interested in the question of parsing an expression built according to a context-free grammar? There are known algorithms for that. $\endgroup$ – Yuval Filmus Jan 25 '16 at 6:09
  • 2
    $\begingroup$ I believe that a general algorithm to do this does not exist, but I am only interested in decidable cases – there is no such thing as decidable cases. Any particular instance can be decided by some algorithm. Perhaps you should clarify what you mean here. $\endgroup$ – Yuval Filmus Jan 25 '16 at 6:11
  • $\begingroup$ @YuvalFilmus the difference is I am asking for knowledge on the most general algorithm to show something primitive recursive without brute forcing a set of expressions up from the axioms. The fact that inferred simply typed lambda calculus exists shows that something like this is possible. $\endgroup$ – 44701 Jan 25 '16 at 6:22
  • 3
    $\begingroup$ If you are asking for an algorithm that takes a lambda expression and outputs "primitive recursive" or "not primitive recursive", then no such algorithm exists. If you are asking for an algorithm that takes a lambda expression and checks whether it can be generated using the rules of some primitive recursive formalism, then this is an instance of parsing, and should be doable. $\endgroup$ – Yuval Filmus Jan 25 '16 at 6:24
0
$\begingroup$

I found this post on stack exchanges CS theory section:

https://cstheory.stackexchange.com/questions/20364/how-to-make-the-lambda-calculus-strong-normalizing-without-a-type-system

It is very similar to what I was looking for.

$\endgroup$

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.