The Mocqua team seminar usually takes places on Thursdays at 11:00 at Loria, either in room C005 or B013. For instructions on how to reach the lab, click this link; once you're at the front desk, ask for Guilhem Gamard. Please send questions and requests about the seminar to guilhem point gamard at loria point fr.
The following links point to an automatically-updated agenda of our talks, suitable for your favorite groupware. In the summary below, all dates are YYYY/MM/DD and all times are local to Nancy (UTC+1 in Winter, UTC+2 in Summer).
English is the preferred language for all talks.
2024-05-30, 11:00:00, Room B011
We provide syntax and semantics aimed at a simply-typed calculus based on pattern-matching, developed to represent quantum reversible operations, in the fashion of Sabry, Valiron and Vizzotto. To do so, a syntactic notion of orthogonal decomposition is introduced, and we show that it fits the expectations of the orthonormal basis in Hilbert spaces. A denotational semantics and an equational theory are developed, and we prove that the latter is complete with regard to the former. We later discuss how an improvement of this language is sound to represent the quantum switch. Finally, we open with conjectures on quantum recursion.
2024-04-12, 11:00:00, Room C005
Aperiodic tilesets derived from cut and project tilings
2024-04-09, 11:00:00, Room C005
Gaussian quantum mechanics is an important fragment of infinite-dimensional quantum theory, in particular for quantum optics. Calculations in Gaussian quantum mechanics often make use of an operation known as "infinite-squeezing", an operation whose mathematical description typically rests on shaky ground. Building on the previous talk, I will show how a simple modification to the symplectic ZX-calculus yields both a sound semantics and a complete ZX-calculus for Gaussian quantum mechanics with infinite-squeezing. I will then show how this new graphical language interprets previous graphical notations and languages for infinite-dimensional quantum systems.
2024-04-09, 10:00:00, Room C005
The last decade has seen the emergence of two successful research directions using drawings for reasoning on respectively dataflow in programs and quantum computations, namely Graphical Linear Algebra and ZX calculus. Taking the parallel development of those two diagrammatical approaches seriously leads to a surprising connection between quantum computing and symplectic geometry. In this talk, I will introduce the elementary symplectic notions, present a graphical language between the two research programs and outline what future developments we can expect, the final goal being a new model of quantum computation, possibly ending the reign of Hilbert spaces.
2024-04-04, 13:00:00, Room A008
Predicting the limit dynamics of automata networks (like deciding if a given network has a fixed point) is a hard problem. We would like to improve our understanding of their attractors on specific families of networks, like disjunctive networks. To do so, we decompose networks into modules, which were defined in my PhD thesis; these modules are automata networks with inputs and outputs. In this presentation we will show what has been done so far using this modular approach, including the definition of output functions (a new way of understanding a network's computation) and an equivalence to the fixed points of a family of cellular automata, culminating in the showcase of a interaction digraph transformation method that's in the works, and could help to prove the dynamical equivalence of families of networks through the transformation of their interaction digraphs.
2024-03-28, 11:00:00, Room A008
In this talk we'll prove that donuts and ping-pong balls are not the same thing. Three times. The first time with fundamental sets (a simplified version of fundamental groups of my own design), the second time with homology and the third time with cohomology. The goal is to provide as much intuition as feasible about these notions, so expect few proofs and lots of handwaving.
2024-02-22, 11:00:00, Room A008
Finite automata are one of the most basic models of computation. A sequence (uₙ)n≥0 such that un can be computed by a finite automaton with the base-k representation of n is called k-automatic sequence. On the other hand, cellular automata are dynamical systems defined by a local rule wich acts uniformly and synchronously on the configuration space.
In 2015, Eric Rowland and Reem Yassawi established a surprising close connection between these two objects. They showed that, if q is a power of a prime number, the columns of linear cellular automata are q-automatic sequences and conversly all q-automatic sequences can be realized by some linear cellular automaton with memory. Moreover, they provide a constructive method to generated a given q-automatic sequences by an explicit cellular automaton.
I will start by presenting several constructions of q-automatic sequences by linear cellular automata. Then, I will present constructions of emblematic sequences from combinatorics on words or number theory, using non-linear cellular automata with signals such as Sturmian words with a quadratic slope or the characteristic sequence of the set of integers that are sums of two squares.
2024-02-02, 10:30:00, Room C005
Evaluating and optimizing quantum computation strategies and architectures based on their energy consumption has attracted attention recently. Quantum thermodynamics provides a promising framework to do so as it formulates the fundamental constraints about energy exchanged with quantum systems. In this talk, I will provide some context about quantum thermodynamics and try to give some overview about how it could be used in the context of quantum computation and about the challenges along the way.
2024-01-25, 11:00:00, Room B013
We give complete equational theories for the props of affine Lagrangian and and affine coisotropic relations over arbitrary fields. Over odd prime fields, the prop of affine Lagrangian relations specializes the odd-prime-dimensional stabiliser fragment of ZX-calculus; and extending to affine coisotropic relations adds quantum discarding. Over fields of characteristic 0, these props give semantics for affinely constrained classical mechanical systems. Therefore, this provides a unifying theory for a subset of classical and quantum mechanical circuits. To prove completeness, we introduce a scalable notation for composite system in terms of ``spiders'' decorated by symmetric matrices. In the quantum semantics, this gives an extremely concise description of graph states; and likewise for impedance matrices in classical mechanics.
This is based on joint work with Titouan Carette and Robert I. Booth:
https://arxiv.org/abs/2401.07914
2024-01-18, 11:00:00, Room A006
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, symmetrical pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching. We then derive a full completeness result, stating that any computable, partial injective function is the image of a term in the language.
2024-01-11, 11:00:00, Room B013
Penrose tilings are non-periodic tilings of the plane by two rhombuses up to isometry. Here we study dynamic percolation : a contamination process on Penrose tilings starting from a random initial configuration.
Given a Penrose tiling we put a state 0 or 1 on each tile. On these configurations we run the Boostrap percolation cellular automaton: state 1 is stable and a 0 cell becomes 1 if it has (at least) two 1 neighbors. We say that a configuration percolates when its limit configuration is 1-uniform, i.e., when running the Bootstrap percolation cellular automaton on the configuration, every tile eventually gets contaminated.
Denote B the set of configuration that percolate. We prove that for any Bernoulli measure μ (of positive parameter d) we have μ(B)=1.
In other words, for any positive parameter d, if we pick an initial configuration c at random on a Penrose tiling following a Bernoulli distribution of parameter d the probability that c percolates (every tile eventually gets contaminated) is 1.
2023-12-07, 13:15:00, Room C005
In this talk, I will summarize the results of papers [1] to [4]. In [1], we introduced the logical connective ⊙ ("sup") in Natural Deduction, which corresponds to conjunction but also adds the elimination rule for disjunction with a non-deterministic cut-elimination. Additionally, two proof terms are added: a sum and a scalar product, enabling the direct encoding of quantum algorithms using the "sup" connective to encode the quantum measurement. In [2], we showed that for the fragment without "sup" but with sum and scalar product, using linear types, linearity can be directly expressed in the proof terms: the proof t(u+v) is shown to be equivalent to t(u) + t(v), and the proof t(a∙u) is shown to be equivalent to a∙t(u). Furthermore, we prove that the "sup" connective corresponds to additive conjunction, with an elimination rule corresponding to additive disjunction. In [3], we provide a categorical model for the linear calculus without "sup" in the category SM of semimodules over a fixed commutative semiring. Finally, in [4], we show that the same category allows modelling the "sup" connective, providing an alternative for nondeterministic languages to Moggi's Powerset Monad, in contexts like the SM category where such a monad does not fit.
References: [1] A. Díaz-Caro and G. Dowek. A new connective in Natural Deduction and its application to quantum computing. Theoretical Computer Science 957:113840, 2023. [2] A. Díaz-Caro and G. Dowek. Linear Lambda-Calculus is Linear. (FSCD 2022) - LIPIcs 228:21, 2022. (Journal long version in review: arXiv:2201.11221, 2023). [3] A. Díaz-Caro and O. Malherbe. Semimodules and the (syntactically-)linear lambda calculus. Under review. arXiv:2205.02142, 2022. [4] A. Díaz-Caro and O. Malherbe. Non-determinism in a Linear Logic type discipline: A concrete categorical perspective. Under review. arXiv:2309.04624, 2023.
2023-11-23, 11:00:00, Room C005
In recent work, we have proposed a new approach for proving expectation-based properties of probabilistic programs, combining eHL, a Hoare style logic to reason about expectations, with a “hopping” proof rule incorporating a relational program logic (pRHL to be precise). The logic has recently been added to EasyCrypt, a proof assistant tailored for reasoning about relational properties of probabilistic programs. As one example application, we have formalised the proof of the logarithmic average case search complexity bound for skip lists, a simple but intricate to analyse probabilistic data structure for dicitionaries. Recently, Barbosa et al. employed the logic proving security of Dilithium, a post-quantum signature scheme recently standardized by the NIST (National Institute of Standards and Technology).
In the talk, I will give an overview of the overall approach, the case studies which were central motivations behind the approach, and, if time permits, give a short demo.
2023-10-19, 11:00:00, Room B013
Will the energy demands for large-scale quantum computers prevent their realization, or could they bring an energy advantage before a computational one? Answering this question mandates a synergy of fundamental physics and engineering: the former for the microscopic aspects of computing performance, and the latter for the energy consumption. In this work, we propose a holistic methodology dubbed Metric-Noise-Resource (MNR) able to quantify and optimize all aspects of a full-stack quantum computer, bringing together concepts from quantum physics (e.g., models of noise and quantum equation of motion), quantum information (e.g., type of quantum error correction, implementation of the algorithm at the logical level), and enabling technologies (e.g., cryogenics, control electronics, and wiring). The computer being seen as a unique physical system, our approach allows us to minimize its resource cost, acknowledging the several interdependencies between the different parts of the computer, whether they affect hardware or software.
As a proof of concept, we use MNR to minimize the power consumption of a complete model of fault-tolerant quantum computer. Comparing this with a classical supercomputer performing the same task, we identify a quantum energy advantage in regimes of parameters distinct from the commonly considered quantum computational advantage. This provides a previously overlooked practical argument for building quantum computers. While our illustration uses highly idealized parameters inspired by superconducting qubits with a specific concatenated error correction scheme, our methodology is universal -- it applies to other qubits and error-correcting codes --. It provides experimenters with guidelines to build energy-efficient quantum processors. In some regimes of high energy consumption, it can reduce this consumption by orders of magnitudes. Beyond the sole question of energy, our approach provides a framework for a multidisciplinary team of scientists aiming to establish clear roadmaps to scale up quantum computers. Overall, our multidisciplinary methodology lays the foundations for resource-efficient quantum technologies.
2023-09-22, 10:10:00, Room C005
L’objectif principal de cette thèse est d’examiner le concept de " type calculable " et d’améliorer notre compréhension globale de cette notion, ainsi que de fournir des techniques pour vérifier ou réfuter cette propriété. Un espace métrisable compact est dit de type calculable si pour tout ensemble homéomorphe à cet espace, semi-calculabilité et calculabilité sont équivalentes. Cette étude s’appuie sur les travaux de Miller, qui a démontré que les sphères de dimension finie sont de type calculable, ainsi que sur les travaux d’Iljazović et d’autres auteurs, qui ont étendu cette propriété à divers espaces tels que les variétés compactes.
Pour commencer, nous établissons l’équivalence entre deux définitions distinctes de type calculable présentes dans la littérature, impliquant respectivement des espaces métriques et des espaces de Hausdorff. Nous soutenons que la version relativisée et plus forte du type calculable présente des propriétés plus favorables et se prête bien à l’analyse topologique. Nous obtenons ainsi des caractérisations du " type calculable fort " de nature purement topologiques, et en lien avec la complexité descriptive des invariants topologiques.
Cela nous amène naturellement à notre deuxième objectif, l’étude du pouvoir expressif des invariants topologiques de faible complexité descriptive et de leur capacité à distinguer des espaces différents. Plus précisément, nous étudions deux familles d’invariants topologiques de faible complexité qui capturent l’extensibilité et la trivialité homotopique des fonctions continues. En utilisant ce cadre, nous revisitons les résultats précédents sur le type calculable et découvrons de nouvelles perspectives. Notamment, nous identifions la complexité du problème de séparation des graphes topologiques finis.
Enfin, notre troisième objectif se concentre sur l’application de la théorie de l’homologie à l’étude de ce que nous appelons la " propriété de surjection " , qui caractérise la propriété de type calculable. Par exemple, nous prouvons qu’un complexe simplicial fini est de type calculable (fort) si et seulement si l’étoile de chaque sommet satisfait la propriété de surjection. De plus, la réduction à l’homologie implique que la propriété de type calculable est décidable pour les complexes simpliciaux finis de dimension au plus 4.
2023-06-22, 11:00:00, Room C005
Let s(n) denote the sum of digits in the binary expansion of the integer n. Hare, Laishram and Stoll (2011) studied the number of odd integers such that s(n) = s(n2) = k, for a given positive integer k. The remaining cases that could not be treated by theses authors were k = 9, 10, 11, 14 or 15. In this talk, I will present the results of our article on the cases k = 9, 10 and 11 and the difficulties to settle for the two remaining cases k = 14 and 15. A related problem is to study perfect squares of odd integers with four binary digits. Bennett, Bugeaud and Mignotte (2012) proved that there are only finitely many solutions and conjectured that the set of solutions is composed of 13, 15, 47 and 111. In the same paper, we give an algorithm to find all solutions with fixed sum of digits value, supporting this conjecture, as well as show related results for perfect squares of odd integers with five binary digits. This is joint work with Aloui, Jamet, Kaneko, Kopecki and Stoll.
2023-06-12, 14:00:00, Room C005
The study of pattern-avoiding inversion sequences began in two independent articles by Mansour–Shattuck and Corteel–Martinez–Savage–Weselcouch in 2015 and 2016. Subsequent works (by Lin–Yan, Martinez–Savage, and Mansour–Yildirim among others) left their enumeration open for only one single pattern, and 23 pairs of patterns of length 3. We solve all of those remaining cases by finding recurrence formulas (as well as a few closed formulas), using four different decompositions of pattern-avoiding inversion sequences. These formulas allow us to compute between 100 and 350 terms of each enumeration sequence in one minute, using C++ programs running on a personal computer.
2023-05-11, 10:00:00, Room B011
The classical computational complexity of counting on the one hand and quantum computing on the other hand at first glance seem disconnected. Yet techniques from quantum computing, particularly from graphical languages, are very useful in reasoning about counting complexity. In this talk, I will discuss both existing results and some ongoing work that connects a classical family of counting problems called holant to quantum computing.
2023-03-09, 11:00:00, Room B013
In the average-case analysis of algorithms working on arrays of numbers (modeled by permutations), the uniform distribution on the set of possible inputs is usually assumed. However, the actual data on which these algorithms are used is rarely uniform, and often displays a bias towards "sortedness". In this talk, we present a non-uniform distribution on permutations, which favors their records (a.k.a. left-to-right maxima). We describe the behavior (on average and in distribution) of some classical permutation statistics in this model, some of which with applications to the analysis of algorithms. We also describe the "typical shape" of permutations in our model, by means of their (deterministic) permuton limit.
This is joint work with Nicolas Auger, Cyril Nicaud and Carine Pivoteau.
2023-02-16, 11:00:00, Room Room B013
We propose a new framework for structured prediction based on machine learning algorithms that optimise over classes of functors rather than functions. This functorial learning approach was at the basis of the recent development of quantum natural language processing (QNLP), where we learn functors from formal grammars to parameterised quantum circuits. In order to find optimal functors efficiently, we introduce diagrammatic differentiation: a graphical language to compute the gradients of quantum circuits and string diagrams in general. We then discuss how to apply the same approach to learn distributed quantum protocols from their specification.
2023-02-09, 11:00:00, Room B011
La suite d’Oldenburger-Kolakoski est l’unique suite infinie sur l’alphabet {1,2} qui commence par un 1 et est un point fixe de l’application de codage par plage. Dans cet exposé, nous prendrons un peu de recul par rapport à cette suite bien connue et très étudiée, en introduisant de l’aléa dans le choix des lettres écrites. Cela nous permettra de montrer des résultats portant sur la convergence de la densité de 1 dans les suites ainsi construites. Dans le cas où les lettres sont choisies selon une suite i.i.d. de variables aléatoires ou selon une chaîne de Markov, la densité moyenne de 1 converge. De plus, dans le cas i.i.d., nous arrivons même à démontrer que la densité converge presque sûrement. Il s’agit d’un travail réalisé conjointement par Chloé Boisson, Damien Jamet, et Irène Marcovici.
2023-02-02, 11:00:00, Room B013
La mécanique quantique nous indique qu'il est fondamentalement impossible d'extraire de l'information d'un état quantique sans l'altérer… et parfois certaines propriétés sont même impossibles à extraire à partir d'une seule copie, y compris en mesurant notre qubit de manière destructive. On pourrait donc penser qu'il est impossible de vérifier, en recevant un étant quantique, si cet état possède certaines propriétés avancées sans le détruire. Ceci pose un vrai problème en cryptographie, où on souhaite souvent vérifier que l'état reçu a été honnêtement préparé : pour palier ce problème, des méthodes dites de cut-and-choose doivent souvent être employées, menant à une analyse de sécurité complexe et un protocole peu efficace. Nous avons montré dans un précédent article (arXiv:2104.04742) que cette intuition est erronée : en changeant substantiellement la procédure de transmission d'un état quantique, il est possible de prouver des propriétés extrêmement avancées sur un état quantique reçu, et ce sans l'altérer, de manière similaire aux protocoles Zero-Knowledge (ZK) classiques. Cependant, cette approche, basée sur la cryptographie post-quantique, est très coûteuse à implémenter et la sécurité obtenue est calculatoire. Dans cette présentation d'un travail en cours, je montrerai qu'il est possible d'obtenir à partir de méthodes complètement différentes un protocole NIZK sur un langage quantique plus simple, mais de manière plus efficace et plus sécurisé (sécurité inconditionnelle sous certaines conditions). Je montrerai également les applications au calcul multipartite, en fournissant un protocole d'Oblivious Transfer quantique plus simple, plus sécurisé, plus rapide (communication optimale), et avec une preuve de sécurité plus simple et modulaire.
2023-01-26, 11:00:00, Room C005
Comment empiler un nombre infini d'oranges pour maximiser la proportion de l'espace couvert ? Kepler a conjecturé que l'empilement des "balles de canon" est optimal. 400 ans se sont écoulés avant que cette conjecture soit démontrée par Hales et Ferguson dont la preuve comporte 6 papiers et plus de 50000 lignes de code. Comment arranger un nombre infini de pièces de monnaie de 3 rayons différents sur une table infinie pour maximiser la proportion de la surface couverte ? Un arrangement de disques est dit triangulé si chacun de ses "trous" est borné par trois disques tangents. Connelly a conjecturé que si de tels arrangements existent, l'un d'eux maximise la proportion de la surface couverte. Nous avons démontré cette assertion pour 31 triplets de rayons de disques et l'avons réfuté pour 40 autres triplets. Je vais vous présenter nos résultats sur les arrangements triangulés à 3 disques et les analogies entre notre preuve et celle de la conjecture de Kepler.
2023-01-19, 11:00:00, Room B013
Over the past decade, a number of quantum processes have been proposed which are logically consistent, yet feature a cyclic causal structure. However, there exists no general formal method to construct a process with an exotic causal structure in a way that ensures, and makes clear why, it is consistent. Here we provide such a method, given by an extended circuit formalism. This only requires directed graphs endowed with boolean matrices, which encode basic constraints on operations. Our framework (a) defines a set of elementary rules for checking the validity of any such graph, (b) provides a way of constructing consistent processes as a circuit from valid graphs, and (c) yields an intuitive interpretation of the causal relations within a process and an explanation of why they do not lead to inconsistencies. We display how several standard examples of exotic processes, including ones that violate causal inequalities, are among the class of processes that can be generated in this way; we conjecture that this class in fact includes all unitarily extendible processes.
2023-01-12, 11:00:00, Room C005
We explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We propose a PROP to model computation in this framework, where the choice is parametrized by an algebraic side effect: the model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching, i.e. superposition. The graphical language comes equipped with a denotational semantics based on linear applications and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to the semantics.
2022-12-07, 11:00:00, Room C005
We introduce the first complete equational theory for quantum circuits. More precisely, we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same quantum evolution if and only if they can be transformed one into the other using the equations. The proof is based on the properties of multi-controlled gates – that are defined using elementary gates – together with an encoding of quantum circuits into linear optical circuits, which have been proved to have a complete axiomatisation. This is a joint work with Alexandre Clément, Nicolas Heurtel, Shane Mansfield, and Benoît Valiron.
2022-10-27, 14:00:00, Room B011
We introduce a first-order quantum programming language, named FOQ, whose terminating programs are reversible. We restrict FOQ to a strict and tractable subset, named PFOQ, of terminating programs with bounded width, that provides a first programming language-based characterization of the quantum complexity class FBQP. Finally, we present a tractable semantics-preserving algorithm compiling each PFOQ program to a quantum circuit of size polynomial in the number of input qubits.
2022-10-06, 11:00:00, Room B013
An automata network is a graph where each node is a finite-state machine. The vertices of the graph should be thought as computers with very limited memory and the edges as network links. Each machine has its own transition table and possibly its own set of states. There is no input of any kind: the machines read the current states of their neighbors in the graph, and use those states (all concatenated) as input symbols. The system runs in rounds and, in my research line, all machines are updated simultaneously in each round. (In other terms this is similar to a cellular automaton, except that the “grid” is an arbitrary graph and there is no uniformity: different cells have different update functions.)
An automata network is usually given as a couple (G,f_v), where G is the graph and (f_v) is a family of Boolean circuits indexed by the vertices of G. The circuit f_v encodes the update fonction of the node v, so updating a node is the same as evaluating a Boolean circuit.
I'll state and give a few proof elements of general complexity results on automata networks. More precisely: if we focus on deterministic networks, then any question expressible in first-order logic on a given signature is either O(1), or NP-hard, or coNP-hard. On the other hand, if we focus on nondeterministic networks, then a large class of questions expressible in MSO logic on a given signature is either O(1), or NP-hard, or coNP-hard.
The intuition behind these results is that there is no hope to “parse” the Boolean circuits of an automata network to try and infer something about its general behavior.