Hi 

The function `simplify-one` in kibit.core is the “brain” behind kibit:

    (defn simplify-one [expr rules]
      (let [alts (logic/run* [q]
        (logic/fresh [pat subst]
          (logic/membero [pat subst] rules)
          (logic/project [pat subst]
            (logic/all (pat expr)
                         (subst q)))))]
        (if (empty? alts) expr (first alts))))

The line `(logic/membero [pat subst] rules)` picks a rule (both the pattern 
and the substitution part). Both `pat` and `subst` are functions who have 
closed over the same logic vars. pat takes a form and subst takes the logic 
var representing the result as arguments. Since both pat and subst contain 
the same logic vars the final expression `(logic/all (pat expr) (subst q))` 
will only succeed if (pat expr) succeeds. If (pat expr) succeeds it has 
presumably bound its logic vars and since the same vars are closed over in 
subst, the final answer is unified with q, giving us a result. 

Rules are compiled with

    (defn compile-rule [rule]
      (let [[pat alt] (logic/prep rule)]
        [(fn [expr] (logic/== expr pat))
         (fn [sbst] (logic/== sbst alt))]))

(logic/prep rule) walks the rule (where a rule is e.g., [(+ ?x 1) (inc 
?x)]) and replaces symbols starting with `?` with logic vars. The 
compile-rule function is defined in the kibit.rules.util namespace.

This is basically how the kibit rule system works. I don’t think it’s 
powerful enough to create a full-blown computer algebra system and often 
It’s not powerful enough for the kind of rules I’d like to express in 
kibit. Two enhancements I’d like to add are

* Predicates on logic vars: 
    [(foo (? x number?)) (bar ?x)] => match (foo 42) but not (foo :bar)
* Segment vars:
    [(* ??x 1 ??y) (* ??x ??y)] => (* 4 3 2 1 2 3 4) would turn into (* 4 3 
2 2 3 4)
    and
    [(* ??x 0 ??y) 0] => (* 1 2 3 0 4 5 6 7) would turn into 0

David Nolen and Kevin Lynagh has discussed enhancements to the core.logic 
unifier on IRC lately. I haven’t been able to follow along as much as I’d 
like so I’m not completely sure what enhancements they are aiming for. You 
can see some of the results of those discussions in many of Kevins gists on 
github (https://gist.github.com/lynaghk)

Cheers,
Jonas 

On Saturday, December 1, 2012 12:08:16 AM UTC+2, Brent Millare wrote:
>
> Hey all,
>
> Before I diving in detail into the code, can someone provide me a high 
> level explanation of how kibit simplifies code? I understand underneath it 
> uses core.logic and rules but its not clear to me how it picks one form 
> over the other.
>
> I'm trying to extend this to data that represents mathematical 
> expressions. Ideally in the future I'd like to have many types of 
> transformations that enable one to shape a mathematical expression in one 
> way or another depending on the  user's requirements.
>
> My current work (which requires dj atm since its under heavy development) 
> is available here
>
> https://github.com/bmillare/dj.math
>
>

-- 
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clojure@googlegroups.com
Note that posts from new members are moderated - please be patient with your 
first post.
To unsubscribe from this group, send email to
clojure+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en

Reply via email to