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

70 questions
Filter by
Sorted by
Tagged with
51 views

• 711
176 views

### A Markov algorithm that does unary multiplication

I am learning Markov algorithms and came across the paper Markov Algorithm by CHEN Yuanmi. I am trying to understand the following example (well, any of the examples in the paper). Example 3: ...
• 155
1 vote
33 views

### Give a finite set of identities $E$ such that the ground word problem is decidable, but the word problem is not

I am studying term rewriting using Baader and Nipkow's book "Term Rewriting and All That". I am trying to solve the following exercise about word problems: 4.1 Give a trivial example of a ...
1 vote
55 views

### How is a homeomorphic embedding a homeomorphism?

How is a homeomorphic embedding (in the sense of term algebra) a homeomorphism? Definition of homeomorphic embedding: Alt text: ...
• 348
49 views

### How can I use induction for proving termination of a string rewriting system?

If we have a string rewriting system within the alphabet $\{X,Y\}^*$ and the rule $XY\to YX$. How can we prove by induction that on every string input the system terminates?
288 views

### What does $\text{dom}(\Gamma)$ mean in the context of an inference rule?

In the wikipedia page on pure type systems, it gives the following inference rule: $\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$ ...
• 3,752
130 views

### What is the difference between deterministic and confluent?

I understand deterministic as a function for some input will always give the same output, and these inputs and outputs can be sets of values represent by a predicate. I understand confluent as ...
• 165
458 views

### What is congruence in lambda-calculus

I see a lot of lecture notes where they use the term "congruence" (ex: congruence relation) or deriving usages such as "the expression e is alpha-congruent to e2". Could someone ...
68 views

• 2,194
77 views

• 281
41 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 ...
• 281
1 vote
34 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 ...
• 281
27 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,255
1 vote
283 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,401
1 vote
31 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 ...
66 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 ...
• 1,710
731 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 ...
• 940
55 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. ...
• 156
180 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 ...
55 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
187 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 ...
• 111
423 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.
• 143
806 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 ...
• 325
162 views

53 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, ...
• 610
118 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: ...
203 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 ...
• 1,199
2k 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 ...
• 1,004
27 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 ...
• 4,127
58 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,127