Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

0
votes
1answer
30 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 ...
2
votes
2answers
31 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
90 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
43 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
20 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
22 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
25 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
23 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
84 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
55 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
265 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
38 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
57 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
40 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
81 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 ...
5
votes
1answer
203 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.
6
votes
1answer
178 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
87 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
70 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
42 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
89 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: ...
3
votes
0answers
134 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
729 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 ...
3
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
46 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 ...
4
votes
0answers
97 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
95 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
229 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
359 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
387 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
312 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
83 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
293 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
199 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
857 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
80 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
222 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
64 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
200 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
200 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
108 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
390 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
195 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
252 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
769 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
92 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 ...