An official website of the United States government
Algorithms for computing congruence closure of ground equations overuninterpreted symbols and interpreted symbols satisfying associativity andcommutativity (AC) properties are proposed. The algorithms are based on aframework for computing a congruence closure by abstracting nonflat terms byconstants as proposed first in Kapur's congruence closure algorithm (RTA97).The framework is general, flexible, and has been extended also to developcongruence closure algorithms for the cases when associative-commutativefunction symbols can have additional properties including idempotency,nilpotency, identities, cancellativity and group properties as well as theirvarious combinations. Algorithms are modular; their correctness and terminationproofs are simple, exploiting modularity. Unlike earlier algorithms, theproposed algorithms neither rely on complex AC compatible well-foundedorderings on nonvariable terms nor need to use the associative-commutativeunification and extension rules in completion for generating canonical rewritesystems for congruence closures. They are particularly suited for integratinginto the Satisfiability modulo Theories (SMT) solvers. A new way to viewGroebner basis algorithm for polynomial ideals with integer coefficients as acombination of the congruence closures over the AC symbol * with the identity 1and the congruence closure over an Abelian group with + is outlined.
more »
« less
Congruence modules in higher codimension and zeta lines in Galois cohomology
This article builds on recent work of the first three authors where a notion of congruence modules in higher codimension is introduced. The main results are a criterion for detecting regularity of local rings in terms of congruence modules, and a more refined version of a result tracking the change of congruence modules under deformation. Number theoretic applications include the construction of canonical lines in certain Galois cohomology groups arising from adjoint motives of Hilbert modular forms.
more »
« less
- Award ID(s):
- 2001368
- PAR ID:
- 10504618
- Publisher / Repository:
- Proc. Nat. Acad. Sci.
- Date Published:
- Journal Name:
- Proceedings of the National Academy of Sciences
- Volume:
- 121
- Issue:
- 17
- ISSN:
- 0027-8424
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Undergraduate mathematics instructors are called by recent standards to promote prospective teachers’ learning of a transformation approach in geometry and its proofs. The novelty of this situation means it is unclear what is involved in prospective teachers’ learning of geometry from a transformation perspective, particularly if they learned geometry from an approach based on the Elements; hence undergraduate instructors may need support in this area. To begin to approach this problem, we analyze the prospective teachers’ use of the conceptual link between congruence and transformation in the context of congruence. We identify several key actions involved in using the definition of congruence in congruence proofs, and we look at ways in which several of these actions are independent of each other, hence pointing to concepts and actions that may need to be specifically addressed in instruction.more » « less
-
Abstract The evolutionary fate of multi-strain pathogens is shaped by host-pathogen ecological interactions. In bacterial pathogens of plants, enhanced strain characterization and advances in our understanding of molecular mechanisms underlying defense pathways open the door for revisiting the role of negative frequency-dependent selection (NFDS) in strain structure, including its interplay with genetic exchange. NFDS arising from specific defense is one potential mechanism for generating, maintaining, and structuring pathogen diversity. In plants, specific protection against microbial pathogens involves Resistance proteins (R-proteins) that recognize virulence factors (effectors) secreted by pathogens, typically to subvert the initial line of host defense. Here we formulate a stochastic computational co-evolution model that explicitly incorporates variable length R-gene and effector repertoires, and migration from their regional pools. We use this model to understand potential mechanisms shaping effector repertoire structure and associated strain coexistence in the generalist plant pathogenP. syringae. The demonstration of a modular structure in our numerical simulations motivates the analysis of genome sequences from 76 strains collected in the Midwestern US and 1104 strains from global sources. We find that effector repertories both locally and globally exhibit a modular structure, with higher similarity within than between clusters. The observed modules are consistent with the core genome phylogeny and are unexplained by plant host species, location of isolation, and genetic linkage between effectors. An extension of the model is needed to take into account the evidence for genetic exchange and the phylogenetic congruence of effector modules. We initialize the system with a phylogenetically congruent modular structure and include recombination rates decreasing as a function of phylogenetic distance. We show that NFDS can counter-balance the effects of mixing due to recombination and in so doing, contributes to the maintenance of strain structure. These findings indicate that the observed similarity clusters may constitute, in part, emergent niches arising from eco-evolutionary dynamics that contribute to strain coexistence.more » « less
-
Kobayashi, Naoki (Ed.)Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing the congruence closure by abstracting nonflat terms by constants as proposed first in Kapur’s congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combinations. The algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into Satisfiability modulo Theories (SMT) solvers.more » « less
-
Abstract Cut-and-paste $$K$$-theory has recently emerged as an important variant of higher algebraic $$K$$-theory. However, many of the powerful tools used to study classical higher algebraic $$K$$-theory do not yet have analogues in the cut-and-paste setting. In particular, there does not yet exist a sensible notion of the Dennis trace for cut-and-paste $$K$$-theory. In this paper we address the particular case of the $$K$$-theory of polyhedra, also called scissors congruence $$K$$-theory. We introduce an explicit, computable trace map from the higher scissors congruence groups to group homology, and use this trace to prove the existence of some nonzero classes in the higher scissors congruence groups. We also show that the $$K$$-theory of polyhedra is a homotopy orbit spectrum. This fits into Thomason’s general framework of $$K$$-theory commuting with homotopy colimits, but we give a self-contained proof. We then use this result to re-interpret the trace map as a partial inverse to the map that commutes homotopy orbits with algebraic $$K$$-theory.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1073/pnas.2320608121
