<p>Quite a bit is know about this. The concept of <a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="nofollow">Pure Type Systems</a> (PTS) is useful for showing Church-Rosser (CR) for large classes of typed $\lambda$-calculi. Paraphrasing (1):</p>

<ul>
<li><p>PTS with only β reduction satisfy CR on typed terms. This follows immediately from CR on 'pseudoterms', together with subject reduction. </p></li>
<li><p>For PTS with βη-reduction, CR on the set of pseudoterms is false. See (2).</p></li>
<li><p>In PTS with βη reduction CR holds for well-typed terms of a <em>fixed type</em>. See (1). </p></li>
</ul>

<p>PTS are very general formalisms and include System F, Fω, LF as well as the calculus of constructions. The last two are dependently typed. Both (1, 2) are quite old papers, and I imagine that more is known in 2015.</p>

<hr>

<p><sup>
1. H. Geuvers, <a href="http://www.cs.ru.nl/~herman/PUBS/LICS92_CRbh.ps.gz" rel="nofollow">The Church-Rosser property for βη-reduction in typed $\lambda$-calculi</a>.
</sup></p>

<p><sup>
2. R. P. Nederpelt, <a href="http://www.win.tue.nl/automath/archive/pdf/aut031.pdf" rel="nofollow">Strong normalization in a typed lambda calculus with lambda structured types</a>.
</sup></p>

CC BY-SA 3.0
2015-12-15T13:53:17.057Z
2015-12-16T11:49:49.010Z
2015-12-16T11:49:49.010Z
Martin Berger
<p>It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$:</p>

<p>$$ t=\lambda x:A.(\lambda y:B.\ y)\ x$$</p>

<p>And we have
$$ t\rightarrow_\beta \lambda x: A.x$$
and
$$ t\rightarrow_\eta \lambda y:B.y$$</p>

<p>It is immediate that if $A\equiv B$, then the two resulting terms are, in fact, $\alpha$ equivalent, but there is no reason for this to be the case, on <em>untyped</em> terms.</p>

<p>On <em>typed</em> terms, it's pretty clear that $A$ has to be equal to $B$ for the resulting term $t$ to be well-typed. The big difficulty that occurs is this: </p>

<blockquote>
  <p><strong>For dependently typed systems, confluence needs to be proven before type preservation!</strong></p>
</blockquote>

<p>This is because you need the property of <em>$\Pi$-injectivity</em>
$$ \Pi x:A.B=_{\beta\eta}\Pi x:A'.B'\ \Leftrightarrow\ A=_{\beta\eta}A'\wedge B=_{\beta\eta} B'$$
in order to prove inversion, which is required to prove preservation/subject reduction.</p>

<p>So you can't even prove that $\beta\eta$-reductions preserve types without confluence, but confluence doesn't even hold on untyped/ill-typed terms!</p>

<p>Breaking out of this vicious circle requires some technical tricks, which are hard to summarize here, but arguably the simplest to understand is to simply stop being interested in $\eta$-reductions, but instead concentrate on <strong>$\eta$-expansions</strong>: $t\rightarrow_{\eta*}\lambda x:A.t\ x$</p>

<p>Of course, you need to restrict this rule to non-$\lambda$ and non-applied terms to even hope to get termination, but with these restrictions it seems that the reduction behavior is much better behaved, and the meta-theory works out without too many problems. A good reference seems to be Neil Ghani, <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.39.9149&amp;rep=rep1&amp;type=pdf">Eta-Expansions in Dependent Type Theory</a>.</p>

<p>A different, and recently quite popular approach, is described by Abel, <a href="http://www2.tcs.ifi.lmu.de/~abel/lfsigma.pdf">Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs</a>.</p>

CC BY-SA 3.0
2015-12-15T20:53:20.803Z
2015-12-15T20:53:20.803Z
cody
<p>It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations involving $\lambda$-terms are derivable: for example, <strong>K</strong>$\neq$<strong>I</strong>, since they don't share the same normal form.</p>

<p>It is also known that one can extend the result to pairs which correspond to product types.</p>

