Research

An infinite sequence over a finite alphabet Σ of symbols is called normal iff the limiting frequency of every finite string w exists and equals |Σ|^{|w|}. A celebrated theorem by Agafonov states that a sequence α is normal iff every finite-state selector (i.e., a DFA accepting or rejecting prefixes of α) selects a normal sequence from α.
Let µ : Σ* → [0, 1] be a probability map (e.g. for all integer n, the sum of µ(w) when w ranges over words of length n is equal to 1). We say that an infinite sequence α is is µ-distributed if, for every finite string w, the limiting frequency of w in α exists and equals µ(w). Thus, α is normal if it is µ-distributed for the equidistributed probability map. Unlike normality, µ-distributedness is not preserved by finite-state selectors for all probability maps µ. This raises the question of how to characterize the probability maps µ for which µ-distributedness is preserved across finite-state selection, or equivalently, by selection by programs using constant space.
We prove the following result: for any finite or countably infinite alphabet Σ, every finite-state selector over Σ selects a µ-distributed sequence from every µ-distributed sequence α iff µ is induced by a Bernoulli distribution on Σ, that is a probability distribution on the alphabet extended to words by taking the product. The primary-and remarkable-consequence of our main result is a complete characterization of the set of probability maps, on finite and infinite alphabets, for which Agafonov-type results hold. The main positive takeaway is that (the appropriate generalization of) Agafonov's Theorem holds for Bernoulli distributions (rather than just equidistributions) on both finite and countably infinite alphabets.
As a further consequence, we obtain a result in the area of symbolic dynamical systems: the shift-invariant measures ν on Σ ω such that any finite-state selector preserves the property of genericity for ν, are exactly the positive Bernoulli measures.

We present a new asynchronous model of computation named Stellar Resolution based on first-order unification. This model of computation is obtained as a formalisation of Girard's transcendental syntax programme, sketched in a series of three articles. As such, it is the first step towards a proper formal treatment of Girard's proposal to tackle first-order logic in a proofs-as-program approach. After establishing formal definitions and basic properties of stellar resolution, we explain how it generalises traditional models of computation, such as logic programming and combinatorial models such as Wang tilings. We then explain how it can represent multiplicative proof-structures, their cut-elimination and the correctness criterion of Danos and Regnier. Further use of realisability techniques lead to dynamic semantics for Multiplicative Linear Logic, following previous Geometry of Interaction models.

We give an account of Agafonov’s original proof of his eponymous theorem. The original proof was only reported in Russian in a journal not widely available, and the work most commonly cited in western literature is instead the english translation of a summary version containing no proofs. The account contains some embellishments to Agafonov’s original arguments, made in the interest of clarity, and provides some historical context to Agafonov’s work.

This paper presents a new abstract method for proving lower bounds in computational complexity. Based on the notion of topological entropy for dynamical systems, the method captures four previous lower bounds results from the literature in algebraic complexity. Among these results lies Mulmuley’s proof that “prams without bit operations” do not compute the maxflow problem in polylogarithmic time, which was the best known lower bounds in the quest for a proof that NC≠Ptime. Inspired from a refinement of Steele and Yao’s lower bounds, due to Ben-Or, we strengthen Mulmuley’s result to a larger class of machines, showing that prams over integer do not compute maxflow in polylogarithmic time.

In a series of papers, the author introduced models of linear logic known as "Interaction Graphs". These models generalise Girard's various geometry of interaction constructions, providing a unifying framework for those. In this work, we exhibit how these models can be understood mathematically through a cocycle property satisfied by zeta functions of dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in the models captures a natural class of Markov processes. We further extend previous constructions to provide a model of linear logic as a type system over the set of all (discrete-time, time-independent) sub-Markov processes.

In a recent paper, the author has shown how Interaction Graphs models for linear logic can be used to obtain implicit characterisations of non-deterministic complexity classes. In this paper, we show how this semantic approach to Implicit Complexity Theory (ICC) can be used to characterise deterministic and probabilistic models of computation. In doing so, we obtain correspondences between group actions and both deterministic and probabilistic hierarchies of complexity classes. As a particular case, we provide the first implicit characterisations of the classes PL (unbounded error probabilistic logarithmic space) and PP (unbounded error probabilistic polynomial time).

We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

Finding lower bounds in complexity theory has proven to be an extremely difficult task. In this article, we analyze two proofs of complexity lower bound: Ben-Or's proof of minimal height of algebraic computational trees deciding certain problems and Mulmuley's proof that restricted Parallel Random Access Machines (PRAMs) over integers can not decide Ptime-complete problems efficiently. We present the aforementioned models of computation in a framework inspired by dynamical systems and models of linear logic : graphings.
This interpretation allows to connect the classical proofs to topological entropy, an invariant of these systems; to devise an algebraic formulation of parallelism of computational models; and finally to strengthen Mulmuley's result by separating the geometrical insights of the proof from the ones related to the computation and blending these with Ben-Or's proof. Looking forward, the interpretation of algebraic complexity theory as dynamical system might shed a new light on research programs such as Geometric Complexity Theory.

