I think you got your xor production backwards; should be If(A,~B,B). I'm not sure what it takes to play. For inspiration, you might look at the first few hundred theorems at Metamath.org. How about If(A, true, false) <-> A? What would be nice would be to come up with a complete axiom set for If, so that you could prove any tautology from the axioms. Again, Metamath might suggest answers for this. On Fri, Mar 18, 2011 at 2:37 PM, <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
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun