2

我是依赖类型的新手，并且拥有 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)

  1. 这是一种有效的方法吗？或者像“ xs是ys的前缀，如果有zs这样xs ++ zs = ys ”会更好？

  2. 引入“forall”量词是否正确（据我所知，在 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 中的量词有类似的问题：这个变体是否可以接受，或者有更好的方法来形成“关系否定”？

谢谢你。

4

1 回答 1

4

我认为这里唯一的问题是您使用Haskell 样式[a]中的列表类型a，而在 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 可以推断xsand的类型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)

我会把那个留作练习:)。

于 2014-12-03T09:27:41.493 回答