7
$\begingroup$

Confluence implies uniqueness of normal forms, which is great. It is also much simpler to reason about, allowing more reusable proofs (indeed I don't imagine a way to prove UN directly for the $\lambda$-calculus).

It is however strictly stronger than UN, saying something about computations without any NF: they can be joined.

That's a nice result, but does anyone really care? What are really the practical goals of proving your calculus is confluent?

$\endgroup$
8
$\begingroup$

I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for instance from the standpoint of abstract term rewriting, which is not my specialty).

For instance, in $\lambda$-calculi and related languages, usually the meaning of expressions is given by (something like) the smallest congruence such that $(\lambda x.M)N=M\{N/x\}$ (this is usually called $\beta$-equivalence). Reduction arises (historically, as well as technically) as an orientation of the above equality, so that one may redefine $\beta$-equivalence as $(\leftarrow\cup\to)^\ast$ (the reflexive-transitive closure of reduction and expansion), and study $\beta$-equivalence by means of reduction (there are "practical" advantages to this: for instance, $M\simeq_\beta N$ is often undecidable, whereas $M\to N$ is always decidable, and sometimes you may be able to replace $\simeq_\beta$ with $\to$ in some definition or statement of some property).

Now, confluence is equivalent to the transitivity of the following relation:

$$M\sim N\quad\text{iff}\quad \exists P.\,M\to^\ast P,\,N\to^\ast P,$$

that is, $M\sim N$ precisely when $M$ and $N$ have a common reduct. Therefore, if you have confluence, $\sim$ is an equivalence relation, and in fact it coincides with $\beta$-equivalence. The relation $\sim$ is technically much more convenient than $(\leftarrow\cup\rightarrow)^\ast$ (it involves only reduction, not arbitrary chains of reductions/expansions). So, if a calculus is confluent, it is usually a quite useful fact to know, although of course it is often only used to prove uniqueness of normal forms (which by the way, as you observe, I wouldn't know how to prove otherwise).

Also note that confluence is a sort of "practically necessary" condition for $\beta$-equivalence to be meaningful: many calculi of interest in practice are Turing complete, in which case the lack of confluence usually implies that everything is $\beta$-equivalent (one is likely to be able to concoct a term which non-deterministically reduces to every possible term). So, in presence of confluence, $\simeq_\beta$ is a meaningful notion which may be taken as the basis, for instance, of denotational semantics; in absence of confluence, something else must be found (like some kind of behavioral equivalance, as in process calculi, which is much more complex).


Edit: as suggested by Guido, I add a further note on the additional interest of confluence with respect to uniqueness of normal forms (UN), which I had not thought of when writing my answer.

Confluence implies the following property: $N\simeq_\beta N'$ with $N$ and $N'$ normal implies $N=N'$ (syntactic equality). In other words, distinct normal forms cannot be $\beta$-equivalent. (This immediately follows from the characterization of $\simeq_\beta$ as $\sim$ given above). This property is interesting because it implies the consistency of $\simeq_\beta$ seen as an equational theory, as soon as there is more than one normal form (as is the case, for instance, in the $\lambda$-calculus).

On the other hand, UN is not enough to obtain the above property, as shown by the following rewriting system:

$$N\leftarrow M\to\Omega\leftarrow M'\to N',$$

in which all five terms are distinct and $\Omega$ is a term that reduces to itself. We have $N\simeq_\beta N'$ and yet $N$ and $N'$ are distinct normal forms.

$\endgroup$
  • 1
    $\begingroup$ This is a good answer, thank you! I was thinking about it earlier and realized that confluence implies the consistency of the equational theory (no two distinct normal forms are equivalent), but UN doesn't! It's easy to construct an example for this. So I would just add this remark to your answer, to show another good consequence of confluence that doesn't arise from UN. $\endgroup$ – Guido Feb 7 '17 at 0:18
  • $\begingroup$ Good point! Although I would not call the property you mention consistency. The fact that no two distinct normal forms are equivalent implies consistency (as soon as you have more than 1 nf), but this latter is just the fact that there exist $M\neq M'$ (not necessarily normal) such that $M\not\simeq_\beta M'$. There are obviously plenty of inconsistent confluent systems (for instance the looping system $M\to M'$ and $M'\to M$). $\endgroup$ – Damiano Mazza Feb 7 '17 at 12:19

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.