Skip to content

Commit 7e7a306

Browse files
authored
Merge pull request #260 from TymonKilich/manual-smallfixes
Updates and adjustments for manual, especially rewriters section
2 parents 3f17853 + a31aa47 commit 7e7a306

File tree

3 files changed

+164
-48
lines changed

3 files changed

+164
-48
lines changed

page/index.md

Lines changed: 41 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,8 @@ where appropriate -->
1818
**Features:**
1919

2020
- Fast expressions
21-
- A [combinator library](/rewrite/#composing_rewriters) for making rewriters.
2221
- A [rule-based rewriting language](/rewrite/#rule-based_rewriting).
22+
- A [combinator library](/rewrite/#composing_rewriters) for making rewriters.
2323
- Type promotion:
2424
- Symbols (`Sym`s) carry type information. ([read more](#creating_symbolic_expressions))
2525
- Compound expressions composed of `Sym`s propagate type information. ([read more](#expression_interface))
@@ -65,17 +65,44 @@ Note however that they are not subtypes of these types!
6565
@show α isa Real
6666
```
6767

68+
As their types are different:
69+
70+
```julia:symtype3
71+
@show typeof(w)
72+
@show typeof(α)
73+
```
74+
6875
(see [this post](https://discourse.julialang.org/t/ann-symbolicutils-jl-groundwork-for-a-symbolic-ecosystem-in-julia/38455/13?u=shashi) for why they are all not just subtypes of `Number`)
6976

7077
You can do basic arithmetic on symbols to get symbolic expressions:
7178

7279
```julia:expr
73-
expr1 = α*sin(w)^2 + β*cos(z)^2
74-
expr2 = α*cos(z)^2 + β*sin(w)^2
80+
expr1 = α*sin(w)^2 + β*cos(z)^2
81+
expr2 = α*cos(z)^2 + β*sin(w)^2
7582

7683
expr1 + expr2
7784
```
7885

86+
SymbolicUtils automatically simplifies
87+
88+
```julia:creating1
89+
2w + 3w - 3z + α
90+
```
91+
92+
and reorders
93+
94+
```julia:creating2
95+
(z + w)*(α + β)
96+
```
97+
98+
expressions of type `Symbolic{<:Number}` (which includes `Sym{Real}`) when they are created. It also does constant elimination (including rational numbers)
99+
100+
```julia:creating3
101+
5 + 2w - 3z + α - (β + 5//3) + 3w - 2 + 3//2 * β
102+
```
103+
104+
It's worth remembering that the expression may be transformed with respect to the input when it's created.
105+
79106

80107
**Function-like symbols**
81108

@@ -88,19 +115,18 @@ using SymbolicUtils
88115
f(z) + g(1, α) + sin(w)
89116
```
90117

118+
This does not work since `z` is a `Number`, not a `Real`.
91119

92120
```julia:sym3
93121
g(1, z)
94122
```
95123

96-
97-
This does not work since `z` is a `Number`, not a `Real`.
124+
This works because `g` "returns" a `Real`.
98125

99126
```julia:sym4
100127
g(2//5, g(1, β))
101128
```
102129

103-
This works because `g` "returns" a `Real`.
104130

105131

106132
## Expression interface
@@ -123,15 +149,21 @@ SymbolicUtils contains [a rule-based rewriting language](/rewrite/#rule-based_re
123149

124150
## Simplification
125151

126-
By default `*` and `+` operations apply the most basic simplification upon construction.
152+
By default `*` and `+` operations apply the most basic simplification upon construction of the expression.
127153

128-
The `simplify` function applies a built-in set of rules to rewrite expressions in order to simplify it.
154+
Commutativity and associativity are assumed over `+` and `*` operations on `Symbolic{<:Number}`.
129155

130156
```julia:simplify1
157+
2 * (w+w+α+β + sin(z)^2 + cos(z)^2 - 1)
158+
```
159+
160+
The `simplify` function applies a built-in set of rules to rewrite expressions in order to simplify it.
161+
162+
```julia:simplify2
131163
simplify(2 * (w+w+α+β + sin(z)^2 + cos(z)^2 - 1))
132164
```
133165

134-
The rules in the default simplify applies simple constant elemination, trigonometric identities.
166+
The rules in the default simplify applies simple constant elimination and trigonometric identities.
135167

136168
If you read the previous section on the rules DSL, you should be able to read and understand the [rules](https://github.com/JuliaSymbolics/SymbolicUtils.jl/blob/master/src/simplify_rules.jl) that are used by `simplify`.
137169

page/rewrite.md

Lines changed: 119 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,11 @@
22

33
## Rule-based rewriting
44

5-
Rewrite rules match and transform an expression. A rule is written using either the `@rule` macro or the `@acrule` macro.
5+
Rewrite rules match and transform an expression. A rule is written using either the `@rule` macro or the `@acrule` macro. It creates a callable `Rule` object.
66

7-
Here is a simple rewrite rule:
7+
### Basics of rule-based term rewriting in SymbolicUtils
8+
9+
Here is a simple rewrite rule, that uses formula for the double angle of the sine function:
810

911
```julia:rewrite1
1012
using SymbolicUtils
@@ -13,37 +15,60 @@ using SymbolicUtils
1315

1416
(w, z, α, β) # hide
1517

16-
r1 = @rule ~x + ~x => 2 * (~x)
18+
r1 = @rule sin(2(~x)) => 2sin(~x)*cos(~x)
1719

18-
r1(sin(1+z) + sin(1+z))
20+
r1(sin(2z))
1921
```
2022

2123
The `@rule` macro takes a pair of patterns -- the _matcher_ and the _consequent_ (`@rule matcher => consequent`). If an expression matches the matcher pattern, it is rewritten to the consequent pattern. `@rule` returns a callable object that applies the rule to an expression.
2224

2325
`~x` in the example is what is a **slot variable** named `x`. In a matcher pattern, slot variables are placeholders that match exactly one expression. When used on the consequent side, they stand in for the matched expression. If a slot variable appears twice in a matcher pattern, all corresponding matches must be equal (as tested by `Base.isequal` function). Hence this rule says: if you see something added to itself, make it twice of that thing, and works as such.
2426

25-
If you try to apply this rule to an expression where the two summands are not equal, it will return `nothing` -- this is the way a rule signifies failure to match.
27+
If you try to apply this rule to an expression with triple angle, it will return `nothing` -- this is the way a rule signifies failure to match.
2628
```julia:rewrite2
27-
r1(sin(1+z) + sin(1+w)) === nothing
29+
r1(sin(3z)) === nothing
2830
```
2931

30-
If you want to match a variable number of subexpressions at once, you will need a **segment variable**. `~~xs` in the following example is a segment variable:
32+
Slot variable (matcher) is not necessary a single variable
3133

3234
```julia:rewrite3
35+
r1(sin(2*(w-z)))
36+
```
37+
38+
but it must be a single expression
39+
40+
```julia:rewrite4
41+
r1(sin(2*(w+z)*(α+β))) === nothing
42+
```
43+
44+
Rules are of course not limited to single slot variable
45+
46+
```julia:rewrite5
47+
r2 = @rule sin(~x + ~y) => sin(~x)*cos(~y) + cos(~x)*sin(~y);
48+
49+
r2(sin(α+β))
50+
```
51+
52+
If you want to match a variable number of subexpressions at once, you will need a **segment variable**. `~~xs` in the following example is a segment variable:
53+
54+
```julia:rewrite6
3355
@syms x y z
3456
@rule(+(~~xs) => ~~xs)(x + y + z)
3557
```
3658

3759
`~~xs` is a vector of subexpressions matched. You can use it to construct something more useful:
3860

39-
```julia:rewrite4
40-
r2 = @rule ~x * +(~~ys) => sum(map(y-> ~x * y, ~~ys));
61+
```julia:rewrite7
62+
r3 = @rule ~x * +(~~ys) => sum(map(y-> ~x * y, ~~ys));
4163

42-
r2(2 * (w+w+α+β))
64+
r3(2 * (w+w+α+β))
4365
```
4466

45-
Notice that there is a subexpression `(2 * w) + (2 * w)` that could be simplified by the previous rule `r1`. Can we chain `r2` and `r1`?
67+
Notice that the expression was autosimplified before application of the rule.
4668

69+
```julia:rewrite8
70+
2 * (w+w+α+β)
71+
```
4772

4873
### Predicates for matching
4974

@@ -54,12 +79,14 @@ Similarly `~~x::g` is a way of attaching a predicate `g` to a segment variable.
5479
For example,
5580

5681
```julia:pred1
82+
@syms a b c d
5783

58-
r = @rule ~x + ~~y::(ys->iseven(length(ys))) => "odd terms"
84+
r = @rule ~x + ~~y::(ys->iseven(length(ys))) => "odd terms";
5985

60-
@show r(w + z + z + w)
61-
@show r(w + z + z)
62-
@show r(w + z)
86+
@show r(a + b + c + d)
87+
@show r(b + c + d)
88+
@show r(b + c + b)
89+
@show r(a + b)
6390
```
6491

6592

@@ -68,13 +95,46 @@ r = @rule ~x + ~~y::(ys->iseven(length(ys))) => "odd terms"
6895
Given an expression `f(x, f(y, z, u), v, w)`, a `f` is said to be associative if the expression is equivalent to `f(x, y, z, u, v, w)` and commutative if the order of arguments does not matter. SymbolicUtils has a special `@acrule` macro meant for rules on functions which are associate and commutative such as addition and multiplication of real and complex numbers.
6996

7097
```julia:acr
71-
@syms x y
98+
@syms x y z
7299

73-
acr = @acrule((~y)^(~n) * ~y => (~y)^(~n+1))
100+
acr = @acrule((~a)^(~x) * (~a)^(~y) => (~a)^(~x + ~y))
74101

75-
acr(x^2 * y * x)
102+
acr(x^y * x^z)
76103
```
77104

105+
although in case of `Number` it also works the same way with regular `@rule` since autosimplification orders and applies associativity and commutativity to the expression.
106+
107+
### Example of applying the rules to simplify expression
108+
109+
Consider expression `(cos(x) + sin(x))^2` that we would like simplify by applying some trigonometric rules. First, we need rule to expand square of `cos(x) + sin(x)`. First we try the simplest rule to expand square of the sum and try it on simple expression
110+
```julia:rewrite9
111+
using SymbolicUtils
112+
113+
@syms x::Real y::Real
114+
115+
sqexpand = @rule (~x + ~y)^2 => (~x)^2 + (~y)^2 + 2 * ~x * ~y
116+
117+
sqexpand((cos(x) + sin(x))^2)
118+
```
119+
120+
It works. This can be further simplified using Pythagorean identity and check it
121+
122+
```julia:rewrite10
123+
pyid = @rule sin(~x)^2 + cos(~x)^2 => 1
124+
125+
pyid(cos(x)^2 + sin(x)^2) === nothing
126+
```
127+
128+
Why does it return `nothing`? If we look at the rule, we see that the order of `sin(x)` and `cos(x)` is different. Therefore, in order to work, the rule needs to be associative-commutative.
129+
130+
```julia:rewrite11
131+
acpyid = @acrule sin(~x)^2 + cos(~x)^2 => 1
132+
133+
acpyid(cos(x)^2 + sin(x)^2 + 2cos(x)*sin(x))
134+
```
135+
136+
It has been some work. Fortunately rules may be [chained together](#chaining rewriters) into more sophisticated rewirters to avoid manual application of the rules.
137+
78138

79139
## Composing rewriters
80140

@@ -94,39 +154,63 @@ rewriters.
94154
- `IfElse(cond, rw1, rw2)` runs the `cond` function on the input, applies `rw1` if cond
95155
returns true, `rw2` if it retuns false
96156
- `If(cond, rw)` is the same as `IfElse(cond, rw, Empty())`
97-
- `Prewalk(rw; threaded=false, thread_cutoff=100)` returns a rewriter which does a pre-order
98-
traversal of a given expression and applies the rewriter `rw`. `threaded=true` will
99-
use multi threading for traversal. `thread_cutoff` is the minimum number of nodes
100-
in a subtree which should be walked in a threaded spawn.
101-
- `Postwalk(rw; threaded=false, thread_cutoff=100)` similarly does post-order traversal.
157+
- `Prewalk(rw; threaded=false, thread_cutoff=100)` returns a rewriter which does a pre-order
158+
(*from top to bottom and from left to right*) traversal of a given expression and applies
159+
the rewriter `rw`. `threaded=true` will use multi threading for traversal. `thread_cutoff`
160+
is the minimum number of nodes in a subtree which should be walked in a threaded spawn.
161+
- `Postwalk(rw; threaded=false, thread_cutoff=100)` similarly does post-order
162+
(*from left to right and from bottom to top*) traversal.
102163
- `Fixpoint(rw)` returns a rewriter which applies `rw` repeatedly until there are no changes to be made.
103164
- `PassThrough(rw)` returns a rewriter which if `rw(x)` returns `nothing` will instead
104165
return `x` otherwise will return `rw(x)`.
105166

167+
### Chaining rewriters
106168

107-
Example using Postwalk, and Chain
169+
Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression.
108170

109-
```julia:rewrite6
171+
To check that, we will combine rules from [previous example](#example of applying the rules to simplify expression) into a chain
110172

173+
```julia:composing1
111174
using SymbolicUtils
112175
using SymbolicUtils.Rewriters
113176

114-
r1 = @rule ~x + ~x => 2 * (~x)
115-
r2 = @rule ~x * +(~~ys) => sum(map(y-> ~x * y, ~~ys));
177+
sqexpand = @rule (~x + ~y)^2 => (~x)^2 + (~y)^2 + 2 * ~x * ~y
178+
acpyid = @acrule sin(~x)^2 + cos(~x)^2 => 1
116179

117-
rset = Postwalk(Chain([r1, r2]))
118-
rset_result = rset(2 * (w+w+α+β))
180+
csa = Chain([sqexpand, acpyid])
119181

120-
rset_result
182+
csa((cos(x) + sin(x))^2)
121183
```
122184

123-
It applied `r1`, but didn't get the opportunity to apply `r2`. So we need to apply the ruleset again on the result.
185+
Important feature of `Chain` is that it returns the expressiona instead of `nothing` if it doesn't change the expression
124186

125-
```julia:rewrite7
126-
rset(rset_result)
187+
```julia:composing2
188+
Chain([@acrule sin(~x)^2 + cos(~x)^2 => 1])((cos(x) + sin(x))^2)
127189
```
128190

191+
its important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example
192+
193+
```julia:composing3
194+
cas = Chain([acpyid, sqexpand])
195+
196+
cas((cos(x) + sin(x))^2)
197+
```
198+
since Pythagorean identity is applied before square expansion, so it is unable to match squares of sine and cosine.
199+
200+
One way to circumvent the problem of order of applying rules in chain is to use `RestartedChain`
201+
202+
```julia:composing4
203+
using SymbolicUtils.Rewriters: RestartedChain
204+
205+
rcas = RestartedChain([acpyid, sqexpand])
206+
207+
rcas((cos(x) + sin(x))^2)
208+
```
209+
210+
It restarts the chain after each successful application of a rule, so after `sqexpand` is hit it (re)starts again and successfully applies `acpyid` to resulting expression.
211+
129212
You can also use `Fixpoint` to apply the rules until there are no changes.
130-
```julia:rewrite8
131-
Fixpoint(rset)(2 * (w+w+α+β))
213+
214+
```julia:composing5
215+
Fixpoint(cas)((cos(x) + sin(x))^2)
132216
```

src/rule.jl

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -179,11 +179,11 @@ cos((1 + a))
179179
A rule with 2 segment variables
180180

181181
```julia
182-
julia> r = @rule ~x - ~y => ~x + (-(~y))
183-
~x - ~y => ~x + -(~y)
182+
julia> r = @rule sin(~x + ~y) => sin(~x)*cos(~y) + cos(~x)*sin(~y)
183+
sin(~x + ~y) => sin(~x) * cos(~y) + cos(~x) * sin(~y)
184184

185-
julia> r(a-2b)
186-
(a + (-(2 * b)))
185+
julia> r(sin(a + b))
186+
cos(a)*sin(b) + sin(a)*cos(b)
187187
```
188188

189189
A rule that matches two of the same expressions:

0 commit comments

Comments
 (0)