Search

We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem., 26 pages, 3 figures, 1 table, submitted to LMCS

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 13:1-13:18

The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems. We give here a new set of rewrite rules for the formalism, and show that it is complete for "Toffoli-Hadamard", the simplest approximately universal fragment of quantum mechanics. We show that the rewriting is terminating, but not confluent (which is expected from the universality of the fragment). We do so using the connection between Sum-over-Paths and graphical language ZH-Calculus, and also show how the axiomatisation translates into the latter. Finally, we show how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation - obtained by adding phase gates with dyadic multiples of π to the Toffoli-Hadamard gate-set - used in particular in the Quantum Fourier Transform., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 36:1-36:17

We propose a generalization of Newman’s lemma which gives a criterion of confluence for a wide class of not-necessarily-terminating abstract rewriting systems. We show that ordinary Newman’s lemma for terminating systems can be considered as a corollary of this criterion. We describe a formalization of the proposed generalized Newman’s lemma in Isabelle proof assistant using HOL logic., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 9:1-9:17

In this talk we discuss the nominal approach to the specification of languages with binders and some applications to programming languages and verification., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 1:1-1:4

We exhibit a strong connection between the matchgate formalism introduced by Valiant and the ZW-calculus of Coecke and Kissinger. This connection provides a natural compositional framework for matchgate theory as well as a direct combinatorial interpretation of the diagrams of ZW-calculus through the perfect matchings of their underlying graphs. We identify a precise fragment of ZW-calculus, the planar W-calculus, that we prove to be complete and universal for matchgates, that are linear maps satisfying the matchgate identities. Computing scalars of the planar W-calculus corresponds to counting perfect matchings of planar graphs, and so can be carried in polynomial time using the FKT algorithm, making the planar W-calculus an efficiently simulable fragment of the ZW-calculus, in a similar way that the Clifford fragment is for ZX-calculus. This work opens new directions for the investigation of the combinatorial properties of ZW-calculus as well as the study of perfect matching counting through compositional diagrammatical technics., LIPIcs, Vol. 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), pages 120:1-120:17

Higher-order rewriting is a framework in which higher-order programs can be described by transformation rules on expressions. A computation occurs by transforming an expression into another using such rules. This step-by-step computation model induced by rewriting naturally gives rise to a notion of complexity as the number of steps needed to reduce expressions to a normal form, i.e., an expression that cannot be reduced further. The study of complexity analysis focuses on the development of automatable techniques to provide bounds to this number. In this paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy, so as to model call-by-value programs. We provide a cost-size semantics: a class of algebraic interpretations to map terms to tuples which bound both the reduction cost and the size of normal forms., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 15:1-15:19

Higher-order unification (HOU) concerns unification of (extensions of) $\lambda$-calculus and can be seen as an instance of equational unification ($E$-unification) modulo $\beta\eta$-equivalence of $\lambda$-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to $\lambda$-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce $E$-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general $E$-unification. We prove that the procedure is sound and complete., Comment: An extended version (with a few more examples and some extra remarks)

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 8:1-8:18

