11

I am not sure that this will bring you more than you already know. But then, I may fail to understand the reasons that make you wonder about term rewriting. It does help. As you may know, grammars are string rewriting systems. At the top of the Chomsky hierarchy, you have type 0 grammars, which define recursively enumerable (RE) anguages, and have the ...


11

Term rewriting is a rewriting formalism. Starting with a term we rewrite the term according to the term rewriting rules until a normal form is found. Unification is finding a solution (substitution with specific properties) to a problem (a pair of terms). Term rewriting uses a notion called "pattern matching". What you probably meant is: what is the ...


10

The reduction rule you ask for is the usual one for IF statements. It consists of two computation rules and one context rule: $\text{IF TRUE}$ $a$ $b$ $\to$ $a$ $\text{IF FALSE}$ $a$ $b$ $\to$ $b$ $\dfrac{a\to a'}{\text{IF}~a\ b\ c\to \text{IF}~a'\ b\ c}$ In both the call-by-value (strict) and call-by-need (lazy) settings, both $a$ ...


9

See also this question: "How is Lambda Calculus a specific type of Term Writing system?". Term rewriting, as introduced in (1), and described in e.g. (2), is a first-order system that cannot handle binding. Consider the $map$ function. $$ \begin{array}{lcl} map(f, []) &\rightarrow& [] \\ map(f, cons(x, l)) &\rightarrow& cons( f\ x, ...


8

A theory, in this sense, is an equivalence relation on the formula, which states when these formula are equivalent (as in: $F$ is equivalent to $G$ iff $F$ implies $G$ and $G$ implies $F$). The theory is usually presented by a set of deduction rules, though this is not an obligation. The word theory is often used in the context of rewriting systems: if you ...


7

Rule 110 is universal, and can be expressed as a Markov algorithm. In particular, Rule 110 corresponds to the Markov system with alphabet $\{0,1,\verb!^!,|,\$ \}$ and a pair of bits for each element in the automaton. The pair of bits records the current status of that element (empty or filled) and the previous status. Elements are updated by doing a left-...


7

Two counterexamples are: $(\lambda x. b x (b c)) c$ and $(\lambda x. x x) (b c)$ (Plotkin). $(\lambda x. a (b x)) (c d)$ and $a ((\lambda y. b (c y)) d)$ (Van Oostrom). The counterexample detailed below is given in The Lambda Calculus: Its Syntax and Semantics by H.P. Barenredgt, revised edition (1984), exercise 3.5.11 (vii). It is attributed to Plotkin (...


6

I can reassure you that this property is not immediately self-evident. In trying to describe/enumerate the set of normal forms, the main observation required is the following: Abstraction preserves normal forms: if $t$ is normal, than so is $\lambda x.t$. Application does not preserve normal forms: if $t$ and $u$ are normal, $t\ u$ may contain a redex! We ...


6

My thought is, it's because Term Rewriting is something extremely fundamental, and that lets you describe things in an extremely low-level way, independent of any hardware. Term-rewriting can describe grammars, but it also gives you the mechanics to described logical systems, like first order logic, etc. Proving and deductions can be written as term-...


6

The set of values is defined for a particular reduction relation. Each reduction relation defines its own set of values. Reduction for the lambda calculus isn't just beta reduction, there are also context rules. There are several common notions of reduction for the lambda calculus, with different sets of context rules. In the full lambda calculus, any ...


5

The two formulations are saying almost the same thing. Hankin's presentation has a symmetry rule ($\frac{M=N}{N=M}$), which is strange: it ends up defining the relation “$M$ reduces to $N$ or $N$ reduces to $M$”. That's unusual; usually, when a relation is written $=$, it's either explicitly defined to be an equivalence relation (with explicit or deducible ...


5

Rule 110 is a binary rewriting system that can perform universal computation, i.e., it has been proven to be universal. It can be implemented by a finite-state transducer: it needs only finite state. However, Rule 110 is not a tag system or a cyclic tag system, so this does not provide an instance of a specific binary tag system that is known to be ...


4

One way of reading the definition of satisfied that might help is to change A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not. to the logically equivalent statement A rule is satisfied by a relation if, for each instance of the rule, if all the premises are in ...


4

The notion you are looking for is that of critical pair (see the wikipedia entry for instance). The idea is to find the "most simple" term which allows both rewrite rules to be applied. In this case the rewrite rules are: $$ f(f(x))\rightarrow x$$ $$ f(a) \rightarrow b$$ To find a critical pair, you look for the most general (in a precise sense) instance ...


4

Consider the potential function $$ \Phi(w_1 \ldots w_n) = \sum_{i=2}^n 2^i 1_{w_i = w_{i-1}}. $$ Applying one of the rewrite rules always decreases the potential: if we change $abb$ to $bab$ at positions $i,i+1,i+2$, then we lost $2^{i+2}$ and might have gained $2^i$. Since the potential is non-negative, every derivation ends. Suppose now that the initial ...


4

I talked to be5invis and he said it's implemented using replace. replace is something like this in Agda: $$ replace : \forall \{a \ b\} \rightarrow (a \equiv b) \rightarrow P \ a \rightarrow P \ b $$ or, using universal polymorphism: $$ replace : \forall \{n\} \{a \ b : Set \ n\} \rightarrow (a \equiv b) \rightarrow P \ a \rightarrow P \ b $$ This is ...


4

It's a very bad idea to omit parentheses. Correct is: $$\lambda b . b (\lambda x y . y) (\lambda x y . x)$$ Next, it is confusing to reuse bound variables, so let me rename them: $$\lambda b . b (\lambda x y . y) (\lambda u v . u)$$ And now we can apply this to $\lambda p q . p$ (which is just "true" with bound vraiables renamed yet again): \begin{align*} (\...


4

I think that what you are looking for is called higher-order rewriting. There are systems in which you can define rewrite rules of the form $F\;(\lambda x.\lambda y.C\;X[x,y]) \longrightarrow X[X[t,u],v]$ for example, where $F$ and $C$ denote a function symbol and a constant symbols respectively. Note that here, $X$ denotes a higher-order variable (or meta-...


4

$S \leftrightarrow^* T$ does not mean that $S \rightarrow^* T$ and $T \rightarrow^* S$! It means that there is a chain of reductions $S = S_0 \rightleftharpoons_1 S_1 \rightleftharpoons_2 S_2 \rightleftharpoons_3 \cdots \rightleftharpoons_n S_n = T$ where each of the $\rightleftharpoons_i$ might be either $\rightarrow$ or $\leftarrow$. The directions can ...


3

Binary Combinatory Logic is an example with simple rewriting rules.


3

Seems like the rule: 000 => 000 001 => 100 010 => 010 100 => 100 011 => 011 101 => 101 110 => 101 111 => 111 Does what I want. Testing this rule by applying it to an arbitrary bit string, this is how it evolves: 0 11110110010010000010100000000001000 1 11110111001000001000100000000001000 2 11101111100000100000100000000100000 3 ...


3

In general, there is no obstacle to define a rewrite system as above, and a few sources do indeed require rules 1. and 2. only as additional hypotheses. However the hypotheses are almost always necessary (but not sufficient!) for both termination and confluence, which is indeed the main object of study of rewriting as a field. Perhaps it's useful to remind ...


3

If $x$ and $y$ are such that $x \leftrightarrow^* y$, then $x \rightarrow^* y$ This is not true in general. It is not even true if $\rightarrow$ is confluent! For example, consider the lambda calculus with for $\beta$ reduction. $(\lambda x. x) y \rightarrow y$, therefore $(\lambda x. x) y \leftrightarrow^* y$, but it is not the case that $y \rightarrow^* (...


3

I am assuming that you have some background in a functional programming language like Haskell or ML or OCaml because that is the easiest thing for me to explain this in terms of. Haskell is, or can be viewed as, a rewrite system. When you simplify little expressions you are rewriting the expression in little steps until you get to the final result (normal ...


3

I do not think $f(f(x))$ and $f(a)$ can be unified. You can not map constant $a$ to the term $f(x)$. My example would be $f(f(a)) = f(b)$ while otherwise $f(f(a)) = a$. It seems the equation $x=b$ maps all terms to $b$. That is too much. I would add $f(b) = a$. This leaves two classes of terms, those equivalent to $a = f(b) = f(f(a)) = \dots$ and those ...


3

Thue language is based on string rewriting and it's just 179 lines of c code. Pure is an LGPL'd functional language based on term rewriting. Not an example, but a course with really complete slides on the theory of term rewriting systems.


3

In first order logic there are formulae that are not necessarily valid. The equality $x + y = y + x$ does not hold for arbitrary interpretations of equality and the addition symbol. It does hold for the interpretation of $+$ and $=$ in standard arithmetic. So if we assume the theory of Peano arithmetic (or first order arithmetic, or even Presburger ...


3

It sounds like what you are asking for is, for a given equational system $\cal E$, to give a canonical representation for equivalence classes modulo $\cal E$. Indeed, if your signature is the binary operation $\_\cdot\_$, and your equation is $$ (x\cdot y)\cdot z=x\cdot(y\cdot z)$$ then you can represent any element as $a_1\cdot(a_2\cdot(\ldots\cdot a_n)\...


3

The theory of higher-order critical pairs can indeed handle this example, as outlined in the following article: Higher-Order Rewrite Systems and their Confluence, Richard Mayr & Tobias Nipkow There are several different notions of higher-order rewrite systems, and several of them are able to handle your example, including those of the paper. The ...


3

It's hard to understand what you are looking for, but perhaps you are looking for program transformations. A famous one is the CPS transform (continuation-passing style), which transforms any lambda term $t$ into a quite different one $t'$, which has a semantics related to that of $t$. E.g., $t'$ might follow the call-by-name evaluation of $t$ (CBN CPS ...


Only top voted, non community-wiki answers of a minimum length are eligible