Rewrite Rule Definitions

©1998 Research Institute for Symbolic Computation (RISC-Linz)

NO WARRANTY

Package Description

This package contains the implementation of command Def for defining rewrite rules.

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr1.gif]

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr3.gif]

Usage

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr4.gif]

Implementation

Begin

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr5.gif]

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr6.gif]
FormFunction

Syntax call
FormFunction[
params,lvars,term,cnd ]
Input
params,lvars : lists of Mathematica symbols
term : a term,
cnd : pair of the form { ppeqs, eqs } where ppeqs is a list of parameter passing equations and eqs is a list of initial equations.

These four terms are those involved in the encoding of a conditional rewrite rule R.
Output
the encoding corresponding to R.
Implementation

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr7.gif]
Def

Syntax call
Def[
vars, {[Graphics:RewriteRuleDefsgr8.gif], ... , [Graphics:RewriteRuleDefsgr9.gif]}]
or
Def[
vars, {[Graphics:RewriteRuleDefsgr10.gif], ... , [Graphics:RewriteRuleDefsgr11.gif]}, TypeCheck->b ]
Input
[Graphics:RewriteRuleDefsgr12.gif]
Effect
for every conditional rewrite rule [Graphics:RewriteRuleDefsgr13.gif] of the form f[[Graphics:RewriteRuleDefsgr14.gif] , ... , [Graphics:RewriteRuleDefsgr15.gif]] → t ⇐ [Graphics:RewriteRuleDefsgr16.gif] ∧"∧ [Graphics:RewriteRuleDefsgr17.gif] perform the following steps
! type check [Graphics:RewriteRuleDefsgr18.gif] only if the option TypeCheck ->True is specified, or no TypeCheck option is specified but
type-checking is switched on;
if [Graphics:RewriteRuleDefsgr19.gif] is ill typed then give an error message and return "⊥",
! add [Graphics:RewriteRuleDefsgr20.gif] to the list of conditional rewrite rules associated with f.
! Return "⊤" if all conditional rewrite rules were successfully inserted in the corresponding rewrite rule lists.
Remarks
The encoding of a CRR of the form f[[Graphics:RewriteRuleDefsgr21.gif] , ... , [Graphics:RewriteRuleDefsgr22.gif]] → t ⇐ [Graphics:RewriteRuleDefsgr23.gif] ∧"∧ [Graphics:RewriteRuleDefsgr24.gif] is
Function[{[Graphics:RewriteRuleDefsgr25.gif], ... , [Graphics:RewriteRuleDefsgr26.gif]}, Module[{[Graphics:RewriteRuleDefsgr27.gif], ... , [Graphics:RewriteRuleDefsgr28.gif]}, RewritesTo[t , {[Graphics:RewriteRuleDefsgr29.gif][Graphics:RewriteRuleDefsgr30.gif], ... , [Graphics:RewriteRuleDefsgr31.gif][Graphics:RewriteRuleDefsgr32.gif]}, {[Graphics:RewriteRuleDefsgr33.gif], ... ,[Graphics:RewriteRuleDefsgr34.gif]}]]] ,
where [Graphics:RewriteRuleDefsgr35.gif], ... , [Graphics:RewriteRuleDefsgr36.gif] are the rule variables, and is added to the list RewriteRuleList[f] of conditional rewrite rules
associated with f.
Implementation

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr37.gif]
Flattening

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr38.gif]
PrintVarDecl

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr39.gif]
Uniform

Syntax call
Uniform[
term ]
Input
term : a term
Output
if term is a constant then return {{},{}}
if term is of the form [Graphics:RewriteRuleDefsgr40.gif]] then return a pair {vars,eqs} where vars is a
list of n fresh variables [Graphics:RewriteRuleDefsgr41.gif],...,[Graphics:RewriteRuleDefsgr42.gif] and eqs is the list of parameter passing equations [Graphics:RewriteRuleDefsgr43.gif]
Example
Uniform[f[x,r[a],b]] returns the pair
{{w$144,w$145,w$146},{w$144≈x,w$145≈r[a],w$146≈b}}
Implementation

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr44.gif]

End

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr45.gif]

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr46.gif]

[Graphics:RewriteRuleDefsgr2.gif][Graphics:RewriteRuleDefsgr47.gif]