首页 文章

证明函数的总体最多需要n个递归调用

提问于
浏览
1

假设我们正在编写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)

由于 go 中的递归路径,Idris总体检查器认为 pickName 不是全部,并且理所当然:事实上,总体证明不依赖于语法上更小的任何术语,而是依赖于如果 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 回答

  • 2

    在序曲中,我们有:

    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 的方式使用"nonstandard recursion patterns" . 它基本上是 fix : ((a -> b) -> (a -> b)) -> (a -> b) ,除了open-recursive函数有义务传递一个额外的证明项来证明递归参数以某种方式"smaller" . Accessible 参数决定了所使用的递归模式;这里是简单的“减少 Nat -size”模式 . 我们最好使用 sizeRec 而不是 accRec sizeAccessible ,但我无法使其正常工作 . 您可以使用"correct"方式进行编辑 .

    函数的每次迭代,如果找到它,都可以删除该名称 .

    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)
    

    现在,您可以在_577063中使用开放,有根据的递归:

    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)
    

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

    我认为,它 grab 了这个想法背后的直觉,即如果你有无限的名字,但只有有限的许多旧的,你肯定有无数的新名称 .

    (此外,您的代码中的逻辑似乎是错误的 . 您是否翻转了 if 的分支?)

相关问题