arxiv: 2604.27986 · v1 · submitted 2026-04-30 · 💻 cs.LO

Recognition: unknown

On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic

Ugo Dal Lago , Guido Fiorillo , Paolo Pistone

Authors on Pith no claims yet

Pith reviewed 2026-05-07 05:59 UTC · model grok-4.3

classification 💻 cs.LO

keywords almost sure terminationprobabilistic programshigher-order recursion schemeslinear logicrelational semanticsgenerating functionsalgebraic functionsdecidability

0 comments

The pith

A type discipline with bounded exponentials makes almost sure termination decidable for a broader class of probabilistic higher-order recursion schemes by reducing it to algebraic generating functions.

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

This paper shows that almost sure termination can be decided for probabilistic higher-order recursion schemes that use a type system with bounded exponentials from linear logic. The approach interprets these programs using the weighted relational model of linear logic to associate generating functions with them. These functions prove to be algebraic, satisfying systems of polynomial equations that can be solved effectively. This extends earlier results limited to affine programs and offers a concrete way to verify termination probabilities. Readers interested in program verification would find this useful because general cases of probabilistic termination are undecidable.

Core claim

By interpreting probabilistic higher-order recursion schemes in the weighted relational model of linear logic, we show that their associated generating functions are algebraic when the schemes are typed with bounded exponentials. This algebraicity allows us to decide whether the probability of termination is one, establishing decidability for a class extending affine PHORS.

What carries the argument

The weighted relational model of linear logic, which interprets programs as generating functions whose algebraicity encodes the decidability of almost sure termination.

If this is right

Almost sure termination becomes decidable for probabilistic higher-order recursion schemes typed with bounded exponentials.
The generating functions satisfy polynomial equations that can be solved algorithmically.
This provides an effective method to check whether the termination probability equals one.
The approach covers programs beyond the affine fragment considered in prior work.

Where Pith is reading between the lines

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

Similar semantic techniques could be used to decide other quantitative properties such as expected runtime.
The algebraicity result might extend to computing exact probabilities rather than just checking equality to one.
This line of work could connect to verification methods for other higher-order probabilistic languages.
Further relaxing the type bounds while preserving algebraicity would enlarge the decidable class.

Load-bearing premise

The weighted relational semantics of linear logic must faithfully capture the actual termination probabilities of the programs, and the algebraicity of the generating functions must hold for all such typed schemes.

What would settle it

A specific probabilistic higher-order recursion scheme typed with bounded exponentials whose associated generating function is transcendental rather than algebraic, or where solving the polynomials gives a termination probability different from the program's true behavior.

Figures

Figures reproduced from arXiv: 2604.27986 by Guido Fiorillo, Paolo Pistone, Ugo Dal Lago.

**Figure 1.** Figure 1: Typing rules of PBHORS<∞. where, as in e.g. [4], we are assuming that ∆ and ∆′ agree on each variable (i.e. they contain the same type bindings but may disagree on the corresponding coefficients). A type judgement is an expression of the form N | ∆ ⊢ t : φ. The typing rules are in view at source ↗

read the original abstract

The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually $\Pi^0_2$-complete. For this reason, a growing literature has explored classes of programs for which this and related problems can be shown (semi-)decidable. In this work we consider the termination problem for the language of Probabilistic Higher-Order Recursion Schemes (PHORS). Using the weighted relational semantics of linear logic, we translate this problem into the computation of suitable generating functions associated with the program interpreted. This way, we establish the decidability of almost sure termination for a class of programs that extends Li et al.'s affine PHORS via a type discipline with bounded exponentials. To achieve this, we show that the generating functions for such programs are always algebraic, that is, solutions of polynomial equations, yielding an effective method to answer the termination problem.

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.

Desk Editor's Note private letter to a colleague

The paper shows decidability of almost-sure termination for bounded-exponential PHORS by proving that their weighted relational interpretations yield algebraic generating functions solvable via polynomial equations.

read the letter

