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!
-
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– Yuval Filmus2016年01月25日 05:59:28 +00:00Commented Jan 25, 2016 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– Yuval Filmus2016年01月25日 06:09:48 +00:00Commented Jan 25, 2016 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– Yuval Filmus2016年01月25日 06:11:10 +00:00Commented Jan 25, 2016 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– 447012016年01月25日 06:22:18 +00:00Commented Jan 25, 2016 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– Yuval Filmus2016年01月25日 06:24:44 +00:00Commented Jan 25, 2016 at 6:24
1 Answer 1
I found this post on stack exchanges CS theory section:
It is very similar to what I was looking for.
Explore related questions
See similar questions with these tags.