typesys.tex

\section{Properties of the type system}
A theorem we would like to have of Lean's type system is that it is consistent, and sound with respect to some semantics in a well understood axiom system such as ZFC. Moreover, we want to relate this to Lean's actual typechecker, in the sense that anything Lean verifies as type-correct will be derivable in this axiom system and hence Lean will not certify a contradiction. But first we must understand some aspects of the type system itself, before relating it to other systems.

It is important to note that \emph{Lean's typechecker is not complete.} Obviously Lean can fail on correct theorems due to, say, running out of resources, but the ``algorithmic equality'' relation does not validate all definitional equalities. In fact, we can show that definitional equality as defined here is undecidable.

\subsection{Undecidability of definitional equality}\label{sec:undecidable}
Recall the type $\acc$ from \autoref{sec:large_elim}:
$$\acc_{<}:=\mu A:\alpha\to\P.\ (\intro:\forall x:\alpha.\;(\forall y:\alpha.\;y<x\to A\;y)\to A\;x)$$
(We are fixing a type $\alpha$ and a relation ${<}:\alpha\to\alpha\to\P$ here.) Informally, we would read this as: ``$x$ is $<$-accessible if for all $y<x$, $y$ is $<$-accessible''. Accessibility is then inductively generated by this clause. If every $x:\alpha$ is accessible, then $<$ is a well-founded relation. One interesting fact about $\acc$ is that we can project out the argument given a proof of $\acc\;x$:
\begin{align*}
\inv_x&:\acc\;x\to\forall y:\alpha.\;y<x\to\acc\;y\\
\inv_x&:=\lambda a:\acc\;x.\;\lambda y:\alpha.\;\rec_{\acc}\;(\lambda z.\;y<z\to\acc\;y)\\
&(\lambda z.\;\lambda h:(\forall w.\;w<z\to\acc\;w).\;\lambda \_.\;h\;y)\;x\;a
\end{align*}
Note that the output type of $\inv_x$ is the same as the argument to $\intro\;x$. Thus, we have
$$a\equiv\intro_\acc\;x\;(\inv_x\;a)$$
by proof irrelevance.

Why does this matter? Normally, any proof of $\acc\;x$ could only be unfolded finitely many times by the very nature of inductive proofs, but if we are in an inconsistent context, it is possible to get a proof of wellfoundedness which isn't actually wellfounded, and we can end up unfolding it forever.

To show how to get undecidability from this, suppose $P:\N\to\bf 2$ is a decidable predicate, such as $P\;n:=\;$``Turing machine $M$ runs for at least $n$ steps without halting'', for which $P\;n$ is decidable but $\forall n.\;P\;n$ is not. Let $>$ be the standard greater-than function on $\N$ (which is not well-founded). We define a function $f:\forall n.\;\acc_{>}\;n\to\bf 1$ as follows:
\begin{align*}
f&:=\rec_{\acc}\;(\lambda\_.\;{\bf 1})\;(\lambda x\;\_\;(g:\forall y.\;y>x\to{\bf 1}).\\
&\qquad\mathsf{if}\;P\;x\;\mathsf{then}\;g\;(x+1)\;(p\;x)\;\mathsf{else}\;())
\end{align*}
where $p\;n$ is a proof of $n<n+1$. Of course this whole function is trivial since the precondition $\acc_{>}n$ is impossible, but definitional equality works in all contexts, including inconsistent ones. This function evaluates as:
$$f\;n\;(\intro_\acc\;n\;h)\rightsquigarrow^*\mathsf{if}\;P\;n\;\mathsf{then}\;f\;(n+1)\;(h\;(n+1)\;(p\;n))\;\mathsf{else}\;()$$
and the \textsf{if} statement evaluates to the left or right branch depending on whether $P\;n\rightsquigarrow^*\mathsf{tt}$ or $P\;n\rightsquigarrow^*\mathsf{ff}$. Now, this is all true of the reduction relation $\rightsquigarrow$, but if we bring in the full power of definitional equivalence we have the ability to work up from a single proof $a:\acc_{>}\;0$:
\begin{align*}
f\;0\;a&\equiv f\;0\;(\intro_\acc\;0\;(\inv_0\;a))\\
&\equiv f\;1\;(\inv_0\;a\;1\;(p\;0))\\
&\equiv f\;1\;(\intro_\acc\;1\;(\inv_1\;(\inv_0\;a\;1\;(p\;0)))\\
&\equiv f\;2\;(\inv_1\;(\inv_0\;a\;1\;(p\;0))\;2\;(p\;1))\\
&\equiv\dots
\end{align*}
where we have shown the case where $P\;0$ and $P\;1$ both evaluate to true. If any $P\;n$ evaluates to false, then we will eventually get an equivalence to $()$, but if $P\;n$ is always true, then $f$ will never reduce to $()$ -- every term definitionally equal to $f\;0\;a$ will contain a subterm def.eq. to $f$. So $a:\acc_{>}\;0\vdash f\;0\;a\equiv()$ holds if and only if $\forall n.\;P\;n$, and hence $\equiv$ is undecidable.

\subsubsection{Algorithmic equality is not transitive}
From the results of the previous section, given that algorithmic equality is implemented by Lean, and hence is obviously decidable, they cannot be equal as relations, so there is some rule of definitional equality that is not respected by algorithmic equality. In the above example, we can typecheck the various parts of the equality chain to see that $\Leftrightarrow$ is not transitive:
\begin{align*}
f\;0\;a&\Leftrightarrow f\;0\;(\intro_\acc\;0\;(\inv_0\;a))\\
&\Leftrightarrow f\;1\;(\inv_0\;a\;1\;(p\;0))\\
&\mbox{but}\\
f\;0\;a&\not\Leftrightarrow f\;1\;(\inv_0\;a\;1\;(p\;0)).
\end{align*}
We can think of the middle step $f\;0\;(\intro_\acc\;0\;(\inv_0\;a))$ as a ``creative'' step, where we pick one of the many possible terms of type $\acc_{>}\;0$ which happens to reduce in the right way. But since the expression $f\;0\;a$ is a normal form, we don't attempt to reduce it, and indeed if we did we would have nontermination problems (since reduction here only makes the term larger).

Note that the fact that we are in an inconsistent context doesn't matter for this: we could have used $a:\acc_{<}\;1$ with the same result.

This instance of non-transitivity can be traced back to the usage of a subsingleton eliminator via $\acc$. There is another, less known source of non-transitivity: quotients of propositions. While this is not a particularly useful operation, since any proposition is already a subsingleton, so a quotient will not do anything, they can technically be formed, and $\lift$ acts like a subsingleton eliminator in this case. So for example, if $p:\P$, $R:p\to p\to\P$, $\alpha:\U_1$, $f:p\to\alpha$, $H:\forall x\;y.\;r\;x\;y\to f\;x= f\;y$, $q:p/R$ and $h:p$, then:
\begin{align*}
\lift_R\;\alpha\;f\;H\;q&\Leftrightarrow \lift_R\;\alpha\;f\;H\;(\mk_R\;h)\Leftrightarrow f\;h\\
&\mbox{but}\\
\lift_R\;\alpha\;f\;H\;q&\not\Leftrightarrow f\;h.
\end{align*}

\subsubsection{Failure of subject reduction}
While the type system given here actually satisfies subject reduction (which is to say, if $\Gamma\vdash e:\alpha$ and $e\rightsquigarrow e'$ (or $\Gamma\vdash e\Leftrightarrow e'$, or $\Gamma\vdash e\equiv e'$), then $\Gamma\vdash e':\alpha$), this is because we use the $\equiv$ relation in the conversion rule $\Gamma\vdash e:\alpha$, $\Gamma\vdash \alpha\equiv\beta$ implies $\Gamma\vdash e:\beta$. If we used algorithmic equality instead, to get a variant typing judgment $\Gamma\Vdash e:\alpha$ closer to what one would expect of the Lean typechecker, we find failure of subject reduction, directly from failure of transitivity. If $\Gamma\vdash\alpha\Leftrightarrow\beta$, $\Gamma\vdash\beta\Leftrightarrow\gamma$, $\Gamma\vdash\alpha\not\Leftrightarrow\gamma$, and $\Gamma\Vdash e:\gamma$, then:
\begin{itemize}
\item $\Gamma\Vdash \mbox{id}_\beta\;e:\beta$ because the application forces checking $\Gamma\vdash\beta\Leftrightarrow\gamma$.
\item $\Gamma\Vdash \mbox{id}_\alpha\;(\mbox{id}_\beta\;e):\alpha$ since the application forces checking $\Gamma\vdash\alpha\Leftrightarrow\beta$.
\item But $\Gamma\not\Vdash \mbox{id}_\alpha\;e:\alpha$ because this requires $\Gamma\vdash\alpha\Leftrightarrow\gamma$ which is false.
\end{itemize}
Since we obviously have $\mbox{id}_\beta\;e\rightsquigarrow e$ by the $\beta$ and $\delta$ rules, this is a counterexample to subject reduction.
\subsection{Regularity}
These lemmas are essentially trivial inductions and are true by virtue of the way we set up the type system, so they are recorded here simply to keep track of the invariants.

\begin{lemma}[Regularity]\label{thm:reg}
\begin{thmlist}
\item If $\Gamma\vdash e:\alpha$, then $\vdash\Gamma\;\mathsf{ok}$.
\item If $\Gamma\vdash e:\alpha$, then $FV(e)\cup FV(\alpha)\subseteq\Gamma$.
\item If $\Gamma\vdash\alpha\type$, then $\Gamma\vdash\alpha:\U_\ell$ for some $\ell$.
\item If $\Gamma\vdash e:\alpha$, then $\Gamma\vdash\alpha\type$.
\item\label{item:defeq_reg2} If $\Gamma\vdash e\equiv e'$, then there exists $\alpha,\alpha'$ such that $\Gamma\vdash e:\alpha$ and $\Gamma\vdash e':\alpha'$.
\item If $\Gamma;t:F\vdash K\spec$, then $\Gamma\vdash F\type$ (and more precisely, $F=\forall x::\alpha.\;\U_\ell$ for some $\alpha,\ell$).
\item If $\Gamma;t:F\vdash K\spec$ and $(c:\alpha)\in K$, then $\Gamma;t:F\vdash\alpha\ctor$.
\item If $\Gamma;t:F\vdash \alpha\ctor$, then $\Gamma,t:F\vdash\alpha\type$.
\end{thmlist}
\end{lemma}
\begin{proof}
By induction on the respective judgments (all of the parts may be proven separately).
\end{proof}

\begin{lemma}[Weakening]\label{thm:weak}
\begin{thmlist}
\item If $\Gamma\vdash e:\alpha$ and $\vdash\Gamma,\Delta\ok$, then $\Gamma,\Delta\vdash e:\alpha$.
\item If $\Gamma\vdash e\equiv e'$ and $\vdash\Gamma,\Delta\ok$, then $\Gamma,\Delta\vdash e\equiv e'$.
\item If $\Gamma,\Delta\vdash e:\alpha$ and $FV(e)\subseteq\Gamma$, then $\Gamma\vdash e:\alpha$.
\item If $\Gamma,\Delta\vdash e\equiv e'$ and $FV(e)\cup FV(e')\subseteq\Gamma$, then $\Gamma\vdash e\equiv e'$.
\item $\Gamma\vdash e:\alpha$ implies $\Gamma\vdash' e:\alpha$, and $\Gamma\vdash e\equiv e'$ implies $\Gamma\vdash' e\equiv e'$, where the modified judgment $\vdash'$ eliminates the weakening rules and replaces the variable and universe rules with
$$\frac{(x:\alpha)\in\Gamma}{\Gamma\vdash x:\alpha}\qquad\frac{}{\Gamma\vdash \U_\ell:\U_{S\ell}}\qquad\frac{\ell\equiv\ell'}{\Gamma\vdash \U_\ell\equiv\U_{\ell'}}$$
\end{thmlist}
\end{lemma}
\begin{proof}
(1,2) and (3,4) are each proven by mutual induction on the first hypothesis. For (5), since weakening is provable for the judgment $\vdash'$ it follows that all rules of $\vdash$ are provable in $\vdash'$.
\end{proof}

