@Jonathan Sterling; April 16, 2020
Someone more familiar with raw terms and operational techniques asked me how to actually define a practical model of a theory that has been defined in an extensional logical framework (e.g. the internal language of locally Cartesian closed categories, or perhaps Martin-Löf’s logical framework). I decided to work out an example that makes contact with operational and syntactical notions that are familiar to a PL researchers: the interpretation of a judgmental theory of typed $\lambda$-calculus into partial equivalence relations (PERs).
Our theory $\mathbb{T}$ is given by the following constants in the logical framework:
$$ \begin{aligned} \mathsf{tp} &: \square\\ \mathsf{tm} &: \mathsf{tp}\to\square\\ \mathsf{arr} &: \mathsf{tp}\times\mathsf{tp}\to\mathsf{tp}\\ \mathsf{tm/arr} &: (\alpha,\beta:\mathsf{tp}) \to (\mathsf{tm}(\alpha)\to\mathsf{tm}(\beta)) \cong \mathsf{tm}(\mathsf{arr}(\alpha,\beta))\\ \mathsf{ans} &: \mathsf{tp}\\ \mathsf{yes}, \mathsf{no} &: \mathsf{tm}(\mathsf{ans}) \end{aligned} $$
In the above, a constant ending in $\square$ denotes a sort of the object theory; the symbol $\cong$ unfolds to the LF-type of strict isomorphisms, i.e. we are using the following abbreviation:
$$ \begin{aligned} (A\cong B) &\equiv (f : A \to B) \\ & \times (g : B\to A) \\& \times ((x : B) \to f(g(x)) =_B x)\\& \times ((x : A) \to g(f(x)) =_A x) \end{aligned} $$
Above we are using the extensional equality type connective of the logical framework; it is important to remember that while the LF has extensional equality, there is no need for any object theory formulated in the LF to have extensional equality. In our example, the specification of an LF-isomorphism between the terms of the object-level function type $\mathsf{arr}(\alpha,\beta)$ and the LF-level function space $\mathsf{tm}(\alpha)\to\mathsf{tm}(\beta)$ bundles up the introduction form, elimination form, $\beta$-law and $\eta$-law for the function type. Whereas logical frameworks without equality are used to reduce object-level binding to meta-level binding, we use a more fully-featured logical framework to reduce not only binding but also typing and computation themselves to the meta-level.
Exercise. Derive $\lambda$-abstraction and application operations from the specification above.
How do we construct semantic interpretations of $\mathbb{T}$? Because we are working in a mathematical logical framework, we do not a priori have anything to go by induction on, so the old style of defining an interpretation as a “function” by recursion on some raw terms or derivations isn’t going to get us very far. Likewise, the logical framework is extensional so we cannot use canonical forms as a crutch. It will turn out that it remains very easy to define interpretations, because they correspond to implementations of the constants described above in a given locally Cartesian closed category. A category is locally Cartesian closed when it has finite limits and dependent products — i.e. just the structure needed to interpret extensional dependent type theory.
As a demonstration, we will show how to define a PER model of $\mathbb{T}$ very simply. To define a model of an LF-theory, we must first choose a locally Cartesian closed category to interpret its judgmental structure; we want all the object types to be interpreted by partial equivalence relations over some computational algebra, but it will be helpful to not assume that the LF-types (the sorts) are necessarily interpreted by PERs (though this is possible). Therefore, we would need to embed the category of PERs into a category that does have an object of all PERs. There are two very good ways to achieve this:
Because the assembly approach is more concrete and user-friendly for those who aren’t comfortable with category theory, we will use it here. The local universes approach is more general and scalable, but there is value in using something that is very concrete.
Programming languages theorists are familiar with the idea of defining partial equivalence relations over some kind of untyped code, perhaps requiring that the relations respect head reduction or even a computational congruence. From there, we often construct interpretations of a language in terms of PERs, but it is never made clear in what sense we have defined an interpretation — in particular, these interpretations don’t actually preserve the $\beta$-laws of a programming language up to equality, so it cannot even be said that one has defined a model. Of course, this never prevented anyone from using PERs to prove any interesting result.
In mathematical logic and recursion theory, it was necessary to impose a bit more order on the situation so that results could be made modular and re-used. In this setting, one therefore uses slightly different definitions than what PL people are used to, but what is gained is that one can speak about a category of PERs over some computational algebra and speak objectively about when a category of PERs has (e.g.) product types, function types, etc. independently of any particular notion of syntax or operational semantics. Knowing how to do this is a big advantage when one is surrounded by people who define these notions separately for every single language they investigate.
In recursion theory, people usually base computation on something called a partial combinatory algebra; this has given realizability a very negative reputation among computer scientists, who (rightly) find the explosion of combinator-expressions $ksaabbbaaccagaa...$ quite distasteful and uninformative, as well as foreign to the everyday practice of studying programming languages. I would like to make the point that we can develop realizability in a more familiar and intuitive way by building it out of the syntax and operational semantics of a more conventional untyped programming language that may extend the $\lambda$-calculus.
The basic notion on which everything else is built is called an applicative structure. An applicative structure $\mathbb{A}$ is given by a set $|\mathbb{A}|$ equipped with a binary operation $@ : |\mathbb{A}|\times|\mathbb{A}|\to|\mathbb{A}|$. We will just write $\mathbb{A}$ for $|\mathbb{A}|$ when it is clear what we mean.