patternMinor
Algorithmic type checking for Calculus of Inductive Constructions
Viewed 0 times
calculusconstructionscheckingtypeforalgorithmicinductive
Problem
So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's documentation on the Calculus of Inductive Constructions (CioC) you can get a sense of things but it is far from algorithmic. Is there any reference on algorithmic type checking for CioC?
Solution
The problem of giving an algorithmic reading to the typing rules in CIC, and dependent type systems in general, is quite subtle.
One recommendation is Randy Pollack's Typechecking in Pure Type Systems, Gille Barthe's Type Checking *Injective Pure Type Systems and McKinna and Pollack's Pure Type Systems formalized.
The first basic idea is to "push" the conversion rule
$$ \frac{\Gamma \vdash t: A\quad A\simeq B}{\Gamma\vdash t : B}$$
into the application rule
$$ \frac{\Gamma \vdash t:A\quad \Gamma\vdash u:A' \quad A\simeq \Pi x: A'.B}{\Gamma\vdash t\ u:B\{x\mapsto u\}}$$
And similarly for "application-like" rules. The theorem is that these modified rules suffice for type-checking (without conversion), with the exception of a possible single application of conversion at the end.
This makes the rules type-directed, which allows a straightforward implementation. There are additional shortcuts which allow skipping verification of $\mathrm{WF}$, for example, if it is known that it is going to be derived later, or it is admissible.
As Luke notes, there is no complete treatment of such shortcuts, and the validity of these is sometimes quite complicated to prove (e.g. the "expansion postponement" rule).
Checking conversion of terms with $\delta$-reductions (defined functions) is a whole bag of worms: when checking
$$ f\ t_1\ldots t_n\simeq f\ u_1\ldots u_n$$
should you just check $t_i\simeq u_i$ for each $i$, or unfold $f$? The answer is, unsurprisingly, it depends. In general clever heuristics are used, e.g. "unfold $f$ if it is a projection, otherwise try checking equivalence of the arguments, and unfold $f$ if that fails".
One recommendation is Randy Pollack's Typechecking in Pure Type Systems, Gille Barthe's Type Checking *Injective Pure Type Systems and McKinna and Pollack's Pure Type Systems formalized.
The first basic idea is to "push" the conversion rule
$$ \frac{\Gamma \vdash t: A\quad A\simeq B}{\Gamma\vdash t : B}$$
into the application rule
$$ \frac{\Gamma \vdash t:A\quad \Gamma\vdash u:A' \quad A\simeq \Pi x: A'.B}{\Gamma\vdash t\ u:B\{x\mapsto u\}}$$
And similarly for "application-like" rules. The theorem is that these modified rules suffice for type-checking (without conversion), with the exception of a possible single application of conversion at the end.
This makes the rules type-directed, which allows a straightforward implementation. There are additional shortcuts which allow skipping verification of $\mathrm{WF}$, for example, if it is known that it is going to be derived later, or it is admissible.
As Luke notes, there is no complete treatment of such shortcuts, and the validity of these is sometimes quite complicated to prove (e.g. the "expansion postponement" rule).
Checking conversion of terms with $\delta$-reductions (defined functions) is a whole bag of worms: when checking
$$ f\ t_1\ldots t_n\simeq f\ u_1\ldots u_n$$
should you just check $t_i\simeq u_i$ for each $i$, or unfold $f$? The answer is, unsurprisingly, it depends. In general clever heuristics are used, e.g. "unfold $f$ if it is a projection, otherwise try checking equivalence of the arguments, and unfold $f$ if that fails".
Context
StackExchange Computer Science Q#41192, answer score: 4
Revisions (0)
No revisions yet.