nLab
meaning explanation

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

Foundations

The meaning explanations of type theory

Idea

Per Martin-Löf’s meaning explanations of type theory provide a way to justify the correctness of the rules of type theory. The meaning of the judgements of type theory are defined by computation of closed terms to canonical form in some untyped notion of computation, such as a lambda calculus extended with constants for the constructors and eliminators of type theory.

From a technical/mathematical point of view, the meaning explanations give rise to a realizability model of type theory, where realizers are terms in some untyped notion of computation, such as an extended lambda calculus. That is, it can be regarded as a description of how types are assigned to untyped computations. However, the term “meaning explanations” also refer to the “philosophical” or “pre-mathematical” component, which regards this as an “explanation” of the “constructive validity” of the judgements of the type theory.

The standard meaning explanations validate not just the rules of intensional type theory but also the stronger rules of extensional type theory. Thus, if one regards it as the “intended semantics” then one may believe in the extensional theory. However, like any particular semantics for a formal theory, the meaning explanation also validates many other “rules” as well which are not usually adding to type theories, so it is not so clear that meaning explanations in their own right argue for extensionality. They can also be modified so as to no longer satisfy extensionality.

Martin-Löf has been quoted as saying

Some people feel that when I have presented my meaning explanations I have said nothing. And this is how it should be. The standard semantics should be just that: standard. It should come as no surprise.

Definition

Suppose we have given some collection of computational objects which we call “terms”, with an untyped notion of “reduction” or “computation”. These could be terms in a lambda calculus, or elements of a partial combinatory algebra, or even programs in a real-world programming language such as C, Java, or Python. We write xyx\Rightarrow y to mean that xx computes or reduces to yy (in some number of steps). We then define simultaneously the following predicates, where a,b,Aa,b,A are terms:

  • AA is a type, often written AtypeA\;type.
  • aa has type AA, written a:Aa:A.
  • aa and bb are equal terms of type AA, written a=b:Aa=b:A.

The definition is by induction-recursion?. We define the property “AA is a type” inductively, and simultaneously we define recursively two functions assigning to each type AA the collection of terms of type AA and the collection of pairs of equal terms of type AA, respectively. Moreover, each such collection may itself be defined inductively.

The clauses which we include in each case depend on what types we want to put into our type theory; in each case the base notion of untyped computation must include a corresponding structure. Here are three paradigmatic examples.

Natural numbers

Suppose that we have terms NN, 00, and s(x)s(x), along with a recursor rec(n,z 0,xr.z s)rec(n,z_0,x r. z_s) such that

rec(0,z 0,xr.z s)z 0rec(0,z_0,x r.z_s) \Rightarrow z_0

and

rec(s(n),z 0,xr.z s)z s[n/x,rec(n,z 0,xr.z s)/r].rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r].

The term rec(n,z 0,xr.z s)rec(n,z_0,x r. z_s) is intended to denote the value at nn of a recursively defined function specified to be z 0z_0 at zero and z sz_s at successors. Here xx and rr are variables which may occur free in z sz_s but are bound in rec(n,z 0,xr.z s)rec(n,z_0,x r. z_s), representing the current index and the result of the last recursive call, respectively.

Then to explain the natural numbers type, we include a clause in the inductive definition of “AA is a type” which says

  • if ANA\Rightarrow N, then AA is a type.

The corresponding clause for elements is

  • if ANA\Rightarrow N, then the collection of terms aa such that a:Aa:A is defined inductively by the clauses:
    • if a0a\Rightarrow 0, then a:Aa:A.
    • if as(b)a\Rightarrow s(b) and b:Ab:A, then a:Aa:A.

And for equality:

  • if ANA\Rightarrow N, then the collection of pairs a,ba,b such that a=b:Aa=b:A is defined inductively by the clauses:
    • if a0a\Rightarrow 0 and b0b\Rightarrow 0, then a=b:Aa=b:A.
    • if as(a)a\Rightarrow s(a') and bs(b)b\Rightarrow s(b') and a=b:Aa'=b':A, then a=b:Aa=b:A.

Function types

