Version control systems typically rely on apatch language, heuristicpatch synthesis algorithmslike diff, andthree-way merge algorithms. Standard patch languages and merge algorithms often fail to identify conflicts correctly when there are multiple edits to one line of code or code is relocated. This paper introduces Grove, a collaborative structure editor calculus that eliminates patch synthesis and three-way merge algorithms entirely. Instead, patches are derived directly from the log of the developer’s edit actions and all edits commute, i.e. the repository state forms a commutative replicated data type (CmRDT). To handle conflicts that can arise due to code relocation, the core datatype in Grove is a labeled directed multi-graph with uniquely identified vertices and edges. All edits amount to edge insertion and deletion, with deletion being permanent. To support tree-based editing, we define a decomposition from graphs intogroves, which are a set of syntax trees with conflicts—including local, relocation, and unicyclic relocation conflicts—represented explicitly using holes and references between trees. Finally, we define a type error localization system for groves that enjoys atotalityproperty, i.e. all editor states in Grove are statically meaningful, so developers can use standard editor services while working to resolve these explicitly represented conflicts. The static semantics is defined as a bidirectional marking system in line with recent work, with gradual typing employed to handle situations where errors and conflicts prevent type determination. We then layer on a unification-based type inference system to opportunistically fill type holes and fail gracefully when no solution exists. We mechanize the metatheory of Grove using the Agda theorem prover. We implement these ideas as theGrove Workbench, which generates the necessary data structures and algorithms in OCaml given a syntax tree specification.
more »
« less
Electrical networks and the grove algebra
Abstract We study the ring of regular functions on the space of planar electrical networks, which we coin thegrove algebra. This algebra is an electrical analog of the Plücker ring studied classically in invariant theory. We develop the combinatorics of double groves to study the grove algebra, and find a quadratic Gröbner basis for the grove ideal.
more »
« less
- Award ID(s):
- 1953852
- PAR ID:
- 10574703
- Publisher / Repository:
- Cambridge University Press
- Date Published:
- Journal Name:
- Canadian Journal of Mathematics
- ISSN:
- 0008-414X
- Page Range / eLocation ID:
- 1 to 34
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Zeev Rudnick (Ed.)Abstract We introduce the ozone group of a noncommutative algebra $$A$$, defined as the group of automorphisms of $$A$$, which fix every element of its center. In order to initiate the study of ozone groups, we study polynomial identity (PI) skew polynomial rings, which have long proved to be a fertile testing ground in noncommutative algebra. Using the ozone group and other invariants defined herein, we give explicit conditions for the center of a PI skew polynomial ring to be Gorenstein (resp. regular) in low dimension.more » « less
-
Abstract Inspired by methods in prime characteristic in commutative algebra, we introduce and study combinatorial invariants of seminormal monoids. We relate such numbers with the singularities and homological invariants of the semigroup ring associated to the monoid. Our results are characteristic independent.more » « less
-
Abstract We develop and study a generalization of commutative rings calledbands, along with the corresponding geometric theory ofband schemes. Bands generalize both hyperrings, in the sense of Krasner, and partial fields in the sense of Semple and Whittle. They form a ring‐like counterpart to the field‐like category ofidyllsintroduced by the first and third authors in the previous work. The first part of the paper is dedicated to establishing fundamental properties of bands analogous to basic facts in commutative algebra. In particular, we introduce various kinds of ideals in a band and explore their properties, and we study localization, quotients, limits, and colimits. The second part of the paper studies band schemes. After giving the definition, we present some examples of band schemes, along with basic properties of band schemes and morphisms thereof, and we describe functors into some other scheme theories. In the third part, we discuss some “visualizations” of band schemes, which are different topological spaces that one can functorially associate to a band scheme .more » « less
-
Abstract Motivated by recent work on the use of topological methods to study collections of rings between an integral domain and its quotient field, we examine spaces of subrings of a commutative ring, endowed with the Zariski or patch topologies. We introduce three notions to study such a space : patch bundles, patch presheaves and patch algebras. When is compact and Hausdorff, patch bundles give a way to approximate with topologically more tractable spaces, namely Stone spaces. Patch presheaves encode the space into stalks of a presheaf of rings over a Boolean algebra, thus giving a more geometrical setting for studying . To both objects, a patch bundle and a patch presheaf, we associate what we call a patch algebra, a commutative ring that efficiently realizes the rings in as factor rings, or even localizations, and whose structure reflects various properties of the rings in .more » « less
An official website of the United States government

