Pith. sign in

REVIEW 2 major objections 5 minor 26 references

Dependent Pearl: Normalization by realizability

T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The adequacy lemma of classical realizability, written as a dependently typed program, is an evaluation function.

desk verdict A clear, honest functional pearl on the computational content of realizability, with an admitted read-back gap between normal mu-tilde-mu configurations and lambda normal forms that should be fixed or qualified. read the letter →

arxiv 1908.09123 v2 pith:LLXR3GJF submitted 2019-08-24 cs.PL cs.LO

Pierre-Évariste Dagand , Lionel Rieg , Gabriel Scherer This is my paper · ORCID
classification cs.PLcs.LO MSC 03B4068N18
keywords classicalrealizabilitydependenttypesmu-tilde-muabstractmachinebi-orthogonalityweaknormalizationsimply-typedlambdacalculuswithsumscall-by-namecall-by-value
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that the adequacy lemma at the heart of a classical realizability proof of weak normalization is not merely a proof: it is an evaluation function. Once the lemma is written as a dependently typed program, applying it to a typing derivation and a semantic substitution returns a normal configuration together with the reduction sequence that reaches it. The paper further shows that choices in the definitions of truth and falsity witnesses for the function type decide whether the extracted evaluator runs call-by-name or call-by-value. If this is right, realizability proofs are demystified: normalization is achieved by running the proof itself, and evaluation order is a consequence of the proof's semantic structure rather than an external choice.

What carries the argument

The central object is the proof-relevant interpretation of classical-realizability predicates: truth witnesses $t\in|A|$, falsity witnesses $e\in\|A\|$, and a pole whose membership proofs are pairs of a normal configuration and a reduction sequence. Orthogonality and bi-orthogonal closure turn these witnesses into a typed model in which membership carries computational data. The untyped $\mu\tilde\mu$ abstract machine supplies the term and co-term syntax in which realizers live, with reduction rules for functions and sums; in the dependent proof those rules become anti-reduction annotations. The machinery works because each annotation must name a specific machine transition, so the proof object itself contains the reduction sequence.

What would settle it

Run the extracted evaluator on closed simply-typed terms with sums while logging every $\mu\tilde\mu$ transition: the claim is falsified if the returned sequence does not start at the initial configuration $\langle \lfloor t\rfloor \mid \star\rangle$, uses transitions other than rules (9)--(12), or ends in a normal configuration that cannot be translated back to a $\lambda$-calculus normal form. The evaluation-order claim can be tested by running Variant (1) and Variant (3) on a term whose call-by-name and call-by-value reductions differ in the first redex; the logs must differ in the first transition.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that the computational content of the adequacy lemma `rea` is a normalization function for the simply-typed $\lambda$-calculus with sums. The dependent type of `rea` forces every claim of membership in the pole to carry a witness: a normal machine configuration together with a reduction sequence. Building that witness is exactly evaluating the term, and the effort of making the lemma dependently typed reverse-engineers the compilation from $\lambda$-terms to the $\mu\tilde\mu$ abstract machine. The typing constraints determine each anti-reduction annotation, and different choices for the falsity-value witnesses of the arrow type—Variant (1) using arbitrary truth witnesses for the argument versus Variant (3) using value witnesses—produce call-by-name and call-by-value evaluators respectively. Sums are accommodated through bi-orthogonal closure, which avoids the ill-foundedness of a naive reducibility predicate at sum types.

Load-bearing premise

The load-bearing premise is that normal configurations of the untyped, unpolarized $\mu\tilde\mu$ machine correspond exactly to normal forms of the simply-typed $\lambda$-calculus with sums; the paper cites this correspondence, relying on prior work rather than proving it here.

Editorial extensions

