The Cook-Levin theorem (the statement that SAT is NP-complete) is a central result in structural complexity theory. What would a proof of the Cook-Levin theorem look like if the reference model of computation were not Turing machines but the lambda-calculus? We will see that exploring the alternative universe of ``structural complexity with lambda-terms instead of Turing machines'' brings up a series of interesting questions, both technical and philosophical. Some of these have satisfactory answers, leading us in particular to a proof of the Cook-Levin theorem using tools of proof-theoretic and semantic origin (linear logic, Scott continuity), but many others are fully open, leaving us wondering about the interactions (or lack thereof) between complexity theory and proof theory/programming languages theory.
Two polynomials f and g are said to be algebraically dependent over a field K if there exists a non-zero bivariate polynomial A with coefficients in K such that A(f,g)=0. If no such polynomial exists, we say that f and g are independent. This is a natural generalization of linear independence to higher degrees. We consider the problem of finding an algorithm to test whether the given set of polynomials are algebraically independent. When the field has characteristic zero, this problem has a randomised polynomial time algorithm using the Jacobian Matrix of the given polynomials. However the criterion fails when the polynomials are taken over the fields of positive characteristic. One can expect that the positive characteristic case also has an efficient algorithm for testing algebraic independence, however, the existing best known upper bound is very far from desired. The talk will cover a result which is an attempt to bridge this gap. We present a new algorithm which is based on a refined generalisation of Jacobian criterion in case of fields of positive characteristic. It also yields a structural result about the algebraically dependent polynomials - approximate functional dependence.
S'il est commun, dans la communauté de réalisabilité, de considérer un type comme l'ensemble de ses preuves, et donc un ensemble de termes, il est aussi commun, dans la communauté des types intersections, de considérer un terme comme l'ensemble de ses comportements possibles, et donc un ensemble de types. Dans cet exposé, je présenterai en détail les types intersections, qui sont moins connus au sein du LAMA. Puis j'essaierai d'expliciter les liens avec la réalisabilité: en quoi il est intéressant de composer les deux, et si l'on peut voir les deux opérations comme duales dans un certain sens. Il ne s'agira pas (ou peu) de travaux personnels, mais d'une présentation générale et transversale du domaine.
Cet exposé considère l'amélioration de Furstenberg du théorème de récurrence de Poincare. Nous commençons avec ce théorème et faisons une connexion avec la théorie d'équirépartition des suites. Les rotations du cercle donnent des exemples élémentaires des suites équiréparties et des systèmes dynamique. En considèrent leur généralisations le théorème de van der Corput joue un rôle central et nous analysons ce théorème et ses conséquences. Le concept d'un ensemble de van der Corput boucle la boucle avec le théorème de Furstenberg-Sárközy.
C'est de travail conjoint avec Robert Tichy de l'Université Technique de Graz.
L'objet de la théorie de Ramsey est l'étude de l'apparition nécessaire de la régularité au sein des structures de grande taille, même lorsque ces dernières sont soumises à des partitions. Par exemple, le théorème de Ramsey affirme que tout graphe infini admet un sous-graphe induit complet (où tous les sommets sont reliés à tous les autres) ou indépendant (où aucun sommet n'est relié à aucun autre). De manière équivalente, pour toute partition finie de l'ensemble des paires de nombres naturels, il existe un ensemble infini de naturels dont les paires sont toutes dans la même partie. Un autre exemple est donné par le théorème de van der Waerden, qui affirme que pour toute partition des entiers naturels en un nombre fini de parties, l'une des parties contient nécessairement des progressions arithmétiques de longueur finie arbitrairement grande (il se peut en revanche qu'aucune des parties ne contienne de progression arithmétique infinie).
Le but de cet exposé sera de présenter dans quelle mesure des résultats de ce type peuvent être obtenus dans des contextes où plus de structure apparaît (espaces vectoriels, espaces métriques, graphes, graphes dirigés, etc), et de montrer comment, à partir des travaux de Kechris, Pestov et Todorcevic de 2005, ces résultats peuvent être utilisés pour démontrer des résultats de dynamique topologique, tels que le théorème suivant, dû à Pestov : Soit G le groupe d'automorphismes des rationnels (vus comme l'unique ordre total dense sans point d'extrémité). Alors, lorsqu'il est équipé de la topologie adéquate, G est extrêmement moyennable, c'est-à-dire que toute action continue de G par homéomorphismes sur un espace compact admet un point fixe.
TBA
Monotonicity is a fundamental notion in mathematics and computation. For usual real-valued functions R → R this simply corresponds to the notion that a function is increasing (or decreasing) in its argument, however this can be parametrised by any partially ordered domain and codomain we wish. In computation we deal with programs that compute Boolean functions, {0,1} → {0,1}. Restricting to increasing functions over this structure can be seen as prohibiting the use of negation in a program; for instance monotone Boolean functions are computed by Boolean circuits without NOT gates. The idea of restricting negation scales to other models of computation, and for some important classes of functions the formulation is naturally robust, not depending on the particular model at hand, e.g. for the polynomial-time functions. Monotone computational problems abound in practice, e.g. sorting a string and detecting cliques in graphs, and 'nonuniform' monotone models of computation, such as monotone circuits, have been fundamental objects of study in computational complexity for decades.
In this talk I will propose a project that develops logical characterisations of monotone complexity classes, via a proof theoretic approach. Namely, the project will identify theories of arithmetic whose formally representable functions coincide with certain monotone classes, and also develop fundamental recursion-theoretic programming languages in which to extract the monotone functions themselves. In particular the project focusses on the role of structural proof theory, i.e. the duplication and erasure of formulae, in controlling monotonicity.
A polyomino P is called 2-convex if for every two cells belonging to P, there exists a monotone path included in P with at most two changes of direction. We present some tomographical properties of 2-convex polyominoes from their horizontal and vertical projections and gives an algorithm that reconstructs them from a given couple of projections. We discuss its complexity.
Balanced words have been studied a lot in the last decades. In particular, Christoffel words that are a special case of finite balanced words. In this talk, I introduce the Balance matrix that studies the balancedness of these words and I define some tools to extend this property by defining a second order of balancedness. I recall some properties about the continued fraction development and the Stern-Brocot tree to prove a recursive formula based on the shape of the path from the root of the Stern-Brocot. Finally, I show that among all infinite paths in the Stern-Brocot tree, the one that converges to φ, the golden ratio, minimizes the growth of the second order balance.
Recurrence relations have been of interest since ancient times. Perhaps the most famous is the Fibonacci numbers, where each additional term in the sequence is obtained as the sum of the previous two. I will show how we can use a graphical language of string diagrams–a “graphical linear algebra”–to reason about recurrence relations, and as a bonus, obtain efficient implementations. This application comes from a general string diagrammatic theory of signal flow graphs–a model of computation originally studied by Claude Shannon in the 1940s–developed in collaboration with Filippo Bonchi and Fabio Zanasi, and published at CONCUR 2014 and PoPL 2015.
Ayant déjà parlé récemment de mes travaux de recherche dans un séminaire de l’équipe de géométrie, je propose, de les représenter en mettant plus l’accent sur mes travaux en complexité arithmétique. La question du temps de calcul nécessaire à l’évaluation des polynômes naturels semble fondamentale. Ainsi, quelle est la meilleure façon de calculer un polynôme f(X_1,…,X_n) à partir des opérations arithmétiques basiques + et *? En fait, certains polynômes sont difficiles à calculer. Par exemple, évaluer le permanent d'une matrice revient à compter le nombre de mariages parfaits dans un graphe. On commencera par une présentation de pistes de recherche actuelles en complexité arithmétique. Puis, on verra comment paralléliser ces calculs de manière efficace. Je présenterai mes derniers résultats : en particulier, je montrerai comment obtenir des bornes inférieures ``presque''-cubiques (et ainsi battre les bornes précédentes quadratiques) sur la taille des circuits arithmétiques de profondeur 3 calculant un polynôme donné. Enfin, je comptais juste montrer comment des conjectures de géométrie algébrique réelle impliquent des bornes inférieures non triviales pour le temps de calcul.
We study a generalization of beta expansion to 2 dimension involving rotation action. Basic questions are its ergodicity and soficness. In particular, sofic cases give rise to a large class of self-similar polygonal tilings, having 2n-th fold (diffractive) symmetry for any n. This is a joint work with Jonathan Caalim.
Je présenterai une nouvelle sémantique de réalisabilité du lambda-mu-calcul simplement typé et je montrerai un résultat de correction pour la valider. Je donnerai ensuite un modèle particulier de ce calcul qui permettra de prouver la complétude. Je finirai par quelques conséquences de ce résultat ainsi que quelques questions ouvertes.
We revisit coinductive proof principles from a lattice theoretic point of view. By associating to any monotone function a function which we call the companion, we give a new presentation of both Knaster-Tarski's seminal result, and of the more recent theory of enhancements of the coinductive proof method (up-to techniques). The resulting theory encompasses parametrised coinduction, as recently proposed by Hur et al., and second-order reasoning, i.e., the ability to reason coinductively about the enhancements themselves. It moreover resolves an historical peculiarity about up-to context techniques. Based on these results, we present an open-ended proof system allowing one to perform proofs on-the-fly and to neatly separate inductive and coinductive phases.
On va montrer comment programmer sur des streams avec l'axiome de l'ultrafiltre, qui en quelque sorte correspond à une forme limitée de programmation concurrente pour calculer un stream infini.
A tout mot infini w uniquement ergodique, considéré comme un élément d'un sous-shift, nous associons un nombre réel nu(w) entre 0 et 1 égal à la mesure de l'ensemble des mots inférieurs ou égal à w. Lopez et Narbel ont montré (2016) que si la complexité du mot est assez basse, le décalage de mots correspond à un échange d'intervalles pour ces nombres associés. Nous montrons que si le mot w est un point fixe d'un ``bon'' morphisme, et en particulier d'un morphisme binaire, alors nu(w) et les valeurs de nu pour tous les décalages de w peuvent être trouvés à l'aide d'un morphisme sur les nombres réels.
Une nouvelle définition, implicite, du champ de gradient d'une image discrète est proposée. L'opération de différentiation qui associe une image a son champ de gradient, défini sur une grille deux fois plus fine, est non linéaire, et peut être vue comme l'inverse de l'opération (linéaire) d'intégration. Alors, la variation totale d'une image est simplement la norme l1 de l'amplitude de son champ de gradient. Cette nouvelle définition de la variation totale donne des contours nets et possède de meilleures propriétés d'isotropie que la définition classique.
TBA
I will present an algebraic approach to stochastic graph-rewriting. Rules are seen as particular elements of an algebra of “diagrams”: the diagram algebra D. Diagrams can be thought of as formal computational traces represented in partial time. They can be evaluated to normal diagrams (each corresponding to a rule) and generate an associative unital non-commutative algebra of rules: the rule algebra R. Evaluation becomes a morphism of unital associative algebras which maps general diagrams in D to normal ones in R. In this algebraic reformulation, usual distinctions between graph observables (real-valued maps on the set of graphs defined by counting subgraphs) and rules disappear. Actual graph-rewriting is recovered as a canonical representation of the rule algebra as linear operators over the vector space generated by (isomorphism classes of) finite graphs. This shift of point of view, away from its canonical representation to the rule algebra itself, has unexpected consequences. We find that natural variants of the evaluation morphism map give rise to concepts of graph transformations hitherto not considered. This is joint work with N. Behr and V. Danos.
Operational Techniques (Kripke Logical Relations and Environmental/Open/Parametric Bisimulations) have matured enough to become now formidable tools to prove contextual equivalence of effectful higher-order programs. However, it is not yet possible to automate such proofs -- the problem being of course in general undecidable. In this talks, we will see how to take the best of these techniques to design an automatic procedure which is able many non-trivial examples of equivalence, including most of the examples from the literature. The talk will describe the main ingredients of this method: - Symbolic reduction to evaluate of programs, - Transition systems of heap invariants, as used with Kripke Logical Relations, - Temporal logic to abstract over the control flow between the program and its environment, - Circular proofs to automate the reasoning over guarded recursive predicates.