Rewriting is a foundation for the operational theory of programming languages. The process of rewriting describes the computation of a result (typically, a normal form), with lambda-calculus being the paradigmatic example for rewriting as an abstract form of program execution. Taking this view, the execution of a program is formalized as a specific evaluation strategy, while the general rewriting theory allows for program transformations, optimizations, parallel/distributed implementations, and provides a base on which to reason about program equivalence. In this talk, we discuss what happens when the notion of termination is asymptotic, that is, the result of computation appears as a limit, as opposed to reaching a normal form in a finite number of steps. - Example 1. A natural example is probabilistic computation. A probabilistic program P is a stochastic model generating a distribution over all possible outputs of P. Even if the termination probability is 1 (almost sure termination), that degree of certitude is typically not reached in a finite number of steps, but as a limit. A standard example is a term M that reduces to either a normal form or M itself, with equal probability 1/2. After n steps, M is in normal form with probability 1/2 + 1/(2²) + … + 1/(2ⁿ). Only at the limit this computation terminates with probability 1. - Example 2. Infinitary lambda-calculi (where the limits are infinitary terms such as Böhm trees), streams, algebraic rewriting systems, effectful computation (e.g. computation with outputs), quantum lambda-calculi provide several other relevant examples. Instances of asymptotic computation are quite diverse, and moreover the specific syntax of each system may be rather complex. In the talk, we present asymptotic rewriting in a way which is independent of the specific details of each calculus, and we provide a toolkit of proof-techniques which are of general application. To do so, we rely on Quantitative Abstract Rewriting System [Claudia Faggian, 2022; Claudia Faggian and Giulio Guerrieri, 2022], building on work by Ariola and Blom [Ariola and Blom, 2002], which enrich with quantitative information the theory of Abstract Rewriting Systems (ARS) (see e.g. [Terese, 2003] or [Baader and Nipkow, 1998]). ARS are indeed the core of finitary rewriting, capturing the common substratum of rewriting theory and term transformation, independently from the particular structure of the objects. It seems then natural to seek a similar foundation for asymptotic computation. The issue is that the arguments relying on finitary termination do not transfer, in general, to limits (a game changer being that asymptotic termination does not provide a well-founded order): we need to develope an opportune formalization and suitable proof techniques. The goal is then to identify and develop methods which only rely on the asymptotic argument - abstracting from structure specific to a setting - and so will apply to any concrete instance. For example, in infinitary lambda calculus, the limit is usually a (possibly infinite) limit term, while in probabilistic lambda calculus, the limit is a distribution over (finite) terms. The former is concerned with the depth of the redexes, the latter with the probability of reaching a result. The abstract notions of limit and of normalization subsumes both, and so abstract results apply to either setting., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 1:1-1:2

This paper defines two decreasing measures for terms of the simply typed λ-calculus, called the 𝒲-measure and the 𝒯^{𝐦}-measure. A decreasing measure is a function that maps each typable λ-term to an element of a well-founded ordering, in such a way that contracting any β-redex decreases the value of the function, entailing strong normalization. Both measures are defined constructively, relying on an auxiliary calculus, a non-erasing variant of the λ-calculus. In this system, dubbed the λ^{𝐦}-calculus, each β-step creates a "wrapper" containing a copy of the argument that cannot be erased and cannot interact with the context in any other way. Both measures rely crucially on the observation, known to Turing and Prawitz, that contracting a redex cannot create redexes of higher degree, where the degree of a redex is defined as the height of the type of its λ-abstraction. The 𝒲-measure maps each λ-term to a natural number, and it is obtained by evaluating the term in the λ^{𝐦}-calculus and counting the number of remaining wrappers. The 𝒯^{𝐦}-measure maps each λ-term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 11:1-11:19

We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 12:1-12:16

We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 30:1-30:19

In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits., 20 pages

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 19:1-19:19

Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000$\times$ faster while actually featuring simpler compiler-specific proofs., 13th International Conference on Interactive Theorem Proving (ITP 2022)

The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for b-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 24:1-24:14

So far, several typed lambda-calculus systems were combined with algebraic rewrite rules, and the termination (in other words, strong normalisation) problem of the combined systems was discussed. By the size-based approach, Blanqui formulated a termination criterion for simply typed lambda-calculus with algebraic rewrite rules which guarantees, in some specific cases, the termination of the rewrite relation induced by beta-reduction and algebraic rewrite rules on strictly or non-strictly positive inductive types. Using the inflationary fixed-point construction, we extend this termination criterion so that it is possible to show the termination of the rewrite relation induced by some rewrite rules on types which are called non-positive types. In addition, we note that a condition in Blanqui’s proof can be dropped, and this improves the criterion also for non-strictly positive inductive types., LIPIcs, Vol. 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021), pages 12:1-12:23

