|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
Substitution is usually defined as an operation on expressions containing variables. (These expressions may be terms, formulas?, propositions, dependent types, etc.) Suppose that an expression in the context of a variable , and that is an expression which has the same type as . Then we denote by
the result of substituting for all occurrences of in .
For example, if is and is , then is .
Note that in this approach, substitution is an operation on syntax, not an element of syntax itself. In particular, the bracket notation is part of “meta-syntax”, not the syntax in question. That is, the literal string of symbols “” is not itself an expression in the language under consideration, but denotes such an expression, in the same way that “” is not literally an integer but denotes the integer .
Substitution for multiple variables does not, in general, commute. That is,
are not in general the same: the former substitutes for occurrences of in , but not for occurrences of in , while the latter has the opposite behavior. We also write
to denote the simultaneous substitution of for and for , in which neither occurrences of in nor occurrences of in are substituted for; this is generally not the same as either iterated substitution.
If the language in question contains variable binders, then there is a subtlety to substitution: if contains free variables that are bound in , then we cannot simply textually substitute for and obtain an expression with the desired meaning.
For instance, if is , and is the free variable , then a literal interpretation of would produce . But is true (universally in its free variables) if the variables have type , while is not. The free variable in has been “captured” by the binder in .
We say that is substitutable for in if performing a literal textual substitution as above would not result in undesired variable capture. If is not substitutable for in , then we can always replace by an α-equivalent expression in which is substitutable for . Since we often consider formulas only up to -equivalence anyway, one usually defines the notation ”” to include an -conversion of , if necessary, to make substitutable for .
In computer implementations of type theories, however, the issue of variable binding and capture is one of the trickiest things to get right. Performing -conversions is difficult and tedious, and other solutions exist, such as using de Brujin indices? to represent bound variables.
A general property of type theories (and other formal mathematics) is that substitution is an admissible rule. Roughly, this means that if is an expression of some type, then so is the result of substitution (as long as and have the same type). This is generally not a rule “put into” the theory, but rather a property one proves about the theory; type theorists say that substitution is an admissible rule? rather than a derivable rule?.
For instance, in the language of dependent type theory we can show that the following substitution rule is admissible:
Here “admissibility” means that if there exist derivations of and , then there also exists a derivation of . By contrast, saying that this is a derivable rule would mean that it can occur itself as part of a derivation, rather than being a meta-statement about derivations.
An alternative approach to substitution is to make substitution part of the object language rather than the metalanguage. That is, the notation
is now actually itself a string of the language under consideration. One then needs reduction or equality rules describing the relationship of this string to the result of actually substituting for as in the usual approach.
Recalling that propositions are interpreted by subobjects, substitution of a term into a proposition is interpreted by pullback or inverse image of the subobject interpreting along the morphism interpreting .
Recalling that dependent types are interpreted by display maps, substitution of a term into a dependent type is interpreted by pullback of the display map interpreting along the morphism interpreting .
In the third case, there is a coherence issue: syntactic substitution in the usual approach is strictly associative, whereas pullback in a category is not. One way to deal with this is by using explicit substitution as described above. Another way is to strictify the category before modeling type theory; see categorical model of dependent types.
Now finally the substitution of for in , hence the proposition
is interpreted as the pullback
Notice that monomorphisms are preserved by pullback, so that this is indeed again the correct interpretation of a proposition.
Specifically, if is the unit type it is interpreted as a terminal object of , and then the function is identified simply with a term . In this case the substitution is evaluation of the proposition at , the resulting monomorphism
over the terminal object is a truth value: the truth value of at .
|type theory||category theory|
|natural deduction||universal construction|
and further developed in