7
$\begingroup$

I was reading this 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?

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Clément May 11 '15 at 7:30
10
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – cody May 11 '15 at 16:59
  • $\begingroup$ @cody: good point... $\endgroup$ – Neel Krishnaswami May 12 '15 at 14:43
5
$\begingroup$

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:

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.

$\endgroup$
  • $\begingroup$ Was this really discovered by Lescanne? The paper you link to is by PA Mellies. $\endgroup$ – Martin Berger May 12 '15 at 3:52
  • 1
    $\begingroup$ @cody: yes, Martin is right, the discovery that explicit substitutions may not terminate is due to Paul-André Malliès. $\endgroup$ – Damiano Mazza May 12 '15 at 8:03
  • $\begingroup$ Sorry, I don't know where that came from. I'll update the answer. $\endgroup$ – cody May 12 '15 at 15:50

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.