How exactly are realizability and the Curry-Howard correspondence related?

Question

Consider, on the one hand:

• the Curry-Howard correspondence between, on the one hand, types and terms (programs) in various flavors of typed $\lambda$-calculus, and on the other, propositions and proofs in various (generally intuitionistic) logical systems,

and on the other hand

• realizability, which is a relation between programs and propositions in various (generally intuitionistic) logical systems (the simplest form of which, Kleene realizability, is defined for example in this question).

Clearly the two have much in common; in fact, the rules describing the logical connectors in both are almost identical (e.g., a realizer of $\varphi\Rightarrow\psi$ is a program taking a realizer of $\varphi$ and returning a realizer of $\psi$, whereas the type corresponding to $\varphi\Rightarrow\psi$ under the C-H correspondence is the type of functions taking the type associated to $\varphi$ as input and returning the type associated to $\psi$ as output).

Now much of this similarity is simply due to the fact that both are ways to make precise the (informal) Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic. So maybe the similarity is just due to the connectors themselves.

Certainly there are important differences. “Programs” in the C-H correspondence are written in a strongly normalizable, so, not Turing-complete, language, so by construction they cannot loop (indeed, “looping” would permit paradoxical proofs since any type is inhabited as soon as we have something like the $Y$ combinator), whereas “programs” in realizability are arbitrary Turing machines which just so happen not to loop in the cases we call them on [see also addendum below]. Also, the C-H correspondence appears to be a mostly formal observation about interpreting Cartesian closed categories with certain adjoints, whereas realizability seems to have deeper mathematical content.

It's also terribly hard to know exactly what to compare, because both the C-H correspondence and realizability have a gadzillion flavors, variants and reformulations, and I don't know where to start looking.

Still, I can't escape the feeling that there's more to be said than “they look similar because they both follow the B-H-K interpretation of connectives”. For example, it seems to me that by reformulating Kleene realizability with terms of the untyped $\lambda$-calculus (with natural numbers as atoms) and then taking a model of the latter where each term is modelled as the set of terms of that type (“K-models” or something, I'm not sure what the right terminology is), realizability is brought even closer to the C-H correspondence.

So, question: do the Curry-Howard correspondence and realizability have more to do with each other than simply following the B-H-K correspondence? Do they admit, for example, a common generalization? Or a common framework in which we could define both? (Side question: is the above above a fair summary of the situation?)

Please treat this as a soft question: I know various flavors of the Curry-Howard correspondence and of realizability, and I'm trying to “connect the dots” (and feel less confused about the relation between the two): any remarks that might help me do that is welcome.

---

Addendum (2023-12-06): I just remembered something worth mentioning in relation to this question as it is an important difference between realizability and Curry-Howard: there are propositional formulas that are uniformly realizable but not intuitionistically provable: so there is a program that realizes them (for all values of the propositional variables), but there is no program in the simply typed $\lambda$-calculus having the type that corresponds to the formula under the Curry-Howard isomorphism. An example of such a formula (due to G. S. Tseitin [= Г. С. Цейтин]) is the formula $$\begin{aligned} &\big(\neg (A \land B) \land (\neg A \Rightarrow (C \lor D)) \land (\neg B \Rightarrow (C \lor D))\big)\\ \mathrel{\Rightarrow} &\big((\neg A \Rightarrow C)\lor(\neg B \Rightarrow C)\lor(\neg A \Rightarrow D)\lor(\neg B \Rightarrow D)\big) \end{aligned}$$ discussed here (for more examples, see V. Plisko, “A Survey of Propositional Realizability Logic”, Bull. Symbolic Logiv, 15 (2009), 1–42, esp. around §6). The answer by Arno to the aforementioned MO question explains quite well what is going on here: Markov's principle (i.e., running two programs in parallel under the promise that one of them will halt), suitably used, gives us a way to realize a disjunction as the right-hand side of the implication above, but this kind of trick will not work to provide a term of the corresponding type. So maybe this suggests a negative to my question: “realizability differs essentially from the Curry-Howard isomorphism in that realizability lets you use techniques such as Markov's principle to prove that programs terminate, which typiing does not permit.”

Answer 1

I am sure more than one exact correspondence can be made, but here's at least one that is technically precise. We shall employ categorical logic.

Executive summary: realizability is the interpretation of intuitionistic logic in which predicates are interpreted using the subobject fibration, whereas the Curry-Howard interpretation uses the families fibration. The two fibrations are related by an adjunction. $\newcommand{\AA}{\mathbb{A}}$ $\newcommand{\Asm}[1]{\mathsf{Asm}(#1)}$

Let me spell out the details a bit. I will follow the setup of these notes so that background material and further details are readily available. Fix a partial combinatory algebra (pca) $\AA$, such as the pca of Turing machines or the untyped $\lambda$-calculus. Let $\Asm{\AA}$ the category of assemblies over $\AA$. Recall that an assembly $X = (|X|, E_X)$ is given by a carrier set $|X|$ and a map $E_X : |X| \to P(\AA)$ which assigns to each $x \in |X|$ a non-empty set $E_X(x)$ of its realizers.

We construe assemblies as types, and wish to set up an interpretation of logic on top of them. The first question is: what are the predicates? Two answers may be given:

1. The predicates on $X$ are the subojects of $X$ (chapter 4 of the notes). Up to equivalence, such a subobject is a map $\phi : |X| \mapsto P(\AA)$ which assigns sets of realizers to the elements of the carrier set $|X|$. The predicates on $X$ form a Heyting algebra $\mathsf{Sub}(X)$, and $\mathsf{Sub}$ itself is a fibration over $\Asm{\AA}$.

2. The predicates on $X$ are the families of assemblies indexed by $X$ (chapter 5 of the notes). Specifically, a predicate on $X$ is a map $F : |X| \to \mathsf{Obj}(\Asm{\AA})$ which assigns assemblies to the elements of the carrier set $|X|$. The families on $X$ form a category $\mathsf{Fam}(X)$ and $\mathsf{Fam}$ itself is a fibration over $\Asm{\AA}$.

The first interpretation is the realizability interpretation, and the second one is the Curry-Howard interpretation. Let us relate them.

Given an assembly $X$, there is a map $$\mathbf{E} : \mathsf{Sub}(X) \to \mathsf{Fam}(X)$$ which assigns to a predicate $\phi : |X| \to P(\AA)$ the family defined by $\mathbf{E} \phi \,x = (\lbrace{\star\rbrace}, (\star \mapsto \phi(x)))$. In words, we convert a subobject $\phi$ to a family of sub-terminal assemblies on $X$. We might call $\mathbf{E} \phi$ the extent of $\phi$.

In the opposite direction we have a map $$\mathbf{T} : \mathsf{Fam}(X) \to \mathsf{Sub}(X)$$ which assigns to a family $F$ the subobject $\mathbf{T} F \, x = \bigcup_{y \in |F(x)|} E_{F(x)}(y)$. That is, $\mathbf{T} F \, x$ throws away the information about the assembly $F(x)$ and just keeps the realizers. We call $\mathbf{T}$ the propositional truncation.

It is obvious that $\phi = \mathbf{T} (\mathbf{E} \phi)$, while in the other direction we have a family map $\eta_X : F \to \mathbf{E} (\mathbf{T} F)$ which is the unit of an adjunction $\mathbf{T} \dashv \mathbf{E}$.

The composition $\mathbf{E} \circ \mathbf{T}$ appears as a type-theoretic construction known as propositional truncation. It allows us to express the relationship between Curry-Howard and logic internally in type theory, see for instance the HoTT book.