可以动态分析谓词吗？答案

【问题标题】：Can predicates be dynamically analyzed?可以动态分析谓词吗？
【发布时间】：2014-08-04 01:30:09
【问题描述】：

假设我有这三个谓词：

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 中（迅速）完成吗？

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

【问题讨论】：

欢迎来到停机问题的精彩世界。祝你好运。
正如 slacks 所暗示的，这在一般情况下被证明是不可能的。您可以期望的最好结果是具有一些误报/误报的近似值。
@SLaks - 相反，停止问题不适用于此处（假设纯谓词，如问题陈述中所述） - 您可以对所有 int 值运行每个谓词并检查如果答案总是相同的，那么它是可判定的。当然，有 2^(2^32) 个可能的谓词这一事实意味着您不会找到始终分隔不同谓词的哈希。
取决于您是否将不终止视为副作用:-)。如果没有副作用包括没有非终止，那么它肯定（理论上）是可行的。
@Servy - 也许我应该说“total”而不是“pure”以避免争议，但许多人确实将不终止视为一种杂质。从库里霍华德的角度来看，偏心导致任何事情都可以证明的逻辑。

标签： c# .net f# functional-programming dynamic-analysis

【解决方案1】：

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

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

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

【讨论】：