13

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 ...


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 ...


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

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 (...


7

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 ...


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-...


6

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 ...


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 ...


6

Generally speaking, in algebra, a congruence relation is an equivalence relation such that operations on equivalent objects yield equivalent objects. In the lambda calculus, a congruence is an equivalence relation such that constructing terms from equivalent terms yields equivalent terms: if $M \equiv M'$ and $N \equiv N'$ then $M\,N \equiv M\,N'$, and if $M ...


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 ...


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

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

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 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

$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 ...


4

First, let us show that the two assumptions are necessary. Here is an example showing what goes wrong when $x = y$. Take $t = x$, $u = 1$, $v = 2$. We have $$ x\{x := 1\}\{x := 2\} = 1\{x := 2\} = 1, $$ whereas $$ x\{x := 2\}\{x := 1\{x := 2\}\} = 2\{x := 1\} = 2. $$ Next, here is an example showing what goes wrong when $x$ is not free in $v$. Take $t = y$, $...


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

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

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 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

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

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 ...


2

Counterexample: $f(c) \rightarrow f(d)$ In general, there are some modularity theorems for termination and confluence that may apply if, e.g. your constants do not appear at all in any rule. There are probably some weaker assumptions that can make this work though.


2

Consider this program: f (m : Nat) x y = (x, if H(m,m) then x else y) my_f = f my_number my_f hard harder where H(x,x) returns True if Turing machine number x halts on input x and False otherwise. Detecting duplicate work (always) would mean solving the halting problem, no matter whether you want to do the analysis statically or dynamically. Hence, no ...


2

Is “duplicate” in RPN enough for replacing variable binding in term expressions? No, it is not strong enough. One can eliminate $\mathsf{dup}$ by replacing each sequence of $\mathsf{dup}$ by a sequence of $x$ preceded by one $\mathsf{sto}(x)$ operation. Since the single variable "$x$" is enough to eliminate all $\mathsf{dup}$ operations, any term expression ...


2

Martin Feather's thesis and papers (and similar theses from the 70s) are full of examples of such rules for functional languages. See http://dl.acm.org/citation.cfm?doid=357153.357154. (pdf) Most of the formal types like such (functional) rules. More recent would be any work by Martin Ward using his functional language WSL including his thesis. See ...


2

Beta-reduction is only allowed when the argument does not contain any free variable that is bound in the function. So before you can beta-reduce $(\lambda x. \lambda y.x) y$, you must rename the bound variable $y$ using alpha-conversion. Formally speaking, beta-reduction and equivalence are defined not over lambda terms, but over lambda terms modulo alpha-...


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