 |
 |
Selected Papers of the 3rd International Conference on Formal Structures and Deduction (FSCD 2018)
Editors: Hélène Kirchner, Paula Severi
1. A diagrammatic calculus of fermionic quantum circuits
We introduce the fermionic ZW calculus, a string-diagrammatic language for fermionic quantum computing (FQC). After defining a fermionic circuit model, we present the basic components of the calculus, together with their interpretation, and show how the main physical gates of interest in FQC can be represented in our language. We then list our axioms, and derive some additional equations. We prove that the axioms provide a complete equational axiomatisation of the monoidal category whose objects are systems of finitely many local fermionic modes (LFMs), with maps that preserve or reverse the parity of states, and the tensor product as monoidal product. We achieve this through a procedure that rewrites any diagram in a normal form. As an example, we show how the statistics of a fermionic Mach-Zehnder interferometer can be calculated in the diagrammatic language. We conclude by giving a diagrammatic treatment of the dual-rail encoding, a standard method in optical quantum computing used to perform universal quantum computation.
2. On the enumeration of closures and environments with an application to random generation
Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. In this paper we investigate some dynamic aspects of evaluation in lambda-calculus considering the quantitative, combinatorial properties of environments and closures. Focusing on two classes of environments and closures, namely the so-called plain and closed ones, we consider the problem of their asymptotic counting and effective random generation. We provide an asymptotic approximation of the number of both plain environments and closures of size $n$. Using the associated generating functions, we construct effective samplers for both classes of combinatorial structures. Finally, we discuss the related problem of asymptotic counting and random generation of closed environemnts and closures.
3. Call-by-name Gradual Type Theory
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism, which were developed in blame calculi and to state the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality ($\eta$) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of Findler and Felleisen's definitions of contracts, and use it to build some concrete domain-theoretic models of gradual typing.
4. Signatures and Induction Principles for Higher Inductive-Inductive Types
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
5. On Nominal Syntax and Permutation Fixed Points
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new $\alpha$-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts. We provide a definition of $\alpha$-equivalence modulo equational theories that take into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.
6. Decreasing Diagrams for Confluence and Commutation
Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be used to obtain such a hierarchy. The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract rewrite systems. It is complete for countable systems, and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps with labels from a well-founded order in order to conclude confluence of the underlying unlabelled relation. Hence it is natural to ask how the size of the label set influences the strength of the technique. In particular, what class of abstract rewrite systems can be proven confluent using decreasing diagrams restricted to 1 label, 2 labels, 3 labels, and so on? Surprisingly, we find that two labels suffice for proving confluence for every abstract rewrite system having the cofinality property, thus in particular for every confluent, countable system. Secondly, we show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse. Thirdly, investigating the possibility of a confluence hierarchy, we determine the first-order (non-)definability of the […]
7. Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix
This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms. In this journal version, we have added an explanation of Retoré's "RB-graphs" in terms of a general construction on graphs with forbidden transitions. In fact, it is by analyzing RB-graphs that we arrived at this construction, and thus obtained a polynomial-time algorithm for finding trails avoiding forbidden transitions; the latter is among the material covered in another paper by the author focusing on graph theory (arXiv:1901.07028).
8. On properties of $B$-terms
$B$-terms are built from the $B$ combinator alone defined by $B\equiv\lambda fgx. f(g~x)$, which is well known as a function composition operator. This paper investigates an interesting property of $B$-terms, that is, whether repetitive right applications of a $B$-term cycles or not. We discuss conditions for $B$-terms to have and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of $B$-terms which have the cyclic property and show that there are infinitely many $B$-terms which do not have the property. Also, we introduce another interesting property about a canonical representation of $B$-terms that is useful to detect cycles, or equivalently, to prove the cyclic property, with an efficient algorithm.