Flavien Breuvart ; Ugo Dal Lago ; Agathe Herrou - On Higher-Order Probabilistic Subrecursion

lmcs:4226 - Logical Methods in Computer Science, December 23, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:25)2021
On Higher-Order Probabilistic SubrecursionArticle

Authors: Flavien Breuvart ; Ugo Dal Lago ORCID; Agathe Herrou

    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 $\mathbb{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 $\mathbb{T}$ essentially unaltered. The paper ends with some observations about the functional expressive power: expectedly, all the considered calculi capture the functions which $\mathbb{T}$ itself represents, at least when standard notions of observations are considered.


    Volume: Volume 17, Issue 4
    Published on: December 23, 2021
    Accepted on: October 14, 2020
    Submitted on: January 22, 2018
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Differential Program Semantics; Funder: European Commission; Code: 818616

    Consultation statistics

    This page has been seen 1015 times.
    This article's PDF has been downloaded 325 times.