How to implement Floyd's Hare and Tortoise algorithm in Agda?

Question

I want to translate the following Haskell code into 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

This allows us to efficiently split a list into two:

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

So, I tried to convert this code to 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))

The only problem is that Agda complains that I'm missing the case for floyd [] (y :: ys). However, this case should never arise. How can I prove to Agda that this case should never arise?

Here's a visual example of how this algorithm works:

+-------------+-------------+
|   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 ^ |
+-------------+-------------+

Here's another example:

+---------------+---------------+
|    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 ^ |
+---------------+---------------+

When the hare (the second argument to floyd) reaches the end of the list, the tortoise (the first argument to floyd) reaches the middle of the list. Thus, by using two pointers (the second one moving twice as fast as the first) we can efficiently split a list into two.

@user3237465 For efficient tail recursion. Either way, it doesn't make any difference to the actual problem. — Aadit M Shah, Feb 17 '16 at 18:03
This `floyd acc [] (y ∷ ys)` case can arise, just by calling that function directly. You could give it a dummy implementation. — Twan van Laarhoven, Feb 17 '16 at 18:04
@TwanvanLaarhoven Indeed, it could arise if we call the `floyd` function directly. However, we're not supposed to. The Haskell type for the `floyd` function is too permissive. I was hoping we could give `floyd` a stricter type in Agda. Perhaps a dependent type? — Aadit M Shah, Feb 17 '16 at 18:07
@Aadit M Shah, it's not efficient — it's unnecessary strict, which means that you can't garbage collect elements of a list as soon as possible, which results in very bad performance. Nobody defines functions like `map`, `_++_` and others using tail recursion, especially in a dependently-typed setting. — effectfully, Feb 17 '16 at 18:09
You could give it the type `floyd : {A : Set} → List A → (xs : List A) → (ys : List A) → length xs ≥ length ys → List A × List A`. — Twan van Laarhoven, Feb 17 '16 at 18:10
@user3237465 I'm used to strict functional programming languages like OCaml and hence I tend to use an accumulator. I keep forgetting that Haskell is non-strict. In OCaml we have both tail recursive and non tail recursive versions of `map`, etc. — Aadit M Shah, Feb 17 '16 at 18:19
Okay, this is the first time I've heard of this algorithm and it seems pretty neat and a quick google search gave me variations/alternates of it that accomplished goals different than yours. Would you please explain the goal that this particular floyd is supposed to accomplish. With such a specification in hand, we can then discuss a dependent type for it ;) — Musa Al-hassy, Feb 17 '16 at 18:21
@MusaAl-hassy I added a visual example of how the algorithm works in the question. — Aadit M Shah, Feb 17 '16 at 18:30
Here's an attempt for a dependent type. `∀ {n A} → (xs : Vec A n) → Σ left ∶ Vec A ⌈ n /2⌉ • Σ right ∶ Vec A ⌊ n /2 ⌋ • xs ≡ left ++ right` where I write `Σ x ∶ X • Y` for the dependent product instead of `Data.Product`'s clunky `Σ[ x ∈ A] Y` ---eww looks like set theory!--- and the ceiling/floor properties can be found in `Data.Nat.Properties`. Of course, as others will note, a separation of concerns might be in order. If the proofs get out of hand, one might form the operation then prove that it satisfies the specification. — Musa Al-hassy, Feb 17 '16 at 19:14

score 6 · Accepted Answer · edited May 23 '17 at 10:28

The same thing as Twan van Laarhoven suggests in the comments but with Vecs. His version is probably better.

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

Also, functions like ≤-refl and ≤-step are somewhere in the standard library, but I was lazy to search.

Here is a silly thing I like to do:

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

This is partly based on the Benjamin Hodgson suggestion in the comment below.

You can often dispense with proofs of `≤` by requiring that the length of one `Vec` be "something plus" the length of the other: `forall {m} -> Vec A n -> Vec A (n + m) -> ...` — Benjamin Hodgson, Feb 17 '16 at 18:18
I think you might have a typo since you're never making any real use of `ys` within `floyd` ... cf http://ideone.com/aKcgNZ which was posted by @user3237465 earlier as a comment — Musa Al-hassy, Feb 17 '16 at 18:19
@Musa Al-hassy, the only use for `ys` we need is to shorten two times faster than `xs`. — effectfully, Feb 17 '16 at 18:22
@BenjaminHodgson But then you'd have to prove that you can split `n` into `ceil (n / 2) + floor (n / 2)` to kick off the algorithm. Which is what floyd seems to be doing in the first place. — gallais, Feb 17 '16 at 18:47

How to implement Floyd's Hare and Tortoise algorithm in Agda?

1 Answers1