{"id":"43763f71-8841-4b22-b3bf-e0b5c7e3320a","arxiv_id":"2506.03382","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"ForNo, a reversible stack language, is claimed to characterize exactly the polynomial-time two-way bijections with zero garbage.","lead":"The paper presents ForNo, a reversible stack-based programming language, and claims it computes exactly the polynomial-time bijections with zero leftover data. The result is plausible but rests on unproved soundness assertions and omitted definitions.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 4 depends on FPTIME-soundness, but Section 4 only cites [6,8] instead of proving that every ForNo term is 'simple'; with the push/pop counter semantics left undefined, the claimed soundness is not verifiable.","rationale":"The reader's weakest assumption is exactly the unproved soundness assertion in Section 4, and I agree that this is the most load-bearing gap. I also examined the completeness side and the Bennett-trick construction in Theorem 4. The completeness proof omits the definitions of EMPTY and TO, but the compiler sketch is plausible and those macros are standard; the Bennett construction is standard and appears to be internally consistent, assuming reversibility. The soundness theorem, by contrast, is the only place where the implicit-complexity claim is discharged, and it is discharged by citation only. I did not find an actual ForNo term that computes outside FPTIME, but the paper gives no way to rule one out: the 'simple' condition from [6,8] is not formalized, and the counter-based push/pop semantics is not defined in the preprint. The linked Coq repository proves the inverse property of push/pop, not soundness, so it does not fill the gap. A formal proof of polynomial-time soundness, or a concrete counterexample, would settle the question; until then the rejection is appropriate.","tokens_in":8054,"tokens_out":14883,"duration_ms":185341,"concrete_test":"Open the linked Coq repository and extract the exact definitions of pushn and popn; check whether PUSH[n] decrements c and leaves the stack unchanged when c>0. Then formalize Theorem 3 by defining a syntax-directed measure mu(T) on ForNo terms and proving, against the big-step semantics of Fig. 1, that for every initial state whose stacks have total length n, the derivation height and all intermediate stack lengths are bounded by a polynomial p_T(n). If some accepted term (e.g., any term nesting FOR over a register not listed in N, or using the counter in a way not covered by [6,8]) violates the measure, soundness is false; if the proof succeeds, the concern is settled and Theorem 4 goes through.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central characterization (Theorem 4, Section 5) rests on the 'if' direction, which uses Theorem 3 (Section 4) to conclude that a zero-garbage ForNo computation of f and its inverse forces f and f^-1 into FPTIME. Theorem 3 is not proved in the paper. The argument says ForNo meets two criteria from [6,8] and that the NORMAL restrictions make all terms 'simple', but the paper never states the definition of 'simple' concretely, never instantiates the cited criteria for ForNo's syntax, and never shows by induction that every accepted term satisfies them. The criteria in [6,8] are stated for stack languages with a specific push/pop behavior; ForNo's Fig. 1 gives only the signatures popn(phi(x),c) and pushn(phi(x),c), not their definitions, and the asserted inverse equality popn(pushn(s,c))=(s,c)=pushn(popn(s,c)) only makes sense under a nonstandard counter-consuming interpretation of PUSH. Because the 'if' direction of Theorem 4 uses Theorem 3 exactly at the point where soundness is needed, an unproved soundness assertion leaves the characterization unsupported. This is not a cosmetic gap: the forbidden term (3) shows the intended invariant is nontrivial, and the paper does not rule out other dangerous patterns beyond the one example.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces ForNo, an imperative stack-based reversible programming language with a syntactic normal-register restriction. It claims ForNo is FPTIME-complete and FPTIME-sound, and uses these properties to prove Theorem 4: a bijection f is a Two-way bijection iff ForNo computes f with zero-garbage. The completeness direction is argued through a compiler from polynomial-time Turing machines, the soundness direction by appeal to criteria from [6,8], and the zero-garbage characterization by a Bennett-trick construction.","tokens_in":8401,"tokens_out":17982,"duration_ms":188656,"significance":"If the main result were fully proved, it would be a valuable contribution linking implicit computational complexity and reversible computing, and it would improve on Kristiansen's RBS by giving zero-garbage computations of two-way bijections. The syntactic restriction in NORMAL blocks is a principled way to prevent self-accelerating loops, and the paper provides a Coq-checked statement of push/pop invertibility. However, the central claim is not currently established: the FPTIME-soundness theorem is asserted rather than proved, the stack operations are not defined in the text, and the Bennett-trick proof contains a concrete error in the COPY macro.","major_comments":[{"comment":"The FPTIME-soundness theorem is the load-bearing step for the 'if' direction of Theorem 4, but it is not proved. The text says ForNo meets two criteria from [6,8] and that the NORMAL restrictions imply all terms are 'simple', yet 'simple' is never defined, the criteria are not instantiated for ForNo's syntax, and no induction establishes that every accepted term satisfies them. The cited criteria are formulated for stack languages with plain stack stores, while ForNo's state includes a global error counter, so it is not immediate that they apply. A complete proof, or a precise theorem with a proof, is required before Theorem 4 can be accepted.","section":"Section 4, Theorem 3"},{"comment":"The functions pushn and popn are only given signatures; their defining equations are absent. The examples (1) and (2) illustrate pop, but not push, and the asserted inverse identity popn(pushn(s,c)) = (s,c) = pushn(popn(s,c)) cannot be verified from the text. Under the natural reading suggested by the examples (pop removes a matching top, otherwise leaves the stack and increments the counter), the second equality fails for a failed pop. Moreover, the reversibility of arbitrary terms is stated with 'we can prove' but no proof is included. Since the 'if' direction of Theorem 4 uses -Tf to compute f^-1, both the operation definitions and the reversibility proof are load-bearing. The authors should define pushn and popn explicitly, prove the inversion identity in the paper, and include a proof of the term-level reversibility statement.","section":"Section 2, Fig. 1"},{"comment":"The macro COPY(x;y) is defined using ROF x, whose semantics iterates over reverse(ω(x)). Consequently it writes the reverse of the content of x into y, not a copy of x. The subsequent uncomputation steps in the Bennett-trick construction require an exact copy, so the composed term Rf does not compute f with zero-garbage as written. Replacing ROF by FOR would fix the macro, but as it stands the 'only if' direction of Theorem 4 is invalid.","section":"Section 5, Theorem 4 proof"},{"comment":"The macros EMPTY and TO are essential to SIMULATE and to the proof of Theorem 2, but their definitions are omitted with only a note that 'one checks' their behavior. Since Corollary 1 and hence the 'only if' direction of Theorem 4 depend on the compiler, the completeness proof is incomplete. The full definitions should be given, together with proofs that they are in ForNo and have the stated effects, including preservation of the soundness of the counter.","section":"Section 3, The compiler J·K"}],"minor_comments":[{"comment":"'Two-way bijectionsboth' should read 'Two-way bijections both'.","section":"Abstract"},{"comment":"The syntactic provisos speak of selection or iteration bodies S1,...,Sn, but the grammar allows IF x=n {T} with an arbitrary T body at top level; clarify how the read-only conditions apply to such T bodies.","section":"Section 2, grammar"},{"comment":"The listing heading says REMOVE−BLANK while the text says REMOVE−BLANKS; the notation should be consistent.","section":"Section 3, Listing 5"},{"comment":"'both τ and ω are sound state' should be 'sound states'.","section":"Section 5, proof of Theorem 4"},{"comment":"The auxiliary judgment H s, L; ωI ⇓ ω′ is used before its components are explained; a one-sentence gloss would improve readability.","section":"Section 2, Fig. 1"}],"recommendation":"major_revision","confidential_remarks":"The paper addresses a real gap in reversible implicit complexity and the main idea is worth pursuing. In my view the current version is not acceptable, but the problems are fixable within the scope of a revision: add a full soundness proof, define the stack operations, correct the COPY macro, and supply the missing compiler macros. I therefore recommend major revision rather than rejection. I would also ask the authors to make the Coq development part of the submission or at least to state the exact definitions used in it, since the text currently leaves the semantics underspecified."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me give you the short version. The new thing here is ForNo, an imperative stack-based reversible language, and the claim that it characterizes two-way bijections with zero garbage. The model is not a trivial variant of Kristiansen's RBS: RBS handles decision problems and leaves garbage, while ForNo is aimed at bijective functions and zero-garbage. That is an actual step forward.\n\nWhat the paper does well: the completeness direction is credible. The compiler from a PTIME Turing machine to ForNo is sketched with macros and the Bennett trick is applied in the expected way. The paper also points to a Coq repository for the push/pop inverse property, which is more than many reversible-calculus papers do.\n\nNow the soft spots. The 'if' direction of Theorem 4 depends on Theorem 3, the FPTIME-soundness of ForNo. Theorem 3 is not proved. The paper says ForNo satisfies two criteria from Kasai-Adachi and Kristiansen-Niggl and that the NORMAL restrictions imply all terms are simple. But it never states the definition of 'simple' for ForNo, never instantiates those criteria, and never gives an induction showing every accepted term meets them. The forbidden term (3) shows one dangerous pattern, but it doesn't rule out other interactions. This is not a cosmetic issue: without soundness, zero-garbage computation in ForNo does not imply both directions are polynomially bounded.\n\nThe push/pop counter semantics is also under-specified. The rules give only signatures, and the behavior is illustrated by two examples. From the text I can infer that a failed pop increments the counter, but the paper never states that formally. The Coq repository may settle the inverse equations, but the semantics itself should be in the paper.\n\nNone of these are fatal to the underlying idea. The completeness direction is decent, and the soundness gap looks fillable—it's a matter of adapting the known criteria to ForNo and writing out the proof. The macro definitions for EMPTY and TO are omitted, but that is minor.\n\nWho is this for? People working in implicit computational complexity and reversible programming. If you red-team a normalizations claim, you'd skip it; if you want a fresh syntactic constraint that might characterize two-way bijections, it's worth a serious look.\n\nMy recommendation: send it to peer review. The gaps are real and load-bearing, and a referee should demand a complete proof of soundness before publication. But the model is new, the question is natural, and the authors are open about relying on external criteria. That deserves referee time, not a desk reject.","headline":"ForNo is a genuinely new reversible model, but the main characterization rests on an unproved soundness assertion, so the draft reads more like a research proposal than a complete theorem.","tokens_in":8873,"tokens_out":2515,"would_cite":true,"duration_ms":27536,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q15","68Q05"],"pacs":[],"model":"deepseek-v4-flash","headline":"Zero-garbage ForNo programs compute exactly the two-way bijections.","keywords":["reversible computation","implicit computational complexity","two-way bijections","zero-garbage computation","stack-based programming language","FPTIME","reversible programming language"],"falsifier":"Construct or find a ForNo term that, on inputs of length $n$, takes more than $p(n)$ steps for every polynomial $p$, while still computing a total function; checking whether the forbidden pattern from Eq. (3) can be smuggled in through a NORMAL block would settle whether soundness holds.","tokens_in":7854,"feed_emoji":"🔁","tokens_out":7864,"duration_ms":86136,"temperature":0.7,"pith_summary":"ForNo is a small imperative language in which every register holds a stack of natural numbers, every program has a syntax-directed inverse, and iterations are bounded by the length of a stack. The paper proves that ForNo is FPTIME-complete and FPTIME-sound: every polynomial-time function is expressible, and every expressible function runs in polynomial time without any external clock. Its main result combines these facts with reversibility to characterize two-way bijections: a bijection $f$ on strings is two-way (both $f$ and $f^{-1}$ are computable in polynomial time, with polynomially related input and output lengths) if and only if ForNo computes $f$ with zero garbage, meaning the only nonempty register left at the end is the output register. The point is to locate a structural boundary around feasible invertibility, in the region where one-way functions cannot exist.","feed_headline":"Reversible stack language characterizes two-way bijections","feed_subtitle":"A zero-garbage reversible program exists for every bijection whose forward and inverse run in polynomial time.","key_machinery":"The object that carries the argument is the ForNo term itself: an imperative, stack-based program with a global error counter that keeps states disjoint, read-only restrictions on registers that lead selections and iterations, and NORMAL blocks that delimit scopes. The compiler from polynomial-time Turing machines to ForNo terms (built by adapting an existing stack-language compiler) gives FPTIME-completeness, while FPTIME-soundness rests on the claim that the same syntactic restrictions make every term 'simple,' so no term's stack lengths can feed back into themselves and grow exponentially. Reversibility is realized by the syntax-directed inverse map, and the garbage-free characterization is assembled by combining these three pieces.","core_discovery":"The central claim is Theorem 4: a bijection $f \\colon \\Sigma^* \\to \\Sigma^*$ is a Two-way bijection if and only if ForNo computes $f$ with zero-garbage. The forward direction says that if ForNo computes $f$ cleanly, then the syntactically defined inverse term computes $f^{-1}$, and FPTIME-soundness puts both in FPTIME; honesty follows from the polynomial bounds on the inverse. The reverse direction starts from any polynomial-time Turing machine for $f$ and for $f^{-1}$, compiles each into ForNo, and then uses the standard reversible-programming construction (run the forward program, copy the output, run its inverse to clear the workspace, and arrange the two directions so the input register is restored) to produce a single ForNo term that computes $f$ with zero garbage.","pith_inferences":["A direct proof that every ForNo term satisfies the simplicity criterion, rather than an appeal to the known stack-language criteria, would make the characterization self-contained and would pin down exactly which syntactic clause blocks exponential growth.","One could test the robustness of the characterization by relaxing the read-only and NORMAL constraints in a controlled way; if some relaxation still keeps FPTIME-soundness, the true culprit of the polynomial bound would be isolated.","The same reversible-programming construction may carry over to other reversible models with syntax-directed inverses, suggesting a general duality between zero-garbage reversible programs and the absence of one-way bijections."],"forward_implications":["Every two-way bijection has a concrete zero-garbage reversible program in ForNo, and every bijection ForNo computes cleanly has a polynomial-time inverse.","ForNo is an implicit characterization of FPTIME: no clock, counter bound, or step-counting is added from outside; syntactic constraints alone keep all runs polynomial.","The zero-garbage reversible functions form a class closed under inversion, and inside that class no bijection can be one-way.","The compiler from Turing machines to ForNo terms supplies a starting point for synthesizing reversible circuits from ordinary polynomial-time algorithms."],"supporting_citations":[{"why":"Supplies the reversible-programming scheme used to run a program, copy the output, and run the inverse to erase garbage.","marker":"[2]"},{"why":"Supports the implicit-computational-complexity viewpoint that syntactic constraints can replace external clocks.","marker":"[3]"},{"why":"Provides the definitions of Honest functions and Two-way bijections that the main theorem uses.","marker":"[5]"},{"why":"Gives the simplicity criterion for loop programs that ForNo borrows to prove polynomial-time soundness.","marker":"[6]"},{"why":"Gives the stack-language framework and the compiler that ForNo adapts for FPTIME-completeness.","marker":"[8]"}],"fun_headline_variants":["Zero-garbage reversible stack language captures two-way bijections","Reversible stack model computes two-way bijections with zero garbage","Clean reversible stack programs exactly characterize two-way bijections","Two-way bijections computed with zero garbage by reversible stack language","Every two-way bijection has a zero-garbage reversible stack program"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole equivalence rests on the still-unproved claim that every ForNo term is 'simple' in the sense used by the cited stack-language criteria; if some valid term could run for super-polynomial time by letting the counter, NORMAL, and ROF interact, Theorem 3 would fail and the characterization would collapse.","fun_headline_variants_meta":{"raw":{"variants":["Zero-garbage reversible stack language captures two-way bijections","Reversible stack model computes two-way bijections with zero garbage","Clean reversible stack programs exactly characterize two-way bijections","Two-way bijections computed with zero garbage by reversible stack language","Every two-way bijection has a zero-garbage reversible stack program"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000687,"raw_usage":{"total_tokens":3002,"prompt_tokens":723,"completion_tokens":2279,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":339,"completion_tokens_details":{"reasoning_tokens":2191}},"tokens_in":339,"tokens_out":2279,"duration_ms":16723,"temperature":1.0,"reasoning_tokens":2191,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:05:12.550590+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct or find a ForNo term that, on inputs of length $n$, takes more than $p(n)$ steps for every polynomial $p$, while still computing a total function; checking whether the forbidden pattern from Eq. (3) can be smuggled in through a NORMAL block would settle whether soundness holds.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the reversible-programming scheme used to run a program, copy the output, and run the inverse to erase garbage."},{"cited_title":"Dal Lago","cited_arxiv_id":null,"evidence_quote":"Supports the implicit-computational-complexity viewpoint that syntactic constraints can replace external clocks."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the definitions of Honest functions and Two-way bijections that the main theorem uses."},{"cited_title":"Kasai and A","cited_arxiv_id":null,"evidence_quote":"Gives the simplicity criterion for loop programs that ForNo borrows to prove polynomial-time soundness."},{"cited_title":"Kristiansen and K.-H","cited_arxiv_id":null,"evidence_quote":"Gives the stack-language framework and the compiler that ForNo adapts for FPTIME-completeness."}],"review_version":1}