Idris中的所有量词和复布尔命题
Idris中的所有量词和复布尔命题
提问于 2014-12-02 14:34:44
我是新的依赖型，并有一个Haskell经验，正在慢慢学习Idris。作为一种努力，我想写一个赫夫曼编码。目前，我正试图编写一个证据，证明代码树的“扁平化”产生了前缀代码，但被量词卡住了。
我有一个简单的归纳命题，即一个列表是另一个列表的前缀：
using (xs : List a, ys : List a)
data Prefix : List a -> List a -> Type where
pEmpty : Prefix Nil ys
pNext : (x : a) -> Prefix xs ys -> Prefix (x :: xs) (x :: ys)- 这是一个有效的方法吗？或者像"xs是ys的前缀，如果存在zs，xs ++ zs = ys“会更好呢？
- 这是引入“所有”量词的正确方法吗？(据我所知，在Agda中，它将类似于
pNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x :: xs) (y :: ys))吗？pNext第一个参数是否应该是隐式的？两个变体之间的语义差异是什么？
然后，我想为一个向量构建一个向量，其中没有一个元素形成另一个元素的前缀：
data PrefVect : Vect n (List a) -> Type where空向量没有前缀：
pvEmpty : PrefVect Nil并给出一个元素x，向量xs，并证明xs的任何元素都不是x的前缀(反之亦然)，x :：xs将保留该属性：
pvNext : (x : [a]) -> (xs : Vect n [a]) ->
All (\y => Not (Prefix x y)) xs ->
All (\y => Not (Prefix y x)) xs ->
PrefVect (x :: xs)这是一个无效的类型，我希望在处理第一个类型，但也有类似的问题，量词在pvNext:这个变体可以接受，还是有一个更好的方式形成一个“否定的关系”？
谢谢。
回答 1
Stack Overflow用户
回答已采纳
发布于 2014-12-03 09:27:41
我认为这里唯一的问题是，您已经使用[a]作为a的类型，在Haskell风格中，而在Idris中，它需要是List a。
在我看来，您的Prefix类型很好，尽管我会将它写成：
data Prefix : List a -> List a -> Type where
pEmpty : Prefix [] ys
pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys)也就是说，x可以是隐式的，您不需要using，因为Idris可以推断xs和ys的类型。这是否是正确的方法实际上取决于您计划使用Prefix类型的目的。当然，测试一个列表是否是另一个列表的前缀是非常容易的。类似于：
testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Maybe (Prefix xs ys)
testPrefix [] ys = Just pEmpty
testPrefix (x :: xs) [] = Nothing
testPrefix (x :: xs) (y :: ys) with (decEq x y)
testPrefix (x :: xs) (x :: ys) | (Yes Refl) = Just (pNext !(testPrefix xs ys
testPrefix (x :: xs) (y :: ys) | (No contra) = Nothing如果您想要证明否定(这似乎是可能的)，那么您需要的类型如下：
testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Dec (Prefix xs ys)我将把这一项作为练习:)。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/27251938
复制相关文章
相似问题
腾讯云开发者
