时间戳

首页 > 解决方案 > 证明最多接受 n 次递归调用的函数的整体性

proof - 证明最多接受 n 次递归调用的函数的整体性

问题描述

假设我们正在编写一个 lambda 演算的实现，作为其中的一部分，我们希望能够选择一个新的非冲突名称：

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)

由于 中的递归路径， Idris 总体检查器认为pickName不是总体的，这是go正确的：确实，总体的证明不依赖于任何在语法上更小的术语，而是依赖于观察到如果bindings有k元素，那么它将不需要不仅仅是k + 1递归调用来找到一个新的名字。但是如何用代码来表达呢？

我也倾向于外部验证，首先编写一个函数，然后编写一个（类型检查，但从不执行）证明它具有正确的属性。在这种整体情况下是否有可能pickName？

受@HTNW 启发，看起来正确的方法是使用 aVect而不是列表。从向量中删除元素将使其大小（以类型表示）在语法上更小，避免自己证明的需要。所以，（稍微重构）版本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'

标签： proofidristotality

解决方案

在 Prelude 中，我们有：

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和 aNat -> 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？）

推荐阅读