Проверка совокупности функций, принимающих не более n рекурсивных вызовов - PullRequest
Новая
       29

Проверка совокупности функций, принимающих не более n рекурсивных вызовов

0 голосов
/ 05 сентября 2018

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

record Ctx where
  constructor MkCtx
  bindings : List String

emptyCtx : Ctx
emptyCtx = MkCtx []

addCtx : String -> Ctx -> Ctx
addCtx name = record { bindings $= (name ::) }

pickName : String -> Ctx -> (String, Ctx)
pickName = go Z
  where
    mkName : Nat -> String -> String
    mkName Z name = name
    mkName n name = name ++ show n

    go n name ctx = let name' = mkName n name in
                    if name' `elem` bindings ctx
                       then go (S n) name ctx
                       else (name', addCtx name' ctx)

Средство проверки целостности Идриса считает, что pickName не является полным из-за рекурсивного пути в go, и это справедливо: действительно, доказательство тотальности не опирается на какой-либо синтаксически меньший термин, а скорее на наблюдение, что если bindings имеет k элементов, тогда для поиска нового имени потребуется не более k + 1 рекурсивных вызовов. Но как это выразить в коде?

Я также склоняюсь к внешней проверке в том смысле, что сначала пишу функцию, а затем пишу (проверка типа, но никогда не выполняю) доказательство того, что она имеет правильные свойства. Возможно ли в этом случае тотальности для pickName?

Вдохновленный @HTNW, похоже, что правильный путь - использовать Vect вместо списка. Удаление элементов из вектора сделает его размер (который выражен в типе) синтаксически меньшим, избегая необходимости доказывать это самостоятельно. Таким образом, (слегка измененная) версия pickName будет 

pickName : String -> Vect n String -> String
pickName name vect = go Z vect
  where
    mkName : Nat -> String
    mkName Z = name
    mkName n = name ++ show n

    go : Nat -> Vect k String -> String
    go {k = Z} n _ = mkName n
    go {k = (S k)} n vect' =
      let name' = mkName n in
      case name' `isElem` vect' of
           Yes prf => go (S n) $ dropElem vect' prf
           No _ => name'

1 Ответ

0 голосов
/ 06 сентября 2018

В прелюдии имеем: 

Smaller x y = size x `LT` size y
instance Sized (List a) where size = length
sizeAccessible : Sized a => (x : a) -> Accessible Smaller x
accRec : (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
         (z : a) -> Accessible rel z -> b

accRec позволяет вам использовать «нестандартные шаблоны рекурсии» таким образом, что компилятор может понимать как total. Это в основном fix : ((a -> b) -> (a -> b)) -> (a -> b), за исключением того, что открытая рекурсивная функция обязана передавать дополнительный термин доказательства, чтобы доказать, что рекурсивный аргумент как-то "меньше" Аргумент Accessible определяет то, что используется шаблон рекурсии; здесь это простой «уменьшающийся Nat размер» паттен. Предпочтительно, мы бы использовали sizeRec вместо accRec + sizeAccessible, но я не могу заставить его работать. Не стесняйтесь редактировать это «правильным» способом.

На каждой итерации вашей функции вы можете удалить имя, если найдете его. 

delFirst : DecEq a => (x : a) -> (xs : List a)
        -> Maybe (ys : List a ** length xs = S (length ys))
delFirst _ [] = Nothing
delFirst x (y :: xs) with (decEq x y)
  delFirst x (x :: xs) | Yes Refl = Just (xs ** Refl)
  delFirst x (y :: xs) | No _ with (delFirst x xs)
    | Nothing = Nothing
    | Just (ys ** prf) = Just (x :: ys ** cong prf)

Теперь вы можете использовать открытую, обоснованную рекурсию в pickName: 

pickName : String -> Ctx -> (String, Ctx)
pickName s ctx = let new = go s (bindings ctx) Z
                  in (new, addCtx new ctx)
  where mkName : Nat -> String -> String
        mkName Z name = name
        mkName n name = name ++ show n
        ltFromRefl : n = S m -> LT m n
        ltFromRefl Refl = lteRefl
        go : String -> List String -> Nat -> String
        go name binds = accRec (\binds, rec, n =>
                          let name' = mkName n name
                           in case delFirst name' binds of
                                   Nothing => name'
                                   Just (binds' ** prf) => rec binds' (ltFromRefl prf) (S n)
                          ) binds (sizeAccessible binds)

A Nat -> a - это то же самое, что и Stream a, поэтому, IMO, это несколько лучше: 

findNew : DecEq a => (olds : List a) -> (news : Stream a) -> a
findNew olds = accRec (\olds, rec, (new :: news) =>
                        case delFirst new olds of
                             Nothing => new
                             Just (olds' ** prf) => rec olds' (ltFromRefl prf) news
                      ) olds (sizeAccessible olds)
  where ltFromRefl : n = S m -> LT m n
        ltFromRefl Refl = lteRefl

pickName : String -> Ctx -> (String, Ctx)
pickName name ctx = let new = findNew (bindings ctx)
                                      (name :: map ((name ++) . show) (iterate S 1))
                     in (new, addCtx new ctx)

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

(Кроме того, логика в вашем коде кажется неправильной. Вы перевернули ветви if?)

...