Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [term-rewriting-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer
77 views

Time Complexity of KnuthBendixCompletion Algorithm [closed]

I am currently studying the Knuth-Bendix completion algorithm and trying to understand the factors that contribute to its time complexity. This algorithm is used to transform a set of rewrite rules ...
Navvye's user avatar
  • 21
0 votes
1 answer
73 views

Is there such a thing as "transformational semantics"?

The Wikipedia article about programming language semantics distinguishes three major approaches to semantics: denotational, operational, and axiomatic. What is the approach called when the meaning of ...
Evan Aad's user avatar
  • 354
5 votes
1 answer
136 views

Commutative operation benefits

With an associative operation I can rewrite a computation tree + / \ + 4 / \ + 3 / \ + 2 / \ 0 1 to be more efficient ...
andi's user avatar
  • 71
2 votes
2 answers
243 views

A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?

I'm looking for an explanation of critical pairs and the Knuth-Bendix completion algorithm that is at once rigorous and of high pedagogical value, i.e. clear, detailed, containing illustrative ...
Evan Aad's user avatar
  • 354
3 votes
1 answer
140 views

Rewrite relations - proof of correctness

Let $T \subseteq \Sigma^* \times \Sigma^*$ be a regular relation. We define the obligatory rewrite relation over $T$ as follows: $$ R^{obl}(T) := N(T) \cdot (T \cdot N(T))^* $$ $$ N(T) := Id(\Sigma^* ...
Denis Kyashif's user avatar
4 votes
0 answers
65 views

Memoisation for term rewriting system

I have a (word) Term Rewriting System (TRS in short) and I want to check for a simple accessibility condition. In symbols, let $\Sigma$ be a finite alphabet. For $a\in \Sigma$, and any words $u,v,w ...
C.P.'s user avatar
  • 992
5 votes
1 answer
169 views

Is there a notion of "inevitable reduction?"

I was just working on a semantics paper and realized I needed a notion of inevitable reduction. I came up with this definition: Let $\rightarrow$ be a binary relation. We say that $a$ inevitably ...
James Koppel's user avatar
2 votes
1 answer
1k views

Automata as term rewriting systems

It came to my mind that automata (say to start DFA) can be thought as a special kind of rewriting systems. So if one has a word w , one tries to reduce it to the $\epsilon$ word. In other words ...
user1868607's user avatar
  • 1,019
5 votes
0 answers
172 views

Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations $c_1$ and $c_2$ such ...
Anton Salikhmetov's user avatar
2 votes
1 answer
300 views

Does having unique normal forms imply weak normalization and confluence?

Consider a term rewriting system $\mathcal{R} = (\Sigma, R)$ over a signature $\Sigma$ with basic rewrite rules $R$. If $\mathcal{R}$ is weakly normalizing and confluent, then we know that each $\...
User7819's user avatar
  • 123
21 votes
2 answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
Nicola Gigante's user avatar
2 votes
1 answer
91 views

Is there a name for this property of a term rewriting system?

Given TRS let's call it top-reducible or left-reducible if no rule's right hand side is contained in any rule's left hand side non-trivially. A term A is contained in an other one B trivially if ...
Adam's user avatar
  • 183
3 votes
1 answer
49 views

Sufficient condition for termination of an orthogonal first-order rewriting system?

I have a terminating orthogonal first-order rewriting system with finite rule set $R$. Question: What would be an algorithmically verifiable sufficient condition on a new rule $l\to r$ such that for ...
Adam's user avatar
  • 183
5 votes
1 answer
177 views

Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that ...
user1868607's user avatar
  • 1,019
6 votes
1 answer
217 views

Graph rewriting with one-to-many pattern matching?

In the single-pushout approach to graph rewriting, many nodes in a pattern graph can be matched to a single node of a target graph. My question is if there is a notion of graph rewriting where the ...
James Koppel's user avatar
3 votes
1 answer
436 views

Solving a "tree-equation"?

Given two trees A and B, each of their nodes except some leaves have a "type" (which also determines the number of children, the node has, having that type). The leaves which don't have a type are ...
Adam's user avatar
  • 183
6 votes
1 answer
168 views

Programming language supporting infinitary rewriting of regular term graphs?

Do any practical programming languages support term graph rewriting of infinite but regular terms? For example the toy language CoCaml [1] supports computations on infinite regular streams. Coq ...
fritzo's user avatar
  • 265
7 votes
1 answer
370 views

Do we care about confluence because of unique normal forms?

Confluence implies uniqueness of normal forms, which is great. It is also much simpler to reason about, allowing more reusable proofs (indeed I don't imagine a way to prove UN directly for the $\...
Guido's user avatar
  • 181
6 votes
1 answer
118 views

Is every well-founded simplification order a well-partial order?

I'm contemplating the proof of Kruskal's Tree Theorem, as presented in the book "Term Rewriting and All That." They use it to prove that every simplification order is well-founded: first by showing ...
James Koppel's user avatar
17 votes
2 answers
2k views

How is Lambda Calculus a specific type of Term Writing system?

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 Calculus. When John ...
hawkeye's user avatar
  • 2,581
2 votes
1 answer
138 views

Composition in explicit substitutions

In the classical λσ calculus of explicit substitutions, there is the following rewrite rule: (a[s])[t] ==> a[s ∘ t] where ...
Stefan's user avatar
  • 390
3 votes
0 answers
63 views

Ground Reachability in String and Term Rewriting Systems

I have two questions concerning ground reachability in string and term rewriting systems. String Rewriting Systems: Let $\Sigma$ be a finite alphabet. I have a set of rules $R$ of the form $a_ib_i =...
verifying's user avatar
  • 1,072
8 votes
1 answer
496 views

What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

In lambda calculus or in combinatory logic we formally define reduction/expansion rules for terms (and in their typed variants reductions must preserve the type). Then we can talk about properties of ...
Petr's user avatar
  • 2,601
4 votes
1 answer
76 views

Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't ...
Blaisorblade's user avatar
  • 2,059
6 votes
0 answers
302 views

Is there a name for this property of a binary relation?

Consider a binary relation $\mathsf{R}$ such that $x\mathsf{R}y$ is the case only if there is some $z$ such that both $x\mathsf{R}z$ and $y\mathsf{R}z$ are the case. (EDIT: note that this may be ...
J Marcos's user avatar
  • 161
3 votes
0 answers
85 views

Which are the rewriting systems corresponding to the levels of the computatational hierarchy?

The lambda calculus is a rewriting system and Turing complete. Which are the rewriting systems corresponding to the other levels of the Chomsky hierarchy? E.g. what is the functionally computing ...
Nikolaj-K's user avatar
  • 505
3 votes
1 answer
220 views

State-of-the-art unification for associative-commutative functions

I am interested what are the open problems on unification methods for associative-commutative functions, and what is the state-of-the-art work? I have found some old work, but nothing new. I am ...
zpavlinovic's user avatar
6 votes
3 answers
273 views

Preserving termination when rewriting recursive programs

Powerful program transformations like partial evaluation, deforestation and supercompilation are based on applying three kinds of transformations: Rewrite using axioms, e.g. a+b = b+a. Unfolding/...
Jules's user avatar
  • 390
3 votes
0 answers
731 views

Insertion and deletion operations for Turing machines

A Turning machine with insertion and deletion operations can be simulated by an ordinary Turing machine with a quadratic time cost. Do we know how insertion and deletion fit into the polynomial time ...
Jeff Burdges's user avatar
  • 1,216
9 votes
1 answer
355 views

Reading list on rewriting systems?

I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
Jonathan Gallagher's user avatar
3 votes
1 answer
192 views

Explanation of definition of normalizing: 9.1.12 in Terese "Term Rewriting Systems"?

A strategy for a rewriting system is a sub-rewriting system with the same objects and same normal forms. Definition (from Terese "Term Rewriting Systems"). Let N be a superset of the normal forms of ...
Jonathan Gallagher's user avatar
3 votes
0 answers
138 views

Expansion normal forms of confluent term rewriting systems

Suppose one has two rewrite rules $\to^\eta,\to^\beta$, both of which are confluent and such that $\to^A := \to^{(\eta \cup \beta)}$ is also confluent. Define a $\beta$-normal form relative to $\eta$ ...
Jonathan's user avatar
4 votes
0 answers
184 views

Term rewriting for proving inequalities

Suppose $f$ is a submodular set function on a universe $U$ of size $n$. For $k \in \{0,\ldots,n\}$, let $$ F(k) = \operatorname*{\mathbb{E}}_{X \in \binom{U}{k}} f(X), $$ where $\binom{U}{k}$ is the ...
Yuval Filmus's user avatar
  • 14.5k
0 votes
1 answer
156 views

Lengths and substitution in L-systems

Am looking into writing up a Lindenmayer systems implementation. I've looked at a few example implementations and the one thing that's giving me trouble at this stage is how symbols and substitutions ...
Engineer's user avatar
  • 111
5 votes
1 answer
335 views

A simple inference in rewriting theory

I was puzzled by a seeming simple inference in rewriting theory: if $y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2$ then $y_1 \overset{*}{\leftrightarrow} y_2$. I don't understand how ...
day's user avatar
  • 2,805
25 votes
3 answers
4k views

What's the difference between term rewriting and pattern matching?

As there was no response at Lambda the Ultimate I try it here again: term rewriting systems are used for instance in automated theorem proving a symbolic calculation, and of course to define formal ...
Jakob's user avatar
  • 1,259
6 votes
1 answer
575 views

reference for lexicographic path ordering

Can you recommend a good reference for reading about lexicographic/recursive path orderings? I'm currently reading about lpo's in Chapter 2 of the Handbook of Automated Reasoning, 'Resolution Theorem ...
Stefan Ciobaca's user avatar