Obtaining the semantics of simple type theory as a particular case of the set-theoretic semantics of dependent type theory
There is a standard set-theoretic semantics for Martin-Löf type theory, where a context $\Gamma$ is interpreted as a set $[\![{\Gamma}]\!]$, a type $A$ in context $\Gamma$ is interpreted as a family of $[\![{\Gamma}]\!]$-indexed sets $(A_\gamma)_{\gamma \in [\![{\Gamma}]\!]}$, a context extension $\Gamma.A$ with a variable of type $A$ is interpreted as the disjoint union: $[\![{\Gamma.A}]\!]=\coprod_{\gamma\in [\![{\Gamma}]\!]}A_\gamma$. A term $a$ of type $A$ is interpreted as a family $[\![{a}]\!]=(a_\gamma\in A_\gamma)_{\gamma \in [\![{\Gamma}]\!]}$. This is essentially what is described here.
I'd like to do two things: check if my definition for the semantics of dependent product types is right, and see how it can be obtained as a more general version of the semantics of function types in simple type theory. Here is the first part, i.e., semantics for pi-types:
-
Suppose the following data are given: a type $A$ in context $\Gamma$, a type $B$ in context $\Gamma.A$. Then $\Pi(A,B)$ is a type in context $\Gamma$. The semantics of this type is given as follows. $[\![{\Pi(A,B)}]\!]$ should be a family $(F_\gamma)_{\gamma\in [\![{\Gamma}]\!]}$ of $[\![{\Gamma}]\!]$-indexed sets. This family is defined as follows: $F_\gamma=\prod_{x\in A_\gamma}B_{(\gamma,x)}$
-
If $A$ is a type in context $\Gamma$, and $b$ is a term of type $B$ in context $\Gamma.A$, then $\lambda.b$ is a term of type $\Pi(A,B)$ in context $\Gamma$. I'd like to define $[\![{\lambda.b}]\!]$. From general considerations, $[\![{\lambda.b}]\!]$ should be a family $(f_\gamma\in \prod_{x\in A_\gamma }B_{(\gamma,x)})_{\gamma\in [\![{\Gamma}]\!]}$. I suppose I can set by definition $f_\gamma$ to be the dependent function which takes every $x$ to $b_{(\gamma,x)}$, where $[\![{b}]\!]=(b_{(\gamma,x)}\in B_{(\gamma,x)})_{\gamma\in [\![{\Gamma}]\!], x\in A_\gamma}$.
-
If $a$ is a term of type $A$ in context $\Gamma$, $B$ is a type in context $\Gamma.A$, and $f$ is a term of type $\Pi(A,B)$ in context $\Gamma$, then $\alpha(f,a)$ is a term of type $B[1.a]$ in context $\Gamma$. ($\alpha$ stands for 'application'.) The problem is how to define $[\![{\alpha(f,a)}]\!]$. Suppose $[\![{f}]\!]=(r_\gamma\in \prod_{x\in A_\gamma} B_{(\gamma,x)})_{\gamma\in [\![{\Gamma}]\!]}$ and $[\![{a}]\!]=(a_\gamma\in A_\gamma)_{\gamma \in [\![{\Gamma}]\!]}$. Then I suppose one can define $[\![{\alpha(f,a)}]\!] = (r_\gamma(a_\gamma)\in B_{(\gamma,a_\gamma)})_{\gamma\in [\![{\Gamma}]\!]}$.
Are these definitions correct?
Next, simple type theory can be obtained as a particular case of dependent type theory, and so the definitions of semantics should carry over to the simple case. But I don't see how, for example, the definition of abstraction carries over. The semantics of Church's type theory essentially says that if $\alpha$ is a term of type $\tau$ and $u$ is a variable of type $\sigma$, then $[\![{\lambda u.\alpha}]\!]^{M,g}$ is the function $f: [\![{\tau}]\!]^{M,g}\to [\![{\sigma}]\!]^{M,g}$ such that for all $x\in [\![{\tau}]\!]^{M,g}$, $f(x)=[\![{\alpha}]\!]^{M,g[u\mapsto x]}$, where $g$ is an assignment function, which is part of the notion of model. In contrast, the semantics for (non-dependent) lambda terms in dependent type theory is defined only with reference to $M$ but not with reference to $g$, and so we would have that $[\![{\lambda u.\alpha}]\!]^{M}$ is just some function $ [\![{\tau}]\!]^{M}\to [\![{\sigma}]\!]^{M}$ without any additional requirements. (I guess I'm implicitly assuming that ${\lambda u.\alpha}$ is a term of type $\tau\to \sigma$ in the empty context, not in an arbitrary context $\Gamma$.) We can specify which function that is, depending on which set-theoretic model $M$ we mean, but there is no requirement like $f(x)=[\![{\alpha}]\!]^{M,g[u\mapsto x]}$.
So we have assignment functions in the semantics of simple type theory, but in dependent type theory they are absent. Is it possible to restate semantics of simple type theory in terms that don't involve assignment functions? And what devices play the role of assignment functions in the semantics of dependent type theory?
0 answers
1 comment thread