patternMinor
Why are recursive types needed as primitives for proofs in dependent type systems?
Viewed 0 times
whyneededaresystemsprimitivestyperecursivefortypesdependent
Problem
I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-preserving intermediate representation for a compiler system.
I understand that (co-)recursive types are representable, computationally, using $\Pi$ as the only type constructor. I've read, though, that they cannot be used to build proofs by induction (forgive me, I can't find where now!), e.g., that I couldn't prove that $0\neq 1$ in plain CoC (even though $\texttt{Nat}$ is typeable as $\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N}$).
I assume this is why they built the calculus of inductive constructions (CIC). Is this correct? But why? I couldn't find any material explaining why such proofs cannot be represented without using (co-)inductive types as primitives. If this is not true, then why add them as primitives in CIC?
I understand that (co-)recursive types are representable, computationally, using $\Pi$ as the only type constructor. I've read, though, that they cannot be used to build proofs by induction (forgive me, I can't find where now!), e.g., that I couldn't prove that $0\neq 1$ in plain CoC (even though $\texttt{Nat}$ is typeable as $\Pi(\mathbb{N}:*).\Pi(S:\mathbb{N}\rightarrow\mathbb{N}).\Pi(Z:\mathbb{N}).\mathbb{N}$).
I assume this is why they built the calculus of inductive constructions (CIC). Is this correct? But why? I couldn't find any material explaining why such proofs cannot be represented without using (co-)inductive types as primitives. If this is not true, then why add them as primitives in CIC?
Solution
I'm not an expert, but I'll share what I understood so far with an example.
Let's consider the boolean type in CoC, using its standard encoding:
$$
\begin{array}{l}
\mathbb{B} = \Pi_{\tau:*} \tau \to \tau \to \tau
\\
\mathsf{tt} = \lambda \tau:*,x:\tau,y:\tau.\ x
\\
\mathsf{ff} = \lambda \tau:*,x:\tau,y:\tau.\ y
\end{array}
$$
We might expect to be able to prove
$$
\Pi_{b : \mathbb{B}} b={\sf tt} \lor b = {\sf ff} \qquad(*)
$$
Indeed, this quickly follows from the dependent elimination/induction principle we have e.g. in CiC
$$
\mathbb{B}_{ind} : \Pi_{P:\mathbb{B}\to*} P({\sf tt}) \rightarrow P({\sf ff}) \rightarrow \Pi_{b:\mathbb{B}} P(b)
$$
However, we can not really expect (*) to hold in all models of CoC!
Intuitively, a value in $\mathbb{B}$ should roughly be a family of functions
$\{f_\tau\}_{\tau}$ assigning to each type $\tau$ a value in the interpretation of $\tau\to\tau\to\tau$. But this does not force $f_\tau$ to be one between the values of $\sf tt,ff$. We could have e.g. (informally)
$$
f_{\mathbb{N}}(n)(m) = n+m
$$
To be sure that the values of $\sf tt,ff$ are the only possible values, we need to restrict ourselves to parametric models. Indeed (I think) the property $(*)$ can be proven from the free theorem associated to the polytype $\mathbb{B}$.
However, as far as I understand, CoC does not rule out ad-hoc models, where parametricity does not hold. In some of those, $()$ is simply false. By soundness, in the presence of a countermodel, we conclude that $()$ is not inhabited in CoC. Consequently, there's no $\mathbb{B}_{ind}$ term in CoC, either.
Let's consider the boolean type in CoC, using its standard encoding:
$$
\begin{array}{l}
\mathbb{B} = \Pi_{\tau:*} \tau \to \tau \to \tau
\\
\mathsf{tt} = \lambda \tau:*,x:\tau,y:\tau.\ x
\\
\mathsf{ff} = \lambda \tau:*,x:\tau,y:\tau.\ y
\end{array}
$$
We might expect to be able to prove
$$
\Pi_{b : \mathbb{B}} b={\sf tt} \lor b = {\sf ff} \qquad(*)
$$
Indeed, this quickly follows from the dependent elimination/induction principle we have e.g. in CiC
$$
\mathbb{B}_{ind} : \Pi_{P:\mathbb{B}\to*} P({\sf tt}) \rightarrow P({\sf ff}) \rightarrow \Pi_{b:\mathbb{B}} P(b)
$$
However, we can not really expect (*) to hold in all models of CoC!
Intuitively, a value in $\mathbb{B}$ should roughly be a family of functions
$\{f_\tau\}_{\tau}$ assigning to each type $\tau$ a value in the interpretation of $\tau\to\tau\to\tau$. But this does not force $f_\tau$ to be one between the values of $\sf tt,ff$. We could have e.g. (informally)
$$
f_{\mathbb{N}}(n)(m) = n+m
$$
To be sure that the values of $\sf tt,ff$ are the only possible values, we need to restrict ourselves to parametric models. Indeed (I think) the property $(*)$ can be proven from the free theorem associated to the polytype $\mathbb{B}$.
However, as far as I understand, CoC does not rule out ad-hoc models, where parametricity does not hold. In some of those, $()$ is simply false. By soundness, in the presence of a countermodel, we conclude that $()$ is not inhabited in CoC. Consequently, there's no $\mathbb{B}_{ind}$ term in CoC, either.
Context
StackExchange Computer Science Q#68296, answer score: 7
Revisions (0)
No revisions yet.