Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDatatype defining rewrite systems for naturals and integers
31
0
0.0
(
0
)
Added by
Antoine Amarilli
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defines a term rewriting system that must be ground-complete. First we define two DDRSs for the ring of integers, each comprising twelve rewrite rules, and prove their ground-completeness. Then we introduce natural number and integer arithmetic specified according to unary view, that is, arithmetic based on a postfix unary append constructor (a form of tallying). Next we specify arithmetic based on two other views: binary and decimal notation. The binary and decimal view have as their characteristic that each normal form resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negat
rate research
Read More
We tackle the issue of representing infinite sets of real- valued vectors. This paper introduces an operator for combining integer and real sets. Using this operator, we decompose three well-known logics extending Presburger with reals. Our decomposition splits a logic into two parts : one integer, and one decimal (i.e. on the interval [0,1]). We also give a basis for an implementation of our representation.
We propose a system of equations that defines Weierstrass--Jacobis eta- and theta-constant series in a differentially closed way. This system is shown to have a direct relationship to a little-known dynamical system obtained by Jacobi. The classically known differential equations by Darboux--Halphen, Chazy, and Ramanujan are the differential consequences or reductions of these systems. The proposed system is shown to admit the Lagrangian, Hamiltonian, and Nambu formulations. We explicitly construct a pencil of nonlinear Poisson brackets and complete set of involutive conserved quantities. As byproducts of the theory, we exemplify conserved quantities for the Ramamani dynamical system and quadratic system of Halphen--Brioschi.
This paper deals with properties of the algebraic variety defined as the set of zeros of a typical sequence of polynomials. We consider various types of nice varieties: set-theoretic and ideal-theoretic complete intersections, absolutely irreducible ones, and nonsingular ones. For these types, we present a nonzero obstruction polynomial of explicitly bounded degree in the coefficients of the sequence that vanishes if its variety is not of the type. Over finite fields, this yields bounds on the number of such sequences. We also show that most sequences (of at least two polynomials) define a degenerate variety, namely an absolutely irreducible nonsingular hypersurface in some linear projective subspace.
Many compilers, synthesizers, and theorem provers rely on rewrite rules to simplify expressions or prove equivalences. Developing rewrite rules can be difficult: rules may be subtly incorrect, profitable rules are easy to miss, and rulesets must be rechecked or extended whenever semantics are tweaked. Large rulesets can also be challenging to apply: redundant rules slow down rule-based search and frustrate debugging. This paper explores how equality saturation, a promising technique that uses e-graphs to apply rewrite rules, can also be used to infer rewrite rules. E-graphs can compactly represent the exponentially large sets of enumerated terms and potential rewrite rules. We show that equality saturation efficiently shrinks both sets, leading to faster synthesis of smaller, more general rulesets. We prototyped these strategies in a tool dubbed ruler. Compared to a similar tool built on CVC4, ruler synthesizes 5.8X smaller rulesets 25X faster without compromising on proving power. In an end-to-end case study, we show ruler-synthesized rules which perform as well as those crafted by domain experts, and addressed a longstanding issue in a popular open source tool.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