The core result is a decidability procedure for almost-sure termination on an extension of Li et al.'s affine PHORS. By adding bounded exponentials to the type discipline, the authors obtain generating functions that are algebraic, hence roots of polynomial systems that can be solved effectively to check whether the value at 1 equals one. This is a concrete step beyond the affine case, where the same property does not hold in general. The technical work rests on an inductive argument over the bounded !^k rules in the weighted relational model, together with a soundness link back to the operational measure. The stress-test confirms that the induction goes through and that no hidden restriction on recursion schemes is required for the argument to close. That is the part that actually moves the frontier. The limitation is built in: bounded exponentials restrict the programs that can be typed, so the result applies only to this fragment. Within that fragment the reduction to algebraicity appears faithful and non-circular. The paper is aimed at people working on probabilistic higher-order verification and on denotational models for linear logic. It is the kind of targeted, technically grounded advance that merits referee time rather than a desk rejection. I would send it out for review.

Referee Report

1 major / 3 minor

Summary. The manuscript establishes the decidability of almost sure termination for Probabilistic Higher-Order Recursion Schemes (PHORS) typed under a discipline with bounded exponentials. It interprets such programs in the weighted relational model of linear logic, associates them with generating functions, and proves that these functions are algebraic (i.e., satisfy systems of polynomial equations), yielding an effective decision procedure for the termination probability at 1. This extends the affine PHORS fragment of Li et al. while preserving decidability.

Significance. If the central claims hold, the result is significant: it enlarges the class of higher-order probabilistic programs for which AST is decidable, a problem that is undecidable in general and Π⁰₂-complete. The reduction to algebraic generating functions supplies a concrete, effective method rather than a mere existence proof. The manuscript supplies the required inductive argument on types (including the bounded !^k rules) and relates the denotational interpretation to the operational measure, directly addressing the faithfulness assumption. These elements—machine-checkable-style inductive proof and effective algebraicity—strengthen the contribution.

major comments (1)

The inductive argument establishing algebraicity for bounded-exponential types (the load-bearing step that converts the weighted semantics into a solvable polynomial system) is presented, but the construction of the explicit polynomial equations from a given type derivation should be stated as a separate lemma or algorithm to confirm that the procedure remains effective and parameter-free once the type is fixed.

minor comments (3)

The abstract and introduction refer to 'bounded exponentials' without a one-sentence reminder of the typing rules; adding a brief display of the !^k introduction/elimination rules would improve accessibility for readers coming from the affine PHORS literature.
Notation for the weighted relational interpretation of PHORS (e.g., the precise weighting of the linear-logic connectives) is introduced gradually; a small worked example computing the generating function for a two-line recursive scheme would clarify the translation from syntax to algebra.
The comparison with Li et al. is correct in spirit, but a short table or paragraph contrasting the affine restriction with the bounded-exponential extension (in terms of allowed recursion depth or probability distributions) would make the enlargement of the decidable fragment more concrete.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment of our work and for the constructive suggestion regarding the presentation of the algebraicity argument. We address the comment below and will revise the manuscript accordingly.

read point-by-point responses

Referee: The inductive argument establishing algebraicity for bounded-exponential types (the load-bearing step that converts the weighted semantics into a solvable polynomial system) is presented, but the construction of the explicit polynomial equations from a given type derivation should be stated as a separate lemma or algorithm to confirm that the procedure remains effective and parameter-free once the type is fixed.

Authors: We agree that isolating the explicit construction of the polynomial system as a separate lemma will improve clarity and make the effectiveness of the decision procedure more transparent. In the revised version we will introduce a new lemma (Lemma 5.8) that, given any type derivation for a bounded-exponential PHORS, constructs the corresponding finite system of polynomial equations by a direct induction on the derivation. The lemma will state that the resulting system depends only on the type structure, the constants appearing in the program, and the bound k on the exponentials, with no additional parameters. Its proof will be a straightforward structural induction that mirrors the existing algebraicity argument but focuses on the syntactic construction of the equations rather than on the semantic properties. This change does not alter any theorems or proofs but renders the effective procedure fully explicit and algorithmic once the type derivation is fixed. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via fresh algebraicity proof

