The "Boyer Benchmark" in the original Gabriel Lisp benchmarks is an if-simplifying benchmark. It's quite interesting -- I highly recommend looking at it to see what it does. The article below debugs the benchmark code, so it at least does what it is supposed to do -- check that tautologies are tautologies. I don't have a reference on Boyer's tautology algorithm itself. http://home.pipeline.com/~hbaker1/BoyerB.ps.gz At 11:37 AM 3/18/2011, rcs@xmission.com wrote:
Here's a Logic & Programming challenge:
Simplify IF expressions.
The general problem is NP-complete, since nested IF expressions can easily encompass Satisfiability problems. It might be even harder, since simplifying an IF expression down to True or False (when applicable) would require a short (or at least feasible) proof of equivalence, while SAT requires only an example.
Nevertheless, it's reasonable to ask for partial solutions. The "simpler-than" ordering includes a lot of beholder input, and also depends on the application at hand.
I'll offer a few "rules" to start the bidding.
If(A,B,C) with A a predicate, B and C arbitrary types (usually the same), has the value B when A is true, and C when A is false. Other notations include A?B:C, Choose(A,B,C), Boole(A,C,B), with Choose and Boole sometimes interpreted per individual bit.
If(True,B,C) -> B If(False,B,C) -> C If(A,B,B) -> B If(A,B,~B) -> A xor B (B a predicate) If(A,B,C) <-> If(~A,C,B) If(A,B,C) <-> If(A, A&B, (~A)&C ) If(A,B,C) <-> B + If(A,0,C-B) (B and C numerical) If(A,B&C,BvC) <-> Majority(A,B,C) (B and C predicates) If(A<B,A,B) <-> Min(A,B) If(A&B,C,D) <-> If(A,If(B,C,D),D)
A similar challenge can be made for Loop expressions. We've adopted a convention for some binary operations, to represent a variable-length version as a kind of summation, using a larger or boldface version of the operator, with upper & lower limits specifying a range, and an expression for argument_k. Would it be useful to change to a generic Loop expression? Most of the simple manipulations for sums and products are applicable to Loops too.
Rich