nLab
prototype CLF

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Constructivism, Realizability, Computability

Contents

Idea

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.

Syntax

Term grammar

The main syntactic class is terms. Type expressions are terms. There are also variables and contexts.

variables (xx, yy, …) ::= (Written as usual. Complain if you can’t tell them apart from metavariables.)

terms (tt, aa, bb, ff, TT, AA, BB, RR, …) ::=

  • λx.b\lambda x.b \qquad (lambda abstraction)

  • faf\,a \qquad (application)

  • a=bCa = b \in C \qquad (equality type)

  • Πx:A.B\Pi x:A.B \qquad (dependent function type)

  • x:A.B\cap x:A.B \qquad (family intersection type)

  • CompComp \qquad (type of computations (realizers))

  • {x:A|B}\{x:A | B\} \qquad (subset/separation type)

  • {x=y|R}\{x = y | R\} \qquad (PER comprehension type)

  • BoolBool \qquad (type of “booleans”) (two-element type)

To be added: an infinite type.

contexts (Γ\Gamma, …) ::= \cdot | Γ,x:T\Gamma,x:T

As usual, the rules may make liberal use of informal list operations to work with contexts.

Judgment forms

a βba \equiv_\beta b \qquad (beta conversion)

The only beta reduction is (λx.b)a βb[a/x](\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:

ΓTtype\Gamma \vdash T\,type \qquad (type validity)

ΓtT\Gamma \vdash t \Vdash T \qquad (element in a type) (realizer of a type)

Note that in Nuprl, the (ΓtT\Gamma \vdash t \Vdash T) form is written (ΓTextt\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.

(Γt:T\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:Tt\,:\,T) form can be translated to this system as either (tTt \Vdash T) or (?tT? \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 (tTt \Vdash T), we think of tt as resulting from the proof of TT. With (?tT? \Vdash t \in T), we think of the “semantic judgment” (tTt \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, (Γ?T\Gamma \vdash ? \Vdash T) will be written as just (ΓT\Gamma \vdash T), although it remains informal.

Abbreviations

Semantic Judgment Forms

aAa=aAa \in A\;\coloneqq\;a = a \in A

ABΠ̲:A.BA \to B\;\coloneqq\;\Pi \underline{\;}:A.B

AB{̲:A|B}A \wedge B\;\coloneqq\;\{\underline{\;}:A | B\}

AA equality is respected in BB.”:

ABΠt:Comp.Πt:Comp.(tB)(t=tA)(t=tB)A \prec B\;\coloneqq\;\Pi t:Comp.\Pi t':Comp. (t \in B)\to(t = t' \in A)\to(t = t' \in B)

AA members are included in BB.”:

ABΠt:Comp.(tA)(tB)A \subseteq B\;\coloneqq\;\Pi t:Comp.(t \in A)\to(t \in B)

AA is a subtype of BB.”:

A<:B(λx.x)(AB)A \lt\!\!:\;B\;\coloneqq\;(\lambda x.x) \in (A \to B)

Note: (A<:BA \lt\!\!:\;B) ought to be logically equivalent to (ABABA \subseteq B \wedge A \prec B), using the rules. And also to (Πt:Comp.Πt:Comp.(t=tA)(t=tB)\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.

AA is a refinement/subquotient of BB.”:

ABABBAA \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.

Computations

The Church booleans:

truλt.λf.ttru\;\coloneqq\;\lambda t.\lambda f.t

flsλt.λf.ffls\;\coloneqq\;\lambda t.\lambda f.f

Type constructors

tru=truBool\top\;\coloneqq\;tru = tru \in Bool

tru=flsBool\bottom\;\coloneqq\;tru = fls \in Bool

“Squash” of AA:

A{̲:|A}\lfloor A \rfloor\;\coloneqq\;\{\underline{\;}:\top | A\}

Rules

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:

  • Use roughly Nuprl-style hidden assumptions, but with unhiding handled automatically.
  • Have an additional judgment form for goals whose realizer is ignored/arbitrary, which interacts with unhiding.
  • Add formal proof terms.

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.

Type Formation

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:

ΓpACΓqBCΓaAΓbBΓa=bCtype ΓAtypeΓ,x:ABtypeΓΠx:A.Btype ΓAtypeΓ,x:ABtypeΓx:A.Btype\begin{gathered} \frac{\Gamma \vdash p \Vdash A \prec C \qquad \Gamma \vdash q \Vdash B \prec C \qquad \Gamma \vdash a \Vdash A \qquad \Gamma \vdash b \Vdash B} {\Gamma \vdash a = b \in C\,type} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash B\,type} {\Gamma \vdash \Pi x:A.B\,type} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash B\,type} {\Gamma \vdash \cap x:A.B\,type} \end{gathered}

The CompComp type, which is called BaseBase in Nuprl:

ΓComptype ΓAtypeΓ,x:ABtypeΓ{x:A|B}type\begin{gathered} \frac{}{\Gamma \vdash Comp\,type} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash B\,type} {\Gamma \vdash \{x:A | B\}\,type} \end{gathered}

The PER comprehension type was originally conceived by Stuart Allen, and then forgotten and subsequently reintroduced. However, I think Nuprl had already had BaseBase, 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:

Γ,x1:Comp,x2:CompRtype Γ,y1:Comp,y2:CompsR[y1,y2/x1,x2]R[y2,y1/x1,x2] Γ,y1:Comp,y2:Comp,y3:ComptR[y1,y2/x1,x2]R[y2,y3/x1,x2]R[y1,y3/x1,x2]Γ{x1=x2|R}type ΓBooltype\begin{gathered} \frac{\begin{array}{l}\Gamma,x1:Comp,x2:Comp \vdash R\,type \\ \Gamma,y1:Comp,y2:Comp \vdash s \Vdash R[y1,y2/x1,x2] \to R[y2,y1/x1,x2] \\ \Gamma,y1:Comp,y2:Comp,y3:Comp \vdash t \Vdash R[y1,y2/x1,x2] \to R[y2,y3/x1,x2] \to R[y1,y3/x1,x2]\end{array}} {\Gamma \vdash \{x1 = x2 | R\}\,type} \\ \\ \frac{}{\Gamma \vdash Bool\,type} \end{gathered}

Miscellaneous

x:TΓΓxT\frac{x:T \in \Gamma}{\Gamma \vdash x \Vdash T}

The untyped beta conversion rules have the same role as Nuprl’s direct computation rules:

A βBΓBtypeΓtAΓtB t βtΓtTΓtT\begin{gathered} \frac{A \equiv_\beta B \qquad \Gamma \vdash B\,type \qquad \Gamma \vdash t \Vdash A} {\Gamma \vdash t \Vdash B} \\ \\ \frac{t \equiv_\beta t' \qquad \Gamma \vdash t \Vdash T} {\Gamma \vdash t' \Vdash T} \end{gathered}

Every type respects itself, and CompComp. (Yes, you can use any term you like as the proof.):

ΓAtypeΓpAA ΓAtypeΓpCompA\begin{gathered} \frac{\Gamma \vdash A\,type}{\Gamma \vdash p \Vdash A \prec A} \\ \\ \frac{\Gamma \vdash A\,type}{\Gamma \vdash p \Vdash Comp \prec A} \end{gathered}

Equality

A reflexivity rule, but any term can be the proof:

ΓtTΓpt=tT\frac{\Gamma \vdash t \Vdash T}{\Gamma \vdash p \Vdash t = t \in T}

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:

Γpt1=t2TΓt1T Γpt1=t2TΓt2T\begin{gathered} \frac{\Gamma \vdash p \Vdash t1 = t2 \in T}{\Gamma \vdash t1 \Vdash T} \\ \\ \frac{\Gamma \vdash p \Vdash t1 = t2 \in T}{\Gamma \vdash t2 \Vdash T} \end{gathered}

Note that the above equality rules make (ΓtT\Gamma \vdash t \Vdash T) and (ΓtT\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:

Γ,x:ABtypeΓpa1=a2AΓbB[a1/x]ΓbB[a2/x]\frac{\Gamma,x:A \vdash B\,type \qquad \Gamma \vdash p \Vdash a1 = a2 \in A \qquad \Gamma \vdash b \Vdash B[a1/x]} {\Gamma \vdash b \Vdash B[a2/x]}

Any two terms are equal as the (consequently unique) proof of a true equality:

ΓtTΓqp1=p2(t=tT)\frac{\Gamma \vdash t \Vdash T} {\Gamma \vdash q \Vdash p1 = p2 \in (t = t \in T)}

That means \top too, which is thus the maximum PER, ordered by subtyping. (Well, just as soon as we make trutru an element of BoolBool.)

Functions

We have the standard application rule, and a variant of function extensionality:

ΓfΠx:A.BΓaAΓfaB[a/x] ΓAtypeΓ,x:Apfx=fxBxFV(f,f)Γqf=fΠx:A.B\begin{gathered} \frac{\Gamma \vdash f \Vdash \Pi x:A.B \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash f\,a \Vdash B[a/x]} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash p \Vdash f\,x = f'\,x \in B \qquad x \notin FV(f,f')} {\Gamma \vdash q \Vdash f = f' \in \Pi x:A.B} \end{gathered}

Unconventionally, we consider function extensionality to be the Π\Pi intro rule, and derive the fact that lambdas implement functions.

Intersection

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:

Γbx:A.BΓaAΓbB[a/x] ΓAtypeΓ,x:Apb=bBxFV(b,b)Γqb=bx:A.B\begin{gathered} \frac{\Gamma \vdash b \Vdash \cap x:A.B \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash b \Vdash B[a/x]} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash p \Vdash b = b' \in B \qquad x \notin FV(b,b')} {\Gamma \vdash q \Vdash b = b' \in \cap x:A.B} \end{gathered}

Computation Formation

Γ,x:CompbCompΓλx.bComp ΓfCompΓaCompΓfaComp\begin{gathered} \frac{\Gamma,x:Comp \vdash b \Vdash Comp}{\Gamma \vdash \lambda x.b \Vdash Comp} \\ \\ \frac{\Gamma \vdash f \Vdash Comp \qquad \Gamma \vdash a \Vdash Comp} {\Gamma \vdash f\,a \Vdash Comp} \end{gathered}

Subset

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.

Γ,x:ABtypeΓaAΓbB[a/x]Γa{x:A|B} Γ,z:{x:A|B}CtypeΓ,x:A,y:BcC[x/z]yFV(c)Γa{x:A|B}Γc[a/x]C[a/z]\begin{gathered} \frac{\Gamma,x:A \vdash B\,type \qquad \Gamma \vdash a \Vdash A \qquad \Gamma \vdash b \Vdash B[a/x]} {\Gamma \vdash a \Vdash \{x:A | B\}} \\ \\ \frac{\Gamma,z:\{x:A | B\} \vdash C\,type \qquad \Gamma,x:A,y:B \vdash c \Vdash C[x/z] \qquad y \notin FV(c) \qquad \Gamma \vdash a \Vdash \{x:A | B\}} {\Gamma \vdash c[a/x] \Vdash C[a/z]} \end{gathered}

PER

The rules for PER comprehension are made simpler by the fact that we required RR to be a pseudo-PER in the formation rule. The idea is that ((t1=t2{x1=x2|Rx1x2})Rt1t2(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.

Γ{x1=x2|R}typeΓt2CompΓpR[t1,t2/x1,x2]Γqt1=t2{x1=x2|R} ΓCtypeΓR[t1,t2/x1,x2]type Γpt1=t2{x1=x2|R} Γ,z:R[t1,t2/x1,x2]cCzFV(c)ΓcC\begin{gathered} \frac{\Gamma \vdash \{x1 = x2 | R\}\,type \qquad \Gamma \vdash t2 \Vdash Comp \qquad \Gamma \vdash p \Vdash R[t1,t2/x1,x2]} {\Gamma \vdash q \Vdash t1 = t2 \in \{x1 = x2 | R\}} \\ \\ \frac{\begin{array}{l} \Gamma \vdash C\,type \qquad \Gamma \vdash R[t1,t2/x1,x2]\,type \\ \Gamma \vdash p \Vdash t1 = t2 \in \{x1 = x2 | R\} \\ \Gamma,z:R[t1,t2/x1,x2] \vdash c \Vdash C \qquad z \notin FV(c) \end{array}} {\Gamma \vdash c \Vdash C} \end{gathered}

Booleans

ΓtruBoolΓflsBool\frac{}{\Gamma \vdash tru \Vdash Bool} \qquad \frac{}{\Gamma \vdash fls \Vdash Bool}

Exercise: Does the following rule express (BoolCompBool \subseteq Comp), (Bool<:CompBool \lt\!\!:\;Comp), or (BoolCompBool \sqsubseteq Comp)?

ΓbBoolΓbComp\frac{\Gamma \vdash b \Vdash Bool}{\Gamma \vdash b \Vdash Comp}

Our elimination rule is intuitively characterizing BoolBool as the least type containing trutru and flsfls. The usual elimination rule is derived; it’s derivable because Church booleans actually work.

Γ,x:BoolCtypeΓcC[tru/x]ΓcC[fls/x]ΓbBoolΓcC[b/x]\frac{\Gamma,x:Bool \vdash C\,type \qquad \Gamma \vdash c \Vdash C[tru/x] \qquad \Gamma \vdash c \Vdash C[fls/x] \qquad \Gamma \vdash b \Vdash Bool} {\Gamma \vdash c \Vdash C[b/x]}

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.

ΓTtypeΓpΓtT\frac{\Gamma \vdash T\,type \qquad \Gamma \vdash p \Vdash \bottom} {\Gamma \vdash t \Vdash T}

Admissible rules

Structural rules

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.

Sanity and Inversion

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 (ΓtT\Gamma \vdash t \Vdash T) is if you could also derive (ΓTtype\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.

Admissible Rules vs PER Semantics

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.

Loose ends

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.

Equality uses respect which uses equality

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 CompComp, we get enough instances of equality formation to prove:

ΓAtypeΓBtypeΓABtype\frac{\Gamma \vdash A\,type \qquad \Gamma \vdash B\,type} {\Gamma \vdash A \prec B\;type}

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 CompComp 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.

Usual Pi-intro rule

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:

ΓAtypeΓ,x:AfxBxFV(f)ΓfΠx:A.B\frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash f\,x \Vdash B \qquad x \notin FV(f)} {\Gamma \vdash f \Vdash \Pi x:A.B}

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

Γ,f:Πx:A.Bf=(λx.fx)Πx:A.B\Gamma,f:\Pi x:A.B \vdash f = (\lambda x.f\,x) \in \Pi x:A.B

but not

Γ,f:Comp,Hf:fΠx:A.Bf=(λx.fx)Comp\Gamma,f:Comp,Hf:f \in \Pi x:A.B \vdash f = (\lambda x.f\,x) \in Comp

.

Congruence rules

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.

Semantic Judgmental Reflection

Equality reflection

With many type theories TT, it’s cumbersome but straightforward to define collections of the formal derivations of TT as type families in TT. 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:

  • Computational meaning pertains principally to closed terms, because free variables don’t compute; they’re just placeholders.
  • Some closed terms are designated as types, and denote PERs on closed terms.
  • For closed terms and types, the equality judgment form (t=tTt = t' \in T) just accesses the PER of the type.
  • For closed terms and types, the judgment of being an element of a type (tTt \in T) is a special case of equality.
  • It’s the judgments about closed terms that are reflected as closed types; judgments about open terms are not involved.

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 CompComp. (And actually, it may be that types need not be computations.) Types are PERs on CompComp, 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:

ΓTtypeΓt1=t2Ttype\frac{\Gamma \vdash T\,type}{\Gamma \vdash t1 = t2 \in T\,type}

?

No, that doesn’t work. The extra complexity has to do with making the axiomatization work for open terms. Consider the type I{x=y|xBoolyBool}I\;\coloneqq\;\{x = y | x \in Bool \wedge y \in Bool\}. Then tru=flsItru = fls \in I. But then consider (x:Itru=xBooltypex:I \vdash tru = x \in Bool\,type). The simple formation rule would derive it, but it doesn’t make sense, because (tru=truBooltru = tru \in Bool) and (tru=flsBooltru = fls \in Bool) are different types, although trutru and flsfls are the same II. 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 TT such that (x:IxTx:I \vdash x \Vdash T) and (TBoolT \prec Bool). But if (x:IxTx:I \vdash x \Vdash T), then TT considers trutru and flsfls equal, while if (TBoolT \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.

Other semantic judgments

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) JJ such that (JJ\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) JJ such that (J<:J\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: (λx.x)J(\lambda x.x) \in J) in the following sense:

ABA<:BB<:AA \approx B\;\coloneqq\;A \lt\!\!:\;B \wedge B \lt\!\!:\;A

This definition of extensional equality is motivated by the “subsumption” (derived) rule:

ΓtAΓA<:BΓtB\frac{\Gamma \vdash t \Vdash A \qquad \Gamma \vdash A \lt\!\!:\;B} {\Gamma \vdash t \Vdash B}

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:

(AB)(ABBA)(A \approx B) \approx (A \sqsubseteq B \wedge B \sqsubseteq A)

However, (ABBAA \subseteq B \wedge B \subseteq A) is generally weaker. For example, \top and CompComp have the same members (computations) but are not extensionally equal, or even isomorphic.

PER theory

More admissible/derived rules

Fun with subsets

Bool eliminations

Combining (Bool<:CompBool \lt\!\!:\;\Comp) with the above elimination rule for BoolBool, you get this alternative elimination rule, where the motive is a family on CompComp:

Γ,x:CompCtypeΓcC[tru/x]ΓcC[fls/x]ΓbBoolΓcC[b/x]\frac{\Gamma,x:Comp \vdash C\,type \qquad \Gamma \vdash c \Vdash C[tru/x] \qquad \Gamma \vdash c \Vdash C[fls/x] \qquad \Gamma \vdash b \Vdash Bool} {\Gamma \vdash c \Vdash C[b/x]}

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:

Γ,x:BoolCtypeΓbBoolΓbC[tru/x]C[fls/x]C[b/x]\frac{\Gamma,x:Bool \vdash C\,type \qquad \Gamma \vdash b \Vdash Bool} {\Gamma \vdash b \Vdash C[tru/x] \to C[fls/x] \to C[b/x]}

This is reasoning about membership, so we really do want to know that BoolBools are CompComps. The usual elimination rule then just applies bb 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.

Subtyping (Conjectural)

References

  • 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.