IRIF, PPS team, Université de Paris
Date(s) : 02/02/2017 iCal
11 h 00 min - 12 h 00 min
What become the notions of conﬂuence and convergence when a parallel rewrite system has both a probabilistic choice and the possibility of non-termination? We present a notion of Probabilistic Abstract Rewrite System (PARS) which deals with this issue by recovering a form of “diamond property”.
This result (the focus of the talk) is of interest in its own, but it is also key to introduce a Geometry of Interaction model for higher-order computation which has the ability to model commutative effects in a parallel setting, and to capture in particular quantum and probabilistic effects. The model (also sketched in the talk) comes with a multi-token machine, a proof net system, and a PCF-style language, which are all instances of PARS with a diamond property.
Being based on a rewrite system equipped with a memory, our model has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages. A success of our approach is to give (essentially for free) an adequate model for a fully-ﬂedged quantum programming language in which entanglement, duplication, and recursion are all available.
(Joint work with Ugo Dal Lago, Benoit Valiron, Akira Yoshimizu)
Référence : https://arxiv.org/pdf/1610.09629v2.pdf