Как реализовать алгоритм Флойда заяц и черепаху в Agda?

Я хочу перевести следующий код Haskell в Agda:

import Control.Arrow (first)
import Control.Monad (join)

safeTail :: [a] -> [a]
safeTail []     = []
safeTail (_:xs) = xs

floyd :: [a] -> [a] -> ([a], [a])
floyd xs     []     = ([], xs)
floyd (x:xs) (_:ys) = first (x:) $ floyd xs (safeTail ys)

split :: [a] -> ([a], [a])
split = join floyd

Это позволяет нам эффективно разделить список на два:

split [1,2,3,4,5]   = ([1,2,3], [4,5])
split [1,2,3,4,5,6] = ([1,2,3], [4,5,6])

Итак, я попытался преобразовать этот код в Agda:

floyd : {A : Set} → List A → List A → List A × List A
floyd xs        []        = ([] , xs)
floyd (x :: xs) (_ :: ys) = first (x ::_) (floyd xs (safeTail ys))

Единственная проблема в том, что Агда жалуется, что мне не хватает случая для floyd [] (y :: ys). Однако такого случая возникнуть не должно. Как я могу доказать Агде, что такого случая никогда не должно возникнуть?

Вот наглядный пример того, как работает этот алгоритм:

+-------------+-------------+
|   Tortoise  |     Hare    |
+-------------+-------------+
| ^ 1 2 3 4 5 | ^ 1 2 3 4 5 |
| 1 ^ 2 3 4 5 | 1 2 ^ 3 4 5 |
| 1 2 ^ 3 4 5 | 1 2 3 4 ^ 5 |
| 1 2 3 ^ 4 5 | 1 2 3 4 5 ^ |
+-------------+-------------+

Вот еще один пример:

+---------------+---------------+
|    Tortoise   |      Hare     |
+---------------+---------------+
| ^ 1 2 3 4 5 6 | ^ 1 2 3 4 5 6 |
| 1 ^ 2 3 4 5 6 | 1 2 ^ 3 4 5 6 |
| 1 2 ^ 3 4 5 6 | 1 2 3 4 ^ 5 6 |
| 1 2 3 ^ 4 5 6 | 1 2 3 4 5 6 ^ |
+---------------+---------------+

Когда заяц (второй аргумент для floyd) достигает конца списка, черепаха (первый аргумент для floyd) достигает середины списка. Таким образом, используя два указателя (второй движется вдвое быстрее, чем первый), мы можем эффективно разделить список на два.


functional-programming haskell theorem-proving agda floyd-cycle-finding
person Aadit M Shah    schedule 17.02.2016    source источник
comment
Почему аккумулятор?   -  person user3237465    schedule 17.02.2016
comment
@ user3237465 Для эффективной хвостовой рекурсии. В любом случае это не имеет никакого значения для реальной проблемы.   -  person Aadit M Shah    schedule 17.02.2016
comment
Этот floyd acc [] (y ∷ ys) случай может возникнуть, просто вызвав эту функцию напрямую. Вы можете создать фиктивную реализацию.   -  person Twan van Laarhoven    schedule 17.02.2016
comment
@TwanvanLaarhoven В самом деле, это могло бы возникнуть, если бы мы вызывали функцию floyd напрямую. Однако мы не должны этого делать. Тип Haskell для функции floyd слишком разрешительный. Я надеялся, что мы сможем дать floyd более строгий шрифт в Agda. Может, зависимый тип?   -  person Aadit M Shah    schedule 17.02.2016
comment
@Aadit M Shah, это неэффективно - это излишне строго, что означает, что вы не можете собрать элементы списка как можно скорее, что приводит к очень плохой производительности. Никто не определяет такие функции, как map, _++_ и другие, использующие хвостовую рекурсию, особенно в параметрах с зависимой типизацией.   -  person user3237465    schedule 17.02.2016
comment
Вы можете указать ему тип floyd : {A : Set} → List A → (xs : List A) → (ys : List A) → length xs ≥ length ys → List A × List A.   -  person Twan van Laarhoven    schedule 17.02.2016
comment
@ user3237465 Я привык к строгим языкам функционального программирования, таким как OCaml, и поэтому предпочитаю использовать аккумулятор. Я все время забываю, что Haskell не является строгим. В OCaml есть как хвостовая, так и не хвостовая рекурсивные версии map и т. Д.   -  person Aadit M Shah    schedule 17.02.2016
comment
Хорошо, я впервые слышу об этом алгоритме, и он кажется довольно изящным, и быстрый поиск в Google дал мне его варианты / альтернативы, которые достигли целей, отличных от ваших. Не могли бы вы объяснить цель, которую должен достигнуть этот конкретный флойд. Имея такую ​​спецификацию, мы можем обсудить для нее зависимый тип;)   -  person Musa Al-hassy    schedule 17.02.2016
comment
@ MusaAl-hassy Я добавил наглядный пример того, как работает алгоритм в вопросе.   -  person Aadit M Shah    schedule 17.02.2016
comment
Вот попытка зависимого типа. ∀ {n A} → (xs : Vec A n) → Σ left ∶ Vec A ⌈ n /2⌉ • Σ right ∶ Vec A ⌊ n /2 ⌋ • xs ≡ left ++ right где я пишу Σ x ∶ X • Y для зависимого продукта вместо неуклюжего Data.Product Σ[ x ∈ A] Y --- eww похоже на теорию множеств! --- а свойства потолка / пола можно найти в Data.Nat.Properties. Конечно, как заметят другие, разделение проблем может быть уместным. Если доказательства выходят из-под контроля, можно сформировать операцию, а затем доказать, что она удовлетворяет спецификации.   -  person Musa Al-hassy    schedule 17.02.2016