\begin{lemma}[Properties of substitution]\label{thm:subst}
\begin{thmlist}
\item If $\Gamma,x:\alpha,\Delta\vdash e_1\equiv e_1'$ and $\Gamma\vdash e_2:\alpha$, then $\Gamma,\Delta[e_2/x]\vdash e_1[e_2/x]\equiv e_1'[e_2/x]$.
\item\label{item:subst_ty} If $\Gamma,x:\alpha,\Delta\vdash e_1:\beta$ and $\Gamma\vdash e_2:\alpha$, then $\Gamma,\Delta[e_2/x]\vdash e_1[e_2/x]:\beta[e_2/x]$.
\item If $\Gamma,x:\alpha\vdash e_1:\beta$ and $\Gamma\vdash e_2\equiv e_2':\alpha$, then $\Gamma\vdash e_1[e_2/x]\equiv e_1[e_2'/x]$.
\end{thmlist}
\end{lemma}
\begin{proof} (1) and (2) must be proven simultaneously by induction on the first hypotheses. All cases are straightforward. In the proof irrelevance case, we know $\Gamma,x:\alpha\vdash e_1:p$ and $\Gamma,x:\alpha\vdash e_1':p$ for some $p$ with $\Gamma,x:\alpha\vdash p:\P$. By the induction hypothesis, $\Gamma\vdash e_1[e_2/x]:p[e_2/x]$ and $\Gamma\vdash e_1'[e_2/x]:p[e_2/x]$ and $\Gamma\vdash p[e_2/x]:\P[e_2/x]$; but $\P[e_2/x]=\P$ so proof irrelevance applies to show $\Gamma\vdash e_1[e_2/x]=e_1'[e_2/x]$.

