On Higher-Order Probabilistic Subrecursion

We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like G\"odel's $\mathbb{T}$ with various forms of probabilistic choice operators may result in calculi which are not equivalen...

Full description

Bibliographic Details
Main Authors: Flavien Breuvart, Ugo Dal Lago, Agathe Herrou
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2021-12-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/4226/pdf
Description
Summary:We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like G\"odel'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.
ISSN:1860-5974