Можно ли динамически анализировать предикаты?

Question

Допустим, у меня есть эти три предиката:

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

С человеческой точки зрения, тривиально сказать, что pred1 а также pred2 эквивалентны в то время как pred3 не является. Под эквивалентом я подразумеваю, что для каждого возможного входного значения значение, выводимое обоими pred1 а также pred2 будет таким же.

Я хотел бы вычислить уникальный хэш для данного предиката; два предиката, являющиеся эквивалентными, должны иметь одинаковый хеш (например, pred1 а также pred2), два предиката не эквивалентны pred1 а также pred3).

Это уже было сделано раньше (опять же на языке.NET)? Я знаю, что побочные эффекты - в основном проклятие такого анализа; но если мы "запрещаем" побочные эффекты, можно ли это сделать в.NET (быстро)?

Каков наилучший подход к этому требованию?

Answer 1

Как уже упоминалось в комментариях, решение этой проблемы теоретически невозможно - по крайней мере, в общем случае, когда предикаты могут выполнять код, который может не завершиться (например, рекурсивный вызов), что означает, что есть доказательство того, что вы никогда не сможете реализовать программу, которая сможет сделать это правильно на всех входах.

На практике это действительно зависит от того, что вы хотите сделать. Если вы хотите применить несколько простых правил для упрощения предикатов, то вы можете сделать это. Он не справится со всеми ситуациями, но может также справиться с делами, которые действительно важны для вас.

Поскольку F# унаследован от языков семейства ML (которые в значительной степени разработаны для решения подобных задач), я собираюсь написать простой пример на F#. В C# вы можете сделать то же самое, используя посетитель над деревьями выражений, но это, вероятно, будет в 10 раз длиннее.

Таким образом, используя цитаты F#, вы можете написать два предиката как:

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

Теперь мы хотим пройтись по дереву выражений и выполнить несколько простых сокращений, таких как:

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

Чтобы сделать это в F#, вы можете рекурсивно перебрать выражение:

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

Когда вы сейчас звоните simplify pred1 а также simplify pred2, результат того же выражения. Очевидно, я не могу вписать полное описание в один ответ, но, надеюсь, вы поймете идею (и почему F# действительно лучший инструмент здесь).