可以动态分析谓词吗？

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#真的是这里最好的工具).