<p>Yes.  With <em>M=(λx.x x)</em> per the question, consider the rewrite &zeta; that takes <em>M M p</em> to <em>M M</em>.</p>

<p>It is confluent, and so characterises a reduction system over the lambda calculus.  Argument sketch for confluence: since <em>M M</em> is closed, we only need to consider critical pairs of the form <em>M M N<sub>1</sub> ... N<sub>k</sub></em>.  These can be resolved.</p>

<p>It is an invisible equivalence, because terms of the form <em>M M I ... I</em> (with zero or more <em>I</em> 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 &zeta;.</p>

<p>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.</p>

CC BY-SA 2.5
2010-08-30T12:15:37.303Z
2010-08-30T12:15:37.303Z
Charles Stewart
<p>In response to another question, <a href="https://cstheory.stackexchange.com/questions/246/extensions-of-beta-theory-of-lambda-calculus">Extensions of beta theory of lambda calculus</a>, Evgenij offered the answer:</p>

<pre>beta + the rule {s = t | s and t are closed unsolvable terms}</pre>

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

<p>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.</p>

<p>Let's call an <em>invisible equivalence</em> 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.</p>

<p>Are there any invisible equivalences over the beta theory of the lambda calculus?</p>

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

CC BY-SA 2.5
2010-08-23T09:31:54.073Z
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
CC BY-SA 2.5
2010-08-23T11:21:21.373Z
@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
CC BY-SA 2.5
2010-08-23T19:26:23.187Z
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 <rest of post>?
Evgenij Thorstensen
CC BY-SA 2.5
2010-08-24T07:47:31.717Z
@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
<pl.programming-languages><lambda-calculus><lo.logic>
Characterising invisible equivalences by confluent rewrite rules
Charles Stewart
# Characterising invisible equivalences by confluent rewrite rules

(Asked by: username_0 on 2010-08-22)

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.

**Tags:** pl.programming-languages, lambda-calculus, lo.logic
> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  
> **username_2**: 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 <rest of post>?  
> **username_0**: @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.  

---

## 1 answers

### Answer by username_0 on 2010-08-30. Score: 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.


---