full rationale

The manuscript translates the AST problem for bounded-exponential PHORS into generating-function algebraicity using the weighted relational model of linear logic. It supplies an inductive argument over types (including the new bounded !^k rules) establishing that the resulting functions satisfy polynomial equations, then shows these equations are effectively solvable for the value at 1. This algebraicity property is proven directly in the paper rather than obtained by re-expressing a fitted parameter or by a load-bearing self-citation chain. Soundness is established by relating the denotational interpretation to the operational measure via the standard weighting, without reducing the target decidability claim to a definition or prior result internal to the present work. The extension beyond Li et al. is handled by the bounded-exponential discipline, which is independently verified.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the correctness of the weighted relational semantics as a model of PHORS termination and on the claim that bounded exponentials force the generating functions to be algebraic. No numerical free parameters are introduced. The semantics itself is imported from prior linear-logic literature rather than postulated ad hoc.

axioms (2)

domain assumption The weighted relational model of linear logic correctly interprets the termination behavior of probabilistic higher-order recursion schemes.
This is the semantic foundation used to translate the termination problem into generating functions.
ad hoc to paper Programs typed with bounded exponentials produce generating functions that are algebraic (solutions of polynomial equations).
This is the key technical property proved in the paper and is not a standard background fact.

pith-pipeline@v0.9.0 · 5454 in / 1493 out tokens · 54413 ms · 2026-05-07T05:59:58.993100+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

5 extracted references · 2 canonical work pages

[1]

118–161, 1963

URL: https://www.sciencedirect.com/science/article/pii/S0049237X08720238, doi:10.1016/S0049-237X(08)72023-8. 12 D.V Chudnovsky and G.V Chudnovsky. On expansion of algebraic functions in power and puiseux series, i.Journal of Complexity, 2(4):271–294, 1986. URL: https://www.sciencedirect.com/science/article/pii/0885064X86900063, doi:10.1016/ 0885-064X(86)9...

work page doi:10.1016/s0049-237x(08)72023-8 1986
[2]

35 Ugo Lago and Martin Hofmann

Springer-Verlag. 35 Ugo Lago and Martin Hofmann. Bounded linear logic, revisited. InProceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA ’09, pages 80–94, Berlin, Heidelberg, 2009. Springer-Verlag.doi:10.1007/978-3-642-02273-9_8. 36 Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relationa...

work page doi:10.1007/978-3-642-02273-9_8 2009
[3]

Moreover, for each f: k ψ∈Com(∆), the total degree ofsσin the variablesxf:kψis at mostk Proof

For eachσ∈Com(JφK), sσ ⏐⏐ JNK+Com(J∆K) ∈R{JNK+ Com(J∆ K)}. Moreover, for each f: k ψ∈Com(∆), the total degree ofsσin the variablesxf:kψis at mostk Proof. By induction on the type derivationN|∆ ⊢t:φ. We immediately see this is true for the axioms. We discuss here the crucial cases: application and abstraction. Application: suppose we know that the thesis i...
[4]

If suppµ̸⊆Com(ψ), then in the product( JuKR)µthere is a factor( JuKR)m with m̸∈Com(ψ); its restriction is then0by inductive hypothesis and so the whole product is0
[5]

Hence, by inductive hypothesis JtKR µ,σ= 0and the product is0 U

If suppµ⊆Com(ψ), then(µ,σ)̸∈Com(!kψ⊸φ). Hence, by inductive hypothesis JtKR µ,σ= 0and the product is0 U. Dal Lago, G. Fiorillo, P. Pistone 31 So we deduce that the restriction ofsσvanishes. Now we prove part (2): letσ∈J!kψ⊸φK. By part (1) of the inductive hypothesis, for allµ suchthat|µ|>kand( JuKR)µ ⏐⏐⏐ JNK+Com(J∆K) ̸= 0wehavethat JtKR µ,σ ⏐⏐⏐ JNK+Com(J∆...