Квантификатор Forall и комплексные логические предложения в Idris

Я новичок в зависимых типах и, имея опыт работы с 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 (насколько я понимаю, в Агде это будет что-то вроде 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: допустим ли этот вариант, или есть лучший способ сформировать «отрицание отношения»?

Спасибо.


prefix logic dependent-type idris
person Yuuri    schedule 02.12.2014    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Я думаю, единственная проблема здесь в том, что вы использовали [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, потому что Идрис может вывести типы 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)

Я оставлю это как упражнение :).

person Edwin Brady    schedule 03.12.2014