pith. sign in

arxiv: 2507.19176 · v2 · submitted 2025-07-25 · 💻 cs.PL

A Programming Language for Feasible Solutions

Weijun Chen , Yuxi Fu , Huan Long This is my paper

Pith reviewed 2026-05-19 03:17 UTC · model grok-4.3

classification 💻 cs.PL
keywords programming languagepolynomial timestatic type systemfeasible computationprogram verificationimperative programmingcomputational complexity
0
0 comments X

The pith

A programming language ensures every program runs in polynomial time while expressing all such problems.

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

The paper introduces an imperative programming language equipped with a static type system. This system guarantees that every program written in the language completes in polynomial time. The same language remains expressive enough to implement any function computable in polynomial time. A sympathetic reader would care because the design builds efficiency and termination directly into the language rules instead of requiring separate checks after the code is written.

Core claim

All programs definable in the language are guaranteed to run in polynomial time. Conversely, all problems solvable in polynomial time can be solved by some programs of the language.

What carries the argument

The static type system that enforces a polynomial runtime bound on all well-typed programs while still permitting every polynomial-time function to be expressed.

If this is right

  • Program analysis for termination and efficiency is handled automatically by the type system.
  • Verification of feasible computations is streamlined because efficiency is guaranteed by construction.
  • An implemented interpreter shows the language can be used in practice.
  • Programmers can write code while knowing efficiency holds without separate runtime proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This style of language could support tools that verify resource use in safety-critical code.
  • Similar type systems might be developed for other bounds such as space or energy.
  • Known polynomial-time algorithms like sorting could be tested for expressibility to check completeness.
  • The work connects to broader questions of characterizing complexity classes through language design.

Load-bearing premise

The static type system is correctly designed and proven to enforce the polynomial runtime bound for all programs while still allowing every polynomial-time function to be expressed.

What would settle it

Either exhibit a well-typed program that requires super-polynomial time on some input, or exhibit a specific polynomial-time function that cannot be written as a program in the language.

Figures

Figures reproduced from arXiv: 2507.19176 by Huan Long, Weijun Chen, Yuxi Fu.

