A normal sequence over {0,1} is an infinite sequence for which every word of length k appears with frequency 2^{-k}. Agafonov’s eponymous theorem states that selection by a finite state selector preserves normality, i.e. if α is a normal sequence and A is a finite state selector, then the subsequence A(α) is either finite or a normal sequence. In this work, we address the following question: does this result hold when considering probabilistic selectors? We provide a partial positive answer, in the case where the probabilities involved are rational. More formally, we prove that given a normal sequence α and a rational probabilistic selector P, the selected subsequence P(α) will be a normal sequence with probability 1.

International audience

The author introduced models of linear logic known as ''Interaction Graphs'' which generalise Girard's various geometry of interaction constructions. In this work, we establish how these models essentially rely on a deep connection between zeta functions and the execution of programs, expressed as a cocycle. This is first shown in the simple case of graphs, before begin lifted to dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in Interaction Graphs captures a natural class of sub-Markov processes. We then extend the realisability constructions and the notion of zeta function to provide a realisability model of second-order linear logic over the set of all (discrete-time) sub-Markov processes.

This paper is the fourth of a series exposing a systematic combinatorial approach to Girard's Geometry of Interaction (GoI) program. The GoI program aims at obtaining particular realisability models for linear logic that accounts for the dynamics of cut-elimination. This fourth paper tackles the complex issue of defining exponential connectives in this framework. For that purpose, we use the notion of \emph{graphings}, a generalisation of graphs which was defined in earlier work. We explain how to define a GoI for Elementary Linear Logic (ELL) with second-order quantification, a sub-system of linear logic that captures the class of elementary time computable functions.

We show a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by Jacques Dixmier (Dixmier 1954.Annals of Mathematics59(2) 279–286) and fragments of linear logic. We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction (Girard 2011.Theoretical Computer Science412(20) 1860–1883). The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation. We also unveil the essential role played by MASAs in previous geometry of interaction constructions.

This article exhibits a series of semantic characterisations of sublinear nondeterministic complexity classes. These results fall into the general domain of logic-based approaches to complexity theory and so-called implicit computational complexity ( icc ), i.e., descriptions of complexity classes without reference to specific machine models. In particular, it relates strongly to icc results based on linear logic, since the semantic framework considered stems from work on the latter. Moreover, the obtained characterisations are of a geometric nature: each class is characterised by a specific action of a group by measure-preserving maps.

Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $\pi$-calculus traces in the spirit of string diagrams.

Interaction graphs were introduced as a general, uniform, construction of dynamic models of linear logic, encompassing all Geometry of Interaction (GoI) constructions introduced so far. This series of work was inspired from Girard's hyperfinite GoI, and develops a quantitative approach that should be understood as a dynamic version of weighted relational models. Until now, the interaction graphs framework has been shown to deal with exponentials for the constrained system ELL (Elementary Linear Logic) while keeping its quantitative aspect. Adapting older constructions by Girard, one can clearly define "full" exponentials, but at the cost of these quantitative features. We show here that allowing interpretations of proofs to use continuous (yet finite in a measure-theoretic sense) sets of states, as opposed to earlier Interaction Graphs constructions were these sets of states were discrete (and finite), provides a model for full linear logic with second order quantification.

In a recent paper, Girard (2012) proposed to use his recent construction of a geometry of interaction in the hyperfinite factor (Girard 2011) in an innovative way to characterize complexity classes. We begin by giving a detailed explanation of both the choices and the motivations of Girard's definitions. We then provide a complete proof that the complexity classco-NLcan be characterized using this new approach. We introduce the non-deterministic pointer machine as a technical tool, a concrete model to compute algorithms.

Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.