-
A collection of cancellative, singly aligned, non-embeddable monoids
Authors:
Milo Edwardes,
Daniel Heath
Abstract:
By classical results of Malcev, cancellative monoids need not be group-embeddable. In this paper, we describe and give presentations for and study an infinite family $\mathcal{M}_n$ of cancellative monoids which are not group-embeddable, originating from Malcev's original work. We show that $\mathcal{M}_n$ is singly aligned for $n \geq 2$, owing to applications in the study of $\mathrm{C}^*$-algeb…
▽ More
By classical results of Malcev, cancellative monoids need not be group-embeddable. In this paper, we describe and give presentations for and study an infinite family $\mathcal{M}_n$ of cancellative monoids which are not group-embeddable, originating from Malcev's original work. We show that $\mathcal{M}_n$ is singly aligned for $n \geq 2$, owing to applications in the study of $\mathrm{C}^*$-algebras by Brix, Bruce and Dor-On. We finish by showing that $\mathcal{M}_1$ is not singly aligned, but is $2$-aligned.
△ Less
Submitted 4 February, 2025; v1 submitted 30 May, 2024;
originally announced May 2024.
-
Pretzel monoids
Authors:
Daniel Heath,
Mark Kambites,
Nóra Szakács
Abstract:
We introduce an interesting class of left adequate monoids which we call pretzel monoids. These, on the one hand, are monoids of birooted graphs with respect to a natural `glue-and-fold' operation, and on the other hand, are shown to be defined in the category of left adequate monoids by a natural class of presentations. They are also shown to be the free idempotent-pure expansions of right cancel…
▽ More
We introduce an interesting class of left adequate monoids which we call pretzel monoids. These, on the one hand, are monoids of birooted graphs with respect to a natural `glue-and-fold' operation, and on the other hand, are shown to be defined in the category of left adequate monoids by a natural class of presentations. They are also shown to be the free idempotent-pure expansions of right cancellative monoids, making them, in some sense, the left adequate analogues of Margolis-Meakin expansions for inverse monoids. The construction recovers the second author's geometric model of free left adequate monoids when the right cancellative monoid is free.
△ Less
Submitted 1 May, 2024;
originally announced May 2024.
-
Dynamic Interface Printing
Authors:
Callum Vidler,
Michael Halwes,
Kirill Kolesnik,
Philipp Segeritz,
Matthew Mail,
Anders J. Barlow,
Emmanuelle M. Koehl,
Anand Ramakrishnan,
Daniel J. Scott,
Daniel E. Heath,
Kenneth B. Crozier,
David J. Collins
Abstract:
Additive manufacturing is an expanding multidisciplinary field encompassing applications including medical devices, aerospace components, microfabrication strategies, and artificial organs. Among additive manufacturing approaches, light-based printing technologies, including two-photon polymerization, projection micro stereolithography, and volumetric printing, have garnered significant attention…
▽ More
Additive manufacturing is an expanding multidisciplinary field encompassing applications including medical devices, aerospace components, microfabrication strategies, and artificial organs. Among additive manufacturing approaches, light-based printing technologies, including two-photon polymerization, projection micro stereolithography, and volumetric printing, have garnered significant attention due to their speed, resolution and/or potential applications for biofabrication. In this study, we introduce dynamic interface printing (DIP), a new 3D printing approach that leverages an acoustically modulated, constrained air-liquid boundary to rapidly generate cm-scale three-dimensional structures within tens of seconds. Distinct from volumetric approaches, this process eliminates the need for intricate feedback systems, specialized chemistry, or complex optics while maintaining rapid printing speeds. We demonstrate the versatility of this technique across a broad array of materials and intricate geometries, including those that would be impossible to print via conventional layer-by-layer methods. In doing so, we demonstrate the rapid fabrication of complex structures in-situ, overprinting, structural parallelisation, and biofabrication utility. Moreover, we showcase that the formation of surface waves at this boundary enables enhanced mass transport, material flexibility, and permits three-dimensional particle patterning. We therefore anticipate that this approach will be invaluable for applications where high resolution, scalable throughput, and biocompatible printing is required.
△ Less
Submitted 30 July, 2024; v1 submitted 22 March, 2024;
originally announced March 2024.
-
Parallel RAM from Cyclic Circuits
Authors:
David Heath
Abstract:
Known simulations of random access machines (RAMs) or parallel RAMs (PRAMs) by Boolean circuits incur significant polynomial blowup, due to the need to repeatedly simulate accesses to a large main memory.
Consider a single modification to Boolean circuits that removes the restriction that circuit graphs are acyclic. We call this the cyclic circuit model. Note, cyclic circuits remain combinationa…
▽ More
Known simulations of random access machines (RAMs) or parallel RAMs (PRAMs) by Boolean circuits incur significant polynomial blowup, due to the need to repeatedly simulate accesses to a large main memory.
Consider a single modification to Boolean circuits that removes the restriction that circuit graphs are acyclic. We call this the cyclic circuit model. Note, cyclic circuits remain combinational, as they do not allow wire values to change over time.
We simulate PRAM with a cyclic circuit, and the blowup from our simulation is only polylogarithmic. Consider a PRAM program $P$ that on a length-$n$ input uses an arbitrary number of processors to manipulate words of size $Θ(\log n)$ bits and then halts within $W(n)$ work. We construct a size-$O(W(n)\cdot \log^4 n)$ cyclic circuit that simulates $P$. Suppose that on a particular input, $P$ halts in time $T$; our circuit computes the same output within $T \cdot O(\log^3 n)$ gate delay.
This implies theoretical feasibility of powerful parallel machines. Cyclic circuits can be implemented in hardware, and our circuit achieves performance within polylog factors of PRAM. Our simulated PRAM synchronizes processors via logical dependencies between wires.
△ Less
Submitted 27 October, 2023; v1 submitted 10 September, 2023;
originally announced September 2023.
-
Symphony: Expressive Secure Multiparty Computation with Coordination
Authors:
Ian Sweet,
David Darais,
David Heath,
William Harris,
Ryan Estes,
Michael Hicks
Abstract:
Context: Secure Multiparty Computation (MPC) refers to a family of cryptographic techniques where mutually untrusting parties may compute functions of their private inputs while revealing only the function output.
Inquiry: It can be hard to program MPCs correctly and efficiently using existing languages and frameworks, especially when they require coordinating disparate computational roles. How…
▽ More
Context: Secure Multiparty Computation (MPC) refers to a family of cryptographic techniques where mutually untrusting parties may compute functions of their private inputs while revealing only the function output.
Inquiry: It can be hard to program MPCs correctly and efficiently using existing languages and frameworks, especially when they require coordinating disparate computational roles. How can we make this easier?
Approach: We present Symphony, a new functional programming language for MPCs among two or more parties. Symphony starts from the single-instruction, multiple-data (SIMD) semantics of prior MPC languages, in which each party carries out symmetric responsibilities, and generalizes it using constructs that can coordinate many parties. Symphony introduces **first-class shares** and **first-class party sets** to provide unmatched language-level expressive power with high efficiency.
Knowledge: Developing a core formal language called $λ$-Symphony, we prove that the intuitive, generalized SIMD view of a program coincides with its actual distributed semantics. Thus the programmer can reason about her programs by reading them from top to bottom, even though in reality the program runs in a coordinated fashion, distributed across many machines. We implemented a prototype interpreter for Symphony leveraging multiple cryptographic backends. With it we wrote a variety of MPC programs, finding that Symphony can express optimized protocols that other languages cannot, and that in general Symphony programs operate efficiently.
[ full abstract at https://doi.org/10.22152/programming-journal.org/2023/7/14 ]
△ Less
Submitted 20 February, 2023;
originally announced February 2023.
-
Relational Verification via Invariant-Guided Synchronization
Authors:
Qi Zhou,
David Heath,
William Harris
Abstract:
Relational properties describe relationships that hold over multiple executions of one or more programs, such as functional equivalence. Conventional approaches for automatically verifying such properties typically rely on syntax-based, heuristic strategies for finding synchronization points among the input programs. These synchronization points are then annotated with appropriate relational invar…
▽ More
Relational properties describe relationships that hold over multiple executions of one or more programs, such as functional equivalence. Conventional approaches for automatically verifying such properties typically rely on syntax-based, heuristic strategies for finding synchronization points among the input programs. These synchronization points are then annotated with appropriate relational invariants to complete the proof. However, when suboptimal synchronization points are chosen the required invariants can be complicated or even inexpressible in the target theory.
In this work, we propose a novel approach to verifying relational properties. This approach searches for synchronization points and synthesizes relational invariants simultaneously. Specifically, the approach uses synthesized invariants as a guide for finding proper synchronization points that lead to a complete proof. We implemented our approach as a tool named PEQUOD, which targets Java Virtual Machine (JVM) bytecode. We evaluated PEQUOD by using it to solve verification challenges drawn from the from the research literature and by verifying properties of student-submitted solutions to online challenge problems. The results show that PEQUOD solve verification problems that cannot be addressed by current techniques.
△ Less
Submitted 9 July, 2019;
originally announced July 2019.
-
Large Scale Scene Text Verification with Guided Attention
Authors:
Dafang He,
Yeqing Li,
Alexander Gorban,
Derrall Heath,
Julian Ibarz,
Qian Yu,
Daniel Kifer,
C. Lee Giles
Abstract:
Many tasks are related to determining if a particular text string exists in an image. In this work, we propose a new framework that learns this task in an end-to-end way. The framework takes an image and a text string as input and then outputs the probability of the text string being present in the image. This is the first end-to-end framework that learns such relationships between text and images…
▽ More
Many tasks are related to determining if a particular text string exists in an image. In this work, we propose a new framework that learns this task in an end-to-end way. The framework takes an image and a text string as input and then outputs the probability of the text string being present in the image. This is the first end-to-end framework that learns such relationships between text and images in scene text area. The framework does not require explicit scene text detection or recognition and thus no bounding box annotations are needed for it. It is also the first work in scene text area that tackles suh a weakly labeled problem. Based on this framework, we developed a model called Guided Attention. Our designed model achieves much better results than several state-of-the-art scene text reading based solutions for a challenging Street View Business Matching task. The task tries to find correct business names for storefront images and the dataset we collected for it is substantially larger, and more challenging than existing scene text dataset. This new real-world task provides a new perspective for studying scene text related problems. We also demonstrate the uniqueness of our task via a comparison between our problem and a typical Visual Question Answering problem.
△ Less
Submitted 18 November, 2018; v1 submitted 23 April, 2018;
originally announced April 2018.
-
Proofs as Relational Invariants of Synthesized Execution Grammars
Authors:
Caleb Voss,
David Heath,
William Harris
Abstract:
The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synthesize invariants that only describe data structures of heavily restricted forms, or require an analyst to provide predicates over program data and structure that are used in a synthesized proof of correctness.
In this…
▽ More
The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synthesize invariants that only describe data structures of heavily restricted forms, or require an analyst to provide predicates over program data and structure that are used in a synthesized proof of correctness.
In this work, we introduce a novel automatic safety verifier of programs that maintain low-level data structures, named LTTP. LTTP synthesizes proofs of program safety represented as a grammar of a given program's control paths, annotated with invariants that relate program state at distinct points within its path of execution. LTTP synthesizes such proofs completely automatically, using a novel inductive-synthesis algorithm.
We have implemented LTTP as a verifier for JVM bytecode and applied it to verify the safety of a collection of verification benchmarks. Our results demonstrate that LTTP can be applied to automatically verify the safety of programs that are beyond the scope of previously-developed verifiers.
△ Less
Submitted 9 October, 2017;
originally announced October 2017.
-
Topological Symmetry Groups of the Petersen Graph
Authors:
D. Chambers,
E. Flapan,
D. Heath,
E. Davie Lawrence,
C. Thatcher,
R. Vanderpool
Abstract:
We characterize all groups which can occur as the topological symmetry group or the orientation preserving topological symmetry group of some embedding of the Petersen graph in S^3.
We characterize all groups which can occur as the topological symmetry group or the orientation preserving topological symmetry group of some embedding of the Petersen graph in S^3.
△ Less
Submitted 5 October, 2017;
originally announced October 2017.
-
Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Authors:
Qi Zhou,
David Heath,
William Harris
Abstract:
Recursion-free Constrained Horn Clauses (CHCs) are logic-programming problems that can model safety properties of programs with bounded iteration and recursion. In addition, many CHC solvers reduce recursive systems to a series of recursion-free CHC systems that can each be solved efficiently.
In this paper, we define a novel class of recursion-free systems, named Clause-Dependence Disjoint (CDD…
▽ More
Recursion-free Constrained Horn Clauses (CHCs) are logic-programming problems that can model safety properties of programs with bounded iteration and recursion. In addition, many CHC solvers reduce recursive systems to a series of recursion-free CHC systems that can each be solved efficiently.
In this paper, we define a novel class of recursion-free systems, named Clause-Dependence Disjoint (CDD), that generalizes classes defined in previous work. The advantage of this class is that many CDD systems are smaller than systems which express the same constraints but are part of a different class. This advantage in size allows CDD systems to be solved more efficiently than their counterparts in other classes. We implemented a CHC solver named Shara. Shara solves arbitrary CHC systems by reducing the input to a series of CDD systems. Our evaluation indicates that Shara outperforms state-of-the-art implementations in many practical cases.
△ Less
Submitted 14 September, 2018; v1 submitted 8 May, 2017;
originally announced May 2017.
-
Completely Automated Equivalence Proofs
Authors:
Qi Zhou,
David Heath,
William Harris
Abstract:
Verifying partial (i.e., termination-insensitive) equivalence of programs has significant practical applications in software development and education. Conventional equivalence verifiers typically rely on a combination of given relational summaries and suggested synchronization points; such information can be extremely difficult for programmers without a background in formal methods to provide for…
▽ More
Verifying partial (i.e., termination-insensitive) equivalence of programs has significant practical applications in software development and education. Conventional equivalence verifiers typically rely on a combination of given relational summaries and suggested synchronization points; such information can be extremely difficult for programmers without a background in formal methods to provide for pairs of programs with dissimilar logic.
In this work, we propose a completely automated verifier for determining partial equivalence, named Pequod. Pequod automatically synthesizes expressive proofs of equivalence conventionally only achievable via careful, manual constructions of product programs To do so, Pequod syntheses relational proofs for selected pairs of program paths and combines the per-path relational proofs to synthesize relational program invariants. To evaluate Pequod, we implemented it as a tool that targets Java Virtual Machine bytecode and applied it to verify the equivalence of hundreds of pairs of solutions submitted by students for problems hosted on popular online coding platforms, most of which could not be verified by existing techniques.
△ Less
Submitted 8 May, 2017;
originally announced May 2017.
-
Chemical enrichment of the intracluster medium by FR II radio sources
Authors:
David Heath,
Martin Krause,
Paul Alexander
Abstract:
We present 2D axisymmetric hydrodynamic simulations investigating the long term effect of FR II radio galaxies on the metal distribution of the surrounding intra-cluster medium (ICM). A light jet is injected into a cooling flow atmosphere for 10-30 Myr. We then follow the subsequent evolution for 3 Gyr on a spherical grid spanning 3 Mpc in radius. A series of passive tracer particles were placed…
▽ More
We present 2D axisymmetric hydrodynamic simulations investigating the long term effect of FR II radio galaxies on the metal distribution of the surrounding intra-cluster medium (ICM). A light jet is injected into a cooling flow atmosphere for 10-30 Myr. We then follow the subsequent evolution for 3 Gyr on a spherical grid spanning 3 Mpc in radius. A series of passive tracer particles were placed in an annulus about the cluster core to simulate metal carrying clouds in order to calculate the metallicity (Z) as a function of time and radial distance from the cluster centre. The jet has a significant effect on the ICM over the entire 3 Gyr period. By the end of the simulations, the jets produced metallicities of ~10% of the initial metallicity of the cluster core throughout much of the cluster. The jets transport the metals not only in mixing regions, but also through upwelling ICM behind the jet, enriching the cluster over both long and short distances.
△ Less
Submitted 13 December, 2006; v1 submitted 11 October, 2006;
originally announced October 2006.
-
A search method for thin positions of links
Authors:
Daniel J. Heath,
Tsuyoshi Kobayashi
Abstract:
We give a method for searching for thin positions of a given link.
We give a method for searching for thin positions of a given link.
△ Less
Submitted 4 September, 2005; v1 submitted 1 August, 2004;
originally announced August 2004.
