汇总和搜索流中的元素

Question

我想要一个find函数用于大小有界类型的流，类似于列表和查找函数。

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

的挑战是它，使其：

1. 是总
2. 消耗不超过恒定 log_2Ñ空间，其中N是编码最大a所需的比特的数量。
3. 时间不超过一分钟，以检查在编译时
4. 没有征收成本运行

通常对于流的总能找得到实现听起来荒谬。流是无限的，并且谓词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)来建立一个List，然后使用List的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