
\section*{Introduction}
\label{sec:intro}

Type theories with an impredicative universe \ensuremath{\mathsf{Prop}}\xspace of propositions,
such as the Calculus of Constructions \citep{coquandHuet:CoC},
lose the normalization property in the presence of a \emph{proof-irrelevant}
propositional equality $\_{=}\_ : \funT A \ensuremath{\mathsf{Type}}\xspace {A \to A \to \ensuremath{\mathsf{Prop}}\xspace}$
with the standard elimination principle.
The loss of normalization is facilitated already by a coercion
function with a reduction rule
\[
\begin{array}{l}
  \ensuremath{\mathsf{cast}}\xspace : \funT {A\,B} \ensuremath{\mathsf{Prop}}\xspace {\Eq \ensuremath{\mathsf{Prop}}\xspace A B \to A \to B} \\
  \cast A A e x \rhd x
\end{array}
\]
that does not inspect the equality proof $e : \Eq \ensuremath{\mathsf{Prop}}\xspace A A$ but only
checks whether the endpoints are (definitionally) equal.

The failure of normalization refutes a conjecture by Werner
\citeyearpar[Conjecture 3.14]{werner:lmcs08}.
Consistency and canonicity is not at stake; thus, the situation is
comparable to type theory with equality reflection
\citep{MartinLoef84,martinLoef:constrMathAndCompPrg}, aka
\emph{Extensional Type Theory}.
At the moment, it is unclear whether the use of impredicativity is essential to
break normalization; predicative type theory might be able to host a
proof-irrelevant propositional equality \citep{abel:nbe09}
while retaining normalization.

\section*{Counterexample to Normalization}

We employ the usual impredicative definition of absurdity $\bot$ and
negation $\neg A$ and a
derived definition of truth $\top$:
\[
\begin{array}{lcl}
  \bot   & : & \ensuremath{\mathsf{Prop}}\xspace \\
  \bot   & = & \funT A \ensuremath{\mathsf{Prop}}\xspace A
\end{array}
\qquad\qquad
\begin{array}{lcl}
  \neg   & : & \ensuremath{\mathsf{Prop}}\xspace \to \ensuremath{\mathsf{Prop}}\xspace \\
  \neg A & = & A \to \bot
\end{array}
\qquad\qquad
\begin{array}{lcl}
  \top   & : & \ensuremath{\mathsf{Prop}}\xspace \\
  \top   & = & \neg \bot \\
\end{array}
\]
The presence of $\ensuremath{\mathsf{cast}}\xspace$ allows us to define self-application under
the assumption that all propositions all equal.  The self-application
term $\omega$ refutes this assumption.
\[
\begin{array}{lcl}
  \delta & : & \top \\
  \delta\;z & = & z\;\top\;z
\end{array}
\qquad
\begin{array}{lcl}
  \omega & : & \neg \funT {A\,B} \ensuremath{\mathsf{Prop}}\xspace {\Eq \ensuremath{\mathsf{Prop}}\xspace A B} \\
  \omega\;h\;A & = & \ensuremath{\mathsf{cast}}\xspace\; \top\, A\; {(h\;\top\,A)}\;
    \delta
\end{array}
\]
Impredicativity is exploited in $\delta$ when applying $z : \bot$ to type
$\top = \bot \to \bot$ so that it can be applied to $z$ again.  The
type of
$\delta$
is $\top$ which we cast to $A$ thanks to
the assumption~$h$ that all propositions are equal.

We build a non-normalizing term $\Omega$ by applying $\omega$ to
itself through $\delta$, reminiscent of the shortest diverging term in untyped
$\lambda$-calculus.
\[
\begin{array}{lcl}
  \Omega & : & \neg \funT {A\,B} \ensuremath{\mathsf{Prop}}\xspace {\Eq \ensuremath{\mathsf{Prop}}\xspace A B} \\
  \Omega\;h & = & \delta\;(\omega\;h)
 
\end{array}
\]
Thanks to the reduction rule of $\ensuremath{\mathsf{cast}}\xspace$, term $\Omega\;h$ reduces to
itself:
\[
\begin{array}{lclcl}
  \Omega\;h
  & = & \delta\;(\omega\;h)
  & \rhd & \omega\;h\;\top\;(\omega\;h) \\
  & = & \cast \top \top {(h\;\top\;\top)} \delta \;(\omega\;h)
 
 
 
  & \rhd & \delta\;(\omega\;h) \\
  & = & \Omega\;h \\
\end{array}
\]
Thus, normalization is lost in the presence of a hypothesis (free
variable) $h$.  As a consequence, normalization that proceeds under
$\lambda$-abstraction can diverge.  This means that equality of open
terms cannot be decided just by normalization.

The counterexample can be implemented in Werner's
type theory with
proof-irrelevance \citeyearpar{werner:lmcs08}, refuting the normalization
conjecture (3.14).  We implement $\ensuremath{\mathsf{cast}}\xspace$ as instance of Werner's
more general equality elimination rule:
\[
\begin{array}{lcl}
  \ensuremath{\mathsf{Eq\_rec}}\xspace & : &
   \funT A \ensuremath{\mathsf{Type}}\xspace \funT P {A \to \ensuremath{\mathsf{Type}}\xspace}
    \funT {a\,b} A {P\;a \to \Eq A a b \to P\;b}
   \\
  \Eqrec A P a b x e & \rhd & x \qquad \mbox{if } a = b
\\[1ex]
  \cast A B e x & = & \Eqrec \ensuremath{\mathsf{Prop}}\xspace {(\lam a A \ensuremath{\mathsf{Prop}}\xspace)} A B x e
\end{array}
\]
The term $\Omega$ also serves as counterexample to normalization in
the theorem prover Lean \citep{deMoura:cade15},
version 3.4.2 \citep{lean342}.
\begin{adjustwidth}{\mathindent}{0em}
\lstinputlisting{propIrrEq.lean}