Figure 1
Figure 1. Figure 1: The syntax of CorePolyC. formally introduces PolyC and establishes its equivalence to CorePolyC in terms of expressive power. Section 5 concludes. 2 Core PolyC Core PolyC (CorePolyC) is a strongly typed programming language. A Core￾PolyC program outputs an integer upon termination. The semantics and the type system guarantee that all well-typed CorePolyC programs terminate. 2.1 Syntax The syntax of CorePol… view at source ↗
Figure 2
Figure 2. Figure 2: Semantics of CorePolyC. during program execution. An environment Σ can be spelt out as [x1 7→ v1][x2 7→ v2] · · · [xm 7→ vm] where dom(Σ) = {x1, . . . , xm}. The empty store environment is denoted by ∅, and Σ[x 7→ v] is an update of Σ defined as follows: ∅(x) = ↑ , Σ[x 7→ v](y) = ( Σ(y) , if y ̸≡ x, v , if y ≡ x, (4) where ↑ indicates undefinedness and ≡ is the syntactic equality. For m-tuples xe and ve, t… view at source ↗
Figure 3
Figure 3. Figure 3: The typing rules of CorePolyC. Example 1 (Fast multiplication) [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Two CorePolyC implementations of fast multiplication. The left one violates the rules Γ−Loop and Γ−Asgmt, while the right one is well-typed. that if the variable x is of type iint, then assignments to it cannot occur within any loop body. The situation with declaration statements is similar. Furthermore, both Γ1, #f ⊢ s1 : Γ1 and Γ ′ 1 , #f ⊢ s1 : Γ ′ 1 hold because ℓ = #f indicates that the current check … view at source ↗
Figure 5
Figure 5. Figure 5: The dependency graph for the proof of Theorem 2. 3 Core PolyC is a Model of FP This section substantiates our claim that CorePolyC captures precisely the poly￾nomial time computability. Unless otherwise stated, all programs will be well￾typed CorePolyC programs. The set of all finite-arity total functions is denoted by F. Given an m-ary program p with input variables xe, for any ve ∈ Z m, we define JpK(ve)… view at source ↗
Figure 6
Figure 6. Figure 6: Examples of the simulation process. The left program simulates the transition δ(q0, 0) = (q1, 1, L), , while the right one simulates the transition δ(q0, 1) = (q3, 0, R). 4. Rightward Movement. The rightward movement is simulated by appending the last digit of x to the end of y. If the head is in the rightmost position, it can still move right. In this case, the head will point to a blank symbol □, so we s… view at source ↗
Figure 7
Figure 7. Figure 7: The cost semantics of CorePolyC. – In the case of Γ−Asgmt, Γ ′ = Γ, so dom I(Γ ′ ) = dom I(Γ) is trivial. We also have that x ̸∈ dom I(Γ) since Asg(#t, Γ(x)). Consequently, (Σ′ )↾Γ′ ∼ (Σ[x 7→ v])↾Γ ∼ (Σ)↾Γ . – In the case of Γ−Seq, the result follows by a simple induction on m. – In the case of Γ−Block, Γ−Loop and Γ−Cond, we have Γ ′ = Γ. Therefore, dom I(Γ ′ ) = dom I(Γ) and (Σ′ )↾Γ′ ∼ (Σ′ )↾Γ . By the in… view at source ↗
Figure 8
Figure 8. Figure 8: An example of transform T1. To be more concise, we will provide proof of the claim later. Consequently, |Jp ′ K(ve)| = |Σ′ (o)| = |E ∅[ ex7→ev ], p ′ | ≥ |E ∅[ ex7→ev ], p | ̸= O(T(n)), which contra￾dicts to the fact that all CorePolyC programs can only produce outputs of size O(T(n)). (3) ⇒ (1). Let p be a program with ic(p, ve) ̸= O(T(n)). Suppose o̸∈ L(p). We construct a new program p ′ as follows: a) I… view at source ↗
Figure 9
Figure 9. Figure 9: An example of transform T2. |Σ′ (o)| = Θ(ic(T2(se), ∅[xe 7→ ve]) = Ω(ic(p ′ , ve)). However, ic(p ′ , ve) ≥ ic(p, ve) ̸= O(T(n)), which implies that |E ∅[ ex7→ev ], p ′ | ≥ |Σ′ | ≥ |Σ′ (o)| ̸= O(T(n)). But (3) states that p ′ can only generate values of size O(T(n)). This is a contradiction. ⊓⊔ Additional Proof Claim. |Σ′ (o)| = |E ∅[ex7→ev], p ′ | ≥ |E ∅[ex7→ev], p |. Proof. It is sufficient to prove that… view at source ↗
read the original abstract

Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are guaranteed by design. This paper introduces a new imperative programming language whose design is grounded in a static type system that ensures the following equivalence property: All definable programs are guaranteed to run in polynomial time; Conversely, all problems solvable in polynomial time can be solved by some programs of the language. The contribution of this work is twofold. On the theoretical side, the foundational equivalence property is established, and the proof of the equivalence theorem is non-trivial. On the practical side, a programming approach is proposed that can streamline program analysis and verification for feasible computations. An interpreter for the language has been implemented, demonstrating the feasibility of the approach in practice.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript introduces a new imperative programming language equipped with a static type system that enforces polynomial runtime for all definable programs. It proves the equivalence that every polynomial-time function is expressible in the language and that no super-polynomial programs can be written, with soundness following from resource-tracking in the types and completeness via explicit constructions encoding arbitrary PTIME algorithms. An interpreter implementation is also provided.

Significance. If the equivalence holds, this supplies a practical framework in which feasibility is guaranteed by design rather than verified post hoc, with direct relevance to program analysis and verification of efficient computations. Credit is due for the explicit constructions demonstrating completeness and the resource-tracking approach to soundness, which together establish both directions without apparent gaps.

minor comments (2)
  1. The abstract asserts a non-trivial proof of equivalence; the main text would benefit from a brief overview paragraph that lists the key lemmas or steps before the detailed argument.
  2. Additional small examples of typed programs and their resource bounds would help readers see how the type system rules are applied in practice.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work on a typed imperative language whose programs exactly capture the polynomial-time computable functions. The recommendation for minor revision is appreciated, and we note the recognition given to both the soundness/completeness proofs and the interpreter implementation.

Circularity Check

0 steps flagged

No significant circularity; equivalence established by independent soundness and completeness arguments

full rationale

The paper defines an imperative language with a static type system whose rules track resource usage to enforce polynomial-time execution. Soundness is shown by induction over the typing derivation, proving that every well-typed program terminates in time bounded by a polynomial in the input size. Completeness is shown by explicit, syntax-directed constructions that embed arbitrary polynomial-time Turing machines or circuits into well-typed programs of the language. Neither direction relies on self-definition, fitted parameters renamed as predictions, or load-bearing self-citations; the proofs are self-contained against the standard definition of PTIME and use only conventional techniques from implicit complexity. The central equivalence therefore stands on its own formal content rather than reducing to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Only the abstract is available, so the ledger is necessarily incomplete. No explicit free parameters or invented entities beyond the language itself are mentioned. The type-system rules are treated as a domain assumption whose correctness is asserted but not shown.

axioms (1)
  • domain assumption The static type system enforces polynomial runtime bounds for every well-typed program.
    This is the central design claim of the language; its validity is required for the equivalence to hold.
invented entities (1)
  • The new imperative programming language with its type system no independent evidence
    purpose: To characterize exactly the polynomial-time computable functions
    The language is introduced by the paper as the vehicle for the equivalence result.

pith-pipeline@v0.9.0 · 5664 in / 1068 out tokens · 55599 ms · 2026-05-19T03:17:26.526573+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    International Journal of Software Engineering & Applications8, 87–100 (2017)

    Ali, N.A.: A survey of verification tools based on hoare logic. International Journal of Software Engineering & Applications8, 87–100 (2017)

    work page 2017

  2. [2]

    MIT press (2008)

    Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)

    work page 2008

  3. [3]

    In: International Conference on Foundations of Software Science and Computation Structures

    Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time com- putation. In: International Conference on Foundations of Software Science and Computation Structures. pp. 27–41. Springer (2004)

    work page 2004

  4. [4]

    In: Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing

    Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the poly- time functions (extended abstract). In: Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing. p. 283–293. STOC ’92, Association for Computing Machinery, New York, NY, USA (1992). https://doi.org/10.1145/ 129712.129740, https://doi.org/10.1145/129712.129740

    work page doi:10.1145/129712.129740 1992

  5. [5]

    Springer Science & Business Me- dia (2013)

    Bertot, Y., Castéran, P.: Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Me- dia (2013)

    work page 2013

  6. [6]

    Princeton University (1985)

    Buss, S.R.: Bounded arithmetic. Princeton University (1985)

    work page 1985

  7. [7]

    In: Structure in Complexity Theory: Proceedings of the Conference held at the Uni- versity of California, Berkeley, California, June 2–5, 1986

    Buss, S.R.: The polynomial hierarchy and intuitionistic bounded arithmetic. In: Structure in Complexity Theory: Proceedings of the Conference held at the Uni- versity of California, Berkeley, California, June 2–5, 1986. pp. 77–103. Springer (1986)

    work page 1986

  8. [8]

    In: Bar-Hillel, Y

    Cobham, A.: The intrinsic computational difficulty of functions. In: Bar-Hillel, Y. (ed.) Logic, methodology and philosophy of science, pp. 24–30. North-Holland Pub. Co. (1965)

    work page 1965

  9. [9]

    In: Proceedings of the twenty-first annual ACM symposium on Theory of computing

    Cook, S., Urquhart, A.: Functional interpretations of feasibly constructive arith- metic. In: Proceedings of the twenty-first annual ACM symposium on Theory of computing. pp. 107–112 (1989)

    work page 1989

  10. [10]

    In: Proceedings of the Seventh Annual ACM Symposium on The- ory of Computing

    Cook, S.A.: Feasibly constructive proofs and the propositional calculus (prelimi- nary version). In: Proceedings of the Seventh Annual ACM Symposium on The- ory of Computing. p. 83–97. STOC ’75, Association for Computing Machin- ery, New York, NY, USA (1975). https://doi.org/10.1145/800116.803756, https: //doi.org/10.1145/800116.803756

    work page doi:10.1145/800116.803756 1975

  11. [11]

    Journal of Symbolic Computation9(3), 251–280 (1990)

    Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. Journal of Symbolic Computation9(3), 251–280 (1990). https://doi.org/https:// doi.org/10.1016/S0747-7171(08)80013-2, https://www.sciencedirect.com/science/ article/pii/S0747717108800132, computational algebraic complexity editorial 28 W. Chen et al

    work page doi:10.1016/s0747-7171(08)80013-2 1990

  12. [12]

    In: Eu- ropean Summer School in Logic, Language and Information

    Dal Lago, U.: A short introduction to implicit computational complexity. In: Eu- ropean Summer School in Logic, Language and Information. pp. 89–109. Springer (2010)

    work page 2010

  13. [13]

    Springer Science & Busi- ness Media (2012)

    Downey, R.G., Fellows, M.R.: Parameterized complexity. Springer Science & Busi- ness Media (2012)

    work page 2012

  14. [14]

    Canadian Journal of mathematics17, 449– 467 (1965)

    Edmonds, J.: Paths, trees, and flowers. Canadian Journal of mathematics17, 449– 467 (1965)

    work page 1965

  15. [15]

    Theoretical computer science50(1), 1–101 (1987)

    Girard, J.Y.: Linear logic. Theoretical computer science50(1), 1–101 (1987)

    work page 1987

  16. [16]

    In: 24th Annual Symposium on Foun- dations of Computer Science (SFCS 1983)

    Gurevich, Y.: Algebras of feasible functions. In: 24th Annual Symposium on Foun- dations of Computer Science (SFCS 1983). pp. 210–214. IEEE (1983)

    work page 1983

  17. [17]

    In: Theoretical Aspects of Computing–ICTAC 2021: 18th International Colloquium, Virtual Event, Nur- Sultan, Kazakhstan, September 8–10, 2021, Proceedings 18

    Hainry, E., Jeandel, E., Péchoux, R., Zeyen, O.: Complexityparser: An automatic tool for certifying poly-time complexity of java programs. In: Theoretical Aspects of Computing–ICTAC 2021: 18th International Colloquium, Virtual Event, Nur- Sultan, Kazakhstan, September 8–10, 2021, Proceedings 18. pp. 357–365. Springer (2021)

    work page 2021

  18. [18]

    In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

    Hainry, E., Kapron, B.M., Marion, J.Y., Péchoux, R.: A tier-based typed pro- gramming language characterizing feasible functionals. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 535–549 (2020)

    work page 2020

  19. [19]

    Proceedings of the ACM on Programming Languages7(POPL), 806–832 (2023)

    Hainry, E., Péchoux, R.: A general noninterference policy for polynomial time. Proceedings of the ACM on Programming Languages7(POPL), 806–832 (2023)

    work page 2023

  20. [20]

    Foundations of Software Science and Computation Struc- tures LNCS 13992 p

    Hainry, E., Péchoux, R., Silva, M.: A programming language characterizing quan- tum polynomial time. Foundations of Software Science and Computation Struc- tures LNCS 13992 p. 156 (2023)

    work page 2023

  21. [21]

    Transactions of the American Mathematical Society117, 285–306 (1965)

    Hartmanis, J., Stearns, R.E.: On the computational complexity of algorithms. Transactions of the American Mathematical Society117, 285–306 (1965)

    work page 1965

  22. [22]

    Theo- retical Computer Science228(1-2), 151–174 (1999)

    Jones, N.D.: Logspace and ptime characterized by programming languages. Theo- retical Computer Science228(1-2), 151–174 (1999)

    work page 1999

  23. [23]

    Inequalities3(3), 159– 175 (1972)

    Klee, V., Minty, G.J.: How good is the simplex algorithm. Inequalities3(3), 159– 175 (1972)

    work page 1972

  24. [24]

    In: European Symposium on Pro- gramming Languages and Systems

    Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination ver- ification for higher-order functional programs. In: European Symposium on Pro- gramming Languages and Systems. pp. 392–411. Springer (2014)

    work page 2014

  25. [25]

    Theoretical computer science 318(1-2), 163–180 (2004)

    Lafont, Y.: Soft linear logic and polynomial time. Theoretical computer science 318(1-2), 163–180 (2004)

    work page 2004

  26. [26]

    In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 81–92 (2001)

    work page 2001

  27. [27]

    In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science

    Marion, J.Y.: A type system for complexity flow analysis. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. pp. 123–132. IEEE (2011)

    work page 2011

  28. [28]

    In: Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28

    Moura, L.d., Ullrich, S.: The lean 4 theorem prover and programming language. In: Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. pp. 625–635. Springer (2021)

    work page 2021

  29. [29]

    Theoretical Com- puter Science 900, 25–34 (2022)

    Oitavem, I.: The polynomial hierarchy of functions and its levels. Theoretical Com- puter Science 900, 25–34 (2022)

    work page 2022

  30. [30]

    Software: Practice and Experience25(7), 789–810 (1995)

    Parr, T.J., Quong, R.W.: Antlr: A predicated-ll (k) parser generator. Software: Practice and Experience25(7), 789–810 (1995)

    work page 1995

  31. [31]

    In: Computer Aided Verification: 32nd International Con- ference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II

    Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2inv: A deep learning framework for program verification. In: Computer Aided Verification: 32nd International Con- ference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II

    work page 2020

  32. [32]

    pp. 151–164. Springer (2020) A Programming Language for Feasible Solutions 29

    work page 2020

  33. [33]

    In: Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing

    Spielman, D., Teng, S.H.: Smoothed analysis of algorithms: why the simplex algo- rithm usually takes polynomial time. In: Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing. p. 296–305. STOC ’01, Association for Computing Machinery, New York, NY, USA (2001). https://doi.org/10.1145/ 380752.380813, https://doi.org/10.1145/380752.380813

    work page doi:10.1145/380752.380813 2001

  34. [34]

    Journal of Computer Security 4 (08 2000)

    Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4 (08 2000). https://doi.org/10.3233/ JCS-1996-42-304 A Missing Proofs of Section 2 A.1 Proof of Lemma 1 Proof. The proof is by structural induction

    work page 2000

  35. [35]

    By the definitions ofJ·K and{|·|}, the followings are valid: –JcK∈B and{|c|}= bool∈Bool whenever c∈{true, false}; –JcK∈Z and{|c|}= iint∈Int whenever c∈D+

    By definition C ={true, false}∪D+. By the definitions ofJ·K and{|·|}, the followings are valid: –JcK∈B and{|c|}= bool∈Bool whenever c∈{true, false}; –JcK∈Z and{|c|}= iint∈Int whenever c∈D+. Therefore JcK and{|c|}are always consistent

    work page

  36. [36]

    Therefore JtK and t are consistent

    T = Bool∪Int, and –JtK = #f∈B whenevert∈Bool; –JtK = 0∈Z whenevert∈Int. Therefore JtK and t are consistent

    work page

  37. [37]

    Since˜t∈dom({|op|}), it can only be the case that˜t = boolm, and thus{|op|}(˜t) = bool

    Assume that op∈{&&, ||, !}. Since˜t∈dom({|op|}), it can only be the case that˜t = boolm, and thus{|op|}(˜t) = bool. Furthermore, as˜v is consistent with˜t, it follows that˜v∈Bm. Regardless of whetherop is &&, ||, or !, it holds that JopK(˜v)∈B. Consequently, JopK(˜v) is consistent with{|op|}(˜t). Similar reasoning can be applied in other cases. ⊓ ⊔ A.2 Pr...

    work page

  38. [38]

    the loop bound in˜s0 is y, and

    work page

  39. [39]

    The notation|˜s|:=∑m i=1|sm|, i.e., the sum of the bit-size of all statement in˜s

    for any storeΣsuch that⟨Σ,˜s⟩⇓Σ′for someΣ′, andt≥t0(|Σ|), one has that⟨Σ[y↦→t],˜s0⟩⇓Σ′[y↦→t]. The notation|˜s|:=∑m i=1|sm|, i.e., the sum of the bit-size of all statement in˜s. Proof. Assume that˜s = (s1,..., sm). We prove by induction onm≥1. Ifm = 1, we prove by induction on the structure of statements

    work page

  40. [40]

    Let ˜s0 := for(i<size(y)) if(i<1) x= e; else break ; and t0 := 1

    Case x=e;. Let ˜s0 := for(i<size(y)) if(i<1) x= e; else break ; and t0 := 1 . Since e does not invoke any function calls,˜s0 and t0 satisfy all the conditions. 40 W. Chen et al

    work page

  41. [41]

    Applying the induction hypothesis, we can obtain ˜s′ 0 and t′

    Case for(j<size(z)) s′. Applying the induction hypothesis, we can obtain ˜s′ 0 and t′

    work page

  42. [42]

    Let˜s0 be the following state- ments

    Assume that ˜s′ 0 =˜s1 for(i<size(y)) s2, (20) where˜s1 corresponds to the declaration stage. Let˜s0 be the following state- ments. 1 ˜s1 2 int i , j ; 3 for (k < size ( y ) ) { 4 if (j < size ( z ) { 5 ˜s2 6 i +=1; 7 if (i >= size ( y ) / size ( z ) ) { i =0; j +=1;} 8 } else break ; 9 } According to Lemma 7,˜s can only produce value bounded by a polynom...

    work page

  43. [43]

    If˜s = (˜s≤m, sm+1), then we first apply the induction hypothesis to obtain ˜s≤m,0, t≤m,˜sm+1,0 and tm+1

    Other cases are trivial. If˜s = (˜s≤m, sm+1), then we first apply the induction hypothesis to obtain ˜s≤m,0, t≤m,˜sm+1,0 and tm+1. Assume that ˜s≤m,0 =˜s≤m,1 for(i<size(y)) s≤m,2, (21) ˜sm+1,0 =˜sm+1,1 for(i<size(y)) sm+1,2, (22) where˜s·,1 corresponds to the declaration stage. Let˜s0 be the following sequence. ˜s≤m,1; ˜sm+1,1 for(i<size(y)) if(i<size(y)/...

    work page