This paper discusses a number of methods to prove termination of higher-order term rewriting systems, with a particular focus on large systems. In first-order term rewriting, the dependency pair framework can be used to split up a large termination problem into multiple (much) smaller components that can be solved individually. This is important because a large problem may take exponentially longer to solve in one go than solving each of its components. Unfortunately, while there are higher-order versions of several of these methods, they often fail to simplify a problem enough. Here, we will explore some of these techniques and their limitations, and discuss what else can be done to incrementally build a termination proof for higher-order systems., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 1:1-1:17

In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 27:1-27:17

We investigate the problem of enumerating all terms generated by a tree-grammar which are also in normal form with respect to a set of directed equations (rewriting relation). To this end we show that deciding emptiness and finiteness of the resulting set is EXPTIME-complete. The emptiness result is inspired by a prior result by Comon and Jacquemard on ground reducibility. The finiteness result is based on modification of pumping arguments used by Comon and Jacquemard. We highlight practical applications and limitations. We provide and evaluate a prototype implementation. Limitations are somewhat surprising in that, while deciding emptiness and finiteness is EXPTIME-complete for linear and nonlinear rewrite relations, the linear case is practically feasible while the nonlinear case is infeasible, even for a trivially small example. The algorithms provided for the linear case also improve on prior practical results by Kallat et al., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 14:1-14:19

ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 30:1-30:16

We present a technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit, as opposite to reaching a normal form in a finite number of steps. Asymptotic termination occurs in several settings, such as effectful, and in particular probabilistic computation -- where the limits are distributions over the possible outputs -- or infinitary lambda-calculi -- where the limits are infinitary normal forms such as Boehm trees. As a concrete application, we obtain a result which is of independent interest: a normalization theorem for Call-by-Value (and -- in a uniform way -- for Call-by-Name) probabilistic lambda-calculus., FSCD 2022

Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem - i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational - that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 25:1-25:18

Matching algorithms are often central sub-routines in many areas of automated reasoning. They are used in areas such as functional programming, rule-based programming, automated theorem proving, and the symbolic analysis of security protocols. Matching is related to unification but provides a somewhat simplified problem. Thus, in some cases, we can obtain a matching algorithm even if the unification problem is undecidable. In this paper we consider a hierarchical approach to constructing matching algorithms. The hierarchical method has been successful for developing unification algorithms for theories defined over a constructor sub-theory. We show how the approach can be extended to matching problems which allows for the development, in a modular way, of hierarchical matching algorithms. Here we focus on regular theories, where both sides of each equational axiom have the same set of variables. We show that the combination of two hierarchical matching algorithms leads to a hierarchical matching algorithm for the union of regular theories sharing only a common constructor sub-theory., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 6:1-6:22

We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant "top" for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events., LIPIcs, Vol. 243, 33rd International Conference on Concurrency Theory (CONCUR 2022), pages 26:1-26:18

This paper develops a formal string diagram language for monoidal closed categories. Previous work has shown that string diagrams for freely generated symmetric monoidal categories can be viewed as hypergraphs with interfaces, and the axioms of these categories can be realized by rewriting systems. This work proposes hierarchical hypergraphs as a suitable formalization of string diagrams for monoidal closed categories. We then show double pushout rewriting captures the axioms of these closed categories., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 29:1-29:20

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 20:1-20:19

We give a formal treatment of simple type theories, such as the simply-typed $\lambda$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $\lambda$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $\beta$- and $\eta$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax., Comment: To appear in the proceedings of FSCD 2021; 16 pages

In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic. We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity. A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 29:1-29:23

LIPIcs, Volume 188, TYPES 2020, Complete Volume, LIPIcs, Vol. 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020), pages 1-204

We study the implicit computational complexity of constructor term rewriting systems where every function and constructor symbol is unary or nullary. Surprisingly, adding simple and natural constraints to rule formation yields classes of systems that accept exactly the four classes of languages in the Chomsky hierarchy., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 5:1-5:17

