3

假设我有这三个谓词:

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

从人类的角度来看,说它是微不足道的,pred1并且pred2是等价的,而pred3不是。等效,我的意思是对于每个可能的输入值,两者输出的值都是pred1相同pred2的。

我想计算给定谓词的唯一哈希;两个等价的谓词应该具有相同的散列(like pred1and pred2),两个不等价的谓词不应该(like pred1and pred3)。

以前是否已经做过(同样,使用 .NET 语言)?我知道副作用基本上是这种分析的祸根;但是如果我们“禁止”副作用,它可以在 .NET 中(迅速)完成吗?

满足此要求的最佳方法是什么?

4

1 回答 1

8

正如评论中已经提到的,解决这个问题在理论上是不可能的——至少在一般情况下,谓词可以运行可能不会终止的代码(例如递归调用),这意味着有证据表明你永远无法实现一个程序将能够在所有输入上正确执行此操作。

在实践中,这真的取决于你想做什么。如果您想应用一些简单的规则来简化谓词,那么您可以这样做。它不会处理所有情况,但它也可以处理对您真正重要的情况。

由于 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 pred1andsimplify pred2时,结果是相同的表达式。显然,我无法将完整的描述放入一个答案中,但希望您能理解(以及为什么 F# 确实是这里最好的工具)。

于 2014-06-13T15:24:16.953 回答