If this is right

  • Extracting the dependently typed adequacy lemma yields an executable normalizer that returns a normal configuration together with a reduction sequence, not merely a proof that one exists.
  • Using Variant (1) for the falsity values of the arrow type gives a call-by-name evaluator; using Variant (3) gives call-by-value, so the witness definitions are evaluation-strategy definitions.
  • Sum types are handled without ill-founded reducibility predicates and without commuting conversions, by bi-orthogonal closure of positive types.
  • The compilation scheme from $\lambda$-calculus to $\mu\tilde\mu$ is forced by the typing constraints of the adequacy proof, so the abstract machine is discovered from the proof rather than imposed separately.
  • Each connective's interpretation can be varied independently, so lazy or strict sums can be combined with call-by-name or call-by-value arrows to obtain complete normalization proofs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • One testable consequence the paper leaves open: the four arrow variants should yield evaluators differing only in evaluation order; this could be checked by logging the first machine transition on a suite of simply-typed terms.
  • The same reverse-engineering recipe could be applied to binary logical relations, where a dependently typed adequacy lemma would likely exhibit a relational evaluator rather than a reduction sequence.
  • Because arrow and sum interpretations vary independently, one could assemble mixed-strategy evaluators (for instance call-by-value functions with lazy sums) and inspect their operational behavior, turning the paper's modularity observation into a construction kit.
  • If the uniqueness conjecture is true, the entire design space collapses: for fixed witness choices there is exactly one pure program (up to $\beta\eta$ equivalence) inhabiting the type of `rea`, which would make normalization proofs canonical objects.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper develops a proof-relevant, dependently typed formalization of Krivine classical realizability for the simply typed lambda-calculus with sums. The main object is an adequacy function `rea` that, given a typing derivation and a substitution witnessing the context, returns a normal configuration of the mu-tilde-mu abstract machine together with a reduction sequence to it. The authors implement the construction in Coq, extract an OCaml evaluator, and show that choosing value witnesses for the arrow type among four variants changes the induced evaluation strategy (call-by-name for Variants (1)-(2), call-by-value for (3)-(4)). They also argue that the compilation from lambda terms to mu-tilde-mu is recovered from the typing constraints of the dependent adequacy proof.

Significance. If the source-level normalization claim is fully established, this is a valuable and pedagogically effective pearl: it exposes the computational content of realizability proofs, provides a machine-checked formalization with extraction, and makes precise the folklore connection between polarity, witness choices, and evaluation order. The claim that the proof itself computes the reduction sequence is the kind of concrete, checkable insight that makes the paper likely to be used by others. The mechanical proof and the parameter-free development are concrete strengths.

major comments (2)
  1. [Section 2.3 / Section 4] The central advertised result is weak normalization of the simply-typed lambda-calculus with sums, but the paper proves only that the compiled mu-tilde-mu machine reaches a normal configuration. Equation (27) defines the pole over machine normal forms, and the anti-reduction witnesses `_lam`, `_app`, `_case` justify machine transitions. Section 2.3 explicitly defers the read-back from mu-tilde-mu normal forms to lambda-calculus normal forms ("Proving this ... requires building more technical knowledge of mu-tilde-mu"), so no theorem in the paper connects the output of `rea` to a beta-normal form of the source term. This is a load-bearing gap for the abstract's claim that the proof "computes a series of reductions from the input term to a normal form."
  2. [Sections 2.3 and 3.3] Relatedly, the reduction sequence produced by `rea` is a sequence of mu-tilde-mu machine steps, including reductions corresponding to commuting conversions (e.g., Example 2.7). The source language's reduction relation is never defined (Section 2 says the rules are folklore), so the paper does not show that the machine reduction sequence maps to a reduction sequence of the source calculus. Without a simulation or read-back result, the machine-level normalization result cannot be transferred to the source calculus whose normalization is claimed in the abstract and introduction.
minor comments (5)
  1. [Lemma 2.5] The heading contains a typo: "Adeqacy" should be "Adequacy".
  2. [Section 3.2] The simplified pole discards the relation between the input machine and the returned normal configuration; although the text immediately acknowledges this, the sentence in Section 3.3 that the program "is, as expected, a normalization function" should be qualified so that readers do not take the simplified version as a correctness claim.
  3. [Section 5] The text states that all four variants are studied in Coq, but only Variants (1) and (3) are analyzed in the paper; a one-sentence summary of the evaluation order induced by Variants (2) and (4) would make the design-space claim self-contained.
  4. [Notation] The paper relies on colors to distinguish object-level and meta-level syntax; some readers will use monochrome prints, so a fallback notation for the main definitions would improve accessibility.
  5. [Section 4] The section mentions extraction and two pole instantiations but does not state the Coq version or the exact statement of the main theorem in the artifact; please add this information to help reproducibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the Coq-checked adequacy program computes normal machines by construction; the only flagged issue is an admitted unproved read-back in Section 2.3, which is a limitation rather than a circular reduction.

full rationale

