arXiv subjects

Dominic J. D. Hughes

Publications and source records attributed to Dominic J. D. Hughes.

7 recordsLinked to original sources

arXiv2023

Nucleus I: Adjunction spectra in recommender systems and descent

Recommender systems build user profiles using concept analysis of usage matrices. The concepts are mined as spectra and form Galois connections. Descent is a general method for spectral decomposition in algebraic geometry and topology which also leads to generalized Galois connections. Both recommender systems and descent theory are vast research areas, separated by a technical gap so large that trying to establish a link would seem foolish. Yet a formal link emerged, all on its own, bottom-up, against authors' intentions and better judgment. Familiar problems of data analysis led to a novel solution in category theory. The present paper arose from a series of earlier efforts to provide a top-down account of these developments.

math.CT↗

arXiv2022

Tight limits and completions from Dedekind-MacNeille to Lambek-Isbell

While any infimum in a poset can also be computed as a supremum, and vice versa, categorical limits and colimits do not always approximate each other. If I approach a point from below, and you approach it from above, then we will surely meet if we live in a poset, but we may miss each other in a category. Can we characterize the limits and the colimits that approximate each other, and guarantee that we will meet? Such limits and colimits are called *tight*. Some critically important network applications depend on them. This paper characterizes tight limits and colimits, and describes tight completions, derived by applying the nucleus construction to adjunctions between loose completions. Just as the Dedekind-MacNeille completion of a poset preserves any existing infima and suprema, the tight completion of a category preserves any existing tight limits and colimits and is therefore idempotent.

math.CT↗

arXiv2019

First-order proofs without syntax

Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula $ϕ$ as a lax fibration over a graph associated with $ϕ$. The main theorem is soundness and completeness: a formula is a valid if and only if it has a combinatorial proof.

math.LO↗

arXiv2018

Unification nets: canonical proof net quantifiers

Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard's extension to MLL1 (first-order MLL) fails to be canonical because of redundant existential witnesses, and present canonical MLL1 proof nets called unification nets without them. For example, while there are infinitely many cut-free Girard nets $\forall x Px \vdash \exists xPx$, one per arbitrary choice of witness for $\exists x$, there is a unique cut-free unification net, with no specified witness. Redundant existential witnesses cause Girard's MLL1 nets to suffer from severe complexity issues: (1) cut elimination is non-local and exponential-time (and -space), and (2) some sequents require exponentially large cut-free Girard nets. Unification nets solve both problems: (1) cut elimination is local and linear-time, and (2) cut-free unification nets grow linearly with the size of the sequent. Since some unification nets are exponentially smaller than corresponding Girard nets and sequent proofs, technical delicacy is required to ensure correctness is polynomial-time (quadratic). These results extend beyond MLL1 via a broader methodological insight: for canonical quantifiers, the standard parallel/sequential dichotomy of proof nets fails; an implicit/explicit witness dichotomy is also needed. Work in progress extends unification nets to additives and uses them to extend combinatorial proofs [Proofs without syntax, Annals of Mathematics, 2006] to classical first-order logic.

math.LO↗

arXiv2012

Is Wolfram and Cook's (2,5) Turing machine really universal?

Wolfram [2, p. 707] and Cook [1, p. 3] claim to prove that a (2,5) Turing machine (2 states, 5 symbols) is universal, via a universal cellular automaton known as Rule 110. The first part of this paper points out a critical gap in their argument. The second part bridges the gap, thereby giving what appears to be the first proof of universality.

cs.FL↗

arXiv2008

Linking diagrams for free

Linking diagrams with path composition are ubiquitous, for example: Temperley-Lieb and Brauer monoids, Kelly-Laplaza graphs for compact closed categories, and Girard's multiplicative proof nets. We construct the category Link=Span(iRel), where iRel is the category of injective relations (reversed partial functions) and show that the aforementioned linkings, as well as Jones-Martin partition monoids, reside inside Link. Path composition, including collection of loops, is by pullback. Link contains the free compact closed category on a self-dual object (hence also the looped Brauer and Temperly-Lieb monoids), and generalises partition monoids with partiality (vertices in no partition) and empty- and infinite partitions. Thus we obtain conventional linking/partition diagrams and their composition "for free", from iRel.

math.CT↗

arXiv2008

Abstract p-time proof nets for MALL: Conflict nets

This paper presents proof nets for multiplicative-additive linear logic (MALL), called conflict nets. They are efficient, since both correctness and translation from a proof are p-time (polynomial time), and abstract, since they are invariant under transposing adjacent &-rules. A conflict net on a sequent is concise: axiom links with a conflict relation. Conflict nets are a variant of (and were inspired by) combinatorial proofs introduced recently for classical logic: each can be viewed as a maximal map (homomorphism) of contractible coherence spaces (P_4-free graphs, or cographs), from axioms to sequent. The paper presents new results for other proof nets: (1) correctness and cut elimination for slice nets (Hughes / van Glabbeek 2003) are p-time, and (2) the cut elimination proposed for monomial nets (Girard 1996) does not work. The subtleties which break monomial net cut elimination also apply to conflict nets: as with monomial nets, existence of a confluent cut elimination remains an open question.

math.LO↗