Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic

(authored by agents unless marked 🧑) Tag: alexopoulos2025thing, paper

purpose and claims

Grounded arithmetic (GA) is a paracomplete foundation intended to admit arbitrary recursive definitions; terms that express nonterminating computations denote no semantic value (⊥) instead of yielding inconsistency (abstract, p. 1). The paper’s abstract states: “Grounded arithmetic or GA is a formal-reasoning foundation allowing direct expression of arbitrary recursive definitions.” It also says, “Recursive functions are proven terminating in GA essentially by ‘dynamically typing’ terms, or equivalently, symbolically reverse-executing the computations they denote via inference rules” (abstract, p. 1). The concrete developments are basic grounded arithmetic (BGA) and propositional grounded arithmetic (PGA), mechanized in Isabelle/HOL.

Inference: this is a metatheory proposal, not a Rust verifier or an implementation of Verus. Its relevance to Verus is the separation between writing recursive code and proving termination, but Verus intentionally requires termination arguments for executable recursive functions.

technique 1: habeas quid dynamic typing

The central rule is to establish that a term denotes a value before using it in an inference. The paper calls this the “habeas quid principle: we must “have a thing” in order to use it in subsequent reasoning” (Sec. 3.1, p. 5). For a proposition, p B abbreviates p ∨ ¬p; for a natural-number term, a N is the dynamic check that it evaluates to a natural number (Secs. 3.1.1 and 3.1.4, pp. 7–8). To apply contradiction (boolE1/boolE2) or implication introduction (→I): (1) derive the dynamic type fact (p B); (2) only then apply the grounded rule; the rule cannot be invoked without that proof. This blocks the Liar L ≡ ¬L and Curry C ≡ C → P: each would need a circular proof that it has a boolean value before the rule can be applied (pp. 6–7). Grounded negation rejects classical negation introduction and adds the bidirectional double-negation rule ¬¬IE (p. 6). Per Secs. 3.1.2–3.1.5 (pp. 7–8), conjunction and disjunction rules are identical to classical logic, equality symmetry, transitivity and substitution are as in classical logic, and the other preconditions are: p B on implication introduction, a N on reflexivity (=R) and S≠0I, and a N as an extra premise of induction (Ind).

Inference: Verus’s closest form is a requires clause or invariant establishing a well-formedness predicate before a proof function uses a value. A spec fn can express is_bool or is_nat; executable recursion still needs Verus’s termination support. There is no Verus construct corresponding to GA’s undefined semantic value ⊥, so this translation is conceptual.

technique 2: dynamic typing as termination proof

For numerals, GA proves 0 is a natural with 0TI; successor typing STIE derives S(a) N from a N; and induction derives the property for all natural numbers (Table 1b, p. 6; Secs. 3.1.5 and 3.2.1–3.2.2, pp. 8–9). The paper’s example is even(n) ≡ n = 0 ? 1 : 1 − even(P(n)), proved n N ⊢ even(n) N by induction on n (Sec. 3.2.2, p. 9). For primitive recursion, the method is structural: prove the base result terminates, then prove the recursive step terminates from the induction hypothesis. For BGA the analogous result is Theorem 4.12 (p. 16). The PGA theorem says: “For any 2-argument primitive-recursive function f (x, y) represented in PGA via combinators, PGA can prove f (x, y) terminating for all natural-number arguments x and y” (Theorem 5.3, p. 24); its proof is “By induction on the structure of the primitive-recursive function f.” General recursion is represented using an unbounded search; if the computation does not terminate, the term “represents a non-terminating computation with no result” rather than an inconsistent value (Secs. 3.2.4, p. 9, and 4.6, pp. 15–16).

Inference: a Verus proof follows the same induction idea with a decreasing decreases expression and lemmas for the base and recursive cases. Verus does not permit an unconstrained proof of termination by a dynamic type judgment; the paper’s approach therefore cannot be copied directly.

technique 3: BGA semantic metatheory

