{"id":"852754e8-1e53-494e-ba81-a939052df226","arxiv_id":"2506.01076","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new categorical account derives big-step semantics from small-step rules and proves their equivalence under a strong separation condition.","lead":"This paper builds a category-theory framework that turns small-step programming-language rules into big-step rules automatically, then proves the two semantics agree whenever the rules satisfy a new condition called strong separation. The value is a single abstract proof that replaces many hand-written, language-by-language equivalence arguments.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 5.4 requires an ω-continuous monad T, but the deterministic case studies in §6 are formulated with T=Id; the paper never proves that the Proposition 3.11 lifting to the powerset monad conservatively extends the intended deterministic semantics.","rationale":"I read the paper in good faith and the categorical proof architecture of Theorem 5.4 is sound: the strong separation condition is exactly what makes Lemmas 5.1 and 5.2 go through, the proof sketches in §5 are backed by detailed appendix calculations, and the use of ω-continuity of χ is sufficient for the monotonicity steps in the induction arguments. The reader's CONDITIONAL verdict already captures the main risks. My stress-test focuses on one load-bearing aspect that the reader listed but did not make the primary weakness: the mismatch between the theorem's ω-continuity hypothesis and the paper's deterministic examples with T=Id. This is not an internal inconsistency in the theorem, but it is a gap in the claimed coverage of the framework. If the conservative-extension step from the Id-law to the powerset-lifted law is not proved, then the deterministic case studies are not consequences of the main theorem as written. The concrete test would settle this by checking that the powerset-lifted semantics assigns at most one value to each deterministic term and agrees with the intended big-step relation. I therefore keep the verdict unchanged at CONDITIONAL, and I partially agree with the reader because they also flagged the ω-continuity issue, though they identified strong separation as the central conceptual risk.","tokens_in":36994,"tokens_out":20780,"duration_ms":194517,"concrete_test":"Instantiate the construction of Proposition 3.11 with T=P (powerset) and the standard powerset distributive law for Example 3.3, then compute ζ_hat and β_hat via equations (19) and (20) for the closed terms of xCL. Check that for every term t, ζ_hat(t) is either {v} for the unique value v with t→★v or ∅, and β_hat(t) is the same set. If any term yields a non-singleton set for a deterministic reduction path, the implicit conservative-extension bridge fails; if all terms behave as singletons/empty, then the deterministic instances are covered and the paper only needs to state and prove this lemma explicitly.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central theorem is conditional on T being ω-continuous, since the least-fixpoint definitions of ζ_hat in (19) and β_hat in (20) need bottom elements in Kleisli hom-sets; the paper explicitly notes in §2.2 that the identity monad is not ω-continuous. Yet the main deterministic case studies, including typed combinatory logic in §6.1 and PCF-style recursion in §6.2, are presented with T=Id. The paper gestures at Proposition 3.11 as a way to adjoin an ω-continuous monad, but it never states or proves the required bridge: that the powerset-valued semantics obtained by lifting a deterministic law is a conservative extension of the original deterministic small-step and big-step semantics, in the sense that ζ_hat(t) and β_hat(t) are singletons exactly when t evaluates to a value and empty otherwise. Without this conservative-extension lemma, Theorem 5.4 does not directly apply to the paper's headline deterministic examples; it applies only to their powerset-lifted versions. This is a real soft spot in the paper's scope claims, even though the internal proof of Theorem 5.4 itself appears coherent. The gap is easily repairable, but it needs to be made explicit and verified, especially because the examples in §6 are presented as direct instantiations of the main theorem.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a categorical framework for deriving big-step operational semantics from small-step operational semantics in higher-order mathematical operational semantics. It introduces separated abstract HO-GSOS laws (Definition 3.1), a strong-separation condition (Definition 3.6), and an abstract notion of big-step SOS (Definition 4.1), together with a construction translating a small-step law into a big-step law. The main result, Theorem 5.4, states that for strongly separated abstract HO-GSOS laws with an omega-continuous distributive law, the canonical big-step semantics zeta_hat equals the multi-step small-step semantics beta_hat. The paper presents case studies for typed combinatory logic, recursion and conditionals, nondeterminism and parallelism, call-by-value, and the lambda calculus with binders, and includes Haskell implementations of several examples and proofs in the appendix.","tokens_in":37239,"tokens_out":3904,"duration_ms":44298,"significance":"If the main theorem and its instantiations are fully justified, this is a valuable contribution: it provides a single abstract account of the equivalence between small-step and big-step operational semantics, going beyond syntax-driven translations and covering a wide range of language features. The paper is careful to state hypotheses, gives a counterexample (Example 2.1) showing that strong separation is genuinely needed, and provides detailed appendix proofs for the central lemmas. The Haskell implementation is a useful companion artifact. The main weakness is the gap between the omega-continuity hypothesis of Theorem 5.4 and the deterministic case studies, which are formulated with the identity monad; this gap is repairable but currently affects the scope claims.","major_comments":[{"comment":"Theorem 5.4 assumes an omega-continuous monad T, as stated at the beginning of Section 5 and needed for the least-fixpoint definitions in (19) and (20). However, the deterministic case studies in Sections 6.1, 6.2, and 6.4 are presented with T = Id, which the paper itself notes is not omega-continuous. Proposition 3.11 is cited as a way to lift a deterministic law to a powerset-valued law, but the paper never proves the required conservative-extension lemma: for every term t, the lifted semantics should satisfy zeta_hat(t) = {v} exactly when t evaluates to v and beta_hat(t) = {v} exactly when t reduces to the value v, and be empty otherwise. Without such a lemma, Theorem 5.4 applies only to the powerset-lifted versions of these examples, not to the deterministic semantics the paper claims to cover.","section":"Section 5, Theorem 5.4; Sections 6.1, 6.2, 6.4"},{"comment":"The paragraph claiming that 'for terms in the original signature (without G# and ) we obtain the same big-step semantics as in (25)' and the subsequent claim that the two variants of the small-step semantics are equivalent in multi-step behaviour are stated without proof. This equivalence is load-bearing for the call-by-value case study, because the auxiliary operators G# and are introduced precisely to satisfy strong separation while recovering the original multi-step relation. A proof or at least a precise statement of this example-level equivalence should be provided.","section":"Section 6.4, call-by-value"}],"minor_comments":[{"comment":"The displayed rules for the call-by-value small-step semantics run together in the text; the rules (a), (b), and (c) should be separated clearly, and each rule should be labelled consistently so that the later references to (a1) and (a2) are easy to follow.","section":"Section 6.4, rule display"},{"comment":"The statement of Theorem 7.3 says the proof 'remains essentially unchanged' from that of Theorem 5.4; since the definition of zeta_hat is modified in Section 7.3, it would help the reader to spell out at least the one place where Proposition 7.2 is substituted for Proposition 5.3 and to verify that strong separation still yields the analogue of Lemma 5.1 in the pointed-strength setting.","section":"Section 7, Theorem 7.3"},{"comment":"The factorization condition in Proposition 3.11 is stated abstractly, and the verification in Remark 3.12 covers only the powerset monad. A brief explanation of how the partiality monad or other omega-continuous monads would satisfy this condition would make the proposition's range of applicability clearer.","section":"Proposition 3.11"}],"recommendation":"major_revision","confidential_remarks":"The core mathematical argument appears coherent, and the main missing piece is the conservative-extension bridge between the deterministic examples and the omega-continuous setting of Theorem 5.4. If the authors add and prove that lemma, I would be willing to accept the paper. The use of self-citation [21] is appropriate background rather than a circular dependency."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The central result here is genuine: Theorem 5.4 gives one uniform categorical proof that, under strong separation, the least-fixpoint big-step semantics equals the multi-step small-step semantics. If that holds up, it replaces a pile of hand-written equivalence proofs with a single argument, and the lambda-calculus extension in Section 7 suggests the method reaches binding operators too. That is a real contribution, and the proof architecture is careful: the mutual inequality argument, the role of strong separation in Lemmas 5.1 and 5.2, and the appendix write-up all look coherent. I also like that the authors give the credit where the definition of strong separation comes from: Bloom and van Glabbeek's cool formats, and Ciobâcă's automatic translation, are cited rather than ignored.\n\nThe soft spot is real and matches the stress-test note. Theorem 5.4 assumes an omega-continuous monad T, because both fixpoint definitions need bottoms. But most of Section 6 is developed with T = Id, which the paper itself notes is not omega-continuous. The gesture toward Proposition 3.11 does not do the work: the paper never proves that lifting a deterministic law to the powerset monad is conservative, i.e., that the lifted big-step and small-step semantics return singletons exactly on terminating computations and empty otherwise. Without that bridge, the headline examples are not direct instantiations of Theorem 5.4; they are instantiations of a lifted version whose semantics has not been connected to the original. This is repairable, and I would not call it a fatal flaw, but it is a gap in the paper's scope claims that a referee should push on.\n\nTwo smaller points. First, the abstract says a general abstract argument has been 'up till now missing.' That is a bit of an oversell given Ciobâcă's syntactic translation and the cool-format line; the related-work section is honest about this, so just soften the abstract. Second, the Haskell code is mentioned but not included or linked; either ship it or drop the claim.\n\nStrong separation is restrictive, and the authors are upfront that naive call-by-value needs auxiliary operators G# and . That is an acceptable trade-off, not a flaw; Example 2.1 does show the condition is needed in general.\n\nAll told: this deserves a serious referee. My own verdict is conditional acceptance, with the omega-continuity bridge as the condition. It is a solid, honest paper that needs a missing lemma and some presentation fixes.","headline":"The main theorem is real and likely correct, but the paper never closes the gap between its omega-continuous monad hypothesis and the deterministic examples run with T = Id.","tokens_in":37829,"tokens_out":1620,"would_cite":true,"duration_ms":19427,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q55","18C15","03B40"],"pacs":[],"model":"deepseek-v4-flash","headline":"A categorical proof now establishes when small-step and big-step operational semantics coincide.","keywords":["operational semantics","big-step semantics","small-step semantics","higher-order abstract GSOS","category theory","monads","lambda calculus","coalgebra"],"falsifier":"Take the call-by-value specification from Section 6.4 rewritten with auxiliary operators, and compute both the multi-step semantics $\\hat{\\beta}$ and the canonical big-step semantics $\\hat{\\zeta}$ for the term $(\\mathit{II})(\\mathit{II})$; the theorem predicts $\\hat{\\zeta}((\\mathit{II})(\\mathit{II})) = \\hat{\\beta}((\\mathit{II})(\\mathit{II}))$ and that both give the same value only if the rewriting recovers the original multi-step relation, so a mismatch would falsify Theorem 5.4. More generally, a computer search over finite rule sets that satisfy strong separation but yield $\\hat{\\zeta} \\neq \\hat{\\beta}$ would settle the theorem's scope.","tokens_in":36731,"feed_emoji":"🔁","tokens_out":6497,"duration_ms":60114,"temperature":0.7,"pith_summary":"This paper claims that the standard equivalence between small-step and big-step operational semantics — a program evaluates to a value exactly when it can be reduced to that value in many small steps — can be proven once, at a high level of abstraction, instead of being re-proven for each programming language. It introduces a categorical notion of big-step SOS alongside the existing higher-order abstract GSOS framework, and shows that from any small-step specification satisfying a condition called strong separation one can automatically derive an equivalent big-step specification. If correct, this gives a single theorem covering typed combinatory logic, recursion and conditionals, nondeterminism and parallelism, call-by-value evaluation with auxiliary operators, and the call-by-name $\\lambda$ calculus with binders. The argument works by splitting syntax into values and computations, and by using $\\omega$-continuous monads so that recursive evaluation can be expressed as a least fixed point.","feed_headline":"One abstract proof settles big-step vs small-step semantics","feed_subtitle":"A rule-format condition called strong separation makes the classic 'evaluates to' equivalence provable once for all.","key_machinery":"The machinery is four interlocking categorical objects. (1) A separated abstract HO-GSOS law partitions the signature into value formers $\\Sigma_v$ and computation formers $\\Sigma_c$, and the behaviour into a value-behaviour part $D$ and a computation part given by a strong monad $T$; this makes the object of closed terms decompose into values plus computations and lets multi-step transitions be defined over the computation part. (2) Strong separation (Definition 3.6) is a commutativity condition on the computation-rule transformation $\\rho_c$: it requires that rules with at least one computation premise have the conclusion shape of a patience rule, so that evaluation is transparent to internal reductions. (3) $\\omega$-continuous monads and $\\omega$-continuous distributive laws $\\chi$ supply least fixed points, so both the multi-step semantics $\\hat{\\beta}$ and the big-step semantics $\\hat{\\zeta}$ are defined as Kleene fixpoints. (4) The translation (17) converts a separated small-step law into an abstract big-step SOS law $\\xi$, and Theorem 5.4 proves the two resulting fixed-point semantics coincide on computations.","core_discovery":"On the paper's own terms, the central claim is Theorem 5.4: for every strongly separated abstract HO-GSOS law with an $\\omega$-continuous distributive law, the canonical big-step semantics $\\hat{\\zeta}$ equals the multi-step small-step semantics $\\hat{\\beta}$ on the computation part. The equality is the abstract form of $t \\Downarrow v \\iff t \\to^{\\ast} v \\wedge v\\downarrow$, and it is established by mutual inequality of least fixed points. The paper also extends the result to languages with variable binders (Theorem 7.3) by reworking the value-forming rules with pointed strength and substitution tensors, obtaining as an instance the call-by-name $\\lambda$-calculus. The abstraction isolates, for the first time, a single sufficient condition — strong separation — under which the small-step relation is compatible with evaluation, so the derived big-step rules faithfully execute the strategy that the small-step rules encode.","pith_inferences":["The strong separation condition is effectively a 'no surprises' constraint on rule formats: the paper itself notes its resemblance to cool formats and patience rules; a practical upshot is that language designers who want the equivalence theorem can use it as a checklist and can repair violations by adding auxiliary operators, as done for call-by-value.","The parametric proof suggests a testable recipe for new language features: encode the feature as value and computation formers, check strong separation, and the equivalence follows without a bespoke argument; a natural next test is probabilistic or weighted semantics, where a quantitative monad would replace the powerset monad.","An implicit consequence is that failures of $\\left(\\star\\right)$ are diagnosable: a separated but not strongly separated specification (such as Example 2.1) provably cannot admit any big-step semantics satisfying the equivalence, so the condition pinpoints why a rule set is too fine-grained for big-step reasoning.","The call-by-value treatment suggests a general principle: a big-step semantics over the original signature may not exist, but a definitional extension with auxiliary operators can restore it — connecting the abstract framework to pretty-big-step semantics, as the paper notes."],"forward_implications":["For any language whose small-step rules fit the strongly separated format, the equivalence $t \\Downarrow v \\iff t \\to^{\\ast} v \\wedge v\\downarrow$ is now obtained by theorem rather than by hand; the paper demonstrates this for extended combinatory logic, typed combinatory logic, PCF-style recursion and conditionals, nondeterministic choice, and parallel composition.","The translation automatically produces big-step rules from small-step rules; the generated rules have the standard judgement shape $t \\Downarrow v$, with values forced to be those terms built from value formers.","Call-by-value can be accommodated, but only after rewriting the small-step system with auxiliary composition operators; the resulting big-step semantics matches the original call-by-value multi-step behaviour.","The lambda calculus with binders is covered via a presheaf category with a substitution tensor: the abstract equivalence is re-proven in that setting (Theorem 7.3), yielding the usual big-step rules for call-by-name $\\lambda$-calculus.","Because the equivalence is parametric in syntax and behaviour, the same proof infrastructure applies to other effects captured by $\\omega$-continuous monads, with nondeterminism (powerset monad) and partiality as the paper's running examples."],"supporting_citations":[{"why":"Supplies the Turi-Plotkin mathematical operational semantics that the paper extends to a higher-order and separated setting.","marker":"[37]"},{"why":"Introduces abstract higher-order GSOS laws, the starting point that the paper refines into separated and strongly separated laws.","marker":"[21]"},{"why":"A syntax-driven automatic translation from small-step to big-step specifications, which the paper abstracts and generalises.","marker":"[11]"},{"why":"Deriving pretty-big-step semantics from small-step semantics, the approach compared with the paper's auxiliary-operator construction.","marker":"[5]"},{"why":"Provides the theory of $\\omega$-continuous monads on which the least-fixed-point definitions of the multi-step and big-step semantics rely.","marker":"[23]"},{"why":"Gives the presheaf and substitution-tensor framework used to extend the result to languages with variable binders.","marker":"[17]"}],"fun_headline_variants":["Abstract proof unifies big-step and small-step semantics","Strong separation proves semantics equivalence once and for all","Higher-order semantics: one condition settles big-step vs small-step","Categorical framework equates small-step and big-step semantics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Strong separation is the load-bearing assumption: without the commutativity condition on rules with computation premises, the derived big-step semantics can diverge from multi-step reduction, as the paper's Example 2.1 shows.","fun_headline_variants_meta":{"raw":{"variants":["Abstract proof unifies big-step and small-step semantics","Strong separation proves semantics equivalence once and for all","Higher-order semantics: one condition settles big-step vs small-step","Categorical framework equates small-step and big-step semantics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000667,"raw_usage":{"total_tokens":3023,"prompt_tokens":908,"completion_tokens":2115,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":524,"completion_tokens_details":{"reasoning_tokens":2050}},"tokens_in":524,"tokens_out":2115,"duration_ms":13075,"temperature":1.0,"reasoning_tokens":2050,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:52:17.819436+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the call-by-value specification from Section 6.4 rewritten with auxiliary operators, and compute both the multi-step semantics $\\hat{\\beta}$ and the canonical big-step semantics $\\hat{\\zeta}$ for the term $(\\mathit{II})(\\mathit{II})$; the theorem predicts $\\hat{\\zeta}((\\mathit{II})(\\mathit{II})) = \\hat{\\beta}((\\mathit{II})(\\mathit{II}))$ and that both give the same value only if the rewriting recovers the original multi-step relation, so a mismatch would falsify Theorem 5.4. More generally, a computer search over finite rule sets that satisfy strong separation but yield $\\hat{\\zeta} \\neq \\hat{\\beta}$ would settle the theorem's scope.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"A syntax-driven automatic translation from small-step to big-step specifications, which the paper abstracts and generalises."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Deriving pretty-big-step semantics from small-step semantics, the approach compared with the paper's auxiliary-operator construction."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the theory of $\\omega$-continuous monads on which the least-fixed-point definitions of the multi-step and big-step semantics rely."},{"cited_title":"Fiore, Gordon D","cited_arxiv_id":null,"evidence_quote":"Gives the presheaf and substitution-tensor framework used to extend the result to languages with variable binders."}],"review_version":1}