Automated Reasoning

There was a post about Automated Reasoning in F#, Scala, Haskell, C++, and Julia that uses a simple algorithm from John Harrison's book Handbook of Practical Logic and Automated Reasoning to simplify this equation:

e = (1 + (0 * x)) * 3) + 12

Factor has support for ML-style pattern matching and I thought it would be fun to contribute a simple solution using the match vocabulary.

We want to define a few types of expressions:

TUPLE: Var s ;
TUPLE: Const n ;
TUPLE: Add x y ;
TUPLE: Mul x y ;

Note: we could have made this simpler by assuming integers are constants and strings are variables rather than define the Const and Var tuples, but I wanted to keep this close to the code in the original blog post.

To be able to pattern match, we need to define some match variables:

MATCH-VARS: ?x ?y ;

We want a way to do a single simplification of an expression:

: simplify1 ( expr -- expr' )
    {
        { T{ Add f T{ Const f 0 } ?x } [ ?x ] }
        { T{ Add f ?x T{ Const f 0 } } [ ?x ] }
        { T{ Mul f ?x T{ Const f 1 } } [ ?x ] }
        { T{ Mul f T{ Const f 1 } ?x } [ ?x ] }
        { T{ Mul f ?x T{ Const f 0 } } [ T{ Const f 0 } ] }
        { T{ Mul f T{ Const f 0 } ?x } [ T{ Const f 0 } ] }
        { T{ Add f T{ Const f ?x } T{ Const f ?y } }
                                       [ ?x ?y + Const boa ] }
        { T{ Mul f T{ Const f ?x } T{ Const f ?y } }
                                       [ ?x ?y * Const boa ] }
        [ ]
    } match-cond ;

We have a way to recursively simplify some expressions:

: simplify ( expr -- expr' )
    {
        { T{ Add f ?x ?y } [ ?x ?y [ simplify ] bi@ Add boa ] }
        { T{ Mul f ?x ?y } [ ?x ?y [ simplify ] bi@ Mul boa ] }
        [ ]
    } match-cond simplify1 ;

Finally, we have a word that tries to simplify a value to a constant:

: simplify-value ( expr -- str )
    simplify {
        { T{ Const f ?x } [ ?x ] }
        [ drop "Could not be simplified to a Constant." ]
    } match-cond ;

To check that it works, we can write a unit test that simplifies the original expression above:

{ 15 } [
    T{ Add f
        T{ Mul f
            T{ Add f
                T{ Const f 1 }
                T{ Mul f
                    T{ Const f 0 }
                    T{ Var f "x" } } }
            T{ Const f 3 } }
        T{ Const f 12 } }
    simplify-value
] unit-test

That's cool, but wouldn't it be better if we could work on quotations directly? Let's make a word that converts a quotation to an expression:

: >expr ( quot -- expr )
    [
        {
            { [ dup string? ] [ '[ _ Var boa ] ] }
            { [ dup integer? ] [ '[ _ Const boa ] ] }
            { [ dup \ + = ] [ drop [ Add boa ] ] }
            { [ dup \ * = ] [ drop [ Mul boa ] ] }
        } cond
    ] map concat call( -- expr ) ;

Now that we have that, our test case is a lot simpler:

{ 15 } [
    [ "x" 0 * 1 + 3 * 12 + ] >expr simplify-value
] unit-test

The code for this is on my GitHub.

Note: this takes advantage of a small feature that I added to the match-cond word to provide a way to easily handle a fall-through pattern like the cond word.