The tag has no wiki summary.

learn more… | top users | synonyms

5
votes
0answers
242 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 ...
2
votes
0answers
56 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 ...
3
votes
1answer
118 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 ...
5
votes
3answers
184 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
209 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
266 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
134 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
92 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
129 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
133 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 ...
5
votes
1answer
297 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 ...
17
votes
3answers
2k 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
217 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 ...