\end{adjustwidth}
Infinite reduction can now be triggered with the command
\lstinline{#reduce Omega}, which diverges.

\section*{A Counterexample Using Propositional Extensionality}

The counterexample of the last section used the absurd assumption that
\emph{all} proposition are equal.  The following counterexample
utilizes just the axiom of propositional extensionality, $\mathsf{propext}$,
which is a default axiom of Lean.
In fact, the weaker statement $\mathsf{tautext}$, which states the equality
of \emph{true} propositions, is sufficient.
\[
  \begin{array}{lcl}
\mathsf{propext} & : & \funT{A\,B} \ensuremath{\mathsf{Prop}}\xspace {(A \leftrightarrow B) \to \Eq \ensuremath{\mathsf{Prop}}\xspace A B} \\
\mathsf{tautext} & : & \funT{A\,B} \ensuremath{\mathsf{Prop}}\xspace {A \to B \to \Eq \ensuremath{\mathsf{Prop}}\xspace A B} \\
  \end{array}
\]
The counterexample uses the standard impredicative definition of
truth,
\[
  \begin{array}{lcl}
\top & = & \funT A \ensuremath{\mathsf{Prop}}\xspace {A \to A}
  \end{array}
\]
and a cast from
$\top \to \top$ to $A$, which are both tautologies under the
assumption $a : A$.
\[
\begin{array}{lcl}
\mathsf{id},\; \delta   & : & \top \to \top \\
\mathsf{id}\;x & = & x \\
\delta\;z & = & z\;(\top \to \top)\;\mathsf{id}\;z
\end{array}
\quad
\begin{array}{lcl}
\omega,\; \Omega & : & \top \\
\omega\;A\;a & = &
  \ensuremath{\mathsf{cast}}\xspace\; (\top \to \top)\; A\;
    (\mathsf{tautext}\;(\top \to \top)\;A\;\mathsf{id}\;a)\;
    \delta \\
\Omega & = & \delta\;\omega
\end{array}
\]
These definitions can be directly replayed in Lean 3.4.2 with the
standard prelude, yielding a
non-normalizing term \lstinline|Omega|.
\begin{adjustwidth}{\mathindent}{0em}
\lstinputlisting{propExtTrue.lean}
\end{adjustwidth}
Note that term \lstinline|Omega| is closed with respect the standard axioms
of Lean, and does not even have a weak head normal form.


\section*{Related Work and Conclusions}

The $\ensuremath{\mathsf{cast}}\xspace$ operator is inspired by Girard's operator
$J : \funT {A\,B} \ensuremath{\mathsf{Prop}}\xspace {A \to B}$ with reduction rule
$J\;A\;A\;M \rhd M$ that destroys the normalization property of
System~F \citep{girard:ssls70,harperMitchell:ipl99}.
In contrast to $J$, our $\ensuremath{\mathsf{cast}}\xspace$ also requires a proof of
equality of $A$ and $B$, but this proof is not inspected and thus does not
block reduction if it is non-canonical.  Thus, the simple lie that all
propositions are equal is sufficient to trigger divergence.

Historically, the Automath system AUT-4 is maybe the first type-theoretic proof
assistant to feature proof-irrelevant propositions
\citep{deBruijn:automath4}.  The terminology used by de Bruijn is
\emph{fourth degree identification}, where proofs are expressions
considered to have degree 4, propositions and values degree 3, types
and $\ensuremath{\mathsf{Prop}}\xspace$ degree 2, and the universe $\ensuremath{\mathsf{Type}}\xspace$ of types degree 1.

Lean's type theory \citep{carneiro:thesis} features an impredicative
universe of proof-irrelevant propositions which hosts both
propositional equality and the accessibility predicate \citep[1.2]{aczel:inductive75}.  As both may
be eliminated into computational universes, decidability of
definitional equality is lost, as
demonstrated by Carneiro \citeyearpar{carneiro:thesis}
for the case of accessibility.  As a consequence,
typing is not decidable.


The type-theoretic proof assistants Agda and Coq have recently
\citep{gilbertCockxSozeauTabareau:popl19}
been equipped with a proof-irrelevant universe of propositions
(``strict \ensuremath{\mathsf{Prop}}\xspace'').  In this universe, propositional equality can be
defined, but cannot be eliminated into types that are not strict
propositions themselves.  Under this restriction,
Gilbert \citeyearpar[4.3]{gilbert:PhD}
formally proved normalization and decidability of type
checking for the predicative case.

Several open problems remain:
\begin{enumerate}
\item Does the theory with impredicative strict \ensuremath{\mathsf{Prop}}\xspace have
  normalization and decidability of type checking as well?
\item Does the addition of Werner's rule, while destroying proof
  normalization, preserve decidability of conversion and type
  checking?  (Since proofs
  are irrelevant for equality, they need not be normalized during type
  checking.)
\item Does Werner's rule preserve normalization in the predicative
  case?  (Our counterexamples make use of impredicativity.)
\end{enumerate}


\subsection*{Acknowledgments}
\noindent
The authors acknowledge support by the Swedish Research Council
(Vetenskapsrådet) under grants 2014-04864 \emph{Termination
  Certificates for Dependently-Typed Programs and Proofs via
  Refinement Types} and
2017-04064 \emph{Syntax and Semantics of Univalent Type Theory}.
Our research group is part of the EU Cost Action
CA15123 The European research network on types for programming and
verification (EUTypes).
We thank Mario Carneiro for contributing the original Lean implementation
of the first counterexample.

\bibliographystyle{alpha}

