-
Abstract clones as noncommutative monoids I
Authors:
Antonio Bucciarelli,
Pierre-Louis Curien,
Antonino Salibra
Abstract:
Clones of functions play a foundational role in both universal algebra and theoretical computer science. In this work, we introduce clone merge monoids (cm-monoids), a unifying one-sorted algebraic framework that integrates abstract clones, clone algebras (previously introduced by the first and the third author), and Neumann's aleph0-abstract clones, while modelling the interplay of infinitary ope…
▽ More
Clones of functions play a foundational role in both universal algebra and theoretical computer science. In this work, we introduce clone merge monoids (cm-monoids), a unifying one-sorted algebraic framework that integrates abstract clones, clone algebras (previously introduced by the first and the third author), and Neumann's aleph0-abstract clones, while modelling the interplay of infinitary operations. Cm-monoids combine a monoid structure with a new algebraic structure called merge algebra, capturing essential properties of infinite sequences of operations.We establish a categorical equivalence between clone algebras and finitely-ranked cm-monoids.This equivalence yields by restriction a three-fold equivalence between abstract clones, finite-dimensional clone algebras, and finite-dimensional, finitely ranked cm-monoids, and is itself obtained by restriction from a categorical equivalence between partial infinitary clone algebras (which generalise clone algebras) and extensional cm-monoids.In a companion work, we develop the theory of modules over cm-monoids, offering a unified approach to polymorphisms and invariant relations,in the hope of providing new insights into algebraic structures and CSP complexity theory.
△ Less
Submitted 13 January, 2025;
originally announced January 2025.
-
Birkhoff-style Theorems Through Infinitary Clone Algebras
Authors:
Antonio Bucciarelli,
Pierre-Louis Curien,
Arturo De Faveri,
Antonino Salibra
Abstract:
Building upon the classical article "Representing varieties of algebras by algebras'' by W. D. Neumann, we revisit the famous Birkhoff's HSP theorem in the light of infinitary algebra.
Building upon the classical article "Representing varieties of algebras by algebras'' by W. D. Neumann, we revisit the famous Birkhoff's HSP theorem in the light of infinitary algebra.
△ Less
Submitted 30 December, 2024; v1 submitted 25 November, 2024;
originally announced November 2024.
-
Term rewriting on nestohedra
Authors:
Pierre-Louis Curien,
Guillaume Laplante-Anfossi
Abstract:
We define term rewriting systems on the vertices and faces of nestohedra, and show that the former are confluent and terminating. While the associated posets on vertices generalize Barnard--McConville's flip order for graph-associahedra, the preorders on faces generalize the facial weak order for permutahedra and the generalized Tamari order for associahedra. Moreover, we define and study contextu…
▽ More
We define term rewriting systems on the vertices and faces of nestohedra, and show that the former are confluent and terminating. While the associated posets on vertices generalize Barnard--McConville's flip order for graph-associahedra, the preorders on faces generalize the facial weak order for permutahedra and the generalized Tamari order for associahedra. Moreover, we define and study contextual families of nestohedra, whose local confluence diagrams satisfy a certain uniformity condition. Among them are associahedra and operahedra, whose associated proofs of confluence for their rewriting systems reproduce proofs of categorical coherence theorems for monoidal categories and categorified operads.
△ Less
Submitted 21 January, 2025; v1 submitted 23 March, 2024;
originally announced March 2024.
-
Topological proofs of categorical coherence
Authors:
Pierre-Louis Curien,
Guillaume Laplante-Anfossi
Abstract:
We give a short topological proof of coherence for categorified non-symmetric operads by using the fact that the diagrams involved form the 1-skeleton of simply connected CW complexes. We also obtain a "one-step" topological proof of Mac Lane's coherence theorem for symmetric monoidal categories, as suggested by Kapranov in 1993. Our analysis is based on a notion of combinatorial homotopy, which w…
▽ More
We give a short topological proof of coherence for categorified non-symmetric operads by using the fact that the diagrams involved form the 1-skeleton of simply connected CW complexes. We also obtain a "one-step" topological proof of Mac Lane's coherence theorem for symmetric monoidal categories, as suggested by Kapranov in 1993. Our analysis is based on a notion of combinatorial homotopy, which we further study in the special case of polyhedral complexes, leading to a second geometrical proof of coherence which is very close to Mac Lane's original argument. We use Morse theory to show that this second method is (strictly) less general than the first. We provide a detailed analysis of how both methods allow us to deduce these two categorical coherence results and discuss possible generalizations to higher categories.
△ Less
Submitted 7 May, 2024; v1 submitted 14 February, 2023;
originally announced February 2023.
-
Rigidification of cubical quasi-categories
Authors:
Pierre-Louis Curien,
Muriel Livernet,
Gabriel Saadia
Abstract:
We construct a cubical analogue of the rigidification functor from quasi-categories to simplicial categories present in the work of Joyal and Lurie. We define a functor from the category of cubical sets of Doherty-Kapulkin-Lindsey-Sattler to the category of (small) simplicial categories. We show that this rigidification functor establishes a Quillen equivalence between the Joyal model structure on…
▽ More
We construct a cubical analogue of the rigidification functor from quasi-categories to simplicial categories present in the work of Joyal and Lurie. We define a functor from the category of cubical sets of Doherty-Kapulkin-Lindsey-Sattler to the category of (small) simplicial categories. We show that this rigidification functor establishes a Quillen equivalence between the Joyal model structure on cubical sets (as it is called by the four authors) and Bergner's model structure on simplicial categories. We follow the approach to rigidification of Dugger and Spivak, adapting their framework of necklaces to the cubical setting.
△ Less
Submitted 24 November, 2022;
originally announced November 2022.
-
The higher dimensional propositional calculus
Authors:
Antonio Bucciarelli,
Pierre-Louis Curien,
Antonio Ledda,
Francesco Paoli,
Antonino Salibra
Abstract:
In recent research, some of the present authors introduced the concept of an n-dimensional Boolean algebra and its corresponding propositional logic nCL, generalising the Boolean propositional calculus to n>= 2 perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for nCL, named nLK. We provide two proofs of completeness: one syntactic and one semantic. The fo…
▽ More
In recent research, some of the present authors introduced the concept of an n-dimensional Boolean algebra and its corresponding propositional logic nCL, generalising the Boolean propositional calculus to n>= 2 perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for nCL, named nLK. We provide two proofs of completeness: one syntactic and one semantic. The former implies as a corollary that nLK enjoys the cut admissibility property. The latter relies on the generalisation to the n-ary case of the classical proof based on the Lindenbaum algebra of formulas and Boolean ultrafilters.
△ Less
Submitted 7 May, 2024; v1 submitted 1 April, 2022;
originally announced April 2022.
-
Tridendriform algebras on hypergraph polytopes
Authors:
Pierre-Louis Curien,
Bérénice Delcroix-Oger,
Jovana Obradović
Abstract:
We extend the works of Loday-Ronco and Burgunder-Ronco on the tridendriform decomposition of the shuffle product on the faces of associahedra and permutohedra, to other families of hypergraph polytopes (or nestohedra), including simplices, hypercubes and some new families. We also extend the shuffle product to take more than two arguments, and define accordingly a new algebraic structure, that we…
▽ More
We extend the works of Loday-Ronco and Burgunder-Ronco on the tridendriform decomposition of the shuffle product on the faces of associahedra and permutohedra, to other families of hypergraph polytopes (or nestohedra), including simplices, hypercubes and some new families. We also extend the shuffle product to take more than two arguments, and define accordingly a new algebraic structure, that we call polydendriform, from which the original tridendriform equations can be crisply synthesized.
△ Less
Submitted 29 November, 2022; v1 submitted 14 January, 2022;
originally announced January 2022.
-
Coherent presentations of monoids with a right-noetherian Garside family
Authors:
Pierre-Louis Curien,
Alen Ðurić,
Yves Guiraud
Abstract:
This paper shows how to construct coherent presentations (presentations by generators, relations and relations among relations) of monoids admitting a right-noetherian Garside family. Thereby, it resolves the question of finding a unifying generalisation of the following two distinct extensions of construction of coherent presentations for spherical Artin-Tits monoids: to general Artin-Tits monoid…
▽ More
This paper shows how to construct coherent presentations (presentations by generators, relations and relations among relations) of monoids admitting a right-noetherian Garside family. Thereby, it resolves the question of finding a unifying generalisation of the following two distinct extensions of construction of coherent presentations for spherical Artin-Tits monoids: to general Artin-Tits monoids, and to Garside monoids. The result is applied to some monoids which are neither Artin-Tits nor Garside.
△ Less
Submitted 28 February, 2023; v1 submitted 1 July, 2021;
originally announced July 2021.
-
Proofs and surfaces
Authors:
Djordje Baralic,
Pierre-Louis Curien,
Marina Milicevic,
Jovana Obradovic,
Zoran Petric,
Mladen Zekic,
Rade T. Zivaljevic
Abstract:
A formal sequent system dealing with Menelaus' configurations is introduced in this paper. The axiomatic sequents of the system stem from 2-cycles of Delta-complexes. The Euclidean and projective interpretations of the sequents are defined and a soundness result is proved. This system is decidable and its provable sequents deliver incidence results. A cyclic operad structure tied to this system is…
▽ More
A formal sequent system dealing with Menelaus' configurations is introduced in this paper. The axiomatic sequents of the system stem from 2-cycles of Delta-complexes. The Euclidean and projective interpretations of the sequents are defined and a soundness result is proved. This system is decidable and its provable sequents deliver incidence results. A cyclic operad structure tied to this system is presented by generators and relations.
△ Less
Submitted 26 May, 2020; v1 submitted 5 July, 2019;
originally announced July 2019.
-
Syntactic approaches to opetopes
Authors:
Pierre-Louis Curien,
Cédric Ho Thanh,
Samuel Mimram
Abstract:
Opetopes are algebraic descriptions of shapes corresponding to compositions in higher dimensions. As such, they offer an approach to higher-dimensional algebraic structures, and in particular, to the definition of weak $ω$-categories, which was the original motivation for their introduction by Baez and Dolan. They are classically defined inductively (as free operads in Leinster's approach, or as z…
▽ More
Opetopes are algebraic descriptions of shapes corresponding to compositions in higher dimensions. As such, they offer an approach to higher-dimensional algebraic structures, and in particular, to the definition of weak $ω$-categories, which was the original motivation for their introduction by Baez and Dolan. They are classically defined inductively (as free operads in Leinster's approach, or as zoom complexes in the formalism of Kock et al.), using abstract constructions making them difficult to manipulate with a computer. In this paper, we present two purely syntactic descriptions of opetopes as sequent calculi, the first using variables to implement the compositional nature of opetopes, the second using a calculus of higher addresses. We prove that well-typed sequents in both systems are in bijection with opetopes as defined in the more traditional approaches. Additionally, we propose three variants to describe opetopic sets. We expect that the resulting structures can serve as natural foundations for mechanized tools based on opetopes.
△ Less
Submitted 14 March, 2019;
originally announced March 2019.
-
Syntactic aspects of hypergraph polytopes
Authors:
Pierre-Louis Curien,
Jovana Obradovic,
Jelena Ivanovic
Abstract:
This paper introduces an inductively defined tree notation for all the faces of polytopes arising from a simplex by truncations. This notation allows us to view inclusion of faces as the process of contracting tree edges. Our notation instantiates to the well-known notations for the faces of associahedra and permutohedra. Various authors have independently introduced combinatorial tools for descri…
▽ More
This paper introduces an inductively defined tree notation for all the faces of polytopes arising from a simplex by truncations. This notation allows us to view inclusion of faces as the process of contracting tree edges. Our notation instantiates to the well-known notations for the faces of associahedra and permutohedra. Various authors have independently introduced combinatorial tools for describing such polytopes. We build on the particular approach developed by Dosen and Petric, who used the formalism of hypergraphs to describe the interval of polytopes from the simplex to the permutohedron. This interval was further stretched by Petric to allow truncations of faces that are themselves obtained by truncations, and iteratively so. Our notation applies to all these polytopes. We illustrate this by showing that it instantiates to a notation for the faces of the permutohedron-based associahedra, that consists of parenthesised words with holes. Dosen and Petric have exhibited some families of hypergraph polytopes (associahedra, permutohedra, and hemiassociahedra) describing the coherences, and the coherences between coherences etc., arising by weakening sequential and parallel associativity of operadic composition. We complement their work with a criterion allowing us to recover the information whether edges of these "operadic polytopes" come from sequential, or from parallel associativity. We also give alternative proofs for some of the original results of Dosen and Petric.
△ Less
Submitted 9 August, 2017;
originally announced August 2017.
-
Categorified cyclic operads
Authors:
Pierre-Louis Curien,
Jovana Obradovic
Abstract:
In this paper, we introduce a notion of categorified cyclic operad for set-based cyclic operads with symmetries. Our categorification is obtained by relaxing defining axioms of cyclic operads to isomorphisms and by formulating coherence conditions for these isomorphisms. The coherence theorem that we prove has the form "all diagrams of canonical isomorphisms commute". Our coherence results come in…
▽ More
In this paper, we introduce a notion of categorified cyclic operad for set-based cyclic operads with symmetries. Our categorification is obtained by relaxing defining axioms of cyclic operads to isomorphisms and by formulating coherence conditions for these isomorphisms. The coherence theorem that we prove has the form "all diagrams of canonical isomorphisms commute". Our coherence results come in two flavours, corresponding to the "entries-only" and "exchangeable-output" definitions of cyclic operads. Our proof of coherence in the entries-only style is of syntactic nature and relies on the coherence of categorified non-symmetric operads established by Došen and Petrić. We obtain the coherence in the exchangeable-output style by "lifting" the equivalence between entries-only and exchangeable-output cyclic operads, set up by the second author. Finally, we show that a generalisation of the structure of profunctors of B\' enabou provides an example of categorified cyclic operad, and we exploit the coherence of categorified cyclic operads in proving that the Feynman category for cyclic operads, due to Kaufmann and Ward, admits an odd version.
△ Less
Submitted 21 November, 2019; v1 submitted 21 June, 2017;
originally announced June 2017.
-
Coherent Presentations of Monoidal Categories
Authors:
Pierre-Louis Curien,
Samuel Mimram
Abstract:
Presentations of categories are a well-known algebraic tool to provide descriptions of categories by means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation, which is described by equational generators. When those form a convergent (abstract) rewriting…
▽ More
Presentations of categories are a well-known algebraic tool to provide descriptions of categories by means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation, which is described by equational generators. When those form a convergent (abstract) rewriting system on objects, there are three very natural constructions that can be used to define the category which is described by the presentation: one consists in turning equational generators into identities (i.e. considering a quotient category), one consists in formally adding inverses to equational generators (i.e. localizing the category), and one consists in restricting to objects which are normal forms. We show that, under suitable coherence conditions on the presentation, the three constructions coincide, thus generalizing celebrated results on presentations of groups, and we extend those conditions to presentations of monoidal categories.
△ Less
Submitted 25 September, 2017; v1 submitted 9 May, 2017;
originally announced May 2017.
-
A formal language for cyclic operads
Authors:
Pierre-Louis Curien,
Jovana Obradović
Abstract:
We propose a $λ$-calculus-style formal language, called the $μ$-syntax, as a lightweight representation of the structure of cyclic operads. We illustrate the rewriting methods behind the formalism by giving a complete step-by-step proof of the equivalence between the unbiased and biased definitions of cyclic operads.
We propose a $λ$-calculus-style formal language, called the $μ$-syntax, as a lightweight representation of the structure of cyclic operads. We illustrate the rewriting methods behind the formalism by giving a complete step-by-step proof of the equivalence between the unbiased and biased definitions of cyclic operads.
△ Less
Submitted 25 April, 2017; v1 submitted 24 February, 2016;
originally announced February 2016.
-
Free algebraic structures on the permutohedra
Authors:
E. Burgunder,
P. -L. Curien,
M. Ronco
Abstract:
Tridendriform algebras are a type of associative algebras, introduced independently by F. Chapoton and by J.-L. Loday and the third author, in order to describe operads related to the Stasheff polytopes. The vector space $\st$ spanned by the faces of permutohedra has a natural structure of tridendriform bialgebra, we prove that it is free as a tridendriform algebra and exhibit a basis. Our result…
▽ More
Tridendriform algebras are a type of associative algebras, introduced independently by F. Chapoton and by J.-L. Loday and the third author, in order to describe operads related to the Stasheff polytopes. The vector space $\st$ spanned by the faces of permutohedra has a natural structure of tridendriform bialgebra, we prove that it is free as a tridendriform algebra and exhibit a basis. Our result implies that the subspace of primitive elements of the coalgebra $\st$ , equipped with the coboundary map of permutohedra, is a free cacti algebra.
△ Less
Submitted 6 May, 2015; v1 submitted 31 March, 2015;
originally announced March 2015.
-
Operads, clones, and distributive laws
Authors:
Pierre-Louis Curien
Abstract:
We show how non-symmetric operads (or multicategories), symmetric operads, and clones, arise from three suitable monads on Cat, each extending to a (pseudo-)monad on the bicategory of categories and profunctors. We also explain how other previous categorical analyses of operads (via Day's tensor products, or via analytical functors) fit with the profunctor approach.
We show how non-symmetric operads (or multicategories), symmetric operads, and clones, arise from three suitable monads on Cat, each extending to a (pseudo-)monad on the bicategory of categories and profunctors. We also explain how other previous categorical analyses of operads (via Day's tensor products, or via analytical functors) fit with the profunctor approach.
△ Less
Submitted 14 May, 2012;
originally announced May 2012.
-
The duality of computation under focus
Authors:
Pierre-Louis Curien,
Guillaume Munch-Maccagnoni
Abstract:
We review the close relationship between abstract machines for (call-by-name or call-by-value) lambda-calculi (extended with Felleisen's C) and sequent calculus, reintroducing on the way Curien-Herbelin's syntactic kit expressing the duality of computation. We use this kit to provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and to transcribe cut elimi…
▽ More
We review the close relationship between abstract machines for (call-by-name or call-by-value) lambda-calculi (extended with Felleisen's C) and sequent calculus, reintroducing on the way Curien-Herbelin's syntactic kit expressing the duality of computation. We use this kit to provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and to transcribe cut elimination as (non confluent) rewriting. A key slogan here, which may appear here in print for the first time, is that commutative cut elimination rules are explicit substitution propagation rules. We then describe the focalised proof search discipline (in the classical setting), and narrow down the language and the rewriting rules to a confluent calculus (a variant of the second author's focalising system L). We then define a game of patterns and counterpatterns, leading us to a fully focalised finitary syntax for a synthetic presentation of classical logic, that provides a quotient on (focalised) proofs, abstracting out the order of decomposition of negative connectives.
△ Less
Submitted 11 June, 2010;
originally announced June 2010.
-
Abstract machines for dialogue games
Authors:
Pierre-Louis Curien,
Hugo Herbelin
Abstract:
The notion of abstract Boehm tree has arisen as an operationally-oriented distillation of works on game semantics, and has been investigated in two papers. This paper revisits the notion, providing more syntactic support and more examples (like call-by-value evaluation) illustrating the generality of the underlying computing device. Precise correspondences between various formulations of the eva…
▽ More
The notion of abstract Boehm tree has arisen as an operationally-oriented distillation of works on game semantics, and has been investigated in two papers. This paper revisits the notion, providing more syntactic support and more examples (like call-by-value evaluation) illustrating the generality of the underlying computing device. Precise correspondences between various formulations of the evaluation mechanism of abstract Boehm trees are established.
△ Less
Submitted 18 June, 2007;
originally announced June 2007.
-
Introduction to linear logic and ludics, part II
Authors:
Pierre-Louis Curien
Abstract:
This paper is the second part of an introduction to linear logic and ludics, both due to Girard. It is devoted to proof nets, in the limited, yet central, framework of multiplicative linear logic and to ludics, which has been recently developped in an aim of further unveiling the fundamental interactive nature of computation and logic. We hope to offer a few computer science insights into this n…
▽ More
This paper is the second part of an introduction to linear logic and ludics, both due to Girard. It is devoted to proof nets, in the limited, yet central, framework of multiplicative linear logic and to ludics, which has been recently developped in an aim of further unveiling the fundamental interactive nature of computation and logic. We hope to offer a few computer science insights into this new theory.
△ Less
Submitted 19 January, 2005;
originally announced January 2005.
-
Introduction to linear logic and ludics, part I
Authors:
Pierre-Louis Curien
Abstract:
This two-parts paper offers a survey of linear logic and ludics, which were introduced by Girard in 1986 and 2001, respectively. Both theories revisit mathematical logic from first principles, with inspiration from and applications to computer science. The present part I covers an introduction to the connectives and proof rules of linear logic, to its decidability properties, and to its models.…
▽ More
This two-parts paper offers a survey of linear logic and ludics, which were introduced by Girard in 1986 and 2001, respectively. Both theories revisit mathematical logic from first principles, with inspiration from and applications to computer science. The present part I covers an introduction to the connectives and proof rules of linear logic, to its decidability properties, and to its models. Part II will deal with proof nets, a graph-like representation of proofs which is one of the major innovations of linear logic, and will present an introduction to ludics.
△ Less
Submitted 18 January, 2005;
originally announced January 2005.
-
Symmetry and interactivity in Programming
Authors:
Pierre-Louis Curien
Abstract:
We recall some of the early occurrences of the notions of interactivity and symmetry in the operational and denotational semantics of programming languages. We suggest some connections with ludics.
We recall some of the early occurrences of the notions of interactivity and symmetry in the operational and denotational semantics of programming languages. We suggest some connections with ludics.
△ Less
Submitted 18 January, 2005;
originally announced January 2005.
-
Playful, streamlike computation
Authors:
Pierre-Louis Curien
Abstract:
We offer a short tour into the interactive interpretation of sequential programs. We emphasize streamlike computation -- that is, computation of successive bits of information upon request. The core of the approach surveyed here dates back to the work of Berry and the author on sequential algorithms on concrete data structures in the late seventies, culminating in the design of the programming l…
▽ More
We offer a short tour into the interactive interpretation of sequential programs. We emphasize streamlike computation -- that is, computation of successive bits of information upon request. The core of the approach surveyed here dates back to the work of Berry and the author on sequential algorithms on concrete data structures in the late seventies, culminating in the design of the programming language CDS, in which the semantics of programs of any type can be explored interactively. Around one decade later, two major insights of Cartwright and Felleisen on one hand, and of Lamarche on the other hand gave new, decisive impulses to the study of sequentiality. Cartwright and Felleisen observed that sequential algorithms give a direct semantics to control operators like call-cc\" and proposed to include explicit errors both in the syntax and in the semantics of the language PCF. Lamarche (unpublished) connected sequential algorithms to linear logic and games. The successful program of games semantics has spanned over the nineties until now, starting with syntax-independent characterizations of the term model of PCF by Abramsky, Jagadeesan, and Malacaria on one hand, and by Hyland and Ong on the other hand.
△ Less
Submitted 18 January, 2005;
originally announced January 2005.
