💻 computer science

On the Termination Problem for Probabilistic Higher-Order Recursive Programs

This paper introduces Probabilistic Higher-Order Recursion Schemes (PHORS) as a model for probabilistic higher-order programs, proves that almost sure termination is undecidable for order-2 PHORS, and proposes a sound, fixpoint-based procedure for approximately computing termination probabilities that is validated through preliminary experiments.

Original authors: Naoki Kobayashi, Ugo Dal Lago, Charles Grellois

Published 2026-08-20

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Naoki Kobayashi, Ugo Dal Lago, Charles Grellois

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

In the vast landscape of computer science, there is a long-standing tradition of using mathematics to predict how a program will behave. For decades, researchers have been able to verify the safety and reliability of software by treating it as a system of states, much like a map of a city where one can trace every possible route a traveler might take. This approach works exceptionally well for programs that follow a fixed set of rules. However, the modern world of computing has moved beyond simple, linear instructions. Today's software often relies on higher-order functions, where code can treat other pieces of code as data, passing them around and modifying them dynamically. Simultaneously, the digital world is increasingly probabilistic, filled with systems that make random choices, such as a coin flip determining the next step in a process. When these two complex worlds collide—programs that can manipulate other programs while making random decisions—the old tools for verification begin to fail. The question arises: can we still predict if such a sophisticated, randomizing program will eventually stop running, or will it get stuck in an endless loop?

A team of researchers from the University of Tokyo, the University of Bologna, and Aix Marseille University has taken a significant step toward answering this question. They introduced a new mathematical model called PHORS, which stands for Probabilistic Higher-Order Recursion Schemes. Think of this model as a way to describe complex, self-referential computer programs that also flip coins to decide their next move. The researchers wanted to know if they could calculate the exact probability that such a program would terminate, or finish its task, rather than running forever. Their investigation led to a surprising and definitive discovery: for programs of a certain complexity, it is mathematically impossible to determine with certainty whether they will almost always stop. In technical terms, they proved that the problem of deciding if a second-order probabilistic program terminates with a probability of one is undecidable. This means no computer algorithm, no matter how powerful, can be built to solve this specific question for all such programs.

This finding is a stark contrast to simpler versions of these problems. For programs that do not use higher-order functions, or for those that are less complex, mathematicians have long known how to calculate these probabilities. The researchers showed that the moment you add a specific layer of complexity—allowing functions to be passed as arguments to other functions while also introducing randomness—the problem jumps from being solvable to being fundamentally unsolvable. They demonstrated this by linking the behavior of these programs to a famous, unsolved mathematical puzzle involving whole numbers and equations. Because that mathematical puzzle cannot be solved by a general algorithm, neither can the question of whether these complex programs will stop. This result implies that we cannot hope to create a tool that gives a precise, exact answer for every possible case.

However, the story does not end in impossibility. While the researchers proved that a perfect, universal solution is out of reach, they also developed a practical method to get very close to the answer. They devised a way to characterize the termination probability using a system of equations that describe how the program's behavior changes at each step. Using this framework, they created a procedure that can calculate a lower bound and an upper bound for the probability of termination. In simpler terms, they built a method that can say, "The program will stop at least this often, and no more than that often." By refining their calculations, they can narrow the gap between these two numbers, providing a highly accurate estimate. They tested this method on several examples, including programs that generate random lists or trees, and found that it worked well, often providing precise estimates for small but non-trivial cases.

The researchers also explored the limits of their own method. They found that while they could easily calculate the minimum probability that a program stops, calculating the maximum probability with arbitrary precision is much harder. In some specific, artificial scenarios, their method struggled to converge on a precise number, suggesting that while their approach is sound and useful, it is not a complete solution for every possible scenario. Nevertheless, their work provides the first theoretical foundation and a working tool for analyzing these complex systems. They have shown that while we cannot always know the exact fate of a probabilistic, higher-order program, we can now reliably estimate its chances of finishing its job. This opens the door to verifying the reliability of modern software that relies on both complex function manipulation and randomization, ensuring that even in a world of uncertainty, we can still understand the likelihood of a system coming to a successful conclusion.

Technical Summary: On the Termination Problem for Probabilistic Higher-Order Recursive Programs

Problem Statement
This paper addresses the model checking problem for probabilistic higher-order programs, specifically focusing on the computation of termination probabilities. While significant progress has been made in model checking for probabilistic finite-state systems and non-probabilistic higher-order programs (via Higher-Order Recursion Schemes, or HORS), the intersection of these two domains remains largely unexplored. The authors investigate the Probabilistic Higher-Order Recursion Scheme (PHORS), a model extending HORS with discrete probabilistic choices. The central problem is determining the probability that a given PHORS terminates (reaches the unit value $e$ ) versus diverges (reaches $\Omega$ ). Specifically, the paper examines the decidability of "almost sure termination" (termination with probability 1) and the feasibility of computing exact or approximate termination probabilities.

