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 ...
• 13.8k

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

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

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.5k
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,418

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

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

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

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))^*.$$...
• 4,771

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

Is there such a thing as "transformational semantics"?

There are several possibilities here, but I think the closest one to what you have in mind is Felleisen's macro expressibility: when a programming language $L$ is extended by some feature, we say that ...
• 28.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 ...
• 6,460
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.8k

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