Ответы (1)


arrow_upward
6
arrow_downward

То же, что Тван ван Лаарховен предлагает в комментариях, но с Vecs. Его версия, наверное, лучше.

open import Function
open import Data.Nat.Base
open import Data.Product renaming (map to pmap)
open import Data.List.Base
open import Data.Vec hiding (split)

≤-step : ∀ {m n} -> m ≤ n -> m ≤ suc n
≤-step  z≤n     = z≤n
≤-step (s≤s le) = s≤s (≤-step le)

≤-refl : ∀ {n} -> n ≤ n
≤-refl {0}     = z≤n
≤-refl {suc n} = s≤s ≤-refl

floyd : ∀ {A : Set} {n m} -> m ≤ n -> Vec A n -> Vec A m -> List A × List A
floyd  z≤n            xs       []          = [] , toList xs
floyd (s≤s  z≤n)     (x ∷ xs) (y ∷ [])     = x ∷ [] , toList xs
floyd (s≤s (s≤s le)) (x ∷ xs) (y ∷ z ∷ ys) = pmap (x ∷_) id (floyd (≤-step le) xs ys)

split : ∀ {A : Set} -> List A -> List A × List A
split xs = floyd ≤-refl (fromList xs) (fromList xs)

open import Relation.Binary.PropositionalEquality

test₁ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ [])
test₁ = refl

test₂ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ 6 ∷ [])
test₂ = refl

Также такие функции, как ≤-refl и ≤-step есть где-то в стандартной библиотеке, но мне было лень искать.

Вот глупая вещь, которую я нравится делать:

open import Function
open import Data.Nat.Base
open import Data.Product renaming (map to pmap)
open import Data.List.Base
open import Data.Vec hiding (split)

floyd : ∀ {A : Set}
      -> (k : ℕ -> ℕ)
      -> (∀ {n} -> Vec A (k (suc n)) -> Vec A (suc (k n)))
      -> ∀ n
      -> Vec A (k n)
      -> List A × List A
floyd k u  0            xs = [] , toList xs
floyd k u  1            xs with u xs
... | x ∷ xs' = x ∷ [] , toList xs'
floyd k u (suc (suc n)) xs with u xs
... | x ∷ xs' = pmap (x ∷_) id (floyd (k ∘ suc) u n xs')

split : ∀ {A : Set} -> List A -> List A × List A
split xs = floyd id id (length xs) (fromList xs)

open import Relation.Binary.PropositionalEquality

test₁ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ [])
test₁ = refl

test₂ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ 6 ∷ [])
test₂ = refl

Это частично основано на предложении Бенджамина Ходжсона в комментарии ниже.

person user3237465    schedule 17.02.2016
comment
Часто можно обойтись без доказательств ≤, потребовав, чтобы длина одного Vec была чем-то плюс длина другого: forall {m} -> Vec A n -> Vec A (n + m) -> ... - person Benjamin Hodgson♦; 17.02.2016
comment
Я думаю, у вас есть опечатка, поскольку вы никогда не используете ys в floyd ... cf ideone.com/ aKcgNZ, который ранее был опубликован пользователем @ user3237465 в качестве комментария - person Musa Al-hassy; 17.02.2016
comment
@Musa Al-hassy, ​​единственное использование ys, которое нам нужно, - это сокращение в два раза быстрее, чем xs. - person user3237465; 17.02.2016
comment
@BenjaminHodgson Но тогда вам нужно будет доказать, что вы можете разделить n на ceil (n / 2) + floor (n / 2), чтобы запустить алгоритм. Похоже, именно этим и занимается в первую очередь. - person gallais; 17.02.2016
comment
≤-refl и ≤-step находятся в Data.Nat.Properties - person Twan van Laarhoven; 19.02.2016