This paper tackles the complex issue of defining exponential connectives in the Interaction Graphs framework. In order to succeed in this, we use the notion of graphings, a generalization of graphs which was defined in earlier work. We explain how one can define a GoI model 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 introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

This paper 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.

This papers exhibits a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by Jacques Dixmier and fragments of linear logic. We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction which interprets proofs as operators in a von Neumann algebra. The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation.

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.

This paper extends the approach developed in previous papers on Interaction Graphs by considering a generalization of graphs named graphings, which is in some way a geometric realization of a graph. This very general framework leads to a number of new models of multiplicative-additive linear logic which generalize Girard's geometry of interaction models and opens several new lines of research in computational complexity and quantum computation.

In a previous paper, the authors showed how Girard proposal succeeds in obtaining a new characterization of co-NL languages as a set of operators acting on a Hilbert Space. In this paper, we extend this work by showing that it is also possible to define a set of operators characterizing the class L of deterministic logarithmic space languages.

In a previous paper, Girard proposed to use his recent construction of a geometry of interaction in the hyperfinite factor in an innovative way to characterize complexity classes. This work provides a complete proof that the complexity class co-NL can be characterized using this new approach. We introduce as a technical tool the non-deterministic pointer machine, a concrete model to computes algorithms in logarithmic space.

This paper presents a parametrized construction of a Geometry of Interaction model (GoI model) for Multiplicative Additive Linear Logic (MALL). Contrarily to former constructions dealing with additive connectives, we are able to solve here the known issue of obtaining a denotational semantics for MALL by introducing a notion of observational equivalence. This work is shown to generalize all previously considered GoI models and pinpoints an essential property, named the trefoil property, which underlies them.

This paper defines a combinatorial approach to J.-Y. Girard's geometry of interaction in the hyperfinite factor, replacing operator-algebraic notion by usual graph-theoretical notions. In particular, it is shown that the Fuglede-Kadison determinant in the type II$_1$  hyperfinite factor can be computed as a measure of the sets of cycles in a graph.

Several techniques for analysis and transformations are used in compilers. Among them, the peeling of loops for hoisting quasi-invariants can be used to optimize generated code, or simply ease developers’ lives. In this paper, we introduce a new concept of dependency analysis borrowed from the field of Implicit Computational Complexity (ICC), allowing to work with composed statements called “Chunks” to detect more quasi-invariants. Based on an optimization idea given on a WHILE language, we provide a transformation method - reusing ICC concepts and techniques - to compilers. This new analysis computes an invariance degree for each statement or chunks of statements by building a new kind of dependency graph, finds the “maximum” or “worst” dependency graph for loops, and recognizes if an entire block is Quasi-Invariant or not. This block could be an inner loop, and in that case the computational complexity of the overall program can be decreased.
In this paper, we introduce the theory around this concept and present a prototype analysis pass implemented on LLVM. We already implemented a proof of concept on a toy C parser3 analysing and transforming the AST representation. In a very near future, we will implement the corresponding transformation within our prototype LLVM pass and provide benchmarks comparisons.

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.

We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring (whose elements can be understood as logic programs or sets of rewriting rules over first-order terms), a construction stemming from an interactive interpretation of cut-elimination known as the geometry of interaction. More precisely, we restrict this framework to terms (logic programs, rewriting rules) using only unary symbols. We prove it is complete for polynomial time computation using an encoding of pushdown automata. Soundness w.r.t. Ptime is proven thanks to a saturation method close to pushdown systems and memoization. As a direct consequence, we get a Ptime-completeness result for a class of logic programming queries that uses only unary function symbols.

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.

This paper presents an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a synctactic restriction, using an encoding of words that derives from proof theory.

A comparison between intuitionistic realizability à la Kleene and classical realizability à la Krivine is provided. It is shown that while in the former the existence of realizers which are not proofs leads to the realization of non-provable sentences, in the latter the existence of realizers that are not proofs does not create any kind of asymmetry between the set of realized sentences and that of proved ones. The existence of such realizers is needed instead for giving a computational interpretation of classical proofs. In this way classical realizability can be used as a framework for an anti-realist account of classical logic. Moreover, this account is shown to be compatible with a single-agent verificationist position, that is without passing through the standard game-theoretic interpretations involving (at least) two players.

An anti-realist theory of meaning suitable for both logical and proper axioms is investigated. As opposed to other anti-realist accounts, like Dummett-Prawitz verificationism, the standard framework of classical logic is not called into question. In particular, semantical features are not limited solely to inferential ones, but also computational aspects play an essential role in the process of determination of meaning. In order to deal with such computational aspects, a relaxation of syntax is shown to be necessary. This leads to a general kind of proof theory, where the objects of study are not typed objects like deductions, but rather untyped ones, in which formulas have been replaced by geometrical configurations.

