Term rewriting is a general model of computation that investigates a wide range of (potentially non-deterministic) methods of replacing subterms of syntactic expression, more precisely an element of a term-algebra (over some set of variables) with other terms.

learn more… | top users | synonyms (1)

2
votes
0answers
57 views

Why did the Mathematica Language choose term rewriting instead of the Lambda Calculus as its basis? [closed]

Now we can see that Church was associated with the Simply Typed Lambda Calculus. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda ...
3
votes
1answer
44 views

call by value: what is a value?

In the 'call by value' evaluation of lambda-calculus, I am bit confused with 'value'. On page 57 of the book Types and Programming languages, it is said: The definition of call by value, in ...
3
votes
1answer
20 views

How to identify strongly confluent cellular automatas?

Lets represent a class of cellular automata as a finite, unidimensional bit array state : [Bit], plus a rewrite rule ...
1
vote
1answer
36 views

Is there any count-preserving cellular automata which tends do “10101010…”?

Suppose that I have a bit string of finite length. Is there any bit rewriting rule rewrire :: (Bit,Bit,Bit) -> (Bit,Bit,Bit), that doesn't change the total count ...
3
votes
0answers
35 views

Efficient explicit-substitution calculus

I've been looking at various calculus with explicit substitutions for efficient implementation of normalisation of terms in the lambda calculus. AFAICT there are basically two approaches: the λσ ...
4
votes
1answer
53 views

Presentation of context rules for the lambda-calculus

Reading Chris Hankin's book, "An Introduction to Lambda Calculus for Computer Scientists", I learnt that the rules for reductions in the pure $\lambda$-Calculus are the $\beta$-reduction rule, $$(\...
1
vote
0answers
47 views

term rewriting vs symbolic programming

I have recently discovered term rewriting when I watched this video - https://channel9.msdn.com/Series/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition It ...
5
votes
1answer
170 views

Simplest Turing-complete ruleset for Markov algorithm

Is there an example of a particular ruleset for a Markov algorithm that is Turing-complete? If so, what is the simplest example of such a ruleset?
6
votes
2answers
163 views

Universal binary rewriting system

What is the simplest example of a rewriting system from binary strings to binary strings $$f:\Sigma^*\rightarrow\Sigma^*\qquad\Sigma=\{0,1\}$$ that can perform universal computation? Binary string ...
1
vote
1answer
114 views

Term Rewriting vs Unification

How is term rewriting different from unification, and what's the difference between term rewriting languages and logic programming, like Prolog?
1
vote
1answer
47 views

Term rewrite system is non-confluent, but cannot find different normal forms of term

I wrote a simple TRS that I believe is non-confluent, but I'm not able to find a term with two normal forms for it. The TRS is defined on the signature $\mathcal F=\{f,\ l,\ s,\ o\}$ and the rewrite ...
4
votes
2answers
195 views

Misunderstanding the Church-Rosser property

I am contemplating the Church-Rosser property and I clearly misunderstand it, but I do not exactly know why. If $x$ and $y$ are such that $x \overset{*}{\leftrightarrow} y$, then $x \overset{*}{\...
2
votes
1answer
74 views

What is a rewrite-based system?

I am reading about this in the context of the K semantic framework. I keep encountering terms such as rewrite-term and rewrite logic. My main aim is to understand what is K doing and how it works, so ...
7
votes
4answers
166 views

Why Term Rewriting?

I've done a bit of googleing and have come up a bit short. I am wondering what are the main reasons for computing scientists, programmers, to study term rewriting, and/or term graph rewriting. As ...
3
votes
1answer
64 views

Is “duplicate” in RPN enough for replacing variable binding in term expressions?

I try to work out some consequences of storing (or "communicating"/"transmitting") a rational number by a term expression using the following operators: $0$, $\mathsf{inc}$, $\mathsf{add}$, $\mathsf{...
1
vote
1answer
175 views

Where can I find rules for source to source transformation optimization rules?

Upon reading Do source code optimizers exist? I knew that such programs existed but the ones I have worked with use a set of rules to drive a transformation algorithm. Ira Baxter provided a link to ...
2
votes
1answer
54 views

Is this $\beta$-reduction well defined?

Would it be possible to apply $(\lambda x.\lambda y. x)$ to the argument $y$? It seems to me that this must not be possible as it would give a different answer if applied to a constant, call it $\...
0
votes
1answer
135 views

Implementation of datatypes in Haskell?

In Haskell, are datatypes converted to the "Church encoding" i.e. folding the data type. For example, given data N = Z | S N in Haskell, it can be converted to ...
4
votes
2answers
148 views

TAPL: Explanation and example(s) for satisfied

This question arises from my reading of "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce. On page 36 is the definition for satisfied A rule is satisfied by a relation if, for ...
2
votes
2answers
98 views

Proving non-confluency and adding an equation to make it confluent and terminating

I currently have a system that has {f(a) = b, f(f(x)) = x} (part of an exam question - look at page 5 - exercise 1). To start off with proving non-confluency, I am ...
2
votes
2answers
222 views

Example of a parsing/rewriting system?

I am studying formal languages and playing with writing my own parsers for them. I have a context free grammar parser already that works well. I am wondering if anyone can point me towards actually ...
6
votes
2answers
165 views

The meaning of modulo in “formula modulo a background theory”

I have been reading some papers where I keep reading stuff like “first-order formula modulo a background theory”. Does anyone know what modulo means in this case ? Is it something like “with respect ...
7
votes
1answer
234 views

Reduction rule for IF?

I'm working through Simon Peyton Jones' "The Implementation of Functional Programming Languages" and on page 20 I see: IF TRUE ((λp.p) 3) ↔ IF TRUE 3 (per β red) (1) ...
11
votes
2answers
590 views

Confluence proof for a simple rewriting system

Assume we have a simple language that consists of the terms: $\mathtt{true}$ $\mathtt{false}$ if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ ...
10
votes
1answer
75 views

Is it possible to derive a string in this rewriting system?

Rewriting system is a set of rules in the form of $A \leftrightarrow B$. If we apply that rule to a string $w$ we replace any substring $A$ in $w$ with a substring $B$ and vice versa. Given a ...