# 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 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}{\mathsf{#1}} ... 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. 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 ... 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 have a specific recommendation for your reading list, but I want to alert you to the excellent survey on "Rewrite Systems" by Dershowitz and Jouannaud in Handbook of Theoretical Computer Science, volume B. 6 The standard presentation of program transformation ideas is unsound, quite unfortunately. They usually think of program transformation as forward deduction. Using equational reasoning, you can deduce new facts from the old program, and lo and behold, it gives a better program! While the new facts are quite clearly facts, nothing guarantees that they ... 5 If you are a bit more careful about definitions, and in particular recursive definitions, then such confusion cannot arise. In your example, we must first decide whether f(x) = x + 1 is supposed to be a recursive definition or not. This cannot be discovered by looking for recursive calls in the body of the definition. Defining a function by recursion is a ... 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 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 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 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 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 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 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 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 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 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 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 ... 1 You could maintain a static call graph and, for a given subexpression such as (x + 1), apply the third transformation only if it does not yield a cycle in the graph. Thus, if the original program had no infinite recursion, the transformed version shouldn't have one, either. A next step could be to allow the introduction of new cycles if a static analyses (... 1 I think you have misunderstood the definitions: TERESE (9.1.1): A strategy$S$for an ARS$\rightarrow$is a sub-ARS$\rightarrow_S$of$\rightarrow$having the same objects and normal forms. This means that If$a\rightarrow_S b$, then$a\rightarrow b$(sub-ARS condition) If there exists$b$such that$a\rightarrow b$, then there exists$b'$such that$a\...