16
$\begingroup$

The beta-eta-theory of the lambda-calculus is Post-complete. Can additional rules be added to extend the beta-theory of the lambda-calculus to get confluent theories other than the beta-eta theory?

Postscript

This question violated my own rule that questions should explain why the questioner cares.

It struck me one night, not long before this site went into private beta, that because extensionality and the principle of the excluded middle are related, the eta rule is some sort of extensionality rule, and there are intermediate logics between intuitionistic and classical logic, then it would be interesting if there was such a thing as "intermediate eta" theories.

If I has done so, it would have been obvious that Evgenij's answer raises an obvious problem in the way I'd formulated the question, rather than being what I was after.

|cite|improve this question|||||
$\endgroup$
8
$\begingroup$

Yes. There is for example beta + the rule {s = t | s and t are closed unsolvable terms}. This is as far as I remember not equal to beta-eta, and is consistent. See mathgate for a short description and reference to Barendregt.

|cite|improve this answer|||||
$\endgroup$
  • $\begingroup$ This is, indeed, a correct answer to my question: beta-eta doesn't equate (\x.x x)(\x.x x x) and (\x.x x)(\x. x x), although they have the same Böhm tree. I misphrased the question: I'm after observable differences. I should probably accept this and ask the question I meant to ask... $\endgroup$ – Charles Stewart Aug 19 '10 at 10:03
  • $\begingroup$ I've been thinking about this answer... this theory isn't generated by new rules (unsolvability is undecidable), and I can't think of any confluent set of rules that generates a subtheory of this theory. But for all I know, there may be one. So, a new question: cstheory.stackexchange.com/questions/398/… $\endgroup$ – Charles Stewart Aug 22 '10 at 21:39
  • $\begingroup$ And my answer to that question shows that Evgenij's intuition was sound, and provides combinatory rewrite rules for a subtheory of this. So accepted. $\endgroup$ – Charles Stewart Sep 17 '10 at 9:14

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.