14

In response to another question, Extensions of beta theory of lambda calculus, Evgenij offered the answer:

beta + the rule {s = t | s and t are closed unsolvable terms}

where a term M is solvable if we can find a sequence of terms such that M's application to them is equal to I.

Evgenij's answer gives an equational theory over the lambda calculus, but not one characterised by a reduction system, i.e., a confluent, recursive set of rewrite rules.

Let's call an invisible equivalence over a theory of the lambda calculus, a reduction system that equates some nontrivial set of closed unsolvable lambda terms, but doesn't add any new equations involving solvable terms.

Are there any invisible equivalences over the beta theory of the lambda calculus?

Postscript An example that characterises an invisible equivalence, but is not confluent. Let M=(λx.x x) and N=(λx.x x x), two unsolvable terms. Adding the rule rewriting N N to M M induces an invisible equivalence containing M M = N N, but has the bad critical pair where N N reduces to both M M and M M N, each of which has one rewrite available, which rewrites to itself.

Community
  • 1
Charles Stewart
  • 4,316
  • 28
  • 45
  • The notion of invisible equivalence is related to the notion of conservative extension. A conservative extension of a theory is a collection of additional terms and equations to the theory which do not add new equations between terms in the original theory. – Dave Clarke Aug 23 '10 at 09:31
  • @supercooldave: Unsolvable terms are normal terms of the theory, such as (λx.x x)(λx.x x), and are reducible to other (unsolvable) terms, so are part of the normal theory of the lambda-calculus. The point is that they are orthogonal to the semantics of the lambda calculus we get from Böhm's theorem. – Charles Stewart Aug 23 '10 at 11:21
  • So you are looking for $\lambda \beta$ plus some rules of the same kind as the beta rule (specified by syntax instead of by semantics) such that ? – Evgenij Thorstensen Aug 23 '10 at 19:26
  • @Evgenij: Yes. It's crucial that the new rules are confluent, and, of course, trivial to find examples if they are not. I'll add an example to show the issue. – Charles Stewart Aug 24 '10 at 07:47

1 Answers1

6

Yes. With M=(λx.x x) per the question, consider the rewrite ζ that takes M M p to M M.

It is confluent, and so characterises a reduction system over the lambda calculus. Argument sketch for confluence: since M M is closed, we only need to consider critical pairs of the form M M N1 ... Nk. These can be resolved.

It is an invisible equivalence, because terms of the form M M I ... I (with zero or more I s) are closed unsolvable terms that reduce only to themselves in the base lambda calculus, thus are distinct, and so the infinite set of these terms is nontrivial, and is obviously equated by ζ.

I don't like accepting my answer to my question, so I'll accept an answer from someone who provides a less absurdly incomplete confluence argument.

Charles Stewart
  • 4,316
  • 28
  • 45