Использование: | в функциональном коде - рекурсия по множествам - PullRequest
Новая
       9

Использование: | в функциональном коде - рекурсия по множествам

0 голосов
/ 07 мая 2018

Как можно использовать рекурсивный набор S в Dafny при написании чистого функционального кода? Я могу использовать: | в императивном коде, проверив не пустоту, выбрать элемент s, затем выполнить рекурсию на S - {s}. Не совсем уверен, как сделать: | детерминированный и использовать его в функциональном коде.

1 Ответ

0 голосов
/ 08 мая 2018

Хороший вопрос! (Хотелось бы, чтобы у downvoters была смелость оставить комментарий ...)

Этот вопрос подробно рассматривается в статье Растана "Компиляция оператора Эпсилона Гильберта" .

В частности, см. Раздел 3.2, в котором описано, как написать детерминированную функцию с помощью рекурсии по наборам. По причинам, которые мне не совсем понятны, лемма ThereIsASmallest, доказывающая лемму кода Dafny, не работает для меня в современном Dafny. Вот версия, которая работает (но безобразно): 

lemma ThereIsASmallest(S: set<int>)
    requires S != {}
    ensures exists x :: x in S && forall y | y in S :: x <= y
{
    var y :| y in S;
    if S != {y} {
        var S' := S - {y};
        assert forall z | z in S :: z in S' || z == y;
        ThereIsASmallest(S');
        var x' :| x' in S' && forall y | y in S' :: x' <= y;
        var x := min2(y, x');
        assert x in S;
    }
}

Наконец, отметим, что техника раздела 3.2 опирается на общий порядок типов. Если вы пытаетесь сделать что-то полностью полиморфное, то, насколько я знаю, это невозможно.

...