This CD is part of the distribution of LeActiveMath and is used in the exercises suite. http://www.leactivemath.org/cd trs1 http://www.leactivemath.org/cd/trs1.ocd private 1 2005-06-30 Rewriting on expressions, including substitution, normal form, rewrite with a certain rule I have a real problem with this CD. I would rather have rewrite to be a service taking an expression and a rewrite rule. normal_form application The function that takes an expression and returns its normal form with respect to the canonical rewrite system given as second argument. simplified_form application The function that takes an expression and returns a simplified form with respect to the list of rewrite rules given as second argument. rewriting_by application The function that takes an expression and returns the rewritten form with respect to the rewrite rule given as second argument. term_rewriting_system application Term rewriting system (canonical) of a set of equations with respect to a reduction ordering. The first argument is a reduction ordering followed by a list of equations. A program that can compute the canonical term rewriting system for a set of equations is required to return a "trs" object. I am following the example of groebner, groebnered symbols. Need to work out the reduction ordering. trs application The constructor for a term rewriting system consisting of rewrite rules that appear as arguments. rewrite_rule application The function denoting the rewrite rule where the left handside is the first argument interpred as expression and the right handside is the second argument interpreted as expression. Notice that there are some restrictions for the rewrite rule to be valid: the first argument cannot be a variable, and the set of variables in the second argument must be a subset of the variables in the first argument. DM asks: In the rewite_rule, I was wondering if the variables must be bound. It is a good question, I wondered too. Let us wonder some more. I would say we need it but I left the simple representation for the time being (also because it is a trs1 CD, maybe I can introduce the symbolic handling in trs2) implying that everything which is a variable can be rewritten. By symbolic handing I mean where function symbols and constants appear as OMVs, hence we need to disambiguate what can be rewritten. (here I am brainstorming with myself.... f(2x)->g(x)*f(x) g(2x)->2f(x) rewrite h(2x): OMA(OMV:h,2x)§{h|g} -> 2f(x) ) this is a complicated example: it is easier if there is a parameter in the expression which I do not want to rewrite. 2 2