gpt4 book ai didi

haskell - 如何在Agda中实现Floyd的兔子和乌龟算法?

转载 作者:行者123 更新时间:2023-12-03 01:12:49 27 4
gpt4 key购买 nike

我想将以下 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))

唯一的问题是 Agda 提示我遗漏了 floyd [] (y::ys) 的案例。然而,这种情况绝对不应该出现。我如何向 Agda 证明这种情况永远不会发生?

<小时/>

以下是该算法如何工作的直观示例:

+-------------+-------------+
| 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 的第一个参数)到达列表的中间。因此,通过使用两个指针(第二个指针的移动速度是第一个指针的两倍),我们可以有效地将列表分成两个。

最佳答案

与评论中的 Twan van Laarhoven 建议相同,但使用 Vec。他的版本可能更好。

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这样的函数在标准库中的某个地方,但我懒得搜索。

<小时/>

这是一件愚蠢的事情我 like要做的事:

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

这部分基于下面评论中的Benjamin Hodgson建议。

关于haskell - 如何在Agda中实现Floyd的兔子和乌龟算法?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/35464008/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com