**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.

Concept# Rewriting

Summary

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
Rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable. Rewriting systems then do not provide an algorithm for changing one term to another, but a set of possible rule applications. When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer programs, and several theorem provers and declarative programming languages are based on term rewriting.
In logic, the procedure for obtaining the conjunctive normal form (CNF) of a formula can be implemented as a rewriting system. The rules of an example of such a system would be:
(double negation elimination)
(De Morgan's laws)
(distributivity)
where the symbol () indicates that an expression matching the left hand side of the rule can be rewritten to one formed by the right hand side, and the symbols each denote a subexpression. In such a system, each rule is chosen so that the left side is equivalent to the right side, and consequently when the left side matches a subexpression, performing a rewrite of that subexpression from left to right maintains logical consistency and value of the entire expression.
Term rewriting systems can be employed to compute arithmetic operations on natural numbers.
To this end, each such number has to be encoded as a term.
The simplest encoding is the one used in the Peano axioms, based on the constant 0 (zero) and the successor function S. For example, the numbers 0, 1, 2, and 3 are represented by the terms 0, S(0), S(S(0)), and S(S(S(0))), respectively.
The following term rewriting system can then be used to compute sum and product of given natural numbers.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (16)

Related courses (11)

Related publications (32)

Related people (4)

Related lectures (37)

Formal grammar

In formal language theory, a grammar (when the context is not given, often called a formal grammar for clarity) describes how to form strings from a language's alphabet that are valid according to the language's syntax. A grammar does not describe the meaning of the strings or what can be done with them in whatever context—only their form. A formal grammar is defined as a set of production rules for such strings in a formal language. Formal language theory, the discipline that studies formal grammars and languages, is a branch of applied mathematics.

Abstract rewriting system

In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set (of "objects") together with a binary relation, traditionally denoted with ; this definition can be further refined if we index (label) subsets of the binary relation.

Confluence (abstract rewriting)

In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system. The usual rules of elementary arithmetic form an abstract rewriting system. For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is eventually obtained.

ME-411: Mechanics of slender structures

Analysis of the mechanical response and deformation of slender structural elements.

FIN-609: Asset Pricing (2011 - 2024)

This course provides an overview of the theory of asset pricing and portfolio choice theory following historical developments in the field and putting
emphasis on theoretical models that help our unde

PHYS-425: Quantum physics III

To introduce several advanced topics in quantum physics, including
semiclassical approximation, path integral, scattering theory, and
relativistic quantum mechanics

Value Definitions and Conditionals

Covers conditional and Boolean expressions, rewrite rules, and value definitions.

Fourier Transform and Large N Limit

Explores Fourier transform and large N limit applications in survival properties and return amplitudes.

Termination Analysis using Dependency Pairs

Explores automated termination analysis using dependency pairs, covering classical and modern techniques, annual competitions, and tools like AProVE.

Giovanni De Micheli, Alessandro Tempia Calvino

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

2024,

We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomo ...

Giovanni De Micheli, Alessandro Tempia Calvino, Heinz Riener, Shubham Rai, Akash Kumar

Individual transistors based on emerging reconfigurable nanotechnologies exhibit electrical conduction for both types of charge carriers. These transistors (referred to as Reconfigurable Field-Effect Transistors (RFETs)) enable dynamic reconfiguration to d ...

2022