natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Proto CLF is a work-in-progress proof assistant design combining ideas from Nuprl, LF, and undecidable type checking based on subsumptive equality types. “CLF” abbreviates “Computational Logical Framework”. So far, it’s just Matt Oliveri’s unpublished metatheory development, but information may appear here.
The main syntactic class is terms. Type expressions are terms. There are also variables and contexts.
variables ($x$, $y$, …) ::=
(Written as usual. Complain if you can’t tell them apart from metavariables.)
terms ($t$, $a$, $b$, $f$, $T$, $A$, $B$, $R$, …) ::=
$\lambda x.b \qquad$ (lambda abstraction)
$f\,a \qquad$ (application)
$a = b \in C \qquad$ (equality type)
$\Pi x:A.B \qquad$ (dependent function type)
$\cap x:A.B \qquad$ (family intersection type)
$Comp \qquad$ (type of computations (realizers))
$\{x:A | B\} \qquad$ (subset/separation type)
$\{x = y | R\} \qquad$ (PER comprehension type)
$Bool \qquad$ (type of “booleans”) (two-element type)
To be added: an infinite type.
contexts ($\Gamma$, …) ::=
$\cdot$ |
$\Gamma,x:T$
As usual, the rules may make liberal use of informal list operations to work with contexts.
$a \equiv_\beta b \qquad$ (beta conversion)
The only beta reduction is $(\lambda x.b)\,a \longrightarrow_\beta b[a/x]$. Conversion is the congruence closure.
The other judgment forms will be defined inductively by the rules below. They are:
$\Gamma \vdash T\,type \qquad$ (type validity)
$\Gamma \vdash t \Vdash T \qquad$ (element in a type) (realizer of a type)
Note that in Nuprl, the ($\Gamma \vdash t \Vdash T$) form is written ($\Gamma \vdash T\;\lfloor ext t \rfloor$). The “extract” part is computed from a derivation, so the user thinks of the judgment as stating that the type is inhabited.
In the rules below, however, no attention is paid to what can be metatheoretically computed with terms or derivations. That is (important) future work.
($\Gamma \vdash t\,:\,T$) is not used in order to avoid the misinterpretation of this judgment form as intrinsic typing of terms. Note the contrast with variables, which are intrinsically typed.
The ($t\,:\,T$) form can be translated to this system as either ($t \Vdash T$) or ($? \Vdash t \in T$). The latter uses the abbreviation “$\in$” defined below, and the abuse of meta-notation that we don’t care what goes in the “$?$”. With ($t \Vdash T$), we think of $t$ as resulting from the proof of $T$. With ($? \Vdash t \in T$), we think of the “semantic judgment” ($t \in T$) as a goal to prove internally. The rules ensure that these two ways of expressing an element of a type are interderivable. From this point on, ($\Gamma \vdash ? \Vdash T$) will be written as just ($\Gamma \vdash T$), although it remains informal.
$a \in A\;\coloneqq\;a = a \in A$
$A \to B\;\coloneqq\;\Pi \underline{\;}:A.B$
$A \wedge B\;\coloneqq\;\{\underline{\;}:A | B\}$
“$A$ equality is respected in $B$.”:
$A \prec B\;\coloneqq\;\Pi t:Comp.\Pi t':Comp. (t \in B)\to(t = t' \in A)\to(t = t' \in B)$
“$A$ members are included in $B$.”:
$A \subseteq B\;\coloneqq\;\Pi t:Comp.(t \in A)\to(t \in B)$
“$A$ is a subtype of $B$.”:
$A \lt\!\!:\;B\;\coloneqq\;(\lambda x.x) \in (A \to B)$
Note: ($A \lt\!\!:\;B$) ought to be logically equivalent to ($A \subseteq B \wedge A \prec B$), using the rules. And also to ($\Pi t:Comp.\Pi t':Comp.(t = t' \in A)\to(t = t' \in B)$). So semantically, thinking of types as PERs, subtypes are subrelations.
“$A$ is a refinement/subquotient of $B$.”:
$A \sqsubseteq B\;\coloneqq\;A \subseteq B \wedge B \prec A$
Note the reversal of $\prec$ in $\sqsubseteq$, compared to $\lt\!\!:$. As relations on types, $\subseteq$, $\lt\!\!:$, and $\sqsubseteq$ ought to be preorders. $\prec$ is not transitive.
The Church booleans:
$tru\;\coloneqq\;\lambda t.\lambda f.t$
$fls\;\coloneqq\;\lambda t.\lambda f.f$
$\top\;\coloneqq\;tru = tru \in Bool$
$\bottom\;\coloneqq\;tru = fls \in Bool$
“Squash” of $A$:
$\lfloor A \rfloor\;\coloneqq\;\{\underline{\;}:\top | A\}$
These rules are not the final rules that are planned to be implemented in CLF. The major differences planned for the final rules from those here are:
The expectation and hope is that the result will look fairly similar to algorithmic elaboration-style type checking rules. These rules will be the primitive tactics, and type checking will thus be a special case of running tactic trees.
We have a strong equality formation rule, inspired by the medium-strength rule from Anand & Rahli, which is also stronger than the usual one. Here is respect-based equality formation:
The $Comp$ type, which is called $Base$ in Nuprl:
The PER comprehension type was originally conceived by Stuart Allen, and then forgotten and subsequently reintroduced. However, I think Nuprl had already had $Base$, subsets, and quotients, which make it definable. The real innovation is how PER comprehension and the strengthened equality formation rule interact to allow internal, logical-relations-style type definitions. We only allow forming a PER type from a pseudo-PER, rather than implicitly taking the symmetric transitive closure of any family:
The untyped beta conversion rules have the same role as Nuprl’s direct computation rules:
Every type respects itself, and $Comp$. (Yes, you can use any term you like as the proof.):
A reflexivity rule, but any term can be the proof:
Terms participating in equality are elements. Normally this would only be admissible, but in CLF, it comes in handy to make it into “selectivity” rules:
Note that the above equality rules make ($\Gamma \vdash t \Vdash T$) and ($\Gamma \vdash t \in T$) interderivable, as promised.
We use a “subsumptive” rewrite rule as equality elimination. “Subsumptive” refers to the property that the proof of the type we rewrite in is unaffected. The terminology “subsumptive” for this is new to CLF, although this is effectively the same equality elimination rule as in Nuprl. The terminology comes from “subsumptive” vs “coercive” implementations of subtyping. Note that formally, CLF has no typed judgmental equality. Semantically, it’s an extensional type theory, but the semantic equality judgment is implemented as the equality type. This is sound due to equality reflection. So this rule is semantically a consequence of equality reflection, equality substitution, and (typed) conversion. As with equality reflection, the proof of equality is irrelevant:
Any two terms are equal as the (consequently unique) proof of a true equality:
That means $\top$ too, which is thus the maximum PER, ordered by subtyping. (Well, just as soon as we make $tru$ an element of $Bool$.)
We have the standard application rule, and a variant of function extensionality:
Unconventionally, we consider function extensionality to be the $\Pi$ intro rule, and derive the fact that lambdas implement functions.
Elements of a family intersection are like elements of a $\Pi$ type, except you don’t have to apply them. An intersection element is already an element of all instances of the family. So the rules for family intersection are analogous to the rules for $\Pi$:
The subset type resembles an existential quantifier. In the elimination rule, the proof part must be computationally irrelevant, since an element of a subset does not include the proof. Nuprl handles this with a hidden assumption, which is the practical way to do it. But it’s also sound to just stick in a free variable side condition.
The rules for PER comprehension are made simpler by the fact that we required $R$ to be a pseudo-PER in the formation rule. The idea is that ($(t1 = t2 \in \{x1 = x2 | R\;x1\;x2\}) \leftrightarrow \lfloor R\;t1\;t2 \rfloor$), using the squash type constructor defined above. So comprehension and equality are almost inverse; you just lose the computational content of the equivalence proof.
Exercise: Does the following rule express ($Bool \subseteq Comp$), ($Bool \lt\!\!:\;Comp$), or ($Bool \sqsubseteq Comp$)?
Our elimination rule is intuitively characterizing $Bool$ as the least type containing $tru$ and $fls$. The usual elimination rule is derived; it’s derivable because Church booleans actually work.
An ex falso quodlibet rule, which is technically about booleans, because of how we defined $\bottom$. Note that this makes $\bottom$ the minimum PER, ordered by inclusion, subtyping, or refinement.
The structural rules of weakening and substitution are admissible. “Strengthening” is not. Nonadmissibility of strengthening means: just because a variable isn’t free in the conclusion doesn’t mean the derivation isn’t using it. This is typical of extensional type theory. Typically it’s considered all the fault of equality reflection, which may be technically true for some systems. But Nuprl turned this apparent bug into a feature: subsets and intersections provide flexible control over which proofs make it into the computational content, and which are merely establishing external facts. Computational irrelevance is implemented by literally omitting the irrelevant proofs from terms. This leads to the lack of strengthening, and to undecidable type checking. The restriction imposed by equality reflection is that equality proofs never have computational content.
CLF follows Nuprl in trying to give the user maximum control over the terms used to represent elements. The hope is that with care, this can allow significantly greater convenience and performance than with decidable dependent type systems, which are committed to retaining enough annotations to effectively reject ill-typed terms.
You’d think a statement should make sense before you try to prove it. And likewise, that a type should be valid before you try to construct an element. But in practice, it also works to consider a typed construction as providing evidence that the type makes sense. Specifically, the only way to derive ($\Gamma \vdash t \Vdash T$) is if you could also derive ($\Gamma \vdash T\,type$). That’s a “sanity check” admissible rule. It’s probably admissible for the judgments defined by the rules above.
Also, since the only way to derive type validity in this system (not using the sanity admissible rule) is to use a type former, a derivation of type validity implies that there are derivations of validity for the subexpressions of the type expression. These are “inversion” admissible rules.
For full Nuprl, it seems practically impossible to prove admissibility of sanity or inversion, if they’re not just included among the primitive rules. But they can be included among the primitive rules, because they’re true in the semantics. Due to the way hypothetical judgments are defined, making the inversion rules true requires making type equality intensional.
The above rules are the result of an experiment to reason about formal derivability in a Nuprl-style system. In the PER semantics that the above rules were based on, type equality is extensional. So the basic rules directly satisfied were more complicated, since they needed extra premises that inversion would’ve made redundant. The above rules are actually admissible rules relative to those basic rules. Sanity and inversion are “probably” admissible for the above rules because what’s actually known is that they’re admissible for the basic rules; they were in fact used to prove the above rules.
So the experiment was partially successful, but I (Matt Oliveri) don’t recommend the approach. It cannot be easily adapted to handle universes, and some of the rules above still have type validity premises that a fully semantic approach could avoid.
It may seem weird that Nuprl is based on a particular PER semantics, if you think of it as a mathematical model. But if you think of it as a proof theoretic technique that reasons about realizability instead of formal derivability, perhaps it’s more palatable.
Thinking that way, all the consequences of the PER semantics are like admissible rules, and can be added to the formal system if they’re useful. But it still seems like a good idea to try and find a stable formal system with enough rules that incompleteness is not a problem in practice.
This raises questions though: If the formal rules of a Nuprl-style system are considered admissible, what defines the system? What are the mathematical models of Nuprl-style systems? If they’re considered unnatural, should Nuprl-style systems be modified?
In my (Matt Oliveri’s) opinion, Nuprl-style systems are potentially relevant and useful to mathematics, but it’s not currently clear exactly how that might work.
Now that we’ve covered the issue that the distinction between derivable and admissible doesn’t really matter for this system, we can get to explaining particular aspects that may seem to be in particular need of an explanation.
The equality formation rule refers to the respect (“$\prec$”) relation. The latter is not primitive, it’s defined in terms of equality. Is that OK? Yes: Because of the rule that all types respect $Comp$, we get enough instances of equality formation to prove:
If it still seems suspiciously circular, rest assured that in the semantics, respecting computational equivalence is more basic than anything in the type system. The rule about respecting $Comp$ just exposes the fact internally.
Because every type respects itself, we get all the instances of equality formation from Martin-Löf type theory. Equality types beyond that are for reasoning about membership.
Taking function extensionality to be $\Pi$ intro seems odd. Not only is it not about lambdas, it’s not apparently about elements at all; just equality. That’s (one place) where the selectivity rules are handy. The function extensionality rule is strong enough to combine with selectivity (and reflexivity) to derive elements of function type. A term is a function when you can apply it to an argument to get a result:
Proving that lambdas are functions additionally uses beta conversion. Lambdas are functions, not by fiat, but because they produce results when applied.
Note that not all functions are denoted by lambdas. At the very least, the empty function is denoted by any term you like. That is, a function type with empty domain has the same PER as $\top$. However, any function is equal to a lambda, when considered only as a function. Formally, we have
but not
.
With such a small set of type constructors, it may be hard to tell, but congruence rules are rarely needed as primitives. Beta conversion was already defined as an untyped congruence closure, and for typed equality, the subsumptive rewrite rule does most of the work of congruence rules. The extensionality rules for $\Pi$ and $\cap$ are needed to help with binders and (our ersatz) hidden assumptions. That may turn out to handle everything, with this judgmental setup.
With many type theories $T$, it’s cumbersome but straightforward to define collections of the formal derivations of $T$ as type families in $T$. This provides a form of syntactic reflection of a system’s judgments within itself. There are ways of making syntactic reflection more convenient and/or powerful.
But Nuprl-style systems provide a quite different kind of judgmental reflection that we’ll call “semantic judgmental reflection”, or just “judgmental reflection” for short. The original example of judgmental reflection, and the basis of the name, is the equality reflection rule of extensional type theory (ETT), which makes the “identity” type family a reflection of the meaning of the element equality judgment of the same system. In a sense, this is still the only judgmental reflection principle in Nuprl-style systems. (But the type family is called “equality”.) The difference is in the interpretation of the equality judgment.
There are two styles of interpretation for ETT: intrinsic and extrinsic. Extrinsic is the original, since an example is Martin-Löf’s meaning explanation, which was the original justification for equality reflection. Intrinsic seems to have become the default one. It’s the style considered in Martin Hofmann’s thesis, for example. But Nuprl and CLF commit to the extrinsic style.
An irony is that by considering terms extrinsically typed, you consider them intrinsically meaningful. In Nuprl and CLF, following Martin-Löf, terms have an intrinsic computational meaning. The role of the Nuprl-style type system is to reason about that. (Remember: this can all be considered a substitute for admissible rules! …Probably.)
There is actually no interpretation necessary, for terms in general. The type system can be layered over the terms as they are, making use of an operational model of their computational meaning. (A denotational semantics would probably work too.) The details need not concern us here, but some things are important:
All of these points are important to the design of a Nuprl-style system. But the one that seems to distinguish the approach from intrinsic typing is that being an element is a special case of equality. In the intrinsic approach, equality is only meaningful when applied to two terms known to have the same type. So being an element must be somehow prior to equality. But with the judgment of being an element as a special case of equality, it’s simultaneous.
A lot of the power of judgmental reflection is that it can be understood as reasoning about the computational content of the language as it actually is. But since it’s probably not necessary to interpret Nuprl-style systems as being about their own syntax, we should speak of “computations”, not “closed terms”. In CLF, however they’re interpreted, computations are axiomatized as the elements of $Comp$. (And actually, it may be that types need not be computations.) Types are PERs on $Comp$, and are accessed by the equality judgment form, which is reflected by the equality type constructor. So you use equality types to reason about equality in types, and also membership of computations in types.
So then what’s with all this respect (“$\prec$”) stuff in the equality formation rule? If terms have an intrinsic computational meaning, and equality reasons about it, shouldn’t the rule be just:
?
No, that doesn’t work. The extra complexity has to do with making the axiomatization work for open terms. Consider the type $I\;\coloneqq\;\{x = y | x \in Bool \wedge y \in Bool\}$. Then $tru = fls \in I$. But then consider ($x:I \vdash tru = x \in Bool\,type$). The simple formation rule would derive it, but it doesn’t make sense, because ($tru = tru \in Bool$) and ($tru = fls \in Bool$) are different types, although $tru$ and $fls$ are the same $I$. The problem is that equality of types and elements is generally different from equality of computations, and we want well-typed open terms to respect equality of elements. The respect-based equality formation rule doesn’t derive the bad type family because you’d need to find some type $T$ such that ($x:I \vdash x \Vdash T$) and ($T \prec Bool$). But if ($x:I \vdash x \Vdash T$), then $T$ considers $tru$ and $fls$ equal, while if ($T \prec Bool$), then it doesn’t. That variables and other open terms cannot generally be treated as computations is the sense in which variables are intrinsically typed: although elements are all realized by computations, an arbitrary element generally cannot be used as a computation, so reasoning about membership is constrained.
Based on the ability to reason about membership, in addition to equality, other types can be defined that seem like semantic judgments. For example, $\prec$, $\subseteq$, $\lt\!\!:$, and $\sqsubseteq$ were defined above. But what kinds of things are these semantic judgments in general?
A lenient answer is that semantic judgments are type (families) $J$ such that ($\lfloor J \rfloor \to J$) is inhabited. That is, the squash-stable types. All such types are isomorphic to equality types, and are the regular subobjects, if you consider a Nuprl-style system as a category. (In a manner analogous to ETT, using inhabitedness of equality types to determine equality of morphisms.)
A stricter definition of semantic judgments is that they are type (families) $J$ such that ($\lfloor J \rfloor \lt\!\!:\;J$). Types formed with equality, squash itself, $\prec$, $\subseteq$, $\lt\!\!:$, and $\sqsubseteq$ are always judgments in this strict sense. These types are extensionally equal to equality types (for example, this one: $(\lambda x.x) \in J$) in the following sense:
This definition of extensional equality is motivated by the “subsumption” (derived) rule:
So $\approx$ gives us subsumptions in both directions. Extensionally equal types denote the same PER.
Thus, the semantic judgments in the strict sense are regular subobjects defined in a convenient way so that they’re inhabited if and only if they’re basically $\top$. $\approx$ is itself a semantic judgment. Also:
However, ($A \subseteq B \wedge B \subseteq A$) is generally weaker. For example, $\top$ and $Comp$ have the same members (computations) but are not extensionally equal, or even isomorphic.
Combining ($Bool \lt\!\!:\;\Comp$) with the above elimination rule for $Bool$, you get this alternative elimination rule, where the motive is a family on $Comp$:
Curiously, you can go in the other direction too, and get both of the original rules from this one.
To get the usual elimination rule, prove that Church booleans are self-eliminating functions:
This is reasoning about membership, so we really do want to know that $Bool$s are $Comp$s. The usual elimination rule then just applies $b$ at that function type.
In Nuprl, it’s often possible to get induction rules without a premise showing that the motive is a valid family. The idea is that for sufficiently concrete types, validity of the motive can be proven pointwise, and moreover the cases of this proof are actually implied by the cases of the main induction.
In the current CLF rules though, it doesn’t seem possible to derive such rules. Also, including such strengthened induction rules as primitive doesn’t seem compatible with the current hybrid approach based on admissible formal rules: the sanity check would require an unusual type validity rule, which would ruin the inversion lemma. Basically the Nuprl-style justification for omitting the motive premise is “too semantic” for the current hybrid approach.
Abhishek Anand, Vincent Rahli, Towards a Formally Verified Proof Assistant, Interactive Theorem Proving (ITP) 2014 (project web, paper web, pdf)
Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli, A Type Theory with Partial Equivalence Relations as Types, Types for Proofs and Programs (TYPES) 2014 (slides, web, pdf)
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. dissertation, University of Edinburgh (1995). (link)
Last revised on May 24, 2019 at 11:20:04. See the history of this page for a list of all contributions to it.