# Tag Info

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 ...

### 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 ...
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 ...
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.
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 ...
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). ...

### 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, ...
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 ...

### 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)}$....
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 ...
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 ...
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, ...

### 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 ...

### 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/...
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 ...

### 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 ...
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))^*.$$...
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  (the proof itself appears in ) concerning $\rightarrow^\infty_\beta$ also holds for $\rightarrow^\infty_{\beta\bot}$: indeed, they ...
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 ...

### 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, ...
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 ...
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, ...
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 ...

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