# Tag Info

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 set of computation rules of the form $$l\rightarrow r$$ where $l$ and $r$ are first order terms of the form $$t :=\ x\ \mid\ f(t_1,\ldots,t_n)$$ where $... 11 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 idea, and your motivation of using it to perform optimizations sounds reasonable -- another related question is whether you could define a bytecode format for it ... 9 (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 typesetting, not for programming; so it is at best “weird” when considered as a programming language. — Donald Knuth, Digital Typography, page 235 I have read a ... 9 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. 9 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 reductions, but clarify the presentation in my opinion. Let's assume your language is given by the following grammar. $$\newcommand{\PROGRAM}[1]{\mathsf{#1}} ... 8 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). A right action should satisfy a [s \circ t] = (a[s])[t], so it makes sense to define the operation \circ that conforms to action on the right. That's all. ... 8 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 instance from the standpoint of abstract term rewriting, which is not my specialty). For instance, in \lambda-calculi and related languages, usually the ... 5 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 order. Proof: Exercise. Note that this nice property is not true for well-founded orders in general! In this sense, well-quasi orders are much more "stable". ... 5 Yes, Prolog. The specification of unification in the Prolog standard omits the occurs check, and as a result variables range over rational trees. Additionally, many Prolog (such as SWI Prolog and YAP) implementations support tabling, which permits defining and using coinductively defined predicates. 5 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 first appears, at least in classical rewrite theory because it behaves poorly under substitution: If t\rightarrow t' is an inevitable reduction, and t ... 4 It is a little bit sketchy, but here is my argument: Suppose that there are three terms t, u, v such that t reduces to u, t reduces to v and suppose that each term has a unique normal form. Since you are weakly normalizing as you said, there exists a normal form for v and u. But since the normal form is unique, then v and u are joinable. Hence, the system is ... 3 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 attention to detail, though a bit dated at this point I guess. Note that neither refers to completion as "Knuth-Bendix" completion in the index, since the ... 3 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 the field of equational logic and completion hasn't seen a complete revolution since 1980 (as compared to, say SMT) there have been substantial improvements, so ... 3 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/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition 3 Here are the standard references on unification: Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998. (Book homepage) Franz Baader and Wayne Snyder. Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 447-533. Elsevier Science Publishers, 2001. (... 2 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 are defined in the same way from \rightarrow^*_\beta and \rightarrow^*_{\beta\bot} respectively, which are transitive by definition! The lemma holds for an ... 2 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 http://www.cs.le.ac.uk/people/rh122/papers/2006/Hec06Nutshell.pdf, see 3.2. A more formal account is in "Formal foundation of consistent EMF model ... 2 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, even if l\rightarrow r shares no function symbols with R you may introduce non-termination! Here is a famous counter-example by Toyama. Take the following ... 2 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 groups. J. Symbolic Computation, 12:397--414, 1991. Charles C. Sims. Computation with Finitely Presented Groups. Cambridge, 1994. Derek F. Holt. The warwick ... 2 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))^*. $$Here is a formal way to justify your idea. Let (u,v) \in \Sigma^* \times \Sigma^*. By definition, (u,v) \in R^{obl}(T) if and only if (u,v) can be ... 1 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 especially interested in term rewriting systems (as opposed to string rewriting systems), the automaton model that you are probably looking for is that of tree ... 1 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, especially since an inner reduction may provoke a head reduction, like so:$$ {\cal R} = \{a \rightarrow b, f(b)\rightarrow f(a)\}$\$ (I'm using letters for function ...