{"id":"77c49357-0dfd-4bfd-964a-0a66495ca93f","arxiv_id":"1908.09123","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"In a dependently-typed Coq formalization, the adequacy lemma of classical realizability for the simply-typed lambda-calculus with sums is shown to be a normalization function, and the choice of truth and falsity witnesses determines whether it evaluates call-by-name or call-by-value.","lead":"This paper shows that a classical proof method for normalization, realizability, is literally a program: its central lemma computes a reduction sequence to a normal form. The authors mechanize this in Coq and show that tweaking the proof's semantic definitions changes the evaluation strategy from call-by-name to call-by-value.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The decisive gap is admitted in Section 2.3: the paper returns a normal mu-tilde-mu machine, but never proves the read-back to a lambda-calculus normal form, so the central weak-normalization claim for the source calculus is conditional.","rationale":"The reader's weakest_assumption identifies exactly this gap, and the paper itself flags it in Section 2.3. I found no independent, stronger objection: the Coq artifact is cited but not linked, which is a reproducibility concern rather than an argument-level gap; the machine-to-lambda correspondence is the point at which the central claim could fail even if every displayed program type-checks. The paper's expository value and the reverse-engineering of mu-tilde-mu from typing constraints are real contributions, so the concern does not warrant rejection, but it does warrant the existing CONDITIONAL verdict. If the read-back theorem is later supplied and proved, the paper would support its headline claim; until then, the claim should be read as normalization at the level of abstract machine configurations.","tokens_in":27104,"tokens_out":4932,"duration_ms":54084,"concrete_test":"Formalize in Coq a read-back function `rb` from normal mu-tilde-mu configurations reachable from `<|t|, alpha>` to lambda terms, and prove: for every closed `t` of type `A`, if `rea t` returns `(<t', alpha>, seq)`, then `rb t'` is a beta-normal form of `t` under the ordinary beta-reduction relation, using the compilation of Figure 4 and the congruence closure of beta. If the proof requires additional hypotheses (e.g., confluence or polarization of the unpolarized machine) not stated in the paper, the claimed theorem must be weakened from 'lambda normal form' to 'normal machine configuration'.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's advertised theorem is weak normalization of the simply-typed lambda-calculus with sums (Sections 1 and 3). The adequacy program `rea` of Section 4 returns, for a closed term `t`, a normal configuration of the mu-tilde-mu machine together with a machine reduction sequence. But the central conclusion requires a further, unproved step: that this normal machine configuration decodes to a beta-normal lambda term reachable from `t`. Section 2.3 admits exactly this: \"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>.\" The pole used in Section 4 (equation 27) is defined over machine normal forms, not lambda normal forms; the anti-reduction functions `_lam`, `_app`, and `_case` justify machine transitions only. Without a read-back theorem for reachable normal configurations, the output of `rea` has not been shown to be a normal form of the source calculus, only of the abstract machine. This is an internally acknowledged gap at a load-bearing position: the slogan \"the proof does the normalization\" is exactly about recovering a lambda-level normal form.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":27276,"tokens_out":7998,"duration_ms":85296,"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":[{"comment":"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.\"","section":"Section 2.3 / Section 4"},{"comment":"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.","section":"Sections 2.3 and 3.3"}],"minor_comments":[{"comment":"The heading contains a typo: \"Adeqacy\" should be \"Adequacy\".","section":"Lemma 2.5"},{"comment":"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.","section":"Section 3.2"},{"comment":"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.","section":"Section 5"},{"comment":"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.","section":"Notation"},{"comment":"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.","section":"Section 4"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is in good shape for a pearl; the Coq development gives me confidence in the internal soundness of the construction. My main reservation is purely about the scope of the claims: the missing read-back theorem is admitted in Section 2.3, but the abstract and conclusion present the result as source-level weak normalization. I would be happy to accept after the authors either supply (or precisely cite with a proof sketch) the read-back/simulation theorem, or explicitly rescope the claims to normalization of the mu-tilde-mu machine."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a clear, honest functional pearl about where the computational content of classical realizability lives. The main caveat is that the advertised lambda-level weak-normalization claim is slightly ahead of what is actually proved: the paper returns a normal mu-tilde-mu machine, and the read-back to a lambda normal form is explicitly deferred in Section 2.3.\n\nWhat is actually new: the adequacy lemma, written as a dependently typed program, becomes an evaluation function; the compilation to mu-tilde-mu is reverse-engineered from the typing constraints rather than assumed; and the alternative witness definitions in Section 5 give a concrete, machine-checked picture of why CBN vs CBV falls out of the semantics. The Coq development is real evidence, and the authors are unusually candid that the high-level idea is folklore. The paper is also readable: it is one of the better gentle introductions to classical realizability and abstract-machine calculi that I know.\n\nThe soft spots are real but mostly minor. The read-back gap is the one that bites. Equation (27) defines the pole over normal machine configurations, and the fundamental lemma shows that a well-typed term reaches one of those. But 'weak normalization of the simply-typed lambda calculus' needs a further theorem saying that a normal machine configuration decodes to a beta-normal lambda term related to the input. The paper says this is easy using Munch-Maccagnoni and Scherer [2015] and does not prove it. That is an admitted gap at a load-bearing point if the slogan 'the proof does normalization' is taken literally. It is probably fixable, but as written the formal statement is machine normalization, not lambda normalization. The authors should either include the read-back or state the machine-level result as the main theorem.\n\nTwo smaller things: the supplementary Coq artifact has no URL or commit hash, so reproducibility is weaker than the claim 'machine-checked' suggests; and Section 3.2's simplified system is explicitly weaker than the dependent one, which is fine but means the pedagogical warm-up is not directly the theorem.\n\nOverall: this deserves peer review. It is a solid pearl with a fixable gap, and the variant analysis is a useful reference. I would bring it to a reading group and would cite it if I worked on realizability or normalization-by-evaluation.","headline":"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.","tokens_in":27877,"tokens_out":3775,"would_cite":true,"duration_ms":39870,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B40","68N18"],"pacs":[],"model":"deepseek-v4-flash","headline":"The adequacy lemma of classical realizability, written as a dependently typed program, is an evaluation function.","keywords":["classical realizability","dependent types","mu-tilde-mu abstract machine","bi-orthogonality","weak normalization","simply-typed lambda calculus with sums","call-by-name","call-by-value"],"falsifier":"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.","tokens_in":26828,"feed_emoji":"🔄","tokens_out":13673,"duration_ms":120379,"temperature":0.7,"pith_summary":"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.","feed_headline":"The proof of normalization is the normalizer","feed_subtitle":"A dependently typed adequacy proof returns the reduction sequence; witness choices set call-by-name or call-by-value.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Provides the reducibility method that the paper reworks into a proof-relevant program.","marker":"Tait [1967]"},{"why":"Introduces bi-orthogonality for normalization, the closure the paper uses for positive types.","marker":"Girard [1987]"},{"why":"Shows that bi-orthogonality (top-top closure) solves the ill-foundedness of reducibility at sum types.","marker":"Lindley and Stark [2005]"},{"why":"Gives the realizability-structure axioms (terms, contexts, pole, anti-reduction) that the proof-relevant model instantiates.","marker":"Krivine [2008]"},{"why":"Provides the mu-tilde-mu abstract machine, the calculus of terms and co-terms used as realizers.","marker":"Curien and Herbelin [2000]"},{"why":"Supplies the mu-tilde-mu syntax variant and the correspondence between normal machine configurations and lambda-calculus normal forms.","marker":"Munch-Maccagnoni and Scherer [2015]"},{"why":"Relates classical realizability to intuitionistic realizability after CPS, supporting the evaluation-order reading.","marker":"Oliva and Streicher [2008]"},{"why":"Proposes an intuitionistic realizability with sums whose strong-forcing and double-negation variants move between call-by-name and call-by-value, paralleling the paper's Variant (1) and Variant (3) analysis.","marker":"Ilik [2013]"}],"fun_headline_variants":["Adequacy lemma is a normalizer","Realizability proof is the evaluation","Proof choices decide call-by-name or call-by-value","Dependent typing turns adequacy into evaluation","Bi-orthogonal closure handles sums in normalization"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Adequacy lemma is a normalizer","Realizability proof is the evaluation","Proof choices decide call-by-name or call-by-value","Dependent typing turns adequacy into evaluation","Bi-orthogonal closure handles sums in normalization"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000328,"raw_usage":{"total_tokens":1889,"prompt_tokens":1059,"completion_tokens":830,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":675,"completion_tokens_details":{"reasoning_tokens":763}},"tokens_in":675,"tokens_out":830,"duration_ms":8249,"temperature":1.0,"reasoning_tokens":763,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:21:37.022763+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the realizability-structure axioms (terms, contexts, pole, anti-reduction) that the proof-relevant model instantiates."}],"review_version":1}