optimization - 总计和在流中搜索元素

Question

我想要一个用于具有大小限制类型的流的find函数，该函数类似于List和Vect的find函数。

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

挑战在于如何做到：


总计
消耗的空间不超过常数log_2 N个空间，其中N是编码最大a所需的位数。
在编译时检查时间不超过一分钟
不增加运行时间成本


通常，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)来构建列表，然后使用列表的find ...呃，等等...仅列表会占用GB的空间。

原则上，这似乎并不困难。尝试的居民数量有限，现代计算机可以在几秒钟内迭代所有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