我想要一个find
函数用于大小有界类型的流,类似于列表和查找函数。汇总和搜索流中的元素
total
find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a
的挑战是它,使其:
- 是总
- 消耗不超过
恒定log_2Ñ空间,其中N是编码最大a
所需的比特的数量。 - 时间不超过一分钟,以检查在编译时
- 没有征收成本运行
通常对于流的总能找得到实现听起来荒谬。流是无限的,并且谓词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}
有没有办法告诉总体检查使用无限燃料验证搜索在特定流是总?
可以用'isCyclic'和'find'来执行而不依赖线性空间'Nat's吗?我甚至没有耐心让'all16bits'在我的机器上完成,我认为'Nat'是罪魁祸首。对所有'unsigned int'进行迭代的未优化C程序在我的机器上需要超过10秒钟,并且我的目标是具有恒定空间消耗的可比性能。 –
你是对的,这是一个长期存在的问题。二进制数可以减轻疼痛。 github上有一个项目,旨在将Coq的二进制数字移植到Idris –
这些二进制数字是一个未经优化的归纳定义吗?我想这会有所帮助,但可以使用优化的任意精度unsigned int来完成吗? (无论哪种解决方案都会消耗$ \ log_2 n $而不是不变的空间。) –