19 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 ...
user avatar
  • 13.2k
11 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 ...
user avatar
  • 1,910
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 ...
user avatar
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.
user avatar
9 votes
Accepted

What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of ...
user avatar
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). ...
user avatar
  • 26.7k
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, ...
user avatar
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 ...
user avatar
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)}$....
user avatar
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 ...
user avatar
  • 13.2k
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 ...
user avatar
  • 13.2k
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, ...
user avatar
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 ...
user avatar
  • 13.2k
4 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/...
user avatar
  • 141
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 ...
user avatar
  • 13.2k
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 ...
user avatar
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))^*. $$...
user avatar
  • 4,721
2 votes
Accepted

Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

I think you'll find that the exact same proof of Lemma 3 in [1] (the proof itself appears in [2]) concerning $\rightarrow^\infty_\beta$ also holds for $\rightarrow^\infty_{\beta\bot}$: indeed, they ...
user avatar
  • 13.2k
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 ...
user avatar
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, ...
user avatar
  • 13.2k
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 ...
user avatar
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, ...
user avatar
  • 13.2k
1 vote

What's the difference between term rewriting and pattern matching?

(I'd rather write this as a comment, but I can't at present.) Correct me if I'm wrong, but as far as I understand, one more difference between pattern matching and term rewriting, apart from what ...
user avatar
  • 361

Only top scored, non community-wiki answers of a minimum length are eligible