Methodology
The authors employ a combination of theoretical reductions, fixpoint characterizations, and abstract interpretation techniques:

Formal Model (PHORS): The paper defines PHORS as a triple $(N, R, S)$ where non-terminals map to types, and rules involve probabilistic choices ( $t_L \oplus_p t_R$ ). The operational semantics define a rewriting relation where probabilities accumulate along reduction paths.
Undecidability Proof: To establish the limits of decidability, the authors reduce the problem to Hilbert's 10th problem (the unsolvability of Diophantine equations). They construct an order-2 PHORS that simulates the evaluation of polynomials with non-negative integer coefficients. By encoding the condition $P(\vec{x}) < Q(\vec{x})$ into the termination behavior of the scheme, they demonstrate that deciding if the termination probability is 1 is undecidable for order-2 PHORS.
Fixpoint Characterization:
- Order- $n$ Characterization: The authors first establish a direct translation of an order- $n$ PHORS into a system of order- $n$ fixpoint equations over real numbers $[0, 1]$ .
- Order- $(n-1)$ Characterization: A more refined translation is presented, reducing the order of the fixpoint equations to $n-1$ . This generalizes the known characterization of Recursive Markov Chains (order-1 PHORS) as polynomial equations. The translation maps a PHORS rule to a tuple of functions representing the probability of reaching specific "targets" (arguments or fresh variables).
Approximation Algorithms:
- Lower Bounds: The least solution of the fixpoint equations provides a semi-decidable procedure for computing lower bounds via Kleene iteration.
- Upper Bounds: For order-2 PHORS (yielding order-1 equations), the authors propose a sound procedure for computing upper bounds using a discretization method inspired by the Finite Element Method (FEM). This involves abstracting functions over $[0, 1]$ using piecewise linear functions on a discrete grid. The method leverages the pointwise convexity of the least solution to ensure soundness. The algorithm iteratively refines upper bounds on a finite domain, handling constraints where the sum of probabilities in specific groups must remain within $[0, 1]$ .

Key Contributions and Results

Undecidability of Almost Sure Termination: The paper proves that the almost sure termination problem for order-2 PHORS is undecidable (specifically $\Pi^0_1$ -hard). This contrasts with Recursive Markov Chains (order-1), where the problem is decidable in PSPACE. Consequently, computing the exact termination probability for order-2 PHORS is not recursively enumerable for any rational threshold $r \in (0, 1]$ .
Fixpoint Characterization: The authors provide a rigorous fixpoint characterization of termination probabilities. For order- $n$ PHORS, the probability is the least solution of order- $(n-1)$ fixpoint equations over real-valued functions. This yields a semi-algorithm for the lower-bound problem ($Pr(G) > r$).
Sound Upper-Bound Procedure: A practical, sound (though potentially incomplete) procedure is developed for computing upper bounds on the termination probability of order-2 PHORS. This method uses discretization and piecewise linear interpolation to over-approximate the least fixpoint.
Experimental Validation: A prototype tool was implemented to compute lower and upper bounds for order-2 PHORS. Preliminary experiments on non-trivial examples (including list generators, tree generators, and randomized algorithms) show that the procedure can compute termination probabilities with high precision (e.g., $10^{-2}$ ) and often converges quickly. The experiments highlight that piecewise linear functions offer significantly better precision and completeness compared to step functions.

Significance and Claims
The paper claims to initiate the theoretical study of probabilistic higher-order model checking. Its primary significance lies in:

Defining the Boundary: Establishing that while order-1 probabilistic higher-order programs (equivalent to Recursive Markov Chains) are decidable, the addition of a single order of higher-order functions (order-2) renders almost sure termination undecidable.
Bridging Theory and Practice: Providing the first theoretical framework (fixpoint equations) and a practical algorithm (discretization) to approximate termination probabilities, which are key to verifying safety and liveness properties in probabilistic higher-order programs.
Open Problems: The authors modestly note that while lower bounds are semi-decidable and upper bounds can be computed for order-2, the existence of an algorithm to compute termination probabilities with arbitrary precision for general order-2 PHORS remains an open question. They also leave the generalization of the upper-bound procedure to arbitrary orders as future work.

The paper concludes that while exact verification is impossible for order-2 and above, the proposed fixpoint-based approximation methods offer a viable path for analyzing probabilistic higher-order programs in practice.

More like this