Suppose that we have a term constructor yielding “ABA\to B” for terms AA and BB, and similarly app(f,a)app(f,a) and λx.t\lambda x.t, such that

app(λx.t,a)t[a/x]. app(\lambda x.t, a) \Rightarrow t[a/x].

Then to explain the function type, we include a clause in the inductive definition of “AA is a type” which says

  • if AA is a type and BB is a type and C(AB)C\Rightarrow (A\to B), then CC is a type.

The clause for elements is:

  • if C(AB)C\Rightarrow (A\to B) for types AA and BB, and for any a:Aa:A we have app(f,a):Bapp(f,a):B, then f:ABf:A\to B. In other words, the collection of elements of type ABA\to B is the collection of terms ff such that for any a:Aa:A we have app(f,a):Bapp(f,a):B.

This is not an inductive definition as we had for the natural numbers; it is merely a simple definition. On the other hand, we are now using the fact that the function mapping types to their collections of elements is recursively defined, since in order to make this definition, we must invoke it at AA and BB.

For equality, of course we have:

  • if C(AB)C\Rightarrow (A\to B) for types AA and BB, and for any a:Aa:A we have app(f,a)=app(g,a):Bapp(f,a)=app(g,a):B, then f=g:ABf=g:A\to B.

Identity types

Suppose we have a term constructor yielding Id A(a,b)Id_A(a,b) for terms A,a,bA,a,b, and similarly some term reflrefl. Then to explain the identity type, we add to the inductive definition of “AA is a type” the clause

  • If AA is a type, a:Aa:A and b:Ab:A, and CId A(a,b)C \Rightarrow Id_A(a,b), then CC is a type.

Here we are finally using the fact that typehood and elements are defined by induction-recursion: this clause in the inductive definition of typehood must refer to the value of the recursive elementhood function at some smaller type.

The clause for elements is:

  • If AA is a type, a:Aa:A, b:Ab:A, and CId A(a,b)C \Rightarrow Id_A(a,b), then p:Cp:C just if a=b:Aa=b:A and preflp \Rightarrow refl. So, the collection of elements of Id A(a,b)\Id_A(a,b) contains something only if a=b:Aa=b:A, in which case it contains precisely those terms which reduce to refl.

Here we use not only the fact that elementhood is recursively defined, but that it is defined by mutual recursion with equality. The clause for equality is:

  • If AA is a type and a:Aa:A, b:Ab:A, and CId A(a,b)C \Rightarrow Id_A(a,b), then p=q:Cp=q:C just if a=b:Aa=b:A, preflp\Rightarrow refl, and qreflq\Rightarrow refl.

Because we have deliberately only put reflrefl (and terms reducing to it) into the identity type, this definition of identity types will validate the “equality reflection” rule of extensional type theory.

There are simple ways to modify the meaning explanation so as to no longer validate the extensional rules. For instance, if we add to the semantics additional “free variables”, so that there are “neutral terms” which do not compute to any canonical form, and modify the rules of the interpretation so as to say that any normalizable neutral term inhabits every type, then extensionality will no longer hold, since the identity type (like any type) will contain all the variables. This is maybe not a particular compelling model of intensionality, but there are proposals for better ways to expand the meaning explanation to deal with intensional type theory.

The rules of type theory

The claim is that by inspecting these definitions, one can arrive at the formal rules of type theory for manipulating judgments such as “AA is a type”, “a:Aa:A”, and “a=b:Aa=b:A”, which no longer refer to any given notion of computation. However, Martin-Löf famously wrote

…there are … certain limits to what verbal explanations can do when it comes to justifying axioms and rules of inference. In the end, everybody must understand for himself.

Moreover, as mentioned above, the meaning explanation (like any particular semantics) validates many other “rules” which are not usually added to type theories, such as

x:Id N(0,1)5:NN x : Id_N(0,1) \vdash 5 : N \to N

(However in Nuprl? rules such as these are, in fact, included.) Thus, some discrimination is required, as well as some choices (e.g. whether to add the extensionality rule for identity types).

References

Revised on May 24, 2013 23:26:09 by David Corfield (87.113.28.17)