Skip to main content

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
0 votes
1 answer
54 views

"Term Rewriting and All That" - Exercise 2.3

I am working through the exercises in the book "Term Rewriting and All That" and got stuck on question 2.3. The question reads: find a reduction $\rightarrow$ on $\mathbb{N}$ such that $\...
Ruben Hensen's user avatar
1 vote
0 answers
26 views

Is it possible to state strong normalization through set inclusion?

In an abstract rewriting system $\langle A, \rightarrow\rangle$, confluence may be stated by using set inclusion. Namely, a rewriting system is confluent iff ${\leftarrow^*\rightarrow^*}\ {\subseteq}\ ...
paulotorrens's user avatar
3 votes
1 answer
208 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: ...
BurnsBA's user avatar
  • 155
1 vote
0 answers
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 ...
Gabriel F. Silva's user avatar
1 vote
0 answers
56 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: ...
Max Heiber's user avatar
0 votes
1 answer
50 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?
Ali Adin's user avatar
2 votes
1 answer
310 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)}$ ...
user56834's user avatar
  • 4,002
2 votes
2 answers
134 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 ...
newlogic's user avatar
  • 173
3 votes
2 answers
469 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 ...
aNormalPerson's user avatar
4 votes
1 answer
68 views

Proving equivalence of two substitutions by induction

I'm trying to prove the following reduction: $$ t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\} $$ under the following assumptions: $x \neq y$ $x$ is not a free variable of $v$ (in symbols, $x \...
user206904's user avatar
3 votes
1 answer
63 views

Coding max as an interaction net

I am reading Yves Lafont's introductory paper Interaction Nets. Early in the beginning he mentions that max cannot be coded as follows since in this coding it is not possible to choose which argument ...
Faustus's user avatar
  • 237
0 votes
1 answer
110 views

"Term Rewriting and All That" - Exercise 3.10

I am studying Term Rewriting by reading Baader/Nipkow's book "Term Rewriting and All That". I am in chapter 3 - Universal Algebra, in the section 3.2 - Algebras, homomorphism and congruences....
Gabriel F. Silva's user avatar
4 votes
0 answers
66 views

Efficient algorithm for factorizing symbolic sum of products

Given a sum of flat symbolic products like $axc + byc + ayc + bxc$, how can I efficiently factorize it as a product of sums like $(a+x)(b+y)c$? For my problem, the products are not commutative -- it's ...
Bruno Kim's user avatar
  • 141
1 vote
1 answer
30 views

Unifiers modulo commutativity in terms of syntactic unifiers and $\approx_{C}$-class

I am studying Term Rewriting by reading Baader's book "Term Rewriting and All That". I am in the chapter of Equational Unification, in the section of Commutative Functions. I am trying to do ...
Gabriel F. Silva's user avatar
1 vote
2 answers
107 views

Term-rewriting software recommendation

Is there an easy to use software that implements term-rewriting? Or do I need to write my own parser for it? I am looking for something that will take in a fixed set of user-specified rules and will ...
Vaibhav Karve's user avatar
1 vote
1 answer
60 views

Is there an algorithm for reducing CNFs further?

I have a Boolean formula in conjunctive normal form (CNF) $$(a\vee b \vee c) \wedge (a \vee b \vee \neg c) \wedge (x \vee y)$$ I know that this can be simplified to $(a\vee b)\wedge (x \vee y)$. Is ...
Vaibhav Karve's user avatar
0 votes
1 answer
31 views

Proof of Simple Properties About Terms, Position of Subterms and Replacement of Subterms

I am studying term rewriting by reading Baader/Nipkow's book: "Term Rewriting and All That". I want to prove a lemma about terms, position of subterms and replacement of subterms. The ...
Gabriel F. Silva's user avatar
1 vote
0 answers
39 views

How is it possible that an equational theory be terminating?

I'm a bit tripped up by this fundamental notion of an equational theory with respect to how we can possibly get termination if we have that we can always orient a set of equations either right to left ...
rb612's user avatar
  • 469
1 vote
1 answer
29 views

Injectivity not required for unification algorithms?

When learning about a general unification algorithm, we learned the rule decompose, which states unifying $$G \cup \{f(a_0,...a_k)=f(b_0,...,b_k)\} \Rightarrow G \cup \{a_0=b_0,...a_k=b_k\}.$$ The ...
rb612's user avatar
  • 469
4 votes
0 answers
90 views

Reference on relating Post systems to string rewriting systems and formal grammars?

wikipedia states: Every Post canonical system can be reduced to a string rewriting system (semi-Thue system). [...] It has been proved that any Post canonical system is reducible to such a ...
user56834's user avatar
  • 4,002
2 votes
1 answer
111 views

Confluence to show equivalent terms have one common reduct

In lemma 30.3.9, Pierce states a confluence property for $F_{\omega}$: $S \to_* T \land S \to_* U \implies \exists V. T \to_* V \land U \to_* V$ He then states the following proposition: $S \...
user1868607's user avatar
  • 2,194
2 votes
1 answer
78 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 \...
TheLast Cipher's user avatar
5 votes
2 answers
279 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 ...
Christopher King's user avatar
4 votes
2 answers
401 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'$ ...
Christopher King's user avatar
10 votes
2 answers
360 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 ...
xavierm02's user avatar
  • 1,255
1 vote
0 answers
402 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?
Łukasz Lew's user avatar
1 vote
0 answers
35 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 ...
User7819's user avatar
  • 281
3 votes
0 answers
41 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 ...
User7819's user avatar
  • 281
2 votes
1 answer
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 ...
User7819's user avatar
  • 281
1 vote
0 answers
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 ...
User7819's user avatar
  • 281
2 votes
0 answers
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 :...
xavierm02's user avatar
  • 1,255
1 vote
2 answers
288 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 ...
TomR's user avatar
  • 1,401
1 vote
0 answers
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 ...
Romain Beguet's user avatar
3 votes
1 answer
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 ...
Ben I.'s user avatar
  • 1,710
5 votes
1 answer
735 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 ...
ice1000's user avatar
  • 950
2 votes
0 answers
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. ...
RoyPJ's user avatar
  • 156
4 votes
1 answer
182 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 ...
Jonathan Gallagher's user avatar
3 votes
1 answer
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 ...
Ptharien's Flame's user avatar
1 vote
0 answers
188 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 ...
jopp's user avatar
  • 111
4 votes
1 answer
429 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.
Mustafa's user avatar
  • 143
8 votes
1 answer
821 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 ...
nicolas's user avatar
  • 325
6 votes
1 answer
163 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\...
noutoff's user avatar
  • 63
3 votes
1 answer
96 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)^...
Timo Junolainen's user avatar
3 votes
0 answers
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, ...
choeger's user avatar
  • 610
4 votes
1 answer
119 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: ...
user avatar
5 votes
0 answers
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 ...
hawkeye's user avatar
  • 1,199
6 votes
1 answer
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 ...
alim's user avatar
  • 1,024
2 votes
1 answer
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 ...
MaiaVictor's user avatar
  • 4,159
2 votes
1 answer
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 ...
MaiaVictor's user avatar
  • 4,159
3 votes
0 answers
136 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 λσ ...
Stefan's user avatar
  • 368