Thursday, August 6, 2015

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.