[GSOC] Expressions, Rules and first Transformations
This is the status report after the 1st week of gsoc. While I still have normal schedule of university classes, I managed to get some time for coding (could'nt stop me doing this)
Table of Contents
1 Expressions
Expressions are encoded as s-exp with metadata. Therefore, they can be constructed by hand, or with the expresso.construct namespace for convenience. The central function is ex, which generates the s-exp with op as symbol and args as arguments and with the appropriate metadata for the operation.
(use 'numeric.expresso.construct) (ex `* 1 2 3) ;=> (clojure.core/* 1 2 3) (properties (ex `/ 3 2 1)) ;=> [:n-ary [:inverse-of clojure.core/*]]
ex gets the properties of the expression from the multimethod props, which can be extended by users
(defmethod props 'exp [_] [:positive [:arity 1]]) (properties (ex 'exp 0)) ;=> [:positive [:arity 1]]
constructing expressions with ex is still tedious, so there is the with-expression macro.
(with-expresso [+ - * /] (+ 1 2 (* 3 4))) ;=> (clojure.core/+ 1 2 (clojure.core/* 3 4)) (properties (with-expresso [+ - * /] (+ 1 2 (* 3 4)))) ;=> [:associative :commutative :n-ary]
It takes a vector as first argument and replaces in the code all occurences of the symbols with their namespaced-qualified name and calls ex with it.
Because expressions are just s-expressions with metadata (which gets preserved by core.logic) it is easy to manipulate them with core.logic.
2 Rules
Rules are the most important part of the core expression rule based transformer (obviously), so I really want a good rule design, in which
- encoding arbitrary transformations as rules is supported
- it is easy to construct rules syntactically
- rules are not a black-box for expresso, so that rules can be optimized (i.e. pruning the rules to those applicable to the expression)
2.1 Rule representation
Expresso rules are represented by a vector of [pat trans guard] where pat is an syntactical pattern, which gets matched against the expression. Guard is a core.logic relation, which gets checked after a succesfull match. Trans specifies the new form of expression. In the simple case it can be a syntactic expression, or it can be a core.logic relation (details later). The macro rule constructs a rule. Variables are encoded as a symbol starting with ?.
(use 'numeric.expresso.rules)
(use 'clojure.core.logic)
(with-expresso [* + - = /]
(def rules [(rule (* ?x 1) :=> ?x)
(rule (* ?x 0) :=> 0)
(rule (+ ?x 0) :=> ?x)
(rule (+ ?x (- ?x)) :=> 0)
(rule (- ?x ?x) :=> (- (* 2 ?x)))])
;if no guard is provided rule inserts the succeed core.logic goal.
(def with-guard (rule (= (* ?a 'x) ?y) :=> (= 'x (/ ?y ?a)) :if (!= ?a 0)))
(apply-rule with-guard (= (* 'x 1) 2)) ;=> (clojure.core/= x (clojure.core// 2 1))
(apply-rule with-guard (= (* 'x 0) 2)) ;=> nil
;the transformation can be a relation itself,
(use 'numeric.expresso.solve)
(def calc-rule (rule ?x :=> (fn [res] (resulto ?x res)) :if (no-variablo ?x)))
(apply-rule calc-rule (* 3 (+ 2 1))) ;=> 9
(apply-rule calc-rule (* 'x 3)) ;=> nil
)
2.2 Expressions specify the matching algorithm
Look closely at the example of the rule with-guard. applying it to (= (* 'x 1) 2) matches with (= (* ?a 'x) ?y). This is not a strange bug, but intented behaviour. Let me explain the reasons for this:
If you have a rule based translator based on normal unification or pattern matching, it will match syntactically, not semantically. This is a problem, because, for example, (* 3 4) and (* 4 3) are semantically equivalent, but not syntactically. So to simplify multiplication with zero you would have to write multiple rules
(with-expresso [*] (rule (* ?x 0) :=> 0) (rule (* 0 ?x) :=> 0))
It is getting (a lot) worse if you have expressions like (* 2 3 0 1), which is normal in clojure.
Therefore, in expresso, the rules decide the matching algorithms. And again, the matching function is stored in a multimethod (which defaults to syntactical matching) and therefore extensible to new operators.
2.3 Write one, match many
Another situation likely to aries when writing rules for (say) simplification is that you have to duplicate rules with an other operator which behaves the same. Basic example: If you use different implementations for the same function - like clojure.core/+ and an optimized other implementation . you would have to dublicate the rules concerning clojure.core/+ with the other implementation.
Expresso uses clojures ad-hoc hierarchies for this. It matches a pattern against an expression, if the operator of expression is an instance of the operator of the pattern. This enables you to do the following
(derive 'clojure.core/+ e/+) (derive 'other.ns/+ e/+) (with-expresso [+ other.ns/+ e/+] (def r (rule (e/+ ?x 0) :=> ?x)) (apply-rule r (+ 3 0)) ;=> 3 (apply-rule r (other.ns/+ 3 0)) ;=> 3 )
2.4 Going absolutely crazy
This makes it also possible to have very powerful abstract rules. Here is an example for representing mathematical properties of groups. It also shows the function transform-with-rules which recursively applies a vector of rules to the expression
(defmulti group-id identity)
(defmethod group-id :default [_] false)
(defmethod group-id [`+ 0] [_] true)
(defmethod group-id [`* 1] [_] true)
(defn is-group-identityo [op id]
(project [op id]
(== true (group-id [op id]))))
(defmulti group-ne identity)
(defmethod group-ne :default [_] nil)
(defmethod group-ne `+ [_] 0)
(defmethod group-ne `* [_] 1)
(defn group-neo [op res]
(project [op]
(== res (group-ne op))))
(with-expresso [- /]
(defmulti group-inverse first)
(defmethod group-inverse :default [_] nil)
(defmethod group-inverse `+ [[_ x]] (- x))
(defmethod group-inverse `* [[_ x]] (/ 1 x))
)
(use 'numeric.expresso.utils)
(defn is-group-inverso [op x y]
(project [op x]
(if-let [inv (group-inverse [op x])]
(== y inv)
fail)))
(def group-rules
[(rule (ex ?op ?x ?id) :=> ?x :if (is-group-identityo ?op ?id))
(rule (ex ?op ?x ?y) :=> (fn [res] (group-neo ?op res))
:if (is-group-inverso ?op ?x ?y))])
(with-expresso [+ * - /]
(transform-with-rules group-rules (+ 1 0)) ;=> 1
(transform-with-rules group-rules (* 3 1)) ;=> 3
;works because + and * are commutative
(transform-with-rules group-rules (+ 0 1)) ;=> 1
(transform-with-rules group-rules (* 1 3)) ;=> 3
(transform-with-rules group-rules (+ 3 (- 3))) ;=> 0
(transform-with-rules group-rules (* 3 (/ 1 3))) ;=> 1
(transform-with-rules group-rules
(+ (* 1 (* 3 (/ 1 3))) (+ (* 1 2) (- (* 2 1))))) ;=> 1
)
3 What's next
In the next week I want to work further on the transformation with rules, try different strategies (postwalk vs prewalk) also in a core.logic context, and give proper support for n-ary expressions. I plan to do this by allowing a &* syntax in the rules which matches the rest of the arguments.
Ang again, please comment.
Keine Kommentare:
Kommentar veröffentlichen