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
Church-Rosser property for dependently typed lambda calculus?
type theory;lambda calculus;dependent type
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.A different, and recently quite popular approach, is described by Abel, Untyped Algorithmic Equality for Martin-Lf's Logical Framework with Surjective Pairs.