-
Tight limits and completions from Dedekind-MacNeille to Lambek-Isbell
Authors:
Dusko Pavlovic,
Dominic J. D. Hughes
Abstract:
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 th…
▽ More
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.
△ Less
Submitted 20 April, 2022;
originally announced April 2022.
-
Nucleus I: Adjunction spectra in recommender systems and descent
Authors:
Dusko Pavlovic,
Dominic J. D. Hughes
Abstract:
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 t…
▽ More
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.
△ Less
Submitted 21 October, 2023; v1 submitted 15 April, 2020;
originally announced April 2020.
-
First-order proofs without syntax
Authors:
Dominic J. D. Hughes
Abstract:
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…
▽ More
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.
△ Less
Submitted 26 June, 2019;
originally announced June 2019.
-
Unification nets: canonical proof net quantifiers
Authors:
Dominic J. D. Hughes
Abstract:
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 u…
▽ More
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.
△ Less
Submitted 9 February, 2018;
originally announced February 2018.
-
WSClean: an implementation of a fast, generic wide-field imager for radio astronomy
Authors:
A. R. Offringa,
B. McKinley,
N. Hurley-Walker,
F. H. Briggs,
R. B. Wayth,
D. L. Kaplan,
M. E. Bell,
L. Feng,
A. R. Neben,
J. D. Hughes,
J. Rhee,
T. Murphy,
N. D. R. Bhat,
G. Bernardi,
J. D. Bowman,
R. J. Cappallo,
B. E. Corey,
A. A. Deshpande,
D. Emrich,
A. Ewall-Wice,
B. M. Gaensler,
R. Goeke,
L. J. Greenhill,
B. J. Hazelton,
L. Hindson
, et al. (28 additional authors not shown)
Abstract:
Astronomical widefield imaging of interferometric radio data is computationally expensive, especially for the large data volumes created by modern non-coplanar many-element arrays. We present a new widefield interferometric imager that uses the w-stacking algorithm and can make use of the w-snapshot algorithm. The performance dependencies of CASA's w-projection and our new imager are analysed and…
▽ More
Astronomical widefield imaging of interferometric radio data is computationally expensive, especially for the large data volumes created by modern non-coplanar many-element arrays. We present a new widefield interferometric imager that uses the w-stacking algorithm and can make use of the w-snapshot algorithm. The performance dependencies of CASA's w-projection and our new imager are analysed and analytical functions are derived that describe the required computing cost for both imagers. On data from the Murchison Widefield Array, we find our new method to be an order of magnitude faster than w-projection, as well as being capable of full-sky imaging at full resolution and with correct polarisation correction. We predict the computing costs for several other arrays and estimate that our imager is a factor of 2-12 faster, depending on the array configuration. We estimate the computing cost for imaging the low-frequency Square-Kilometre Array observations to be 60 PetaFLOPS with current techniques. We find that combining w-stacking with the w-snapshot algorithm does not significantly improve computing requirements over pure w-stacking. The source code of our new imager is publicly released.
△ Less
Submitted 7 July, 2014;
originally announced July 2014.
-
Is Wolfram and Cook's (2,5) Turing machine really universal?
Authors:
Dominic J. D. Hughes
Abstract:
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.
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.
△ Less
Submitted 30 August, 2012;
originally announced August 2012.
-
Linking diagrams for free
Authors:
Dominic J. D. Hughes
Abstract:
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 mono…
▽ More
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.
△ Less
Submitted 11 May, 2008;
originally announced May 2008.
-
Abstract p-time proof nets for MALL: Conflict nets
Authors:
Dominic J. D. Hughes
Abstract:
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 wer…
▽ More
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.
△ Less
Submitted 15 January, 2008;
originally announced January 2008.
