Revisiting the duality of computation: an algebraic analysis of classical realizability models

TL;DR

This paper explores algebraic structures underlying classical realizability models, introducing disjunctive and conjunctive algebras to reflect dual computational strategies and extending the algebraic foundation of logic and computation.

Contribution

It introduces disjunctive and conjunctive algebras as new structures generalizing implicative algebras, highlighting the duality of call-by-name and call-by-value computation.

Findings

Disjunctive algebras are particular cases of implicative algebras.

Conjunctive algebras focus on conjunctions and call-by-value evaluation.

Algebraic structures reflect the duality of computational strategies.

Abstract

In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen's forcing, and even more, gives rise to unexpected models of set theories. Pursuing the algebraic analysis of these models that was first undertaken by Streicher, Miquel recently proposed to lay the algebraic foundation of classical realizability and forcing within new structures which he called implicative algebras. These structures are a generalization of Boolean algebras based on an internal law representing the implication. Notably, implicative algebras allow for the adequate interpretation of both programs (i.e. proofs) and their types (i.e. formulas) in the same structure. The very definition of implicative algebras takes position on a presentation of logic through universal quantification and the implication and, computationally, relies on the call-by-name $\lambda$-calculus. In this paper, we investigate the relevance of this choice, by introducing two similar structures. On the one hand, we define disjunctive algebras, which rely on internal laws for the negation and the disjunction and which we show to be particular cases of implicative algebras. On the other hand, we introduce conjunctive algebras, which rather put the focus on conjunctions and on the call-by-value evaluation strategy. We finally show how disjunctive and conjunctive algebras algebraically reflect the well-known duality of computation between call-by-name and call-by-value.