Search Results

Documents authored by Mimram, Samuel

Artifact
Software
DOI: 10.4230/artifacts.22463
Delooping generated groups in homotopy type theory

Authors: Camil Champin and Samuel Mimram

Abstract
Cite as

Camil Champin, Samuel Mimram. Delooping generated groups in homotopy type theory (Software, Proofs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22463,
   title = {{Delooping generated groups in homotopy type theory}}, 
   author = {Champin, Camil and Mimram, Samuel},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:4fc863802e40f99733703893622a7aa23c50c308;origin=https://github.com/smimram/generated-deloopings-agda;visit=swh:1:snp:209bea02bef97c56fbcc2da7af07f6b27e89b12c;anchor=swh:1:rev:6b457f58ef54a2ef8e7338fbe7d56a893cc79831}{\texttt{swh:1:dir:4fc863802e40f99733703893622a7aa23c50c308}} (visited on 2024-11-28)},
   url = {https://github.com/smimram/generated-deloopings-agda},
   doi = {10.4230/artifacts.22463},
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.6
Delooping Generated Groups in Homotopy Type Theory

Authors: Camil Champin, Samuel Mimram, and Émile Oleon

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces (up to continuous deformation) and proofs as homotopy invariant constructions. In this context, loop spaces of pointed connected groupoids provide a natural representation of groups, and any group can be obtained as the loop space of such a type, which is then called a delooping of the group. There are two main methods to construct the delooping of an arbitrary group G. The first one consists in describing it as a pointed higher inductive type, whereas the second one consists in taking the connected component of the principal G-torsor in the type of sets equipped with an action of G. We show here that, when a presentation is known for the group, simpler variants of those constructions can be used to build deloopings. The resulting types are more amenable to computations and lead to simpler meta-theoretic reasoning. We also investigate, in this context, an abstract construction for the Cayley graph of a generated group and show that it encodes the relations of the group. Most of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.
Cite as

Camil Champin, Samuel Mimram, and Émile Oleon. Delooping Generated Groups in Homotopy Type Theory. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{champin_et_al:LIPIcs.FSCD.2024.6,
  author =	{Champin, Camil and Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Delooping Generated Groups in Homotopy Type Theory}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.6},
  URN =		{urn:nbn:de:0030-drops-203356},
  doi =		{10.4230/LIPIcs.FSCD.2024.6},
  annote =	{Keywords: homotopy type theory, delooping, group, generator, Cayley graph}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.16
Categorical Coherence from Term Rewriting Systems

Authors: Samuel Mimram

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
The celebrated Squier theorem allows to prove coherence properties of algebraic structures, such as MacLane’s coherence theorem for monoidal categories, based on rewriting techniques. We are interested here in extending the theory and associated tools simultaneously in two directions. Firstly, we want to take in account situations where coherence is partial, in the sense that it only applies for a subset of structural morphisms (for instance, in the case of the coherence theorem for symmetric monoidal categories, we do not want to strictify the symmetry). Secondly, we are interested in structures where variables can be duplicated or erased. We develop theorems and rewriting techniques in order to achieve this, first in the setting of abstract rewriting systems, and then extend them to term rewriting systems, suitably generalized in order to take coherence in account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal and symmetric monoidal categories.
Cite as

Samuel Mimram. Categorical Coherence from Term Rewriting Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mimram:LIPIcs.FSCD.2023.16,
  author =	{Mimram, Samuel},
  title =	{{Categorical Coherence from Term Rewriting Systems}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.16},
  URN =		{urn:nbn:de:0030-drops-180009},
  doi =		{10.4230/LIPIcs.FSCD.2023.16},
  annote =	{Keywords: coherence, rewriting system, Lawvere theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.11
Division by Two, in Homotopy Type Theory

Authors: Samuel Mimram and Émile Oleon

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Natural numbers are isomorphism classes of finite sets and one can look for operations on sets which, after quotienting, allow recovering traditional arithmetic operations. Moreover, from a constructivist perspective, it is interesting to study whether those operations can be performed without resorting to the axiom of choice (the use of classical logic is usually necessary). Following the work of Bernstein, Sierpiński, Doyle and Conway, we study here "division by two" (or, rather, regularity of multiplication by two). We provide here a full formalization of this operation on sets, using the cubical variant of Agda, which is an implementation of the homotopy type theory setting, thus revealing some interesting points in the proof. As a novel contribution, we also show that this construction extends to general types, as opposed to sets.
Cite as

Samuel Mimram and Émile Oleon. Division by Two, in Homotopy Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{mimram_et_al:LIPIcs.FSCD.2022.11,
  author =	{Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Division by Two, in Homotopy Type Theory}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.11},
  URN =		{urn:nbn:de:0030-drops-162920},
  doi =		{10.4230/LIPIcs.FSCD.2022.11},
  annote =	{Keywords: division, axiom of choice, set theory, homotopy type theory, Agda}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.34
A Sound Foundation for the Topological Approach to Task Solvability

Authors: Jérémy Ledent and Samuel Mimram

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit’s paper in 1999. They proved that, for wait-free protocols where the processes communicate through read/write registers, a task is solvable if and only if there exists some map between simplicial complexes satisfying some properties. This approach was then extended to many different contexts, where the processes have access to various synchronization and communication primitives. Usually, in those cases, the existence of a simplicial map from the protocol complex to the output complex is taken as the definition of what it means to solve a task. In particular, no proof is provided of the fact that this abstract topological definition agrees with a more concrete operational definition of task solvability. In this paper, we bridge this gap by proving a version of Herlihy and Shavit’s theorem that applies to any kind of object. First, we start with a very general way of specifying concurrent objects, and we define what it means to implement an object B in a computational model where the processes are allowed to communicate through shared objects A_1, ..., A_k. Then, we derive the notion of a decision task as a special case of concurrent object. Finally, we prove an analogue of Herlihy and Shavit’s theorem in this context. In particular, our version of the theorem subsumes all the uses of the combinatorial topology approach that we are aware of.
Cite as

Jérémy Ledent and Samuel Mimram. A Sound Foundation for the Topological Approach to Task Solvability. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ledent_et_al:LIPIcs.CONCUR.2019.34,
  author =	{Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
  title =	{{A Sound Foundation for the Topological Approach to Task Solvability}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.34},
  URN =		{urn:nbn:de:0030-drops-109365},
  doi =		{10.4230/LIPIcs.CONCUR.2019.34},
  annote =	{Keywords: Fault-tolerant protocols, Asynchronous computability, Combinatorial topology, Protocol complex, Distributed task}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2018.28
Concurrent Specifications Beyond Linearizability

Authors: Éric Goubault, Jérémy Ledent, and Samuel Mimram

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

Abstract
With the advent of parallel architectures, distributed programs are used intensively and the question of how to formally specify the behaviors expected from such programs becomes crucial. A very general way to specify concurrent objects is to simply give the set of all the execution traces that we consider correct for the object. In many cases, one is only interested in studying a subclass of these concurrent specifications, and more convenient tools such as linearizability can be used to describe them. In this paper, what we call a concurrent specification will be a set of execution traces that moreover satisfies a number of axioms. As we argue, these are actually the only concurrent specifications of interest: we prove that, in a reasonable computational model, every program satisfies all of our axioms. Restricting to this class of concurrent specifications allows us to formally relate our concurrent specifications with the ones obtained by linearizability, as well as its more recent variants (set- and interval-linearizability).
Cite as

Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent Specifications Beyond Linearizability. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.OPODIS.2018.28,
  author =	{Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
  title =	{{Concurrent Specifications Beyond Linearizability}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.28},
  URN =		{urn:nbn:de:0030-drops-100888},
  doi =		{10.4230/LIPIcs.OPODIS.2018.28},
  annote =	{Keywords: concurrent specification, concurrent object, linearizability}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2018.50
Brief Announcement: On the Impossibility of Detecting Concurrency

Authors: Éric Goubault, Jérémy Ledent, and Samuel Mimram

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
We identify a general principle of distributed computing: one cannot force two processes running in parallel to see each other. This principle is formally stated in the context of asynchronous processes communicating through shared objects, using trace-based semantics. We prove that it holds in a reasonable computational model, and then study the class of concurrent specifications which satisfy this property. This allows us to derive a Galois connection theorem for different variants of linearizability.
Cite as

Éric Goubault, Jérémy Ledent, and Samuel Mimram. Brief Announcement: On the Impossibility of Detecting Concurrency. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 50:1-50:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2018.50,
  author =	{Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
  title =	{{Brief Announcement: On the Impossibility of Detecting Concurrency}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{50:1--50:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.50},
  URN =		{urn:nbn:de:0030-drops-98392},
  doi =		{10.4230/LIPIcs.DISC.2018.50},
  annote =	{Keywords: concurrent specification, concurrent object, linearizability}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.15
Coherence of Gray Categories via Rewriting

Authors: Simon Forest and Samuel Mimram

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Over the recent years, the theory of rewriting has been extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to low-dimensional weak categories, and consider in details the first non-trivial case: presentations of tricategories. By a general result, those are equivalent to the stricter Gray categories, for which we introduce a notion of rewriting system, as well as associated tools: critical pairs, termination orders, etc. We show that a finite rewriting system admits a finite number of critical pairs and, as a variant of Newman's lemma in our context, that a convergent rewriting system is coherent, meaning that two parallel 3-cells are necessarily equal. This is illustrated on rewriting systems corresponding to various well-known structures in the context of Gray categories (monoids, adjunctions, Frobenius monoids). Finally, we discuss generalizations in arbitrary dimension.
Cite as

Simon Forest and Samuel Mimram. Coherence of Gray Categories via Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{forest_et_al:LIPIcs.FSCD.2018.15,
  author =	{Forest, Simon and Mimram, Samuel},
  title =	{{Coherence of Gray Categories via Rewriting}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.15},
  URN =		{urn:nbn:de:0030-drops-91855},
  doi =		{10.4230/LIPIcs.FSCD.2018.15},
  annote =	{Keywords: rewriting, coherence, Gray category, polygraph, pseudomonoid, precategory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.27
Homological Computations for Term Rewriting Systems

Authors: Philippe Malbos and Samuel Mimram

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
An important problem in universal algebra consists in finding presentations of algebraic theories by generators and relations, which are as small as possible. Exhibiting lower bounds on the number of those generators and relations for a given theory is a difficult task because it a priori requires considering all possible sets of generators for a theory and no general method exists. In this article, we explain how homological computations can provide such lower bounds, in a systematic way, and show how to actually compute those in the case where a presentation of the theory by a convergent rewriting system is known. We also introduce the notion of coherent presentation of a theory in order to consider finer homotopical invariants. In some aspects, this work generalizes, to term rewriting systems, Squier's celebrated homological and homotopical invariants for string rewriting systems.
Cite as

Philippe Malbos and Samuel Mimram. Homological Computations for Term Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{malbos_et_al:LIPIcs.FSCD.2016.27,
  author =	{Malbos, Philippe and Mimram, Samuel},
  title =	{{Homological Computations for Term Rewriting Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.27},
  URN =		{urn:nbn:de:0030-drops-59821},
  doi =		{10.4230/LIPIcs.FSCD.2016.27},
  annote =	{Keywords: term rewriting system, Lawvere theory, Tietze equivalence, resolution, homology, convergent pres entation, coherent presentation}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.89
Presenting a Category Modulo a Rewriting System

Authors: Florence Clerc and Samuel Mimram

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
Presentations of categories are a well-known algebraic tool to provide descriptions of categories by the 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 (in the spirit of rewriting modulo), 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 is based on restricting to objects which are normal forms, one consists in turning equational generators into identities (i.e. considering a quotient category), and one consists in formally adding inverses to equational generators (i.e. localizing the category). We show that, under suitable coherence conditions on the presentation, the three constructions coincide, thus generalizing celebrated results on presentations of groups. We illustrate our techniques on a non-trivial example, and hint at a generalization for 2-categories.
Cite as

Florence Clerc and Samuel Mimram. Presenting a Category Modulo a Rewriting System. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 89-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{clerc_et_al:LIPIcs.RTA.2015.89,
  author =	{Clerc, Florence and Mimram, Samuel},
  title =	{{Presenting a Category Modulo a Rewriting System}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{89--105},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.89},
  URN =		{urn:nbn:de:0030-drops-51916},
  doi =		{10.4230/LIPIcs.RTA.2015.89},
  annote =	{Keywords: presentation of a category, quotient category, localization, residuation}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.223
A Homotopical Completion Procedure with Applications to Coherence of Monoids

Authors: Yves Guiraud, Philippe Malbos, and Samuel Mimram

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
One of the most used algorithm in rewriting theory is the Knuth-Bendix completion procedure which starts from a terminating rewriting system and iteratively adds rules to it, trying to produce an equivalent convergent rewriting system. It is in particular used to study presentations of monoids, since normal forms of the rewriting system provide canonical representatives of words modulo the congruence generated by the rules. Here, we are interested in extending this procedure in order to retrieve information about the low-dimensional homotopy properties of a monoid. We therefore consider the notion of coherent presentation, which is a generalization of rewriting systems that keeps track of the cells generated by confluence diagrams. We extend the Knuth-Bendix completion procedure to this setting, resulting in a homotopical completion procedure. It is based on a generalization of Tietze transformations, which are operations that can be iteratively applied to relate any two presentations of the same monoid. We also explain how these transformations can be used to remove useless generators, rules, or confluence diagrams in a coherent presentation, thus leading to a homotopical reduction procedure. Finally, we apply these techniques to the study of some examples coming from representation theory, to compute minimal coherent presentations for them: braid, plactic and Chinese monoids.
Cite as

Yves Guiraud, Philippe Malbos, and Samuel Mimram. A Homotopical Completion Procedure with Applications to Coherence of Monoids. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 223-238, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{guiraud_et_al:LIPIcs.RTA.2013.223,
  author =	{Guiraud, Yves and Malbos, Philippe and Mimram, Samuel},
  title =	{{A Homotopical Completion Procedure with Applications to Coherence of Monoids}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{223--238},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.223},
  URN =		{urn:nbn:de:0030-drops-40649},
  doi =		{10.4230/LIPIcs.RTA.2013.223},
  annote =	{Keywords: higher-dimensional rewriting, presentation of monoid, Knuth-Bendix completion, Tietze transformation, low-dimensional homotopy for monoids, coherence}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.35
A Non-Standard Semantics for Kahn Networks in Continuous Time

Authors: Romain Beauxis and Samuel Mimram

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
In a seminal article, Kahn has introduced the notion of process network and given a semantics for those using Scott domains whose elements are (possibly infinite) sequences of values. This model has since then become a standard tool for studying distributed asynchronous computations. From the beginning, process networks have been drawn as particular graphs, but this syntax is never formalized. We take the opportunity to clarify it by giving a precise definition of these graphs, that we call nets. The resulting category is shown to be a fixpoint category, i.e. a cartesian category which is traced wrt the monoidal structure given by the product, and interestingly this structure characterizes the category: we show that it is the free fixpoint category containing a given set of morphisms, thus providing a complete axiomatics that models of process networks should satisfy. We then use these tools to build a model of networks in which data vary over a continuous time, in order to elaborate on the idea that process networks should also be able to encompass computational models such as hybrid systems or electric circuits. We relate this model to Kahn's semantics by introducing a third model of networks based on non-standard analysis, whose elements form an internal complete partial order for which many properties of standard domains can be reformulated. The use of hyperreals in this model allows it to formally consider the notion of infinitesimal, and thus to make a bridge between discrete and continuous time: time is "discrete", but the duration between two instants is infinitesimal. Finally, we give some examples of uses of the model by describing some networks implementing common constructions in analysis.
Cite as

Romain Beauxis and Samuel Mimram. A Non-Standard Semantics for Kahn Networks in Continuous Time. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 35-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{beauxis_et_al:LIPIcs.CSL.2011.35,
  author =	{Beauxis, Romain and Mimram, Samuel},
  title =	{{A Non-Standard Semantics for Kahn Networks in Continuous Time}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{35--50},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.35},
  URN =		{urn:nbn:de:0030-drops-32212},
  doi =		{10.4230/LIPIcs.CSL.2011.35},
  annote =	{Keywords: Kahn network, non-standard analysis, fixpoint category, internal cpo}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.227
Computing Critical Pairs in 2-Dimensional Rewriting Systems

Authors: Samuel Mimram

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Rewriting systems on words are very useful in the study of monoids. In good cases, they give finite presentations of the monoids, allowing their manipulation by a computer. Even better, when the presentation is confluent and terminating, they provide one with a notion of canonical representative for the elements of the presented monoid. Polygraphs are a higher-dimensional generalization of this notion of presentation, from the setting of monoids to the much more general setting of n-categories. Here, we are interested in proving confluence for polygraphs presenting 2-categories, which can be seen as a generalization of term rewriting systems. For this purpose, we propose an adaptation of the usual algorithm for computing critical pairs. Interestingly, this framework is much richer than term rewriting systems and requires the elaboration of a new theoretical framework for representing critical pairs, based on contexts in compact 2-categories.
Cite as

Samuel Mimram. Computing Critical Pairs in 2-Dimensional Rewriting Systems. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 227-242, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{mimram:LIPIcs.RTA.2010.227,
  author =	{Mimram, Samuel},
  title =	{{Computing Critical Pairs in 2-Dimensional Rewriting Systems}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{227--242},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.227},
  URN =		{urn:nbn:de:0030-drops-26552},
  doi =		{10.4230/LIPIcs.RTA.2010.227},
  annote =	{Keywords: Rewriting system, polygraph, presentation of a category, critical pair, unification, confluence, compact 2-category, context}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact