正如评论中已经提到的,解决这个问题在理论上是不可能的——至少在一般情况下,谓词可以运行可能不会终止的代码(例如递归调用),这意味着有证据表明你永远无法实现一个程序将能够在所有输入上正确执行此操作。
在实践中,这真的取决于你想做什么。如果您想应用一些简单的规则来简化谓词,那么您可以这样做。它不会处理所有情况,但它也可以处理对您真正重要的情况。
由于 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
andsimplify pred2
时,结果是相同的表达式。显然,我无法将完整的描述放入一个答案中,但希望您能理解(以及为什么 F# 确实是这里最好的工具)。