What is realizability?

I recently decided to confront the fact that I didn’t know what “realizability” meant. I see it in programming languages papers from time to time, and could see little rhyme or reason to how it was used. Any time I tried to look it up, I got some nonsense about constructive mathematics and Heyting arithmetic, which I also knew nothing about, and gave up.

This blog post is basically a copy of my personal notebook on the subject, which is NOT AUTHORITATIVE, but maybe it will help you.

My best understanding of realizability right now, in programming languages (PL) terms, is:

1. A technique for assigning each syntactic type to a collection of semantic terms;
2. By induction over syntactic types;
3. Where the semantic terms that are realizers—i.e., included in the collection related to some syntactic type—are a sub-collection of all possible terms in the semantic domain. That is, there are valid semantic terms not associated with any syntactic type.

I use the word “collection” rather than “set” to avoid invoking set theory.

Graphically, we can represent this as follows:

The point of the technique is that clause 2 gives us a proof technique by induction, and clause 3 means we can relate the collection of terms (or proofs) to some other well-known collection. This yields a proof technique for metatheoretic properties about the collection, such as that there are only terminating terms in the collection of realizers, or there are only recursive functions and therefore some classical things remain unprovable.

I’m not entirely sure that clause 2, induction, is necessary, and I can’t find anything explicit about clause 3, but they seem to be true historically and in many uses of the term.

Okay so how did I get to this understanding?

What is realizability, historically?

kleene1945 - On the Interpretation of Intuitionistic Number Theory

Realizability seems to come from Kleene’s paper “On the Interpretation of Intuitionistic Number Theory”. I say “seems to” as Kleene attributes the “detailed investigation of the notion of realizability” to David Nelson, attributes several of the results in the paper to Nelson, and claims that the main results of the paper are joint work with Nelson. But the paper only has Kleene’s name on it, and Kleene claims in the first footnote that they introduced the idea of realizability to Nelson in a seminar. So anyway, realizability seems to come from Kleene, and this is the canonical paper cited for the technique.

In this paper, realizability is quite specific. It’s a technique that takes an intuitionistic first-order logic formula about Peano arithmetic (Heyting arithmetic) and constructs a natural number from it, representing the (constructive) proof of that formula. Only provable formulas are realized. The point of this exercise is to prove various metatheorems about the realized language: is it consistent, and what are provable/unprovable in the intuitionistic formulae.

Intuitively, something is unprovable if there exists a formula, but there does not exist a realization of it. This can be shown by connecting the formula to the set of realizers (in this case, natural numbers), but showing that there cannot exist a related natural number (or, more often, function on natural numbers represented by its Gödel number) with the properties required of the realizability interpretation. The simplest example: since “false” is unprovable (it has no realization, by construction), the intuitionistic logic is consistent.

This also lets us prove something about the class of all provable statements. Since we have a method for constructing something from any provable (or true) statement, we can say something about the set of all provable statement in relation to the realizers. Kleene mentions one consequence is that the intuitionistic calculus cannot prove the existance of any function other than a general recursive function, since those are the only functions constructed in the realizability interpretation. This tells us, for example, that the intuitionistic calculus is different from classical set theory, which contains other functions.

An important detail in this paper that clarifies the distinction between the intuitionistic and the classical happens in Clause 6, on page 113. This is the definition of the realizability interpretation for existential quantification ∃x.A(x). This has a realization if, for some x, A(x) has a realization. It’s important to notice that this second “for some x” quantification happens in the metalanguage, namely, classical set theory, and therefore could be choosen by Choice. Kleene discusses this on page 118, where he uses the word “classically” as a modifier on various quantifiers to remind us that, when working with the quantification and realizers directly, we are working in a classical system in which intuitionistic proofs also exist.

What seems to be going on here is that the realizers are something like the intuitionistic subset of classical set theory. I think that statement isn’t exactly true; Kleene uses classical choice when working with the realizers to show there are unprovable theorems. For example, a realizer parameterized over (classically) all variables may not correspond to an intuitionistic formula. So it’s not that the realizers are only intuitionistic, I think. But any particular realizer is (must be)? The important point may be the realizers are a subset of the whole system, and thus we can prove interesting metatheorems that rely on distinguishing the realizers (and therefore, the formulae they realizer) from all the things in the full system.

