<p>In general it is quite possible for even pure <span class="math-container">$\lambda$</span>-terms to be weakly normalizing and confluent without being SN: take
<span class="math-container">$$ K\ I\ \Omega$$</span>
where <span class="math-container">$K=\lambda xy.x, \ I=\lambda x.x$</span> and <span class="math-container">$\Omega=(\lambda x. x\ x)(\lambda x.x\ x)$</span>.</p>

<p>The following surprising result was first discovered by <a href="http://link.springer.com/chapter/10.1007%2FBFb0014062" rel="nofollow noreferrer">Mellies</a>:</p>

<blockquote>
  <p>STLC with explicit substitutions may not terminate.</p>
</blockquote>

<p>This is surprising as:</p>

<ol>
<li>Explicit substitutions alone terminate.</li>
<li>Explicit substitutions with an explicit <span class="math-container">$\beta$</span>-rule simulates the "usual" reduction with re-naming.</li>
<li>STLC with the usual <span class="math-container">$\beta$</span> rule is terminating.</li>
</ol>

<p>Most of the subsequent work on explicit substitutions work on repairing this apparent defect.</p>

CC BY-SA 3.0
2015-05-12T03:52:38.290Z
Was this really discovered by Lescanne? The paper you link to is by PA Mellies.
Martin Berger
CC BY-SA 3.0
2015-05-12T08:03:26.473Z
@cody: yes, Martin is right, the discovery that explicit substitutions may not terminate is due to Paul-André Malliès.
Damiano Mazza
CC BY-SA 3.0
2015-05-12T15:50:06.520Z
Sorry, I don't know where that came from. I'll update the answer.
cody
CC BY-SA 4.0
2015-05-11T17:06:39.207Z
2019-02-11T23:31:27.243Z
2019-02-11T23:31:27.243Z
cody
<blockquote>
  <p>Is it the case that a confluent weakly normalizing system is strongly normalizing?  Why/why not?</p>
</blockquote>

<p>No, it's not necessarily the case. </p>

<ol>
<li>Weak normalization means: there exists a reduction strategy that will lead to a normal form. </li>
<li>People often use confluence to mean what rewriting people call "local confluence": this is the property that if $a \leadsto b$ and $a \leadsto c$, then $b$ and $c$ can be joined -- i.e., there exists a $d$ such that $b \leadsto^\ast d$ and $c \leadsto^\ast d$. </li>
</ol>

<p>This does not rule out the existence of infinite reduction sequences. </p>

<p>As an example, start with the STLC and add a new base type $X$ and constant $c,d : X$ with the reduction rule $c \leadsto c$ and $c \leadsto d$.</p>

<p>There is a weak normalization strategy: use a weak normalization strategy for the STLC and immediately reduce any $c$ to $d$. The calculus is also Church-Rosser, since it inherits this property from the STLC. But it isn't strongly normalizing since you can reduce a $c$ forever. </p>

CC BY-SA 3.0
2015-05-11T16:59:58.867Z
Any term where $c$ appears in the $\beta$-normal form will not be weakly normalizing in your example. Maybe it's best to add an additional rule $c\rightsquigarrow d$ with $d$ irreducible.
cody
CC BY-SA 3.0
2015-05-12T14:43:11.547Z
@cody: good point...
Neel Krishnaswami
CC BY-SA 3.0
2015-05-11T08:33:02.897Z
2015-05-12T10:46:35.180Z
2015-05-12T10:46:35.180Z
Neel Krishnaswami
<p>I was reading <a href="https://hal.inria.fr/inria-00073380">this</a> abstract and saw that they prove weak normalization and confluence. My limited understanding suggests that those two properties should provide strong normalization, which then leaves me confused about why they'd leave that out in the abstract, thus suggesting I might be wrong.</p>

<p>Is it the case that a confluent weakly normalizing system is strongly normalizing? Why/why not?</p>

CC BY-SA 3.0
2015-05-11T07:30:17.050Z
For what system or variation of lambda-calculus? You should probably have a look at *2.1.4 Preservation of Strong Normalization: the $\lambda v$-Calculus* of the document you are refereeing to, *A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory*, by César Muñoz.
Clément
<lambda-calculus>
Weakly normalizing + confluent = strongly normalizing?
user
# Weakly normalizing + confluent = strongly normalizing?

(Asked by: username_0 on 2015-05-11)

I was reading [this](https://hal.inria.fr/inria-00073380) abstract and saw that they prove weak normalization and confluence. My limited understanding suggests that those two properties should provide strong normalization, which then leaves me confused about why they'd leave that out in the abstract, thus suggesting I might be wrong.

Is it the case that a confluent weakly normalizing system is strongly normalizing? Why/why not?

**Tags:** lambda-calculus
> **Comments:**
> **username_1**: For what system or variation of lambda-calculus? You should probably have a look at *2.1.4 Preservation of Strong Normalization: the $\lambda v$-Calculus* of the document you are refereeing to, *A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory*, by César Muñoz.  

---

## 2 answers

### Answer by username_5 on 2015-05-11. Score: 10 | Accepted answer

> Is it the case that a confluent weakly normalizing system is strongly normalizing? Why/why not?

No, it's not necessarily the case.

1. Weak normalization means: there exists a reduction strategy that will lead to a normal form.
2. People often use confluence to mean what rewriting people call "local confluence": this is the property that if $a \leadsto b$ and $a \leadsto c$, then $b$ and $c$ can be joined -- i.e., there exists a $d$ such that $b \leadsto^\ast d$ and $c \leadsto^\ast d$.

This does not rule out the existence of infinite reduction sequences.

As an example, start with the STLC and add a new base type $X$ and constant $c,d : X$ with the reduction rule $c \leadsto c$ and $c \leadsto d$.

There is a weak normalization strategy: use a weak normalization strategy for the STLC and immediately reduce any $c$ to $d$. The calculus is also Church-Rosser, since it inherits this property from the STLC. But it isn't strongly normalizing since you can reduce a $c$ forever.

> **Comments:**
> **username_2**: Any term where $c$ appears in the $\beta$-normal form will not be weakly normalizing in your example. Maybe it's best to add an additional rule $c\rightsquigarrow d$ with $d$ irreducible.  
> **username_5**: @cody: good point...  

---

### Answer by username_2 on 2015-05-11. Score: 6

In general it is quite possible for even pure $\lambda$-terms to be weakly normalizing and confluent without being SN: take
$$ K\ I\ \Omega$$
where $K=\lambda xy.x, \ I=\lambda x.x$ and $\Omega=(\lambda x. x\ x)(\lambda x.x\ x)$.

The following surprising result was first discovered by [Mellies](http://link.springer.com/chapter/10.1007%2FBFb0014062):

> STLC with explicit substitutions may not terminate.

This is surprising as:

1. Explicit substitutions alone terminate.
2. Explicit substitutions with an explicit $\beta$-rule simulates the "usual" reduction with re-naming.
3. STLC with the usual $\beta$ rule is terminating.

Most of the subsequent work on explicit substitutions work on repairing this apparent defect.

> **Comments:**
> **username_3**: Was this really discovered by Lescanne? The paper you link to is by PA Mellies.  
> **username_4**: @cody: yes, Martin is right, the discovery that explicit substitutions may not terminate is due to Paul-André Malliès.  
> **username_2**: Sorry, I don't know where that came from. I'll update the answer.  

---

