Тотальность и поиск элементов в потоках

Question

Я хочу find функция для потоков ограниченных по размеру типов, которая аналогична функциям поиска для списков и Vects.

total
find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a

Задача состоит в том, чтобы сделать это:

1. быть полным
2. потреблять не более константы log_2 N пробел, где N - количество битов, необходимых для кодирования наибольшего a,
3. не более минуты, чтобы проверить во время компиляции
4. не накладывать затраты времени выполнения

Вообще, полная реализация find для Streams звучит абсурдно. Потоки бесконечны и предикат const False сделает поиск продолжаться вечно. Хороший способ справиться с этим общим случаем - техника бесконечного топлива.

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

total
find : Fuel -> (a -> Bool) -> Stream a -> Maybe a
find Dry _ _ = Nothing
find (More fuel) f (value :: xs) = if f value
                                   then Just value
                                   else find fuel f xs

Это хорошо работает для моего варианта использования, но мне интересно, можно ли в определенных специализированных случаях проверить целостность без использования forever, В противном случае, кто-то может страдать от скучной жизни в ожидании find forever ?predicateWhichHappensToAlwaysReturnFalse (iterate S Z) заканчивать.

Рассмотрим особый случай, когда a является Bits32,

find32 : (Bits32 -> Bool) -> Stream Bits32 -> Maybe Bits32
find32 f (value :: xs) = if f value then Just value else find32 f xs

Две проблемы: это не тотально и не может вернуться Nothing хотя есть конечное число Bits32 жители попробовать. Может быть, я мог бы использовать take (pow 2 32) чтобы создать список, а затем использовать поиск списка... ну, подождите... один только список занял бы ГБ места.

В принципе это не кажется трудным. Конечно, есть много жителей, и современный компьютер может перебирать все 32-битные перестановки за считанные секунды. Есть ли способ проверить целостность the (Stream Bits32) $ iterate (+1) 0 в конце концов возвращается к 0 и как только он утверждает, что все элементы были проверены с (+1) чисто?

Вот начало, хотя я не уверен, как заполнить дыры и специализироваться find достаточно, чтобы сделать его полным. Может быть, интерфейс поможет?

total
IsCyclic : (init : a) -> (succ : a -> a) -> Type

data FinStream : Type -> Type where
  MkFinStream : (init : a) ->
                (succ : a -> a) ->
                {prf : IsCyclic init succ} ->
                FinStream a

partial
find : Eq a => (a -> Bool) -> FinStream a -> Maybe a
find pred (MkFinStream {prf} init succ) = if pred init
                                          then Just init
                                          else find' (succ init)
  where
    partial
    find' : a -> Maybe a
    find' x = if x == init
              then Nothing
              else
                if pred x
                then Just x
                else find' (succ x)

total
all32bits : FinStream Bits32
all32bits = MkFinStream 0 (+1) {prf=?prf}

Есть ли способ сказать контролеру совокупности использовать бесконечное топливо, проверяя, что поиск по определенному потоку является полным?

Answer 1

Давайте определим, что означает цикличность последовательности:

%default total

iter : (n : Nat) -> (a -> a) -> (a -> a)
iter Z f = id
iter (S k) f = f . iter k f

isCyclic : (init : a) -> (next : a -> a) -> Type
isCyclic init next = DPair (Nat, Nat) $ \(m, n) => (m `LT` n, iter m next init = iter n next init)

Вышесказанное означает, что у нас есть ситуация, которую можно изобразить следующим образом:

--   x0 -> x1 -> ... -> xm -> ... -> x(n-1) --
--                      ^                     |
--                      |---------------------

где m строго меньше, чем n (но m может быть равен нулю). n это некоторое количество шагов, после которого мы получаем элемент последовательности, с которой мы столкнулись ранее.

data FinStream : Type -> Type where
  MkFinStream : (init : a) ->
                (next : a -> a) ->
                {prf : isCyclic init next} ->
                FinStream a

Далее, давайте определим вспомогательную функцию, которая использует верхнюю границу под названием fuel вырваться из петли:

findLimited : (p : a -> Bool) -> (next : a -> a) -> (init : a) -> (fuel : Nat) -> Maybe a
findLimited p next x Z = Nothing
findLimited p next x (S k) = if p x then Just x
                                else findLimited pred next (next x) k

Сейчас find можно определить так:

find : (a -> Bool) -> FinStream a -> Maybe a
find p (MkFinStream init next {prf = ((_,n) ** _)}) =
  findLimited p next init n

Вот несколько тестов:

-- I don't have patience to wait until all32bits typechecks
all8bits : FinStream Bits8
all8bits = MkFinStream 0 (+1) {prf=((0, 256) ** (LTESucc LTEZero, Refl))}

exampleNothing : Maybe Bits8
exampleNothing = find (const False) all8bits               -- Nothing

exampleChosenByFairDiceRoll : Maybe Bits8
exampleChosenByFairDiceRoll = find ((==) 4) all8bits       -- Just 4

exampleLast : Maybe Bits8
exampleLast = find ((==) 255) all8bits                     -- Just 255