Questions tagged [term-rewriting]

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.

Filter by
Sorted by
Tagged with
1
vote
1answer
35 views

If well-founded induction holds, then the relation $\to$ on a reduction system terminates

I am trying to understand a proof from "Term Rewriting and All That" by Baader and Nipkow. Well-founded induction (WFI) is the following statement: $\forall x \in A(\forall y \in A(x \stackrel{+}{\...
2
votes
1answer
87 views

Elegant algorithm to semi-decide if two lambda calculus terms are equivalent

Given two lambda terms $t_1$ and $t_2$, it is semi-decidable if they are equivalent (i.e. can be rewritten as each other using alpha, beta, and eta conversions). An algorithm to do this is to try ...
3
votes
2answers
62 views

When are you supposed to eta-reduce?

Wikipedia lists the following algorithm for normalizing a lambda calculus term $t$: If $t$ is not in head normal form, beta reduce the beta redex in the head position to get $t'$. Then normalize $t'$ ...
10
votes
2answers
115 views

Confluence of beta expansion

Let $\to_\beta$ be $\beta$-reduction in the $\lambda$-calculus. Define $\beta$-expansion $\leftarrow_\beta$ by $t'\leftarrow_\beta t \iff t\to_\beta t'$. Is $\leftarrow_\beta$ confluent? In other ...
1
vote
0answers
93 views

What's are the consequences of subject expansion property?

Subject reduction is a well and widely used property of typed rewriting systems. Subject expansion is much less known. What are the applications of this property and which systems enjoy it?
1
vote
0answers
25 views

Confluence versus the property of every term having at most one normal form

If a term rewriting system is confluent, then every term has at most one normal form. Is the converse also true, or is confluence a strictly stronger property? I.e. if every term has at most one ...
3
votes
0answers
28 views

Question about termination of term rewrite systems

Let $\mathcal{R} = (R, \Sigma)$ be a term rewrite system over a signature $\Sigma$ with set of basic rewrite rules $R$. It is known that $\mathcal{R}$ is terminating IF every basic rewrite rule $l \to ...
2
votes
1answer
28 views

Identifying/equating constants in a term rewrite system

Suppose we have a term rewrite system $\mathcal{R} = (R, \Sigma)$ with basic rewrite rules $R$ over a signature $\Sigma$. Suppose also that this rewrite system $\mathcal{R}$ is confluent and ...
1
vote
0answers
27 views

Adding ground rules to term rewriting system

Suppose we have a term rewriting system $\mathcal{R} = (\Sigma, R)$ with signature $\Sigma$ and set of basic rewrite rules $R$. Suppose we also have a set $S$ of ground rewrite rules, i.e. rewrite ...
2
votes
0answers
24 views

Name for “confluence unless both sides are normal”

I am looking for a name for the property $\mathbf{?_2}$ (and for that, it is sufficient to find a name for the property $\mathbf{?_1}$ since "Uniform" could then be added in front of it). Confluence :...
1
vote
2answers
121 views

Term rewrite system for terms of lambda calculus?

Are there term rewrite systems, that can rewrite complex lambda term (with nested function application) into some other lambda terms, I.e. reorde function application and, possibly, introduce new ...
1
vote
0answers
26 views

Evaluation semantics: reduction rule for a split statement

Assume a language with statements such as $x := e$, $\text{assume}(e)$, etc., and particularly a $\text{split}\ stmt_1 ... stmt_n$ statement, constructed from $n$ statements. Informally, the semantics ...
3
votes
1answer
56 views

Understanding a boolean expression in λ-calculus

(NOTE: This is not a homework question at at all. Rather, this was something that I thought that I understood (at least on the surface), but now appear to have no clue about, and am not currently ...
4
votes
1answer
440 views

How was Idris' `rewrite` implemented?

I know in Agda, rewrite is a syntax sugar that desugars to a with abstraction. For example, if we have (I'm using the ...
1
vote
0answers
48 views

Provably correct algorithm/CAS for checking term equalities

Within my research of term rewriting systems (TRS) I stumbled upon a paper (Siekmann, J., and P. Szabó. “The Undecidability of the DA-Unification Problem.” The Journal of Symbolic Logic, vol. 54, no. ...
4
votes
1answer
76 views

Higher order rewriting theory and critical pairs with the beta rule

In a higher-order pattern rewrite system, one specifies rewrites on beta normal forms of terms. Is it possible to have a rewrite like: $\gamma := \lambda x . F(m) \to F(\lambda x . m)$ for some ...
3
votes
1answer
43 views

Is there a generic algorithm for translating equational rules into corresponding data structures?

When implementing a term rewriting system, one “optimization” one can do is to represent operators known to have certain equational properties with a more directly representative data structure. For ...
1
vote
0answers
114 views

Computing critical pairs, confluence and Normal terms

Down below is a Term rewriting system where I am trying to find the critical pairs, decide if it is confluent and find the Normal terms. I think it's difficult to understand all these concepts and I ...
4
votes
1answer
250 views

Lambda Calculus in Rewriting systems

How to do or implement Lambda Calculus in a Rewriting systems? Rewriting systems are Turing complete. But I can't figure out how to do lambda calculus or functions with them.
7
votes
1answer
281 views

Intuitive explanation of neutral / normal form in lambda calculus

It is possible to distinguish Normal terms which don't contain beta redex as a sub-expression, from others like so ...
6
votes
1answer
102 views

Properties of a term rewrite rule

While doing some bibliography on term-rewriting, I often found these two properties to define a term rewrite rule (see for example here and this one): A term rewrite rule is a pair $\langle l,r\...
3
votes
1answer
72 views

Semi-Thue system, which terminates

I observed that with rewrite rules: $abb \rightarrow bab $ $baa \rightarrow aba $ Every derivation ends, moreover, if there is same amount of $a$'s and $b$'s in input, then derivation ends in $(ab)^...
3
votes
0answers
46 views

Termination of deterministic term rewriting

Consider a simple language: $$t ::= plus ~ t ~ t ~ | ~ gen ~ t ~ | ~ except ~ N ~ t ~ | ~ N$$ with N constructors plus, gen and except, N being the natural numbers, and $G = \{t_n\}$ a finite, ...
4
votes
1answer
104 views

In what cases is graph rewriting not enough to avoid duplicate work?

As I understand, evaluating something like the following in normal order evaluation is inefficient due to duplicate work: ...
5
votes
0answers
156 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 ...
5
votes
1answer
1k 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 which ...
2
votes
1answer
21 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 ...
2
votes
1answer
50 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
114 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
103 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
298 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
394 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
426 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 ...
3
votes
1answer
396 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
98 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
312 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
223 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 ...
11
votes
3answers
1k 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
84 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{...
2
votes
1answer
225 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
66 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
223 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
224 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
109 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
3answers
479 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
210 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
265 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) ...
14
votes
2answers
804 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$ ...
11
votes
1answer
98 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 ...