-
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Authors:
Pedro H. Azevedo de Amorim,
Satoshi Kura,
Philip Saville
Abstract:
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.
Extending this pic…
▽ More
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.
Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics.
Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV.
Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata's $\top\top$-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.
△ Less
Submitted 20 May, 2025;
originally announced May 2025.
-
Ranking and Invariants for Lower-Bound Inference in Quantitative Verification of Probabilistic Programs
Authors:
Satoshi Kura,
Hiroshi Unno,
Takeshi Tsukada
Abstract:
Quantitative properties of probabilistic programs are often characterised by the least fixed point of a monotone function $K$. Giving lower bounds of the least fixed point is crucial for quantitative verification. We propose a new method for obtaining lower bounds of the least fixed point. Drawing inspiration from the verification of non-probabilistic programs, we explore the relationship between…
▽ More
Quantitative properties of probabilistic programs are often characterised by the least fixed point of a monotone function $K$. Giving lower bounds of the least fixed point is crucial for quantitative verification. We propose a new method for obtaining lower bounds of the least fixed point. Drawing inspiration from the verification of non-probabilistic programs, we explore the relationship between the uniqueness of fixed points and program termination, and then develop a framework for lower-bound verification. We introduce a generalisation of ranking supermartingales, which serves as witnesses to the uniqueness of fixed points. Our method can be applied to a wide range of quantitative properties, including the weakest preexpectation, expected runtime, and higher moments of runtime. We provide a template-based algorithm for the automated verification of lower bounds. Our implementation demonstrates the effectiveness of the proposed method via an experiment.
△ Less
Submitted 5 April, 2025;
originally announced April 2025.
-
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Authors:
Satoshi Kura,
Hiroshi Unno
Abstract:
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniqu…
▽ More
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniques developed for qualitative verification. In contrast, our approach necessitates only small amounts of modification, facilitating the reuse of existing techniques and implementations. On the theoretical side, we propose a dependent refinement type system for a generalised higher-order fixed point logic (HFL). Combined with continuation-passing style encodings of properties into HFL, our dependent refinement type system enables reasoning about several quantitative properties, including weakest pre-expectations, expected costs, moments of cost, and conditional weakest pre-expectations for higher-order probabilistic programs with continuous distributions and conditioning. The soundness of our approach is proved in a general setting using a framework of categorical semantics so that we don't have to repeat similar proofs for each individual problem. On the empirical side, we implement a type checker for our dependent refinement type system that reduces the problem of type checking to constraint solving. We introduce admissible predicate variables and integrable predicate variables to constrained Horn clauses (CHC) so that we can soundly reason about the least fixed points and samplings from probability distributions. Our implementation demonstrates that existing CHC solvers developed for non-probabilistic programs can be extended to a solver for the extended CHC with only small efforts. We also demonstrate the ability of our type checker to verify various concrete examples.
△ Less
Submitted 3 July, 2024;
originally announced July 2024.
-
Higher-Order Weakest Precondition Transformers via a CPS Transformation
Authors:
Satoshi Kura
Abstract:
Weakest precondition transformers are essential notions for program verification, and various extensions have been studied. However, only a few consider both higher-order languages and syntactic calculation of weakest precondition transformers. In this paper, we consider weakest precondition transformers for a higher-order functional language with computational effects and recursion and show that…
▽ More
Weakest precondition transformers are essential notions for program verification, and various extensions have been studied. However, only a few consider both higher-order languages and syntactic calculation of weakest precondition transformers. In this paper, we consider weakest precondition transformers for a higher-order functional language with computational effects and recursion and show that we can calculate them via a CPS transformation. We prove this in a general framework of categorical semantics. Because of this generality, two existing methods for program verification can be understood as instances of our result. Specifically, we show how to instantiate our result to (1) verification of trace properties by Kobayashi et al. and (2) expected cost analysis by Avanzini et al.
△ Less
Submitted 24 January, 2023;
originally announced January 2023.
-
Decision Tree Learning in CEGIS-Based Termination Analysis
Authors:
Satoshi Kura,
Hiroshi Unno,
Ichiro Hasuo
Abstract:
We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate so…
▽ More
We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects cycles in a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.
△ Less
Submitted 4 July, 2021; v1 submitted 23 April, 2021;
originally announced April 2021.
-
General Semantic Construction of Dependent Refinement Type Systems, Categorically
Authors:
Satoshi Kura
Abstract:
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and poset…
▽ More
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to refinement type systems. We demonstrate the usage of our construction by giving semantics to a refinement type system and proving soundness.
△ Less
Submitted 16 October, 2020;
originally announced October 2020.
-
Graded Algebraic Theories
Authors:
Satoshi Kura
Abstract:
We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and finitary graded monads are equivalent via equivalence of categories, which extends the equivalence for monads. We also give sums and tensor products of graded algebraic theories to combine computational effects as an example…
▽ More
We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and finitary graded monads are equivalent via equivalence of categories, which extends the equivalence for monads. We also give sums and tensor products of graded algebraic theories to combine computational effects as an example of importing techniques based on algebraic theories to graded monads.
△ Less
Submitted 4 March, 2020; v1 submitted 17 February, 2020;
originally announced February 2020.
-
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Authors:
Satoshi Kura,
Natsuki Urabe,
Ichiro Hasuo
Abstract:
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes-such as "the execution takes more than 100 st…
▽ More
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes-such as "the execution takes more than 100 steps with probability at most 1%." To this goal, we devise a theory of supermartingales that overapproximate higher moments of runtime. These higher moments, combined with a suitable concentration inequality, yield useful upper bounds of tail probabilities. Moreover, our vector-valued formulation enables automated template-based synthesis of those supermartingales. Our experiments suggest the method's practical use.
△ Less
Submitted 15 February, 2019; v1 submitted 16 November, 2018;
originally announced November 2018.
