Julia-lang 表达式和交换性的比较

Julia-lang comparison of expression and commutativity

好的,我的标题不是很好,但可以通过示例轻松解释。

julia>a = :(1 + 2)
julia>b = :(2 + 1)

julia>a == b
false

我有两个表达式 a 和 b。我想知道他们是否会给我相同的结果 而无需评估

虽然像 + 或 * 这样的交换运算符可以推断出结果是相同的。

编辑: 另一种理解它的方法是比较一个非常具体的表达式子集,这些表达式可以推断出函数的交换性: Expr(:call, +, a, b) <=> Expr(:call, +, b, a)

这是不可能的。在不对它们进行评估的情况下找出两个程序是否具有相同的结果称为 函数问题 并且可证明等同于解决停机问题。

无法计算代码段是否会产生相同的结果。

我们可以编写一个相当简单的函数来检查两个数组是否具有相同的元素,模数排序:

function eq_modulo_ordering!(xs, ys)  # note !, mutates xs and ys
    while !isempty(xs)
        i = findfirst(isequal(pop!(xs)), ys)
        i === nothing && return false
        deleteat!(ys, i)
    end
    isempty(ys)
end
eq_modulo_ordering(xs, ys) = eq_modulo_ordering!(copy(xs), copy(ys))

我们可以使用 then use this function 来检查两个 top-level 表达式是否等价。

function expr_equiv(a::Expr, b::Expr, comm)
    a.head === b.head || return false
    a.head === :call || return a == b
    a.args[1] ∈ comm || return a == b

    eq_modulo_ordering(a.args, b.args)

end
expr_equiv(a, b, comm) = a == b
expr_equiv(a, b) = expr_equiv(a, b, [:+])

在我们想要检查两个表达式在顶层之外是否完全等价的情况下,我们可以修改我们的函数以使用相互递归来检查子表达式是否为 expr_equiv,而不是 isequal.

function eq_modulo_ordering!(xs, ys, comm)  # note !, mutates xs and ys
    while !isempty(xs)
        x = pop!(xs)
        i = findfirst(b -> expr_equiv(x, b, comm), ys)
        i === nothing && return false
        deleteat!(ys, i)
    end
    isempty(ys)
end
eq_modulo_ordering(xs, ys, comm) = eq_modulo_ordering!(copy(xs), copy(ys), comm)

function expr_equiv(a::Expr, b::Expr, comm)
    a.head === b.head || return false
    a.head === :call || return a == b
    a.args[1] ∈ comm || return all(expr_equiv.(a.args, b.args, Ref(comm)))

    eq_modulo_ordering(a.args, b.args, comm)
end
expr_equiv(a, b, comm) = a == b
expr_equiv(a, b) = expr_equiv(a, b, [:+])

我们现在可以按预期使用 expr_equiv,可选择提供可交换的函数列表。

julia> expr_equiv(:((a + b + b) * c), :((b + a + b) * c))
true

julia> expr_equiv(:((a + a + b) * c), :((b + a + b) * c))
false

julia> expr_equiv(:(c * (a + b + b)), :((b + a + b) * c), [:+, :*])
true