Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA New Proof Rule for Almost-Sure Termination
218
0
0.0
(
0
)
Added by
Carroll Morgan
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates almost surely. Proving that can be hard, and this paper presents a new method for doing so; it is expressed in a program logic, and so applies directly to source code. The programs may contain both probabilistic- and demonic choice, and the probabilistic choices may depend on the current state. As do other researchers, we use variant functions (a.k.a. super-martingales) that are real-valued and probabilistically might decrease on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.
rate research
Read More
The extension of classical imperative programs with real-valued random variables and random branching gives rise to probabilistic programs. The termination problem is one of the most fundamental liveness properties for such programs. The qualitative (aka almost-sure) termination problem asks whether a given program terminates with probability 1. Ranking functions provide a sound and complete approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via ranking supermartingales (RSMs). RSMs have been extended to lexicographic RSMs to handle programs with involved control-flow structure, as well as for compositional approach. There are two key limitations of the existing RSM-based approaches: First, the lexicographic RSM-based approach requires a strong nonnegativity assumption, which need not always be satisfied. The second key limitation of the existing RSM-based algorithmic approaches is that they rely on pre-computed invariants. The main drawback of relying on pre-computed invariants is the insufficiency-inefficiency trade-off: weak invariants might be insufficient for RSMs to prove termination, while using strong invariants leads to inefficiency in computing them. Our contributions are twofold: First, we show how to relax the strong nonnegativity condition and still provide soundness guarantee for almost-sure termination. Second, we present an incremental approach where the process of computing lexicographic RSMs proceeds by iterative pruning of parts of the program that were already shown to be terminating, in cooperation with a safety prover. In particular, our technique does not rely on strong pre-computed invariants. We present experimental results to show the applicability of our approach to examples of probabilistic programs from the literature.
Extending our own and others earlier approaches to reasoning about termination of probabilistic programs, we propose and prove a new rule for termination with probability one, also known as almost-certain termination. The rule uses both (non-strict) super martingales and guarantees of progress, together, and it seems to cover significant cases that earlier methods do not. In particular, it suffices for termination of the unbounded symmetric random walk in both one- and two dimensions: for the first, we give a proof; for the second, we use a theorem of Foster to argue that a proof exists. Non-determinism (i.e. demonic choice) is supported; but we do currently restrict to discrete distributions.
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase ranking functions, where we will discuss theoretical aspects of such ranking functions for several kinds of program representations; and (2) using control-flow refinement, in particular partial evaluation of Constrained Horn Clauses, to simplify the control-flow allowing, among other things, to prove termination with simpler ranking functions.
We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is $Pi^0_2$-complete. We also provide a compositional representation of our semantics in terms of an intersection type system. In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods. We have constructed prototype implementations of our method of computing lower bounds of termination probability, and AST verification.
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh synthetic take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects. Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs -- simplifying the metatheory of strong sums over the collection of types, for although there can be no relation classifying relations, one easily accommodates a family classifying small families. Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan logical relations as types, iterating our modal account of the phase distinction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
