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

Question

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

Answer 1

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

Об этом подробно говорится в статье Растана "Составление эпсилон-оператора Гильберта".

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

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 опирается на общий порядок типов. Если вы пытаетесь сделать что-то полностью полиморфное, то, насколько я знаю, это невозможно.