The derivation is self-contained: the adequacy program `rea` (Section 4) is implemented and type-checked in Coq, and its output type `m∈⊥⊥` (Eq. 27) is by definition a reduction sequence to a normal mu-tilde-mu configuration. The weak-normalization claim for the source calculus additionally needs the read-back from normal mu-tilde-mu machines to lambda-normal forms; Section 2.3 explicitly defers this to Munch-Maccagnoni and Scherer [2015]: 'Proving this ... requires building more technical knowledge of mu-tilde-mu than what is presented in this article; here we focus on computing the normal machine from <|t|, alpha>.' That is a genuine limitation, but it is not circular: the read-back is an external correspondence result, not an input to the definition of `rea`, and no fitted parameter or renamed prediction is involved. The Section 5 conclusion that Variants (1) and (3) induce call-by-name and call-by-value is a direct consequence of the two definitions of `||A->B||_V` and of the mu-tilde-mu reduction rules, not a regression to those definitions disguised as a prediction. I therefore find no circular step.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no free parameters. Its central derivation relies on the standard properties of orthogonality, on the soundness of the metatheory and extraction, and on an externally cited correspondence between mu-tilde-mu machine normal forms and lambda-calculus normal forms. No new entities are postulated.

assumptions (3)
  • domain assumption The mu-tilde-mu abstract machine of Figure 3 is a faithful representation of the simply-typed lambda-calculus with sums: a normal configuration <u|alpha> corresponds to a lambda-term normal form.
    Invoked in Section 2.3; the paper explicitly defers the proof to Munch-Maccagnoni and Scherer [2015].
  • standard math The pole of normalizing configurations is closed under the anti-reduction rules (9)-(12) of the machine.
    Used throughout Sections 3 and 4 to turn a reduction step into a justification that the unreduced configuration is in the pole; follows directly from the definition.
  • domain assumption The metatheory of Coq with Prop is sound and its extraction to OCaml preserves the computational behavior of the adequacy program.
    The paper's claim that the extracted program computes reduction sequences relies on the soundness of the proof assistant and of its extraction mechanism (Section 4).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Dependent Pearl: Normalization by realizability." pith.science (2026). https://pith.science/paper/LLXR3GJF

@misc{pith2026190809123,
  author       = {Pith},
  title        = {Pith review of: Dependent Pearl: Normalization by realizability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LLXR3GJF}},
  note         = {Machine review of arXiv:1908.09123}
}
read the original 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.

Figures

Figures reproduced from arXiv: 1908.09123 by the authors.

Figure 1
Figure 1. Source language: simply-typed λ-calculus 1Available as supplementary material [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. The Krivine Abstract Machine pushes an applied argument t into the context e, and an end-of-stack symbol ⋆) as well as machine configurations ⟨t | e ⟩, pairing a term and a context together to compute. Remark. For this simplified abstract machine, the terms t of the machine configuration are exactly the usual (untyped) λ-terms – with only function types, no sums, integers, or unit type. This is not the case in gener… view at source ↗
Figure 3
Figure 3. An untyped µµ˜ abstract machine ⌊λx.t⌋ ≜ µ(x · α). ⟨ ⌊t⌋ | α ⟩ ⌊t u⌋ ≜ µα. ⟨ ⌊t⌋ | ⌊u⌋ · α ⟩ ⌊σi t⌋ ≜ σi ⌊t⌋  match t with [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: A compilation scheme from the λ-calculus to µµ˜ (fragment with functions and sums) may contain α). For example, in the Krivine machine, application t u expects to be put against a context e, and this reduces to ⟨t | u · e ⟩. In µµ˜, application t u is not a primitive t…
Figure 5
Figure 5. Figure 5: Summary of the simply-typed setting 4 A DEPENDENTLY-TYPED REALIZABILITY PROGRAM In the following, we undo the simplification presented in Section 3.2, by moving back to dependent types. The best way to make sure that our program is type-correct is to run a type-checker…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 15 canonical work pages

  1. [2015]

    Structures for structural recursion. In ICFP. https: //doi.org/10.1145/2858949.2784762 Paul Downen, Luke Maurer, Zena M. Ariola, and Simon Peyton Jones

    arXiv

  2. [9]

    Constructing Type Systems over an Operational Semantics. J. Symb. Comput. 14, 1 (1992). https: //doi.org/10.1016/0747-7171(92)90026-Z Hugo Herbelin

    doi:10.1016/0747-7171(92)90026-z 1992

  3. [10]

    C’est maintenant qu’on calcule, au cœur de la dualité. (2011). http://pauillac.inria.fr/~herbelin/ habilitation/ Thèse d’habilitation à diriger les recherches (French). Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson

    work page 2011

  4. [12]

    Continuation-passing style models complete for intuitionistic logic. Ann. Pure Appl. Logic 164, 6 (2013). https://doi.org/10.1016/j.apal.2012.05.003 Jean-Louis Krivine

    work page doi:10.1016/j.apal.2012.05.003 2013

  5. [17]

    A Survey of Classical Realizability. In TLCA. https://doi.org/10.1007/978-3-642-21691-6_1 Guillaume Munch-Maccagnoni

    work page doi:10.1007/978-3-642-21691-6_1

  6. [19]

    Polarised Intermediate Representation of Lambda Calculus with Sums. In LICS. https://doi.org/10.1109/LICS.2015.22 Paulo Oliva and Thomas Streicher

    work page doi:10.1109/lics.2015.22 2015

  7. [20]

    On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundam. Inform. 84, 2 (2008). Andrew M. Pitts

    work page 2008

  8. [21]

    In Applied Semantics, International Summer School, APPSEM

    Operational Semantics and Program Equivalence. In Applied Semantics, International Summer School, APPSEM. https://doi.org/10.1007/3-540-45699-6_8 Andrew M Pitts and Ian DB Stark

    doi:10.1007/3-540-45699-6_8

