REVIEW 4 major objections 5 minor 9 references
Towards a Characterization of Two-way Bijections in a Reversible Computational Model
T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read Zero-garbage ForNo programs compute exactly the two-way bijections.
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (4)
- [Section 4, Theorem 3] 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 2, Fig. 1] 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 5, Theorem 4 proof] 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 3, The compiler J·K] 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.
minor comments (5)
- [Abstract] 'Two-way bijectionsboth' should read 'Two-way bijections both'.
- [Section 2, grammar] 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 3, Listing 5] The listing heading says REMOVE−BLANK while the text says REMOVE−BLANKS; the notation should be consistent.
- [Section 5, proof of Theorem 4] 'both τ and ω are sound state' should be 'sound states'.
- [Section 2, Fig. 1] The auxiliary judgment H s, L; ωI ⇓ ω′ is used before its components are explained; a one-sentence gloss would improve readability.
Circularity Check
No circularity: the main theorem rests on external soundness criteria and a separately proved compiler; the only notable weakness is an unproved soundness assertion, which is a proof gap, not a circular step.
full rationale
The derivation chain in Theorem 4 is not circular. The 'if' direction uses Theorem 3 (FPTIME-soundness) to conclude that a zero-garbage ForNo computation puts both f and f^-1 in FPTIME. Theorem 3 is not proved in the paper; instead Section 4 states that ForNo meets two criteria from [6,8] and that the NORMAL restrictions make all terms 'simple'. This is reliance on external prior work, not a self-citation and not an input that is renamed as a prediction. The external criteria are about simple loop programs and stack languages, not about Two-way bijections or zero-garbage, so the conclusion is not equivalent to the premise by construction. The 'only if' direction uses Corollary 1, which is proved by an explicit compiler from polynomial-time Turing machines (Theorems 1 and 2), plus the standard Bennett trick; neither step presupposes the theorem being proved. No fitted parameters, predicted quantities, or self-referential definitions occur. The most serious concern is that Theorem 3's soundness argument is only summarized and cited, leaving a possible verification gap; but that is a correctness or completeness-of-proof issue, not circularity. Accordingly, no circular step is identified and the score is 0.
Assumptions & free parameters
assumptions (5)
- domain assumption The criteria of Kasai-Adachi [6] and Kristiansen-Niggl [8] for polynomial-time stack languages apply to ForNo exactly as stated.
- ad hoc to paper The omitted macros EMPTY and TO exist within ForNo and have the behaviors described in the text.
- ad hoc to paper The push and pop operations pushn and popn are total functions on S×N satisfying the inversion identity popn(pushn(s,c))=(s,c).
- domain assumption The Bennett trick and the COPY macro are valid in ForNo under the declared NORMAL restrictions.
- standard math FPTIME functions are exactly those computed by polynomial-time Turing machines with the stated tape conventions and output length bound.
invented entities (1)
-
Error counter c
Cite this review
Pith. "Pith review of Towards a Characterization of Two-way Bijections in a Reversible Computational Model." pith.science (2026). https://pith.science/paper/ED7BVLWJ
@misc{pith2026250603382,
author = {Pith},
title = {Pith review of: Towards a Characterization of Two-way Bijections in a Reversible Computational Model},
year = {2026},
howpublished = {\url{https://pith.science/paper/ED7BVLWJ}},
note = {Machine review of arXiv:2506.03382}
}
read the original abstract
We introduce an imperative, stack-based, and reversible computational model that characterizes Two-way Bijections both implicitly, concerning their computational complexity, and with zero-garbage.
Figures
Reference graph
Works this paper leans on
-
[1]
Computational complexity: A modern approach
Sanjeev Arora and Boaz Barak. Computational complexity: A modern approach. Cambridge University Press, page Chapter 6, 2009
work page 2009
-
[2]
H. B. Axelsen and R. Gl¨ uck. What Do Reversible Programs Compute? In Foundations of Software Science and Computation Structure , 2011
work page 2011
- [3]
-
[4]
Foundations of cryptography: Volume 2, basic applications
Oded Goldreich. Foundations of cryptography: Volume 2, basic applications. Cambridge University Press, page Chapter 2, 2008
work page 2008
-
[5]
L. A. Hemaspaandra and M. Ogihara. The Complexity Theory Companion . Texts in Theo- retical Computer Science. An EATCS Series. Springer, 2002
work page 2002
-
[6]
T. Kasai and A. Adachi. A Characterization of Time Complexity by Simple Loop Programs. J. Comput. Syst. Sci. , 20(1):1–17, 1980
work page 1980
-
[7]
L. Kristiansen. Reversible Computing and Implicit Computational Complexity. Sci. Comput. Program., 213:102723, 2022
work page 2022
-
[8]
L. Kristiansen and K.-H. Niggl. On the Computational Complexity of Imperative Program- ming Languages. Theor. Comput. Sci. , 318:139–161, 2004
work page 2004
Show all 9 references
-
[9]
Matthew J. B. Robshaw. One-way function. In H. C. A. Tilborg and S. Jajodia, editors, Encyclopedia of Cryptography and Security , pages 1731–1732. Springer, 2011. 8
2011
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.