{"id":"3a247e9a-54dc-4725-8fe6-221db8ad5d94","arxiv_id":"1908.02078","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A program transformation that abstracts each variable by several type-based size measures, together with a data-flow inference that keeps only the measures that affect resource cost, is formalized and proved sound.","lead":"This paper shows how to automatically pick the right way to measure data sizes when estimating how much time or memory a program will use. It proves the method sound and tests it on benchmarks used by other cost analyzers.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3 overstates completeness: non-recursive types with nullary constructors can be useful but are never inferred, so the relevance-inference guarantee fails as written.","rationale":"The reader's weakest assumption correctly identifies the most load-bearing defect: Theorem 3 is not valid as stated because the inference algorithm ignores non-recursive types in match guards, while Definition 17 defines usefulness without requiring the change to be observable by any typed-norm. The Dir/price example, which appears in the paper itself, makes the mismatch concrete: rtypes(x) is empty under genG, yet varying x between Up and Down changes the trace steps, so the type is useful and should be inferred by Theorem 3. This is a genuine theoretical gap in a central contribution, not a matter of style or related-work disagreement. The concern does not, however, invalidate Theorem 1's soundness of the transformation: abstracting a match guard to top simply makes the abstract program less deterministic, and any concrete trace can still be mimicked, so worst-case upper bounds and best-case lower bounds remain sound. The failure is one of completeness/precision of the relevance inference, which is exactly what contribution (2) promises. The fix is local: either tighten Definition 17 so usefulness is tied to norm-observability, or enrich genG to propagate non-recursive types whose constructors select between branches with different cost behavior. Because the paper already includes the counterexample and the surrounding implementation evidence is otherwise strong, this warrants a conditional acceptance rather than rejection; the reader's CONDITIONAL verdict is therefore unchanged.","tokens_in":45126,"tokens_out":6193,"duration_ms":71666,"concrete_test":"Run the Section 4.1 inference on the paper's own Dir/price example: iterate gen_P to lfp and inspect rtypes_i(x) for the two match rules. Separately instantiate Definition 17 with C0 = <price, match(x,Up) . y:=10, [x|->Up]> and C0' with x|->Down; the trace-step sets differ, proving useful_Dir_i(x). If the implementation reports Dir not in rtypes_i(x), Theorem 3 is falsified. The fix should either restrict Definition 17 so 'useful' requires the type to be observable through some typed-norm (recursive, integer, or annotated non-recursive positions), or extend genG to add non-recursive types when a nullary constructor distinguishes rules with different recursive behavior; then re-run the example to confirm Dir is in rtypes_i(x).","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4.1's genG for match(x,p) adds type_i(x) only when type_i(x) is recursive, and adds only types already in sigma for pattern variables. For data Dir = Up | Down and rules price(x,y) <- match(x,Up), y:=10 / match(x,Down), y:=0, lfp(gen_P) gives rtypes(x)=empty for both rules, since Dir is non-recursive and the patterns have no variables. Yet Definition 17 considers Dir useful for x: varying x between Up and Down changes which program rule fires, hence changes Tr(C0). So useful_Dir_i(x) holds but Dir is not in rtypes_i(x), contradicting Theorem 3. The text's justification ('non-recursive types are ignored because they cannot directly affect the number of recursions') is false for nullary constructors that select base versus recursive branches, and the absence of a norm-observable size change does not make the type non-useful under Definition 17. The cost-transfer soundness of Theorem 1 survives because weaker guards only add abstract traces, but the paper's claimed completeness of relevant typed-norms inference and its 'smallest sets' guarantee do not.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a transformational framework for resource analysis in which programs in a rule-based representation are abstracted to constraint programs using typed-norms. For each variable, the relevant types are inferred by a data-flow analysis, and the abstract program is generated with respect to these types. The authors prove soundness of the transformation (Theorem 1), prove termination and a so-called soundness of the relevant-type inference (Theorems 2 and 3), extend the framework to polymorphic types and context-sensitive norms, and evaluate it in the SACO system against RAML and sized-types benchmarks.","tokens_in":45301,"tokens_out":6213,"duration_ms":63800,"significance":"If the claims held, the paper would make a solid contribution: it provides a clean separation between the size-abstraction phase and the cost solver, formal proofs in Appendix A for the trace-preservation result, and an automatic method for pruning typed-norms that is validated on external benchmarks. The experimental comparison is honest and includes cases where the approach fails, such as hanoi. However, the completeness guarantee for relevant-type inference, which is a central advertised contribution, is not valid as stated: Definition 17 and the inference function genG in Section 4.1 are inconsistent for non-recursive discriminator types. The soundness of Theorem 1 is unaffected, but the 'smallest sets' claim and the inference soundness theorem need repair.","major_comments":[{"comment":"The inference function genG^P_i(match(x,p),sigma) in Figure 6 adds type_i(x) only when type_i(x) is recursive, and the surrounding text states that non-recursive types are ignored because they cannot directly affect the number of recursions. This is false for nullary constructors of non-recursive types. Consider data Dir = Up | Down and rules f(x) <- match(x,Up), base; f(x) <- match(x,Down), f(x). In the first rule, Dir is not recursive and the pattern has no variables, so lfp(gen_P)(1)(x) contains no Dir. Yet varying x from Up to Down changes the set of trace steps, so useful_Dir_1(x) holds by Definition 17. Theorem 3 therefore fails as written. The same issue arises for nonmatch(x,p), whose genG clause also omits type_i(x). The fix is either to restrict Definition 17 to types whose variation is observable by the typed norms, or to extend genG to track non-recursive types that discriminate between rules, and to update Theorem 3 accordingly.","section":"Section 4.1, Definition 17, Theorem 3"},{"comment":"Even if the counterexample above were excluded, the theorem is stronger than what the algorithm can deliver because Definition 17 defines usefulness in terms of arbitrary value variations and trace sets, not in terms of changes in any typed-norm size. A value variation of a type T can change the control flow without changing any ||.||_T or ||.||+_T value, since Up and Down both have size 1. Because the abstraction in Section 3.2 only tracks numeric sizes, a type that is useful under Definition 17 may be invisible to the abstract program. Conversely, the algorithm may also infer types that are not useful under Definition 17, since genG adds every recursive type of x in match guards regardless of whether the procedure is recursive; the text acknowledges this in practice but the formal definition does not. The paper's claim that the inferred sets are the 'smallest sets' of relevant typed-norms that preserve precision is therefore not supported in either direction.","section":"Section 4.2, Definitions 16-17, Theorem 3"}],"minor_comments":[{"comment":"The definition of rule mapping combination contains the typo 'integerdividedom' in two places; it should be set difference.","section":"Definition 15"},{"comment":"Line 32 of Figure 8 writes 'main(<> x <r'>)' using a multiplication symbol instead of the angle-bracket separator used elsewhere; this is a typographical error.","section":"Figure 8"},{"comment":"Theorem 3 is labeled 'Soundness', but it is a completeness statement: it says every useful type is inferred. The authors should rename it to avoid confusion with the soundness of the transformation in Theorem 1.","section":"Section 4.2"},{"comment":"The Dir/Up/Down example already shows that non-recursive discriminator types collapse in the abstraction; this observation should be reconciled with the claims of Section 4, since the mismatch is not merely a proof gap but a substantive overclaim.","section":"Section 3.2, after Example 7"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a strong candidate after revision. The main defect is specific and local to the relevant-type inference completeness statement, while the transformation soundness and the experimental evaluation appear solid. I recommend major revision rather than rejection because the central cost-transfer theorem survives and the completeness issue can be fixed within the manuscript's scope."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper does three things well. First, it gives a clean, formalized transformation from a rule-based representation to an abstract program where each variable is measured by all relevant typed norms, with operational semantics for both sides and a soundness theorem (Theorem 1) that preserves trace steps. That part is careful and convincing. Second, it extends the earlier LOPSTR version with polymorphic types and context-sensitive annotated norms; the extension is straightforward but useful, and the examples show real precision gains. Third, the experimental comparison against RAML and sized types on standard list benchmarks is honest and well done. No parameters are fitted to the outcomes, and the authors report where their own solver fails (e.g., hanoi).\n\nThe soft spot is the relevant-types inference and its claimed soundness. The algorithm in Section 4.1 deliberately ignores non-recursive types in match(x,p) guards. The surrounding text says non-recursive types \"cannot directly affect the number of recursions.\" That is false as stated. A non-recursive type with nullary constructors—like data Dir = Up | Down—can switch between a base rule and a recursive rule without changing any typed-norm size. Under Definition 17 such a type is useful for the matched variable, but genG never puts it in rtypes. So Theorem 3, which promises that every useful type is inferred, is not valid as written. The soundness of the abstraction itself survives—ignoring guards only makes the abstract program less deterministic, and Theorem 1 still holds—but the completeness claim for relevance inference needs either a restricted definition of \"useful\" (e.g., requiring the change to be observable in some typed-norm size) or an extended inference that tracks discriminant constructors even in non-recursive types. This is a fixable gap, but it is load-bearing for the inference contribution.\n\nMinor notes: the paper claims to be the first algorithm for inferring useful typed-norms; that is plausible, but the comparison with the useless-variable elimination of Albert et al. 2008 could be sharper. Also, no code or commit hashes are shipped, though the web interface makes reimplementation feasible.\n\nWho is this for? Researchers in static resource analysis and termination who want a principled way to combine typed norms. The transformation part deserves serious engagement; the relevance inference should be read with the above caveat.\n\nRecommendation: engage with the paper, but require a fix to Theorem 3 before accepting it.","headline":"The program transformation and its soundness theorem are solid, but the paper overstates the completeness of its relevant-types inference: Theorem 3 is not valid as written for non-recursive types whose constructors select different trace branches.","tokens_in":45838,"tokens_out":2402,"would_cite":true,"duration_ms":25650,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that replacing data by typed-norm sizes in a rule-based program preserves the step-by-step shape of every trace, so upper and lower cost bounds computed on the abstract program are automatically valid for the original…","keywords":["resource analysis","typed-norms","data-flow analysis","program transformation","cost analysis","size abstraction","upper bounds","polymorphic types"],"falsifier":"Run the paper's data-flow inference on a program where a nullary constructor of a non-recursive type selects between a terminating base rule and a recursive rule. Definition 17 declares that type useful because replacing the constructor changes the set of trace steps, while Section 4.1's match rule deliberately ignores non-recursive types, so the inference output will omit the type. Observing a concrete trace whose step count changes when only that constructor changes, with no typed-norm size changing, directly falsifies Theorem 3.","tokens_in":44888,"feed_emoji":"⏱️","tokens_out":7679,"duration_ms":77451,"temperature":0.7,"pith_summary":"Resource analyzers need to know how data sizes change as a program runs, and the choice of size measure (norm) determines how precise the inferred cost bounds are. This paper proposes to measure each data value by several typed-norms—norms that count constructors of a specific recursive type inside the value—and to decide automatically which norms are relevant. The method transforms a program, written in a small rule-based form, into an abstract program where every variable is replaced by one integer per relevant norm; the paper proves that this transformation preserves the sequence of evaluation steps, so any upper or lower cost bound obtained on the abstract program is a valid bound on the concrete program. A companion data-flow analysis infers a smallest set of relevant typed-norms by propagating, through guards and calls, the types that can influence whether a recursive step is taken. Experiments on list-manipulation and object-oriented benchmarks show bounds orders of magnitude tighter than term-size norms, at comparable analysis times.","feed_headline":"Typed-norm inference trims resource analysis to useful sizes","feed_subtitle":"A data-flow pre-pass picks only the type-level sizes that affect cost, making abstract bounds sharper and faster to solve.","key_machinery":"The central object is a symbolic typed-norm \\|t\\|_T and its sum variant, which count how many constructors of type T occur inside a term, using max when the term's own type differs. The abstraction function (·)^α rewrites guards and assignments into linear constraints over abstract size variables, and the data-flow functions gen_P, genS, and genG compute which types must be tracked by propagating type relevance through match guards and procedure calls; the least fixed point of gen_P yields the relevant types. What carries the argument is the trace-preservation theorem: the abstract operational semantics mimics every concrete step with identical decorations, so the subsequent cost-relation solver can be treated as a black box.","core_discovery":"The central claim is that typed-norm-based size abstraction can be made both sound and automatic. Given a rule-based program, the transformation replaces each variable x by one abstract integer variable X_T for each relevant type T in the constituent types of x, with equalities such as X_{IntList} = 1 + X'_{IntList} for a match on Cons. The soundness theorem shows that for every concrete trace there is an abstract trace with exactly the same step decorations and consistent size constraints, which transfers worst-case upper bounds and best-case lower bounds from the abstract program back to the original. The second claim is that the relevant typed-norms are computable: a monotone data-flow analysis over rules, guards, and calls reaches a least fixed point, and a soundness result states that every 'useful' type—one whose variation changes the set of trace steps—is included in the inferred relevant types. The paper also extends the framework to polymorphic types by monomorphisation and to context-sensitive norms by annotating non-recursive type occurrences with their positions.","pith_inferences":["Editorial inference: the proof of Theorem 3 appears to overreach—a nullary constructor of a non-recursive type can switch between a base rule and a recursive rule, changing trace steps while leaving every typed-norm size unchanged; restricting 'useful' to recursive and integer types, or counting branch-selecting constructors, would make the theorem valid as stated.","Editorial inference: since the soundness theorem preserves full step sequences, not just total cost, the transformation is also a candidate front-end for amortized analyses, which need per-step potential rather than only aggregate bounds.","Editorial inference: the position annotations for context-sensitive norms are a finite set of paths through a type tree; the same data-flow machinery might infer these paths automatically, making context sensitivity a derived feature rather than an input annotation."],"forward_implications":["Any cost bound proven on the abstract program—upper on worst case or lower on best case—automatically holds for the original program, because every concrete trace has an abstract mirror with the same sequence of steps.","Tracking several typed-norms per value yields materially tighter bounds than a single term-size norm: on list benchmarks the evaluated bounds are often an order of magnitude smaller, while total analysis time stays comparable.","Discarding irrelevant typed-norms before solving does more than save time: by shrinking the number of size variables it can change which ranking functions the solver finds, so the inferred bound can differ and in the experiments is usually smaller.","Because the framework is defined on a rule-based representation, the same transformation applies to functional, imperative, and logic programs; logic programs only need matching to be read as unification.","Polymorphic procedures can be analyzed by instantiating each type variable to a fresh monomorphic type, and context-sensitive norms refine the bound when one non-recursive type appears in several positions of a data structure."],"supporting_citations":[{"why":"Provides the foundational two-phase mechanical program analysis that the abstract-program/cost-relations pipeline is built on.","marker":"(Wegbreit 1975)"},{"why":"Introduces norms as size measures for proving termination; the paper generalizes these to typed-norms.","marker":"(Bossi et al. 1991)"},{"why":"Supplies the notion of typed-norms and their combination in termination analysis, which the abstraction in Section 3 builds on.","marker":"(Bruynooghe et al. 2007)"},{"why":"Shows how type-based norms can be combined for termination, motivating why more than one norm per variable is needed.","marker":"(Genaim et al. 2002)"},{"why":"Removes useless variables in cost analysis; the relevant-type inference of Section 4 extends this idea to typed-norms.","marker":"(Albert et al. 2008)"},{"why":"Supplies the sized-types resource-analysis baseline used for comparison in Section 6.","marker":"(Serrano et al. 2014)"},{"why":"Supplies the type-based amortized analysis baseline used for comparison in Section 6.","marker":"(Hoffmann et al. 2012)"}],"fun_headline_variants":["Data-flow analysis auto-infers typed-norms for resource bounds","Transform programs to abstract sizes for faster resource analysis","Typed-norms inferred automatically sharpen cost bounds","Resource analysis gets a data-flow pre-pass for useful norms","Automatic typed-norm inference makes size bounds tighter"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof that every useful type is inferred assumes that any change in program behavior that alters cost is reflected as a change in the size of some value under a typed-norm; a flag-like constructor that is never counted by a norm would violate this.","fun_headline_variants_meta":{"raw":{"variants":["Data-flow analysis auto-infers typed-norms for resource bounds","Transform programs to abstract sizes for faster resource analysis","Typed-norms inferred automatically sharpen cost bounds","Resource analysis gets a data-flow pre-pass for useful norms","Automatic typed-norm inference makes size bounds tighter"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000223,"raw_usage":{"total_tokens":1459,"prompt_tokens":951,"completion_tokens":508,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":567,"completion_tokens_details":{"reasoning_tokens":431}},"tokens_in":567,"tokens_out":508,"duration_ms":58637,"temperature":1.0,"reasoning_tokens":431,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:55:41.066043+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the paper's data-flow inference on a program where a nullary constructor of a non-recursive type selects between a terminating base rule and a recursive rule. Definition 17 declares that type useful because replacing the constructor changes the set of trace steps, while Section 4.1's match rule deliberately ignores non-recursive types, so the inference output will omit the type. Observing a concrete trace whose step count changes when only that constructor changes, with no typed-norm size changing, directly falsifies Theorem 3.","supporting_citations":[],"review_version":1}