Show all 26 references
  1. [24]

    A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. In POPL. https://doi.org/10.1145/3158152 Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer

    doi

  2. [25]

    Logical relations for fine-grained concurrency. In POPL. https://doi.org/10.1145/2480359.2429111 Noam Zeilberger

  3. [26]

    (August 2013)

    Polarity in Proof Theory and Programming. (August 2013). http://noamz.org/talks/logpolpro.pdf Lecture Notes for the Summer School on Linear Logic and Geometry of Interaction in Torino, Italy

    2013

  4. [1967]

    The journal of symbolic logic 32, 2 (1967)

    Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32, 2 (1967). https://doi.org/10.2307/2271658 The Coq Development Team

    1967 doi

  5. [1985]

    Un interpreéteur du lambda-calcul. (1985). https://www.irif.fr/~krivine/articles/interprt.pdf Jean-Louis Krivine

    1985

  6. [1987]

    Linear Logic. Theor. Comput. Sci. 50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4 Robert Harper

    1987 doi

  7. [1992]

    Journal of Logic and Computation 2, 3 (1992), 297–347

    Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2, 3 (1992), 297–347. https://doi.org/10.1093/logcom/2.3.297 Robert Atkey, Neil Ghani, and Patricia Johann

    1992 doi

  8. [1998]

    Higher order operational techniques in semantics (1998)

    Operational reasoning for functions with local state. Higher order operational techniques in semantics (1998). Lionel Rieg

    1998

  9. [2000]

    The duality of computation. In ICFP. https://doi.org/10.1145/357766.351262 Olivier Danvy

  10. [2007]

    Higher-Order and Symbolic Computation (2007)

    A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation (2007). https://doi.org/10.1007/s10990-007-9018-9 Jean-Louis Krivine

    2007 doi

  11. [2008]

    Structures de réalisabilité, RAM et ultrafiltre sur N. (Sept. 2008). https://hal.archives-ouvertes.fr/ hal-00321410 34 p. Jean-Louis Krivine

    2008

  12. [2009]

    Panoramas et synthèses 27 (2009), 197–229

    Realizability in classical logic. Panoramas et synthèses 27 (2009), 197–229. https://hal. archives-ouvertes.fr/hal-00154500 Rodolphe Lepigre

    2009

  13. [2011]

    In FoSSaCS

    Realizability and Parametricity in Pure Type Systems. In FoSSaCS. https: //doi.org/10.1007/978-3-642-19805-2_8 Aloïs Brunel

    doi

  14. [2012]

    λ-calcul, machines et orthogonalité. (2012). http://guillaume.munch.name/files/ gdt-logique_24-10-11.pdf Lecture notes from the Groupe de Travail de Logique. Guillaume Munch-Maccagnoni

    2012

  15. [2013]

    In W ACT

    Logical Relations and Parametricity – A Reynolds Programme for Category Theory and Programming Languages. In W ACT. https://doi.org/10.1016/j.entcs.2014.02.008 Danko Ilik

    2014 doi

  16. [2014]

    A relationally parametric model of dependent type theory. In POPL. https://doi.org/10.1145/2535838.2535852 Henk Barendregt and Giulio Manzonetto

  17. [2016]

    A theory of effects and resources: adjunction models and polarised calculi. In POPL. https://doi.org/10.1145/2837614.2837652 Pierre-Louis Curien and Hugo Herbelin

  18. [2018]

    A tutorial on computational classical logic and the sequent calculus. J. Funct. Program. (2018). Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola

    2018

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.