In this work, we consider the following order reconfiguration problem: Given a graph G together with linear orders ω and ω' of the vertices of G, can one transform ω into ω' by a sequence of swaps of adjacent elements in such a way that at each time step the resulting linear order has cutwidth (pathwidth) at most k? We show that this problem always has an affirmative answer when the input linear orders ω and ω' have cutwidth (pathwidth) at most k/2. Using this result, we establish a connection between two apparently unrelated problems: the reachability problem for two-letter string rewriting systems and the graph isomorphism problem for graphs of bounded cutwidth. This opens an avenue for the study of the famous graph isomorphism problem using techniques from term rewriting theory., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 8:1-8:15

We present three techniques for improving the Knuth-Bendix completion procedure and its variants: An order extension by semantic labeling, a new confluence criterion for terminating term rewrite systems, and inter-reduction for maximal completion., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 2:1-2:9

Equational unification is the problem of solving an equation modulo equational axioms. In this paper, we provide a relationship between equational unification and homological algebra for equational theories. We will construct a functor from the category of sets of equational axioms to the category of abelian groups. Then, our main theorem gives a necessary condition of equational unifiability that is described in terms of abelian groups associated with equational axioms and homomorphisms between them. To construct our functor, we use a ringoid (a category enriched over the category of abelian groups) obtained from the equational axioms and a free resolution of a "good" module over the ringoid, which was developed by Malbos and Mimram., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 61:1-61:16

Front Matter, Table of Contents, Preface, Conference Organization, LIPIcs, Vol. 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020), pages 0:i-0:viii

We investigate the concept of definable, or inner, automorphism in the logical setting of partial Horn theories. The central technical result extends a syntactical characterization of the group of such automorphisms (called the covariant isotropy group) associated with an algebraic theory to the wider class of quasi-equational theories. We apply this characterization to prove that the isotropy group of a strict monoidal category is precisely its Picard group of invertible objects. Furthermore, we obtain an explicit description of the covariant isotropy group of a presheaf category., Comment: 16 pages. Submitted to FSCD 2021

We present the Z-property and instantiate it to various rewrite systems: associativity, positive braids, self-distributivity, the lambda-calculus, lambda-calculi with explicit substitutions, orthogonal TRSs, .... The Z-property is proven equivalent to Takahashi’s angle property by means of a syntax-free notion of development. We show that several classical consequences of having developments such as confluence, normalisation, and recurrence, can be regained in a syntax-free way, and investigate how the notion corresponds to the classical syntactic notion of development in term rewriting., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 24:1-24:22

Rewriting modulo equations has been researched for several decades but due to the lack of suitable orderings, there are some limitations to rewriting modulo permutation equations. Given a finite set of permutation equations E, we present a new RPO-based ordering modulo E using (permutation) group actions and their associated orbits. It is an E-compatible reduction ordering on terms with the subterm property and is E-total on ground terms. We also present a completion and ground completion method for rewriting modulo a finite set of permutation equations E using our ordering modulo E. We show that our ground completion modulo E always admits a finite ground convergent (modulo E) rewrite system, which allows us to obtain the decidability of the word problem of ground theories modulo E., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 19:1-19:17

Graphical calculi such as the ZH-calculus are powerful tools in the study and analysis of quantum processes, with links to other models of quantum computation such as quantum circuits, measurement-based computing, etc. A somewhat compact but systematic way to describe a quantum process is through the use of quantum multiple-valued decision diagrams (QMDDs), which have already been used for the synthesis of quantum circuits as well as for verification. We show in this paper how to turn a QMDD into an equivalent ZH-diagram, and vice-versa, and show how reducing a QMDD translates in the ZH-Calculus, hence allowing tools from one formalism to be used into the other., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 89:1-89:15

A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems. Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : x ∧ (y ∨ z) → (x ∧ y) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 14:1-14:19

International audience; We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.

