nLab variable



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/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) 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




In logic, a variable is a symbol that stands for an arbitrary instantiation of some given type (although in single-typed theories the type is trivial). Thus, every variable of type TT is a term of type TT (although typically there are other terms).

Logicians have developed several ways to precisely specify what variables are and how to keep track of them, and the only thing more annoyingly pedantic than learning one of these is translating between different ones.

Free and bound variables

If we keep track of context, every introduction of a variable changes the context. Thus, whatever terms of type TT there may (or may not) be in a given context Γ\Gamma, in the context (Γ,x:T)(\Gamma, x\colon T) —which is Γ\Gamma extended by a free variable xx of type TT— there is (at least) one more term of type TT, and that term is xx itself.

Conversely, we may be able to take a term aa in the context (Γ,x:T)(\Gamma, x\colon T) and apply some operation ff to it to create a term f(a)f(a) (possibly of a different type) in the context Γ\Gamma; then any appearances of the variable xx in the term aa have become bound variables in the term f(a)f(a). That is, the appearances of xx are bound by the operator ff, and xx has no meaning outside of its scope.

So for example, if (say in something simple like Peano arithmetic, supplemented with the abbreviations used in practice) I write 2x2x, this is a term (for a natural number) in a context with a free variable xx, whereas if I write 3 x=0 42x+53 \sum_{x=0}^4 2x + 5, this is a term (also for a natural number) in a context with no free variables; here, xx is bound. The variable xx has a meaning after the operator x=0 4\sum_{x=0}^4 (whose notation also specifies the variable that will have a meaning inside it) and before the plus sign (which, following the standard order of operations, marks the end of the scope of x=0 4\sum_{x=0}^4) but has no meaning outside of that (where the 33 and 55 are, or even where the 00 and 44 are). And indeed, the ultimate meaning of 2x2x depends on what xx is, but the ultimate meaning of 3 x=0 42x+53 \sum_{x=0}^4 2x + 5 is simply 6565.

In categorical semantics

In the internal language of a category 𝒞\mathcal{C} a morphism

f:BA f\colon B \to A

is a term f(x)f(x) of type AA where xx is a free variable of type BB, which in symbols is given by

x:Bf(x):A. x\colon B \vdash f(x)\colon A \,.

We may think of the free variables here as being placeholders for all the generalized elements UxBU \stackrel{x}{\to} B of BB.

Then the assertion

x:Bf(x):A x\colon B \vdash f(x)\colon A

indicates that with BfAB \stackrel{f}{\to} A given we may send UxBU \stackrel{x}{\to} B to the composition

(UxBfA)=(Uf(x)A). (U \stackrel{x}{\to} B \stackrel{f}{\to}A ) = (U \stackrel{f(x)}{\to} A) \,.

A free variable becomes a bound variable after application of a quantifier: for instance the image of f:PXf\colon P \to X under base change

𝒞 /X𝒞 \mathcal{C}_{/X} \stackrel{\to}{\stackrel{\leftarrow}{\to}} \mathcal{C}

represents, for the left adjoint the type

x:X,P(x) \exists x\colon X , P(x)

(existential quantifier), and the the right adjoint the type

x:X,P(x) \forall x\colon X , P(x)

(universal quantifier) in which now xx is a bound variable.


A textbook account with an eye towards applications in computer science is in section 1.2 of

An exposition on the relation between free variables and universal quantification is in

  • Andrej Bauer, Free variables are not “implicitly universally quantified”! (web)

Last revised on December 3, 2020 at 09:27:52. See the history of this page for a list of all contributions to it.