Several techniques for analysis and transformations are present and used since the creation of compilers. Among them, the peeling of loops for hoisting quasi-invariants can be used to optimize generated code, or simply ease developers’ lives. In this paper, we introduce a new concept of dependency analysis borrowed from the field of Implicit Computational Complexity (ICC), allowing to work with composed statements called “Chunks” to detect more quasi- invariants. From a proven optimization idea given on a WHILE language, we provide a transformation method - reusing ICC concepts and techniques - to compilers. This new analysis computes an invariance degree for each statement or chunks of statements by building a new kind of dependency graph, finds the “maximum” or “worst” dependency graph for loops, and recognizes if an en- tire block is Quasi-Invariant or not. This block could be an inner loop, and in that case the computational complexity of the overall program can be decreased.
In this paper, we introduce the theory around this concept and present a proof-of-concept tool that we developed: an analysis and a transformation passes on a toy C parser written in Python called “pycparser” implemented by Eli Bendersky1. In the near future, we will implement these techniques on real compilers, as some of our optimisations are visibly better than current optimisations implemented in both GCC and LLVM.

This is a short review (in french) of J.-Y. Girard's book "The blind spot. Lectures on logic" (European Mathematical Society 2011).

Invited Talk at the ANR-DFG Beyond Logic conference.

A one-page popularised account (in French) of the PRAMs lower bounds result in collaboration with Luc Pellissier.

The topic of this paper is the problem of characterizing the meaning of logical constants. Our proposal stands in the line of proof-theoretic semantics, exploiting in an essential way the proofs-as-programs correspondence. We first present the inferentialist position in order to point out some of its problems. Their analysis and solutions are carried out in the light of the Curry-Howard correspondence. It is on this basis that we can formulate a necessary condition for logicality, which naturally emerges from the computational point of view adopted here.

Semantic evaluation has proven to be a valuable tool to prove computational complexity results on monomorphic type systems. Can we apply it in presence of impredicative polymorphism? The linearity and stratification at work in light logics might make it possible.

We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, it stemmed from a first lower bound result for a variant of Parallel Random Access Machines.
We analyse this original proof, together with two other proofs of lower bounds from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that, abstracted to a more general setting that exploits the classic notion of topological entropy, this three proofs share the same structure. This reformulation recentres the proofs around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, the latter stemmed from a first lower bound result for a variant of Parallel Random Access Machines (PRAMs).
We analyse this original proof from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that Mulmuley's method can be abstracted to a more general setting, exploiting the classic notion of topological entropy. This reformulation recentres the proof around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, the latter stemmed from a first lower bound result for a variant of Parallel Random Access Machines (PRAMs).
We analyse this original proof from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that Mulmuley's method can be abstracted to a more general setting, exploiting the classic notion of topological entropy. This reformulation recentres the proof around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

Interaction Graphs models were introduced as a generalisation of Girard's Geometry of Interaction constructions based on the interpretation of proofs as (finite, weigthed) graphs. Recent results use these models to bring into vision a new relation between dynamic and denotational semantics, providing formal grounds to the claim that Interaction Graphs models can be understood as a quantitative generalisation of dynamic semantics.

In a recent paper, we defined a generic construction of models of the exponential-free fragment of Linear Logic (MALL). These models provide a new framework for the study of computational complexity which allows for the use of techniques and invariants form ergodic theory and operator theory.

This paper provides a new characterization of deterministic polynomial time computation via a semiring based on the resolution rule, an algebraic structure originally introduced to build interactive models of linear logic. We study a specific sub-semiring restricted to unary symbols and show it is expressive enough to represent the computation of a type of pushdown automata that are known to correspond to deterministic polynomial time computation. Moreover, we show that acceptance by observations (the counterpart of a program in our construction) based on this sub-semiring can be decided in polynomial time, using an adaptation of the memoization technique to our algebraic context.

The aim of Implicit Computational Complexity is to study algorithmic complexity only in terms of restrictions of languages and computational principles. Based on previous work about realizability models for linear logic, we propose a new approach where we consider semantical restrictions instead of syntactical ones. This leads to a hierarchy of models mirroring subtle distinctions about computational principles. As an illustration of the method, we explain how to obtain characterizations of the set of regular languages and the set of logarithmic space predicates.

In a recent work, Girard proposed a new and innovative approach to computational complexity based on the proofs-as-programs correspondence. The authors recently showed how Girard proposal succeeds in obtaining characterizations of L and co-NL languages as sets of operators in the hyperfinite factor of type II$_{1}$.

We exhibit a new relationship between dynamic and denotational semantics. We first define the categorical outlay needed to define Interaction Graphs models, a generalisation of Girard’s Geometry of Interaction models, which are strongly related to game semantics. We then show how this category is mapped to weighted relational models of linear logic. This brings into vision a new bridge between the dynamic and denotational approaches, and provides formal grounds for considering interaction graphs models as quantitative versions of GoI and game semantics models.

We explain how recent developments in the fields of realizability models for linear logic -- or geometry of interaction -- and implicit computational complexity can lead to a new approach of computational complexity. This semantic-based approach should apply uniformly to various computational paradigms, and enable the use of new mathematical methods and tools to attack problem in computational complexity. This paper provides the background, motivations and perspectives of this complexity-through-realizability theory to be developed, and illustrates it with recent results.