Wanda is a fully automatic termination analysis tool for higher-order term rewriting. In this paper, we will discuss the methodology used in Wanda. Most pertinently, this includes a higher-order dependency pair framework and a variation of the higher-order recursive path ordering, as well as some non-termination analysis techniques and delegation to a first-order tool. Additionally, we will discuss Wanda’s internal rewriting formalism, and how to use Wanda in practice for systems in two different formalisms. We also present experimental results that consider both formalisms.

International audience; Different graphical calculi have been proposed to represent quantum computation. First the ZX-calculus [4], followed by the ZW-calculus [12] and then the ZH-calculus [1]. We can wonder if new Z *-calculi will continue to be proposed forever. This article answers negatively. All those language share a common core structure we call Z *-algebras. We classify Z *-algebras up to isomorphism in two dimensional Hilbert spaces and show that they are all variations of the aforementioned calculi. We do the same for linear relations and show that the calculus of [2] is essentially the unique one. The most common formalization of quantum computing is the circuit model, a diagram-matical language representing unitary matrices in a two dimensional Hilbert space, see [20] for an introduction. Verification of quantum processes requires a sound and complete equational theory for quantum circuits, i.e. a complete presentation of unitaries by generators and relations. This is known to be a difficult open problem. By relaxing the unitarity condition and allowing all linear maps, at least three different complete equational theories were found. The ZX-calculus was introduced in [4] and was designed as a part of the categorical quantum mechanics program. It relies on the interaction between two complementary observables. The ZX-calculus has proven to be a good language to reason about quantum processes [7, 11]. However, finding a set of rules to make it complete has been open for a long time, and part of the solution [15] involved a secondary graphical language: the ZW-calculus [12, 5]. This calculus is built on two tripartite entanglement classes (GHZ and W-states) unraveling new structures. Yet another complete graphical language was later introduced, the ZH-calculus [1], inspired by hyper-graph states. Compared to quantum circuits, these three languages share an important advantage. Processes and matrices are not represented merely by diagrams, but by graphs (hence the term graphical language). Isomorphic graphs represent the same quantum evolution. This peculiarity is embedded in the only topology matters paradigm. This is a subtle feature: a usual diagrammatic language (like quantum circuits) starts with a given set of primitives (usually quantum gates) for which the notion of inputs and outputs is significant. When only topology matters, one can readily switch an input into an output, and conversely. This property follows from some specificities of the building blocks of those languages. One goal of this article is to give a formal definition of these specificities. Then, we will be able to prove that the three existing graphical calculi for quantum computing, ZX, ZH and ZW , are essentially the only possible graphical calculi for quantum computing.

Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes a- such as strictly positive datatypes, complete case analysis, and well-founded induction a- that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: Yours.

The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.

We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to tuples of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type nat may be associated to a pair ⟨ cost, size ⟩ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexity, which makes it particularly useful to obtain complexity bounds for higher-order rewriting systems. We show that rewriting systems compatible with tuple interpretations admit finite bounds on derivation height. Furthermore, we demonstrate how to mechanically construct tuple interpretations and how to orient β and η reductions within our technique. Finally, we relate our method to runtime complexity and prove that specific interpretation shapes imply certain runtime complexity bounds., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 31:1-31:22

Uniqueness of normal forms w.r.t. conversion (UNC) of term rewriting systems (TRSs) guarantees that there are no distinct convertible normal forms. It was recently shown that the UNC property of TRSs is decidable for shallow TRSs (Radcliffe et al., 2010). The existing procedure mainly consists of testing whether there exists a counterexample in a finite set of candidates; however, the procedure suffers a bottleneck of having a sheer number of such candidates. In this paper, we propose a new procedure which consists of checking a smaller number of such candidates and enumerating such candidates more efficiently. Correctness of the proposed procedure is proved and its complexity is analyzed. Furthermore, these two procedures have been implemented and it is experimentally confirmed that the proposed procedure runs much faster than the existing procedure.

Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete, and return tree grammars from which the set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions.

This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.