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.

Improve this question
$\endgroup$

1 Answer 1

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

Improve this answer
$\endgroup$
3
  • $\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, 2010 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, 2010 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, 2010 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.