Search

We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like Gödel's T with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they all guarantee almost-sure termination. Along the way, we introduce a probabilistic variation of the classic reducibility technique, and we prove that the simplest form of probabilistic choice leaves the expressive power of T essentially unaltered. The paper ends with some observations about the functional expressive power: expectedly, all the considered calculi capture the functions which T itself represents, at least when standard notions of observations are considered. [ABSTRACT FROM AUTHOR]

In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experimental results. As a first step towards our goal, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. The model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem | or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (although possibly incomplete) procedure for approximately computing the termination probability. We have implemented the procedure for order-2 PHORS, and confirmed that the procedure works well through preliminary experiments. [ABSTRACT FROM AUTHOR]

We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique. [ABSTRACT FROM AUTHOR]

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomial overhead in time. Is λ-calculus a reasonable machine? Is there a way to measure the computational complexity of a λ-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based on a standard notion in the theory of λ-calculus: the length of a leftmost-outermost derivation to normal form is an invariant, i.e. reasonable, cost model. Such a theorem cannot be proved by directly relating λ-calculus with Turing machines or random access machines, because of the size-explosion problem: there are terms that in a linear number of steps produce an exponentially large output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modeled after linear logic proof nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that the LSC is invariant with respect to the λ-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the λ-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, called useful. Useful evaluation produces a compact, shared representation of the normal form, by avoiding those steps that only unshare the output without contributing to β-redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reductions and the thorough analysis of their properties. [ABSTRACT FROM AUTHOR]

Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions. [ABSTRACT FROM AUTHOR]

We define realizability semantics for Light Affine Logic ( $\mathsf{LAL}$ ) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of $\mathsf{LAL}$ which is considerably simpler than the standard proof based on proof nets and is entirely semantical in nature. The model construction uses a new instance of a resource monoid; a general method for interpreting systems based on Linear Logic introduced earlier by the authors. [ABSTRACT FROM AUTHOR]

We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proofnet as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the amount of resources needed to compute the normal form. Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic, and light linear logic. [ABSTRACT FROM AUTHOR]

Imposing linearity and ramification constraints allows to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polynomial-time computable functions, as the works by Leivant, Hofmann, and others show. This article shows that fine-tuning these two constraints leads to different expressive strengths, some of them lying well beyond polynomial time. This is done by introducing a new semantics, called algebraic context semantics. The framework stems from Gonthier's original work (itself a model of Girard's geometry of interaction) and turns out to be a versatile and powerful tool for the quantitative analysis of normalization in the lambda calculus with constants and higher-order recursion. [ABSTRACT FROM AUTHOR]

We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families. [ABSTRACT FROM AUTHOR]