-
Hypercubical manifolds in homotopy type theory
Authors:
Samuel Mimram,
Émile Oleon
Abstract:
Homotopy type theory is a logical setting in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces up to homotopy, and proofs as homotopy invariant constructions. In this context, we introduce a type which corresponds to the hypercubical manifold, a space first introduced by Poincaré in 1895. Its importance stems from the fact that…
▽ More
Homotopy type theory is a logical setting in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces up to homotopy, and proofs as homotopy invariant constructions. In this context, we introduce a type which corresponds to the hypercubical manifold, a space first introduced by Poincaré in 1895. Its importance stems from the fact that it provides an approximation of the group Q of quaternionic units, in the sense of being the first step of a cellular resolution of Q. In order to ensure the validity of our definition, we show that it satisfies the expected property: it is the homotopy quotient of the 3-sphere by the expected action of Q. This is non-trivial and requires performing subtle combinatorial computations based on the flattening lemma, thus illustrating the effective nature of homotopy type theory. Finally, based on the previous construction, we introduce new higher-dimensional generalizations of this manifold, which correspond to better cellular approximations of Q, converging toward a delooping of Q.
△ Less
Submitted 24 June, 2025;
originally announced June 2025.
-
Polynomials in homotopy type theory as a Kleisli category
Authors:
Elies Harington,
Samuel Mimram
Abstract:
Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work in multiple directions. We begin by generalizing the construction of…
▽ More
Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work in multiple directions. We begin by generalizing the construction of the free symmetric monoid monad on types in order to handle arities in an arbitrary universe. Then, we extend this monad to the (wild) category of spans of types, and thus to a comonad by self-duality. Finally, we show that the resulting Kleisli category is equivalent to the traditional category of polynomials. This thus establishes polynomials as a (homotopical) model of linear logic. In fact, we explain that it is closely related to a bicategorical model of differential linear logic introduced by Melliès.
△ Less
Submitted 7 December, 2024; v1 submitted 15 November, 2024;
originally announced November 2024.
-
Delooping cyclic groups with lens spaces in homotopy type theory
Authors:
Samuel Mimram,
Émile Oleon
Abstract:
In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precis…
▽ More
In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called delooping. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to untruncated types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups $\mathbb{Z}_m$ which are cellular, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of lens spaces, which constitute an important family of spaces in algebraic topology. Our definition is based on the computation of an iterative join of suitable maps from the circle to an arbitrary delooping of $\mathbb{Z}_m$. In some sense, this work generalizes the construction of real projective spaces by Buchholtz and Rijke, which handles the case m=2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.
△ Less
Submitted 16 May, 2024;
originally announced May 2024.
-
Delooping presented groups in homotopy type theory
Authors:
Camil Champin,
Samuel Mimram,
Emile Oleon
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 homotopy 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…
▽ More
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 homotopy 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 for constructing 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 (or even a generating set) 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. Finally, we develop a type theoretical notion of 2-polygraph, which allows manipulating higher inductive types such as the ones involved in the description of deloopings. These allow us to investigate in this context a construction for the Cayley graph of a generated group and show that it encodes the relations of the group, as well as a Cayley complex which encodes relations between relations. Many of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.
△ Less
Submitted 1 July, 2025; v1 submitted 6 May, 2024;
originally announced May 2024.
-
Rewriting techniques for relative coherence
Authors:
Samuel Mimram
Abstract:
A series of works has established rewriting as an essential tool in order to prove coherence properties of algebraic structures, such as MacLane's coherence theorem for monoidal categories, based on the observation that, under reasonable assumptions, confluence diagrams for critical pairs provide the required coherence axioms. We are interested here in extending this approach simultaneously in two…
▽ More
A series of works has established rewriting as an essential tool in order to prove coherence properties of algebraic structures, such as MacLane's coherence theorem for monoidal categories, based on the observation that, under reasonable assumptions, confluence diagrams for critical pairs provide the required coherence axioms. We are interested here in extending this approach simultaneously in two directions. Firstly, we want to take into account situations where coherence is partial, in the sense that it only applies to a subset of the structural morphisms. Secondly, we are interested in structures which are cartesian in the sense that 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 to take coherence into account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal and symmetric monoidal categories.
△ Less
Submitted 18 June, 2025; v1 submitted 28 February, 2024;
originally announced February 2024.
-
Polygraphs: From Rewriting to Higher Categories
Authors:
Dimitri Ara,
Albert Burroni,
Yves Guiraud,
Philippe Malbos,
François Métayer,
Samuel Mimram
Abstract:
Polygraphs are a higher-dimensional generalization of the notion of directed graph. Based on those as unifying concept, this monograph on polygraphs revisits the theory of rewriting in the context of strict higher categories, adopting the abstract point of view offered by homotopical algebra. The first half explores the theory of polygraphs in low dimensions and its applications to the computation…
▽ More
Polygraphs are a higher-dimensional generalization of the notion of directed graph. Based on those as unifying concept, this monograph on polygraphs revisits the theory of rewriting in the context of strict higher categories, adopting the abstract point of view offered by homotopical algebra. The first half explores the theory of polygraphs in low dimensions and its applications to the computation of the coherence of algebraic structures. It is meant to be progressive, with little requirements on the background of the reader, apart from basic category theory, and is illustrated with algorithmic computations on algebraic structures. The second half introduces and studies the general notion of n-polygraph, dealing with the homotopy theory of those. It constructs the folk model structure on the category of strict higher categories and exhibits polygraphs as cofibrant objects. This allows extending to higher dimensional structures the coherence results developed in the first half.
△ Less
Submitted 1 December, 2023;
originally announced December 2023.
-
Free precategories as presheaf categories
Authors:
Simon Forest,
Samuel Mimram
Abstract:
Precategories generalize both the notions of strict $n$-category and sesquicategory: their definition is essentially the same as the one of strict $n$-categories, excepting that we do not require the various interchange laws to hold. Those have been proposed as a framework in which one can express semi-strict definitions of weak higher categories: in dimension 3, Gray categories are an instance of…
▽ More
Precategories generalize both the notions of strict $n$-category and sesquicategory: their definition is essentially the same as the one of strict $n$-categories, excepting that we do not require the various interchange laws to hold. Those have been proposed as a framework in which one can express semi-strict definitions of weak higher categories: in dimension 3, Gray categories are an instance of them and have been shown to be equivalent to tricategories, and definitions of semi-strict tetracategories have been proposed, and used as the basis of proof assistants such as Globular. In this article, we are mostly interested in free precategories. Those can be presented by generators and relations, using an appropriate variation on the notion of polygraph (aka computad), and earlier works have shown that the theory of rewriting can be generalized to this setting, enjoying most of the fundamental constructions and properties which can be found in the traditional theory, contrarily to polygraphs for strict categories. We further study here why this is the case, by providing several results which show that precategories and their associated polygraphs bear properties which ensure that we have a good syntax for those. In particular, we show that the category of polygraphs for precategories form a presheaf category.
△ Less
Submitted 29 November, 2022;
originally announced November 2022.
-
Rewriting in Gray categories with applications to coherence
Authors:
Simon Forest,
Samuel Mimram
Abstract:
Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categor…
▽ More
Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categories as particular cases, and are adapted to mechanized computations. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier's theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, Frobenius monoids.
△ Less
Submitted 29 November, 2022; v1 submitted 11 September, 2021;
originally announced September 2021.
-
Globular weak $ω$-categories as models of a type theory
Authors:
Thibaut Benjamin,
Eric Finster,
Samuel Mimram
Abstract:
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a…
▽ More
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $ω$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $ω$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories
△ Less
Submitted 2 February, 2024; v1 submitted 8 June, 2021;
originally announced June 2021.
-
Tietze Equivalences as Weak Equivalences
Authors:
Simon Henry,
Samuel Mimram
Abstract:
A given monoid usually admits many presentations by generators and relations and the notion of Tietze equivalence characterizes when two presentations describe the same monoid: it is the case when one can transform one presentation into the other using the two families of so-called Tietze transformations. The goal of this article is to provide an abstract and geometrical understanding of this well…
▽ More
A given monoid usually admits many presentations by generators and relations and the notion of Tietze equivalence characterizes when two presentations describe the same monoid: it is the case when one can transform one presentation into the other using the two families of so-called Tietze transformations. The goal of this article is to provide an abstract and geometrical understanding of this well-known fact, by constructing a model structuree on the category of presentations, in which two presentations are weakly equivalent when they present the same monoid. We show that Tietze transformations form a pseudo-generating family of trivial cofibrations and give a proof of the completeness of these transformations by an abstract argument in this setting.
△ Less
Submitted 14 October, 2021; v1 submitted 10 January, 2021;
originally announced January 2021.
-
Directed Homotopy in Non-Positively Curved Spaces
Authors:
Eric Goubault,
Samuel Mimram
Abstract:
A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the "geometry" of the space of possible executions of the program. Here, we study the particular case of programs using only mutexes, which are the most widely used synchronization primitive. We show that in this case, the resulting programs have non-pos…
▽ More
A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the "geometry" of the space of possible executions of the program. Here, we study the particular case of programs using only mutexes, which are the most widely used synchronization primitive. We show that in this case, the resulting programs have non-positive curvature, a notion that we introduce and study here for precubical sets, and can be thought of as an algebraic analogue of the well-known one for metric spaces. Using this it, as well as categorical rewriting techniques, we are then able to show that directed and non-directed homotopy coincide for directed paths in these precubical sets. Finally, we study the geometric realization of precubical sets in metric spaces, to show that our conditions on precubical sets actually coincide with those for metric spaces. Since the category of metric spaces is not cocomplete, we are lead to work with generalized metric spaces and study some of their properties.
△ Less
Submitted 10 July, 2020; v1 submitted 19 August, 2019;
originally announced August 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.
-
A Type-Theoretical Definition of Weak ω-Categories
Authors:
Eric Finster,
Samuel Mimram
Abstract:
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a…
▽ More
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.
△ Less
Submitted 9 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 Categorical Theory of Patches
Authors:
Samuel Mimram,
Cinzia Di Giusto
Abstract:
When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system requires to handle lots of situations depending on the operations performed by users on files, and it is thus difficult to ensure that all the co…
▽ More
When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system requires to handle lots of situations depending on the operations performed by users on files, and it is thus difficult to ensure that all the corner cases have been correctly addressed. Here, instead of verifying the implementation of such a system, we adopt a complementary approach: we introduce a theoretical model, which is defined abstractly by the universal property that it should satisfy, and work out a concrete description of it. We begin by defining a category of files and patches, where the operation of merging the effect of two coinitial patches is defined by pushout. Since two patches can be incompatible, such a pushout does not necessarily exist in the category, which raises the question of which is the correct category to represent and manipulate files in conflicting state. We provide an answer by investigating the free completion of the category of files under finite colimits, and give an explicit description of this category: its objects are finite sets labeled by lines equipped with a transitive relation and morphisms are partial functions respecting labeling and relations.
△ Less
Submitted 13 November, 2013;
originally announced November 2013.
-
Computing Flowpipe of Nonlinear Hybrid Systems with Numerical Methods
Authors:
Olivier Bouissou,
Alexandre Chapoutot,
Samuel Mimram
Abstract:
Modern control-command systems often include controllers that perform nonlinear computations to control a physical system, which can typically be described by an hybrid automaton containing high-dimensional systems of nonlinear differential equations. To prove safety of such systems, one must compute all the reachable sets from a given initial position, which might be uncertain (its value is not p…
▽ More
Modern control-command systems often include controllers that perform nonlinear computations to control a physical system, which can typically be described by an hybrid automaton containing high-dimensional systems of nonlinear differential equations. To prove safety of such systems, one must compute all the reachable sets from a given initial position, which might be uncertain (its value is not precisely known). On linear hybrid systems, efficient and precise techniques exist, but they fail to handle nonlinear flows or jump conditions. In this article, we present a new tool name HySon which computes the flowpipes of both linear and nonlinear hybrid systems using guaranteed generalization of classical efficient numerical simulation methods, including with variable integration step-size. In particular, we present an algorithm for detecting discrete events based on guaranteed interpolation polynomials that turns out to be both precise and efficient. Illustrations of the techniques developed in this article are given on representative examples.
△ Less
Submitted 10 June, 2013;
originally announced June 2013.
-
A Non-Standard Semantics for Kahn Networks in Continuous Time
Authors:
Romain Beauxis,
Samuel Mimram
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…
▽ More
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.
△ Less
Submitted 25 August, 2011;
originally announced August 2011.
-
The Structure of First-Order Causality (extended version)
Authors:
Samuel Mimram
Abstract:
Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that i…
▽ More
Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that is strategies which actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. Here, we present an original methodology to achieve this task, which requires to combine advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model, by the means of generators and relations: those strategies can be generated from a finite set of atomic strategies and the equality between strategies admits a finite axiomatization, this equational structure corresponding to a polarized variation of the notion of bialgebra. This work thus bridges algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanized analysis of causality in programming languages.
△ Less
Submitted 25 January, 2011;
originally announced January 2011.
-
Computing Critical Pairs in 2-Dimensional Rewriting Systems
Authors:
Samuel Mimram
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 no…
▽ More
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.
△ Less
Submitted 19 April, 2010;
originally announced April 2010.
-
The Structure of First-Order Causality
Authors:
Samuel Mimram
Abstract:
Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that…
▽ More
Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that is strategies which actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. Here, we present an original methodology to achieve this task, which requires to combine advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model, by the means of generators and relations: those strategies can be generated from a finite set of atomic strategies and the equality between strategies admits a finite axiomatization, this equational structure corresponding to a polarized variation of the notion of bialgebra. This work thus bridges algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanized analysis of causality in programming languages.
△ Less
Submitted 27 August, 2009;
originally announced August 2009.
-
Presentation of a Game Semantics for First-Order Propositional Logic
Authors:
Samuel Mimram
Abstract:
Game semantics aim at describing the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. In this article, we introduce a game semantics for a fragment of first order propositional logic. One of the main difficulties that has to be faced when constructing such semantics is to make them precise by characterizing definable strategies - that is strate…
▽ More
Game semantics aim at describing the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. In this article, we introduce a game semantics for a fragment of first order propositional logic. One of the main difficulties that has to be faced when constructing such semantics is to make them precise by characterizing definable strategies - that is strategies which actually behave like a proof. This characterization is usually done by restricting to the model to strategies satisfying subtle combinatory conditions such as innocence, whose preservation under composition is often difficult to show. Here, we present an original methodology to achieve this task which requires to combine tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of definable strategies by the means of generators and relations: those strategies can be generated from a finite set of ``atomic'' strategies and that the equality between strategies generated in such a way admits a finite axiomatization. These generators satisfy laws which are a variation of bialgebras laws, thus bridging algebra and denotational semantics in a clean and unexpected way.
△ Less
Submitted 7 May, 2008;
originally announced May 2008.