-
Persistent homology of partially ordered spaces
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos
Abstract:
In this work, we explore links between natural homology and persistent homology for the classification of directed spaces. The former is an algebraic invariant of directed spaces, a semantic model of concurrent programs. The latter was developed in the context of topological data analysis, in which topological properties of point-cloud data sets are extracted while eliminating noise. In both appro…
▽ More
In this work, we explore links between natural homology and persistent homology for the classification of directed spaces. The former is an algebraic invariant of directed spaces, a semantic model of concurrent programs. The latter was developed in the context of topological data analysis, in which topological properties of point-cloud data sets are extracted while eliminating noise. In both approaches, the evolution homological properties are tracked through a sequence of inclusions of usual topological spaces. Exploiting this similarity, we show that natural homology may be considered a persistence object, and may be calculated as a colimit of uni-dimensional persistent homologies along traces. Finally, we suggest further links and avenues of future work in this direction.
△ Less
Submitted 6 August, 2024; v1 submitted 5 May, 2023;
originally announced May 2023.
-
Algebraic coherent confluence and higher globular Kleene algebras
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos,
Georg Struth
Abstract:
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We ins…
▽ More
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.
△ Less
Submitted 24 November, 2022; v1 submitted 29 June, 2020;
originally announced June 2020.
-
Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
Authors:
Cameron Calk,
Anupam Das,
Tim Waring
Abstract:
We propose a graph-based extension of Boolean logic called Boolean Graph Logic (BGL). Construing formula trees as the cotrees of cographs, we may state semantic notions such as evaluation and entailment in purely graph-theoretic terms, whence we recover the definition of BGL. Naturally, it is conservative over usual Boolean logic.
Our contributions are the following:
(1) We give a natural sema…
▽ More
We propose a graph-based extension of Boolean logic called Boolean Graph Logic (BGL). Construing formula trees as the cotrees of cographs, we may state semantic notions such as evaluation and entailment in purely graph-theoretic terms, whence we recover the definition of BGL. Naturally, it is conservative over usual Boolean logic.
Our contributions are the following:
(1) We give a natural semantics of BGL based on Boolean relations, i.e. it is a multivalued semantics, and show adequacy of this semantics for the corresponding notions of entailment. (2) We show that the complexity of evaluation is NP-complete for arbitrary graphs (as opposed to ALOGTIME-complete for formulas), while entailment is $Π^p_2$-complete (as opposed to coNP-complete for formulas). (3) We give a 'recursive' algorithm for evaluation by induction on the modular decomposition of graphs. (Though this is not polynomial-time, cf. point (2) above). (4) We characterise evaluation in a game-theoretic setting, in terms of both static and sequentical strategies, extending the classical notion of positional game forms beyond cographs. (5) We give an axiomatisation of BGL, inspired by deep-inference proof theory, and show soundness and completeness for the corresponding notions of entailment.
One particular feature of the graph-theoretic setting is that it escapes certain no-go theorems such as a recent result of Das and Strassburger, that there is no linear axiomatisation of the linear fragment of Boolean logic (equivalently the multiplicative fragment of Japaridze's Computability Logic or Blass' game semantics for Mutliplicative Linear Logic).
△ Less
Submitted 27 April, 2020;
originally announced April 2020.
-
Time-reversal homotopical properties of concurrent systems
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos
Abstract:
Directed topology was introduced as a model of concurrent programs, where the flow of time is described by distinguishing certain paths in the topological space representing such a program. Algebraic invariants which respect this directedness have been introduced to classify directed spaces. In this work we study the properties of such invariants with respect to the reversal of the flow of time in…
▽ More
Directed topology was introduced as a model of concurrent programs, where the flow of time is described by distinguishing certain paths in the topological space representing such a program. Algebraic invariants which respect this directedness have been introduced to classify directed spaces. In this work we study the properties of such invariants with respect to the reversal of the flow of time in directed spaces. Known invariants, natural homotopy and homology, have been shown to be unchanged under this time-reversal. We show that these can be equipped with additional algebraic structure witnessing this reversal. Specifically, when applied to a directed space and to its reversal, we show that these refined invariants yield dual objects. We further refine natural homotopy by introducing a notion of relative directed homotopy and showing the existence of a long exact sequence of natural homotopy systems.
△ Less
Submitted 12 December, 2018;
originally announced December 2018.
