Algebraic type theories

(Part 5 of a series.)

Although we have not yet finished discussing algebraic theories, we will continue our discussion in the more general framework of algebraic type theories, which allow us to simultaneously define multiple theories which may or may not refer to each other. (Algebraic type theories are also known as many-sorted algebraic theories, for reasons which will be apparent momentarily.)

As one of many motivations, consider group actions, which arise from a group \(G\) and a set \(X\), along with a function \(\cdot:G\times X\to X\) which is compatible with the group in the sense that \(\mathord{\sf{\text{e}}}\cdot x = x\) and \((g\circ h)\cdot x = g\cdot (h\cdot x)\). (We say that \(g\cdot x\) is obtained from the action of \(g\) on \(x\).)

For example, a permutation group has as elements permutations (of a set of size \(n\)), where \(\circ\) is composition of permutations. The action of a permutation group on an appropriately–sized ordered set is obtained by applying the permutation.

Although we can separately define groups and sets as algebraic theories, we cannot define group actions, because \(\cdot\) refers to both theories at once. To support multiple sorts of terms, we annotate each term with a type. This affects the right-hand side of each judgment, as well as each variable in the context. So our theory of groups would be written:

We read \(\Gamma\vdash e:G\) as saying that, in any context \(\Gamma\), \(e\) is a term of type \(G\), and \(x:G\vdash x\circ e=x:G\) as saying that, given any term \(x\) of type \(G\), then \(x\circ e\) and \(x\) are equal terms of type \(G\).

In the same theory, we can also define a type corresponding to some set, like:

for the set with two elements. Then a group action on \(\mathord{\sf{\text{bool}}}\) consists of a \(\cdot\) constant which takes a term of type \(G\) and a term of type \(\mathord{\sf{\text{bool}}}\):

Notice that we can no longer describe the arity of function symbols numerically, since the types of the arguments are now relevant. We instead use arities of the form \(A_1,\cdots,A_n\to B\); we say \(\cdot\) has arity \(G,\mathord{\sf{\text{bool}}}\to\mathord{\sf{\text{bool}}}\).

In an algebraic type theory, the hypothesis rule must now maintain the type of the variable:

and the substitution rule must require that the types of the substituted terms match the types of the variables.

Of course, if they did not match, then we would not be able to obtain a derivation of the substituted term from a derivation of the original term in the manner previously described. (As before, weakening can be derived from substitution.)

Equalities are now annotated with the type of the two terms; terms can only be equated when their types are equal. Thus, the basic axioms are now:

A set-theoretic model of an algebraic type theory is an interpretation function \([\![- ]\!]\) which

  1. sends each type \(A\) to a set \([\![A ]\!]\), and

  2. each judgment \(x_1:A_1,\cdots,x_n:A_n\vdash t:B\) to a function \([\![A_1 ]\!]\times\cdots\times[\![A_n ]\!]\to [\![B ]\!]\), such that

  3. for each judgment \(\Gamma\vdash s=t:A\), it is the case that \([\![\Gamma\vdash s:A ]\!]=[\![\Gamma\vdash t:A ]\!]\).

We extend the interpretation function to contexts by \([\![x_1:A_1,\cdots,x_n:A_n ]\!]= [\![A_1 ]\!]\times\cdots\times[\![A_n ]\!]\).

As with algebraic theories, we also require that the hypothesis rule is modeled by a projection out of the context tuple, \((x_1,\cdots,x_n)\mapsto x_i\), and and that substitution of terms modeled by \(f_1,\cdots,f_n\) into a term modeled by \(g\) is modeled by \(\hat x\mapsto g(f_1(\hat x),\cdots,f_n(\hat x))\). It is worth verifying that these functions have the correct sets as domain and codomain.

Lastly, as with algebraic theories, it is the case that, for any choice of \([\![- ]\!]\) on types only, the behavior of \([\![- ]\!]\) on judgments is determined precisely by a choice of \([\![f ]\!]:[\![A_1 ]\!]\times\cdots\times[\![A_n ]\!]\to[\![B ]\!]\) for each function symbol \(f\) of arity \(A_1,\cdots,A_n\to B\). Again, it is worth verifying that the previous proof goes through.

Posted March 2nd, 2013 in Academic. Tagged: .

2 comments:

  1. Mathias Rav:

    This is starting to look like what I learned during our Programming languages course (and related courses). Very well written!

  2. Carlo:

    Thanks! I’m picking up the pace soon; I just wanted to be extra careful about the basics.

Leave a response: