2

我想要一个find大小有界类型的流的函数，它类似于 Lists 和 Vects 的查找函数。

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

挑战在于如何做到：

  1. 完全
  2. 消耗不超过常数log_2 N 空间，其中 N 是编码最大所需的位数a。
  3. 在编译时检查不超过一分钟
  4. 不强加运行时成本

通常，Streams 的总 find 实现听起来很荒谬。流是无限的，一个谓词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)结束的无聊生活。

考虑特殊情况 where ais 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...呃，等等...单独的列表会占用 GBs 的空间。

原则上，这似乎不应该是困难的。有许多居民可以尝试，现代计算机可以在几秒钟内遍历所有 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}

有没有办法告诉整体检查器使用无限燃料来验证对特定流的搜索是否完全？

4

1 回答 1

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
于 2017-09-03T13:59:59.493 回答