假设我们正在编写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 回答
在序曲中,我们有:
accRec
允许您以编译器可以理解为total
的方式使用"nonstandard recursion patterns" . 它基本上是fix : ((a -> b) -> (a -> b)) -> (a -> b)
,除了open-recursive函数有义务传递一个额外的证明项来证明递归参数以某种方式"smaller" .Accessible
参数决定了所使用的递归模式;这里是简单的“减少Nat
-size”模式 . 我们最好使用sizeRec
而不是accRec
sizeAccessible
,但我无法使其正常工作 . 您可以使用"correct"方式进行编辑 .函数的每次迭代,如果找到它,都可以删除该名称 .
现在,您可以在_577063中使用开放,有根据的递归:
Nat -> a
和Stream a
是一样的,所以IMO,这有点好看:我认为,它 grab 了这个想法背后的直觉,即如果你有无限的名字,但只有有限的许多旧的,你肯定有无数的新名称 .
(此外,您的代码中的逻辑似乎是错误的 . 您是否翻转了
if
的分支?)