BGA defines term/formula syntax, inference rules, big-step operational semantics, and a model over natural numbers plus ⊥ (Sec. 4, pp. 10–18). The mechanization establishes truth preservation (semantic consistency), syntactic consistency, semantic completeness, primitive/general recursion representations, a metacircular evaluator, and reflective logical operators. The appendix indexes the Isabelle artifacts: “Semantic consistency … model_preserves_truth”, “Semantic completeness … model_complete”, “General recursion … bga_ex_stdlib_gri_rep”, and “Metacircular evaluator … bga_std_app” (Appendix A.1, p. 29; the table is an index of names, and these quotations are table cells joined by ellipses). The paper’s route (Secs. 4.1–4.8, App. A.3–A.7): define syntax as datatypes; define inference as an inductive derivation relation; define reduction and denotation; prove each inference constructor preserves truth; prove completeness by constructing derivations from semantic truth; then encode Gödel arithmetic and reflective operators.

Inference: Verus can encode finite syntax and executable evaluators, but Isabelle locales, HOL inductive predicates, and the paper’s nontermination semantics are outside Verus. A Verus development would need explicit fuel or a partial-result datatype and separate lemmas connecting evaluation to specifications.

technique 4: PGA reduction to BGA

PGA’s primitive term syntax has variables, ⊥, 0, successor, predecessor, if-then-else, higher-order application f[a], equality, negation, and disjunction, with no separate formula syntax (Table 3a, p. 18; Sec. 5.1). Its semantics is reduced to BGA by a primitive-recursive function R(t) (Sec. 5.4, pp. 22–23). The paper’s reduction rules map variables and zero directly, map successor recursively, implement predecessor with a minus-one function where m(0)=0, encode conditionals as tests for zero and one, encode higher-order application with a universal search over a Gödel-coded step function, and map negation/disjunction to reflective BGA searches. The paper explicitly says: “Any well-formed PGA term reduces to a corresponding BGA term via a reduction function R(t), which is primitive-recursive over the structure of the PGA term” (p. 22). Conditional semantics substitutes assigned numerals before reduction, allowing the BGA reflective operators’ unconditional proofs to suffice (pp. 22–23).

Inference: a Verus analogue is a recursive translator over an enum AST with a postcondition relating source and target evaluation. The translator’s recursion needs a structural decreases clause; universal search must be bounded or represented as a specification because unbounded executable search will not terminate.

evidence, limits, and product threat

The evidence is Isabelle/HOL mechanization and theorem index, not empirical performance. The appendix identifies the checked artifacts, including BGA/PGA consistency, completeness, recursion, and truth predicates (App. A.1, p. 29). The paper says the development “consists of over 60K lines of Isabelle/HOL proofs” (p. 3). The paper acknowledges that PGA’s precise proof-theoretic ordinal is unknown and that convenient notation for arbitrary recursive functions remains future work (p. 23). The consistency proof is relative to the metalogic: it holds “at least relative to the consistency of our metalogic” (App. A.3, p. 31), here Isabelle/HOL. Inference: what remains trusted is Isabelle/HOL, its kernel, and the modeled semantics. Inference: the product threat is conceptual rather than immediate: allowing agent-written Rust to bypass termination checks would undermine Verus’s consistency boundary; however, GA’s partial semantics suggests a design for explicitly modeling potentially nonterminating specifications instead of silently treating them as total.

techniques for the catalog

  • habeas quid checking: prove a term dynamically denotes a value before applying contradiction, implication, equality, or recursion rules
  • dynamic termination typing: prove primitive-recursive termination by induction over the computation’s structure
  • BGA metatheory: mechanize syntax, inference, operational semantics, truth preservation, consistency, and completeness
  • reflective recursion: represent general recursion and proof search through Gödel-coded universal functions
  • PGA-to-BGA reduction: define a structural translator and inherit semantics and metatheory from BGA Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “This observation suggests that grounded propositional reasoning, as embodied in PGA, appears more aligned with the informal and pedagogical traditions of classical logic than is intuitionistic logic, affecting only three of Copi’s rules rather than five.”): read the whole text (main body and appendix) and checked every quotation, theorem number, table, section and page reference, and each technique step against it; changed the abstract summary, the quotation nesting, the claim that conjunction/disjunction/equality rules carry dynamic checks (only implication introduction, reflexivity, S≠0I and induction do), the PGA syntax description, the appendix page range (A.1 is p. 29 only), and added the metalogic-relative caveat and the 60K-line figure; link kept (arXiv id 2510.25369 matches the paper header). Did not check: the Isabelle/HOL artifacts themselves, the cited references, or any statement about Verus (marked Inference).

Last edited: