c# - 可以动态分析谓词吗？

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# 确实是这里最好的工具)。