22
votes
Accepted
How is Lambda Calculus a specific type of Term Writing system?
The answer is it depends what you mean by Term Rewrite System.
When it was introduced, the concept of Term Rewrite Systems, or TRSes, described what is now called first order TRSes, which is simply a ...
- 13.7k
12
votes
Has the semantics of TeX (as a programming language) ever been formalized?
No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in.
(What follows is a subjective and personal commentary). I think it is an intriguing and well-posed ...
- 2,040
9
votes
Accepted
Has the semantics of TeX (as a programming language) ever been formalized?
(With apologies for a long answer that goes in a direction different from the scope of the site: frankly I was surprised to see the question here in the first place….)
TeX was designed for ...
- 295
9
votes
Accepted
Solving a "tree-equation"?
The process you seem to be looking for (merging two descriptions of labeled trees) is called unification. According to the linked Wikipedia article it can be solved in linear time.
- 50.9k
8
votes
Accepted
Composition in explicit substitutions
Substitutions form a monoid and they act on terms. We have a choice of writing them as either left or right actions. Sometime in the previous millenium someone decided they act on the right (page 5). ...
- 28.3k
8
votes
Programming language supporting infinitary rewriting of regular term graphs?
Yes, Prolog.
The specification of unification in the Prolog standard omits the occurs check, and as a result when this spec is properly implemented variables range over rational trees. Additionally, ...
- 32.4k
8
votes
Accepted
Do we care about confluence because of unique normal forms?
I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for ...
- 5,273
6
votes
Commutative operation benefits
One example where commutativity helps is in computing the determinant. Nisan showed that any non-commutative algebraic formula that computes the $n \times n$ determinant must have size $2^{\Omega(n)}$....
- 743
5
votes
Accepted
Is every well-founded simplification order a well-partial order?
Every simplification order is indeed a well-partial order because of this simple statement:
If $R$ is a well-quasi order, and $S$ is a partial order, and $R\subseteq S$, then $S$ is a well-partial ...
- 13.7k
5
votes
How is Lambda Calculus a specific type of Term Writing system?
This presentation by Beckman and Meijer goes over lambda calculus, term rewriting, and mentions Mathematica. I think it answers the question in an intuitive way: https://channel9.msdn.com/Series/...
- 151
5
votes
Accepted
Is there a notion of "inevitable reduction?"
I have never heard of this exact concept in rewrite theory, which certainly doesn't prove it hasn't been considered.
However, I will make the point that it may not be quite as useful a concept as it ...
- 13.7k
4
votes
Accepted
Does having unique normal forms imply weak normalization and confluence?
It is a little bit sketchy, but here is my argument: Suppose that there are three terms t, u, ...
- 156
4
votes
A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?
The two obvious references are:
Chapter 7 of Term Rewriting and All That, notable for its pedagogy and accessible examples
Chapter 7 of Term Rewriting Systems, notable for its completeness and ...
- 13.7k
3
votes
Accepted
Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups
This is going to be a somewhat incomplete answer, since you are asking some pretty broad questions about the applications of the techniques.
First let me start by saying that while the research in ...
- 13.7k
2
votes
Accepted
Graph rewriting with one-to-many pattern matching?
Belatedly posting this answer:
This is called set node or multi-object matching. This is implemented in tools like Henshin https://www.eclipse.org/henshin/publications.php and described informally in ...
- 455
2
votes
A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?
There is a rather technically-detailed description to be found in any of the following:
D.F. Holt, D.B.A. Epstein, and S. Rees.
The use of knuth-bendix methods to solve the word problem in automatic ...
- 773
2
votes
Accepted
Rewrite relations - proof of correctness
To simplify, let $D$ be the domain of $T$ and let $R = \{\epsilon\} \cup (\Sigma^* \setminus \Sigma^*D\Sigma^*)$. Then by definition
$$
N(T) = Id_R \quad \text{and} \quad R^{obl}(T) = N(T)(TN(T))^*.
$$...
- 4,771
2
votes
Sufficient condition for termination of an orthogonal first-order rewriting system?
This is an entire field of research! In general, you cannot ensure termination of $R\cup\{l\rightarrow r\}$ by examining simply $l\rightarrow r$ and the knowledge that $R$ is terminating.
Indeed, ...
- 13.7k
1
vote
Accepted
Automata as term rewriting systems
As mentioned in the comments, regular grammars are more or less a (string) rewriting system, where the arrow of a derivation is in the reverse direction of the rewriting arrow. Since you seem to be ...
- 5,840
1
vote
Is there a name for this property of a term rewriting system?
I'm not sure there is a name for this specific property, though I would say "All right-hand sides are in head-normal form".
To be honest, this seems like a very strange property to request, ...
- 13.7k
Only top scored, non community-wiki answers of a minimum length are eligible