Questions tagged [term-rewriting-systems]
The term-rewriting-systems tag has no usage guidance.
35
questions
5
votes
1
answer
135
views
Commutative operation benefits
With an associative operation I can rewrite a computation tree
+
/ \
+ 4
/ \
+ 3
/ \
+ 2
/ \
0 1
to be more efficient ...
- 71
2
votes
2
answers
220
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 ...
- 354
3
votes
1
answer
139
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^* ...
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 ...
- 992
5
votes
1
answer
168
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 ...
- 455
2
votes
1
answer
989
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 ...
- 921
5
votes
0
answers
167
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 ...
2
votes
1
answer
290
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 $\...
- 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 ...
- 1,588
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 ...
- 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 ...
- 183
5
votes
1
answer
173
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 ...
- 921
6
votes
1
answer
210
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 ...
- 455
3
votes
1
answer
425
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 ...
- 183
6
votes
1
answer
167
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 ...
- 265
7
votes
1
answer
348
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 $\...
- 181
6
votes
1
answer
114
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 ...
- 455
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 ...
- 2,581
2
votes
1
answer
132
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 ...
- 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 =...
- 1,062
8
votes
1
answer
468
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 ...
- 2,571
4
votes
1
answer
72
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 ...
- 2,049
6
votes
0
answers
301
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 ...
- 161
3
votes
0
answers
84
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 ...
- 505
3
votes
1
answer
217
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 ...
- 296
6
votes
3
answers
266
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/...
- 390
3
votes
0
answers
711
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 ...
- 1,206
9
votes
1
answer
351
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 ...
3
votes
1
answer
188
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 ...
3
votes
0
answers
136
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$ ...
- 31
4
votes
0
answers
183
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 ...
- 14.3k
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 ...
- 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 ...
- 2,775
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 ...
- 1,259
6
votes
1
answer
565
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 ...
- 189