The tag has no usage guidance.

learn more… | top users | synonyms

2
votes
1answer
63 views

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

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 ...
3
votes
1answer
59 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 ...
4
votes
0answers
41 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 =...
4
votes
1answer
63 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 ...
4
votes
1answer
48 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 ...
5
votes
0answers
261 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 ...
3
votes
0answers
65 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
139 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
208 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/...
3
votes
0answers
278 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 ...
8
votes
1answer
286 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
140 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
97 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
150 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
142 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
306 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 ...
23
votes
3answers
3k 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
295 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 ...