The term-rewriting-systems tag has no wiki summary.
5
votes
3answers
125 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.
...
3
votes
0answers
123 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 ...
7
votes
1answer
216 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
1answer
115 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
0answers
76 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$ ...
4
votes
0answers
86 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 ...
0
votes
1answer
109 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 ...
3
votes
1answer
237 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 ...
11
votes
2answers
833 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 ...
6
votes
1answer
171 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 ...
