Can predicates be dynamically analyzed?

Question

Let's say I have these three predicates:

Predicate<int> pred1 = x => x > 0;
Predicate<int> pred2 = x => x > 0 && true;
Predicate<int> pred3 = x => false;

From a human point of view, it's trivial to say that pred1 and pred2 are equivalent while pred3 is not. By equivalent, I mean that for every possible input value, the value outputted by both pred1 and pred2 will be the same.

I would like to calculate a unique hash for a given predicate ; two predicates being equivalent should have the same hash (like pred1 and pred2), two predicates being not equivalent shall not (like pred1 and pred3).

Has it already been done before (again, in a .NET language)? I know side effects are basically the bane of such analysis ; but if we "forbid" side-effects, can it be done in .NET (swiftly)?

What would be the best approach to this requirement?

Answer 1

As already mentioned in the comments, solving this is theoretically impossible - at least in the general case when the predicates can run code that may not terminate (e.g. a recursive call), meaning that there is a proof that you cannot ever implement a program that will be able to do this correctly on all inputs.

In practice, it really depends on what you want to do. If you want to apply a couple of simple rules to simplify the predicates, then you can do that. It won't handle all situations, but it may as well handle the cases that actually matter to you.

Since F# is inherited from the ML-family of languages (which have been pretty much designed for solving these kinds of problems), I'm going to write a simple example in F#. In C#, you could do the same using a visitor over expression trees, but it would probably be 10x longer.

So, using F# quotations, you can write two predicates as:

let pred1 = <@ fun x -> x > 0 @>
let pred2 = <@ fun x -> x > 0 && true @>

Now, we want to walk over the expression tree and perform some simple reductions like:

if true then e1 else e2   ~> e1
if false then e1 else e2  ~> e2
if e then true else false ~> e

To do that in F#, you can iterate over the expression recursively:

open Microsoft.FSharp.Quotations

// Function that implements the reduction logic
let rec simplify expr =
  match expr with
  // Pattern match on 'if then else' to handle the three rules
  | Patterns.IfThenElse(Simplify(True), t, f) -> t
  | Patterns.IfThenElse(Simplify(False), t, f) -> f
  | Patterns.IfThenElse(cond, Simplify(True), Simplify(False)) -> cond      

  // For any other expression, we simply apply rules recursively
  | ExprShape.ShapeCombination(shape, exprs) ->
      ExprShape.RebuildShapeCombination(shape, List.map simplify exprs)
  | ExprShape.ShapeVar(v) -> Expr.Var(v)
  | ExprShape.ShapeLambda(v, body) -> Expr.Lambda(v, simplify body)

// Helper functions and "active patterns" that simplify writing the rules    
and isValue value expr = 
  match expr with
  | Patterns.Value(v, _) when v = value -> Some()
  | _ -> None

and (|Simplify|) expr = simplify expr
and (|True|_|) = isValue true
and (|False|_|) = isValue false

When you now call simplify pred1 and simplify pred2, the result is the same expression. Obviously, I cannot fit a complete description into a single answer, but hopefully you get the idea (and why F# is really the best tool here).