Dependent Pearl: Normalization by realizability

TL;DR

This paper presents a dependently-typed program that models normalization proofs for the simply-typed lambda calculus with sums using Krivine's realizability, making semantic proof techniques more accessible.

Contribution

It offers a novel dependently-typed implementation of normalization by realizability, illustrating how evaluation order is influenced by reducibility predicate definitions.

Findings

Normalization corresponds to an evaluation procedure in the dependently-typed program.

Choices in defining reducibility predicates affect evaluation order and behavior.

The approach provides an accessible, programmatic perspective on semantic proof techniques.

Abstract

For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness. Why do they work? At which point in the proof is "the real work" done? Hoping to build a programming intuition of these proofs, we implement a normalization argument for the simply-typed lambda-calculus with sums: instead of a proof, it is described as a program in a dependently-typed meta-language. The semantic technique we set out to study is Krivine's classical realizability, which amounts to a proof-relevant presentation of reducibility arguments -- unary logical relations. Reducibility assigns a predicate to each type, realizability assigns a set of realizers, which are abstract machines that extend lambda-terms with a first-class notion of contexts. Normalization is a direct consequence of an adequacy theorem or "fundamental lemma", which states that any well-typed term translates to a realizer of its type. We show that the adequacy theorem, when written as a dependent program, corresponds to an evaluation procedure. In particular, a weak normalization proof precisely computes a series of reduction from the input term to a normal form. Interestingly, the choices that we make when we define the reducibility predicates -- truth and falsity witnesses for each connective -- determine the evaluation order of the proof, with each datatype constructor behaving in a lazy or strict fashion. While most of the ideas in this presentation are folklore among specialists, our dependently-typed functional program provides an accessible presentation to a wider audience. In particular, our work provides a gentle introduction to abstract machine calculi which have recently been used as an effective research vehicle.