Юлия-Ланг сравнение выражения и коммутативности - PullRequest
Новая
       84

Юлия-Ланг сравнение выражения и коммутативности

0 голосов
/ 21 октября 2018

ОК, мой заголовок не очень хороший, но его легко объяснить на примере. 

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

julia>a == b
false

У меня есть два выражения a и b.Я хотел бы знать, если они дадут мне те же результаты без оценки .

Я полагаю, что коммутативные операторы, такие как + или *, могут сделать вывод, что результаты будут одинаковыми.

РЕДАКТИРОВАТЬ: Другой способ понять это - сравнить очень специфическое подмножество выражений, которые могут сделать выводкоммутативность функции: Expr (: call, +, a, b) <=> Expr (: call, +, b, a)

Ответы [ 2 ]

0 голосов
/ 21 октября 2018

Мы можем написать довольно простую функцию, чтобы проверить, имеют ли два массива одинаковые элементы, упорядочив по модулю: 

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))

Мы можем использовать эту функцию, чтобы проверить, если два верхнего уровня выражения эквивалентны. 

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
0 голосов
/ 21 октября 2018

Это невозможно.Выяснение того, имеют ли две программы один и тот же результат без их оценки, называется Функциональная проблема и доказуемо эквивалентно решению проблемы остановки.

Невозможно вычислить, выполнять ли фрагменты кодабудет иметь тот же результат.

...