谓词能被动态分析吗？

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