5
$\begingroup$

I am reading a dissertation about dependent type programming language (Norell, 2007), and had much trouble understanding the definition of context mappings/substitutions as shown in the figure below fig.

I don't know much about type theory. From what I understand, a context mapping/substitution is a function from one context to another context. And a context is a list of variables each with a type. In the definition above, the author said that a context mapping is a list of patterns. Based on the answer to my other question here, a pattern is a specific kind of term. So, how can a function from terms to terms (i.e. a substitution of terms) be the same as a list of terms?

I tried to make guesses at its meaning but couldn't quite make sense out of it, and the next sections seem to confirm this notion that a substitution is a list of terms.

We write Match(σ, p̄) ⇒ q̄ for the successful matching of p̄ against σ. (matching a substitution against a list of patterns.)

Additionally, the author also used the substitution as if it's a function, as in vσ : Aσ . This seems to be a function application with the function symbol written on the right.

Another point of confusion is the sentence that says a context mapping σ .. with σ being in the source context (Delta). When viewing σ as a function between two contexts, this seems to say that the function is in the first context (Delta)?

Again, this may seem obvious to some one with training, but just confuses me.

My questions are:

Is a substitution/context mapping a function, a list of terms, or both? If the last case, how to interpret a substitution as a list of terms?

$\endgroup$

2 Answers 2

4
$\begingroup$

A substitution is not a mapping from terms to term. You can view a substitution $σ$ such that $Δ \vdash σ : Γ$ either:

  • as a mapping from variables in $\Gamma$ to terms in $\Delta$;
  • as a list of terms the same length as $\Gamma$.

This is pretty much the same thing, because a list is intended to represent the mapping (the first variable of $\Gamma$ is mapped to the first term in the list, the second variable to the second term, etc) and conversely from a mapping you can build the list $[σ(x_1),σ(x_2), \dots]$ if $x_1, x_2, \dots$ are the variables in $\Gamma$.

On top of this, there are typing conditions, roughly saying that if variable $x$ is assigned a type $A$ in $\Gamma$, then $\sigma(x)$ should have type $A$. Things are more complicated because of dependent types: since $A$ can depend on the previous variables in $\Gamma$, but $\sigma(x)$ should be a term in $\Delta$, you need to do something to $A$ to obtain a type in (a prefix of) $\Delta$ and not (a prefix of) $\Gamma$: instead of $A$ $\sigma(x)$ should really have type $Aσ$. More on this in a second.

While substitutions only map variables to term, you can make them act on types and terms, which is the operation denoted as $vσ$/$Aσ$. What this operation does is that it traverses the term/type until it hits a variable, which is replaced by the relevant term. So for instance say we have $$g : \mathbb{N} \to \mathbb{N} \vdash [f \mapsto (λ x. g(x + 1)), y \mapsto 0] : (f : \mathbb{N} \to \mathbb{N}, y : \mathbb{N}),$$ call it $σ$ and apply it, say to $f~y$, we get $$(f~y)σ = (fσ)~(yσ) = (σ(f))~(σ(y)) = (λx.g(x+1))~0.$$

Note how the substitution operation changes the context in which a term lives. In general, if $Γ \vdash t : A$, and $\Delta \vdash \sigma : \Gamma$, then $\Delta \vdash tσ : Aσ$. This is a bit confusing, because substitutions have a contravariant action on types/terms, they acts "backwards". The reason we still write $\Delta \vdash \sigma : \Gamma$ and not the other way around is that $\sigma$ is "of type $\Gamma$ in context $\Delta$" as explained above.

With these ingredients, you should be able to check/convince yourself that the identity mapping $id_{\Gamma}$ as described in the text indeed 1) is a well-typed substitution, i.e. $\Gamma \vdash id_{\Gamma} : \Gamma$ 2) acts as the identity, i.e. $t~id_{\Gamma} = t$ for any term $t$. Similarly, you can also define a notion of composition of substitutions: if $\Gamma \vdash σ : \Delta$ and $\Delta \vdash \tau : \Xi$ then $\Gamma \vdash \tau \circ \sigma : \Xi$ (try it out!).

As for context mapping, I'm lacking a little bit of context here, but I guess that they are the equivalent of patterns, but for substitutions instead of terms. Roughly, a restricted class of substitutions consisting only of constructors and variables, subject to linearity constraints.

$\endgroup$
2
  • $\begingroup$ Thanks for the answer. Does " a mapping from variables in Γ to terms in Δ;" mean that the context mapping should be written as "σ: Γ -> Δ " and not "σ: Δ -> Γ" as in the text. The direction also confused me quite a bit. $\endgroup$
    – tinlyx
    Nov 28, 2023 at 10:31
  • $\begingroup$ Yeah, this notation is even more confusing than $\Gamma \vdash \sigma : \Delta$… $\endgroup$ Nov 28, 2023 at 10:33
1
$\begingroup$

Consider two contexts $\Gamma$ and $\Delta$ and the set of all functions from $\Gamma$-variables, -terms, -types, and -subcontexts to $\Delta$-variables, -terms, -types, and -subcontexts. Such functions are useful because they represent transformations on the very objects we're studying in type theory in the same way, for example, vector space theorists consider transformations on vectors.

Concretely, we may say a transformation $f\colon \Gamma \to \Delta$ is a tuple $(f_\text{var}, f_\text{term}, f_\text{type}, f_\text{ctx})$ of functions that are mutually inductively defined for the cases on variables, terms, types, and subcontexts. For example, $f_\text{term}$ would accept a subcontext $\Xi$ of $\Gamma$ (i.e., $\Xi=\Gamma,\Theta$ for some $\Theta$), a term $t$ in $\Xi$, and its type $T$ also in $\Xi$, and it would output a term $f_\text{term}(\Xi, t, T)$ in $\Delta,f_\text{ctx}(\Xi)$. Complementarily, $f_T(\Xi, S)$ would output its type. People often conflate the notations of these component functions into a single one. The typing condition on term transformations then becomes a single line

$$\Gamma,\Xi \vdash t\colon\; T \ \Rightarrow \ \Delta,f(\Xi) \vdash f(t)\colon\; f(T)$$

Now such generally defined transformations between terms aren't so useful on their own because they are too general to easily reason and derive theorems about them. That's why we want to look at a nicely behaving subclass of these transformations, much like vector space theorists look at linear functions between vector spaces instead of arbitrary ones. A very nice subclass in our case emerges when restricting the transformations to the following inductively defined functions:

  • variables in the domain context are mapped to terms in the codomain context:

    $$x\colon\; T\in \Gamma \ \Rightarrow \ \Delta \vdash f(x)\colon\; f(T)$$

  • terms, types, and subcontexts are mapped inductively in the straightforward way

Thus, substitutions are functions, but they are so restricted that they can equivalently be given as the list of terms they map the domain context's variables to.

I think terminology-wise context mappings are just substitution mappings notated in the other direction, but I may be wrong here.

PS: Details may vary from type theory to type theory. The above text represents the general idea on dependent type theories.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.