amadio1998 - Domains and Lambda-Calculi, Chapter 15

Chapter 15 of Amadio and Currien’s book “Domains and Lambda-Calculus” introduces realizability in its historical context. The introduction formalizes Kleene’s work as an example, and discusses its use.

They emphasize two things, which seem to confirm some of my understanding:

1. The realizability relation is defined inductively over formulas, and relates formulas to proofs.
2. The use lets us reason about all proofs in the system.

This is the best definition of realizability I’ve seen, and applies both to Kleene’s original, but also to uses in PL.

The authors point out that Kleene’s original goal was to prove consistency. They then confirm my above intuitions, that the realizability interpretation also lets us prove metatheorems about what is provable/unprovable in the realized system. However, they note that one application of this is to find unprovable true statements, which can be consistently axiomatized back into the original system. There are proofs in the set of realizers, i.e., true statements, that are never constructed by the realizability interpretation. These could be added back to the original system to enrich it.

This latter use seems to confirm one feature of realizability that isn’t explicit stated anywhere, but seems to be true of all realizability interpretations I’ve seen: that the realizers are a strict subsystem of some larger formal system.

How is “realizability” used in PL?

In programming languages, we’re not often concerned with intuitionistic vs classical logic; we’re working constructively by default. In fact, many of the uses of “realizability” in PL don’t seem to be related to logic at all, but to modeling well-typed programs. And while, sure, these are related by Curry-Howard, the difference seems important to me. So what does realizability mean in this context?

In most uses in PL, the important feature seems to be clause 3 in my definition above: the collection of all values is larger than the set of realizers. In PL, this suggests that we’re ascribing types to “untyped” terms, and the realizers are those that are semantically well typed, but not necessarily syntactically well typed. The full collection contains also untyped terms, and we can therefore prove through realizability that the type system rules out ill-typed terms.

There do seem to be some examples in PL that are explicitly relating classical and intuitionistic ideas, namely those trying to import constructive interpretations of classic logic. I’m not really interested in those, and I think the connection to realizability is much more clear in those applications, so I’ll ignore that area.

Let’s look at some examples.

benton2010 - Realizability and Compositional Compiler Correctness for a Polymorphic Language

In “Realizability and Compositional Compiler Correctness for a Polymorphic Language”, Benton and Hur define a “realizability” interpretation of System F types realized by terms in low-level language, for proving some compiler correctness properties. The terms realize the types, and this lets us talk about which low-level programs are valid to link with, without restricting the set of linkable programs to only those generated by the compiler.

This has lost all connection to intuitionistic vs classical logic, but I suppose it keeps the key features of the technique: types (formula) of one language are realized by terms in another, and there is some concern that the realizers should be a subset of all terms. Not all low-level programs should be valid, but some set of them should be.

nakano2000 - A Modality for Recursion

“A Modality for Recursion” was actually the start of my realizability journey. This paper starts by defining a collection of models (β-models) of the untyped λ-calculus. It then defines the class of realizability models, in terms of β-models, for an extrinsically typed λ-calculus with equi-recursive types. A realizability model is parameterized by a β-model, and is a relation inductively defined over types to their realizers, which are values drawn from the β-model.

So why is this realizability? Well, I don’t see anything to do with intuitionistic vs classical. But, the set of all values is larger than the set of realizers, which seems to be important to all uses of “realizability”, and important for this result in particular. In this paper, this is used to show that the dot modality rules out some valid β-model terms, namely those that would correspond to non-terminating λ terms.

Later in the paper, they define a “realizability interpretation”. This seems to be distinct from the collection of all realizability models in that they pick a particular set of realizers? So, it ought to be a realizability model, I guess? But they don’t say so explicitly. The interpretation is still quite heavily parameterized, but it does seem to fix or restrict the set of realizers. Anyway, this interpretation includes all the features of my definition above: it’s inductively defined over types, relating types to (a semantic model of) untyped λ terms, for the purposes of proving something about the collection of realizers as they related to the collection of all untyped λ terms.