(3) is proven by induction on the structure of $e_1$ and applying compatibility lemmas in each case.
\end{proof}

With this theorem we can upgrade lemma \ref{item:defeq_reg2} to:
\begin{lemma}[Regularity continued]
\begin{thmlist}
\item If $\Gamma\vdash e\equiv e'$, then there exists $\alpha$ such that $\Gamma\vdash e\equiv e':\alpha$.
\item\label{item:red_equiv} If $\Gamma\vdash e:\alpha$ and $e\rightsquigarrow e'$, then $\Gamma\vdash e\equiv e':\alpha$.
\item\label{item:alg_defn} If $\Gamma\vdash e:\alpha$ and $\Gamma\vdash e':\alpha$, and $\Gamma\vdash e\Leftrightarrow e'$, then $\Gamma\vdash e\equiv e'$.
\end{thmlist}
\end{lemma}
\begin{proof}
Straightforward induction on the derivation of $\Gamma\vdash e\equiv e'$. We need lemma \ref{item:subst_ty} to typecheck both sides of the $\beta$ rule. Note that the induction hypothesis is not strong enough for the application rule, except that we explicitly require that both sides have agreeing types in this case.
\end{proof}

Lemma \ref{item:red_equiv} implies subject reduction for $\rightsquigarrow$, and lemma \ref{item:alg_defn} is the main reason we are interested in algorithmic equality, since it is a thing we can check which implies ``true'' well-typedness. It is this that will allow us to conclude that Lean is consistent given that the ideal typing judgment we are developing here is consistent.