<p>But I wonder if one can further extend the result for dependently typed lambda calculus (perhaps) with polymorphic types, e.g. the Calculus of Constructions?</p>

<p>Any references would also be great!</p>

<p>Thanks</p>

<type-theory><lambda-calculus><dependent-type>
Church-Rosser property for dependently typed lambda calculus?
StudentType
# Church-Rosser property for dependently typed lambda calculus?

(Asked by: username_0 on 2015-12-15)

It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations involving $\lambda$-terms are derivable: for example, **K**$\neq$**I**, since they don't share the same normal form.

It is also known that one can extend the result to pairs which correspond to product types.

But I wonder if one can further extend the result for dependently typed lambda calculus (perhaps) with polymorphic types, e.g. the Calculus of Constructions?

Any references would also be great!

Thanks

**Tags:** type-theory, lambda-calculus, dependent-type


---

## 2 answers

### Answer by username_2 on 2015-12-15. Score: 10 | Accepted answer

It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$:

$$ t=\lambda x:A.(\lambda y:B.\ y)\ x$$

And we have
$$ t\rightarrow\_\beta \lambda x: A.x$$
and
$$ t\rightarrow\_\eta \lambda y:B.y$$

It is immediate that if $A\equiv B$, then the two resulting terms are, in fact, $\alpha$ equivalent, but there is no reason for this to be the case, on *untyped* terms.

On *typed* terms, it's pretty clear that $A$ has to be equal to $B$ for the resulting term $t$ to be well-typed. The big difficulty that occurs is this:

> **For dependently typed systems, confluence needs to be proven before type preservation!**

This is because you need the property of *$\Pi$-injectivity*
$$ \Pi x:A.B=\_{\beta\eta}\Pi x:A'.B'\ \Leftrightarrow\ A=\_{\beta\eta}A'\wedge B=\_{\beta\eta} B'$$
in order to prove inversion, which is required to prove preservation/subject reduction.

So you can't even prove that $\beta\eta$-reductions preserve types without confluence, but confluence doesn't even hold on untyped/ill-typed terms!

Breaking out of this vicious circle requires some technical tricks, which are hard to summarize here, but arguably the simplest to understand is to simply stop being interested in $\eta$-reductions, but instead concentrate on **$\eta$-expansions**: $t\rightarrow\_{\eta\*}\lambda x:A.t\ x$

Of course, you need to restrict this rule to non-$\lambda$ and non-applied terms to even hope to get termination, but with these restrictions it seems that the reduction behavior is much better behaved, and the meta-theory works out without too many problems. A good reference seems to be Neil Ghani, [Eta-Expansions in Dependent Type Theory](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.39.9149&rep=rep1&type=pdf).

A different, and recently quite popular approach, is described by Abel, [Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs](http://www2.tcs.ifi.lmu.de/~abel/lfsigma.pdf).


---

### Answer by username_1 on 2015-12-15. Score: 8

Quite a bit is know about this. The concept of [Pure Type Systems](https://en.wikipedia.org/wiki/Pure_type_system) (PTS) is useful for showing Church-Rosser (CR) for large classes of typed $\lambda$-calculi. Paraphrasing (1):

* PTS with only β reduction satisfy CR on typed terms. This follows immediately from CR on 'pseudoterms', together with subject reduction.
* For PTS with βη-reduction, CR on the set of pseudoterms is false. See (2).
* In PTS with βη reduction CR holds for well-typed terms of a *fixed type*. See (1).

PTS are very general formalisms and include System F, Fω, LF as well as the calculus of constructions. The last two are dependently typed. Both (1, 2) are quite old papers, and I imagine that more is known in 2015.

---

1. H. Geuvers, [The Church-Rosser property for βη-reduction in typed $\lambda$-calculi](http://www.cs.ru.nl/~herman/PUBS/LICS92_CRbh.ps.gz).

2. R. P. Nederpelt, [Strong normalization in a typed lambda calculus with lambda structured types](http://www.win.tue.nl/automath/archive/pdf/aut031.pdf).


---

