Yos*_*aka 7 haskell functional-programming
我正在阅读Richard Bird撰写的名为"与Haskell一起思考功能"的书,并且遇到了关于无限列表上的归纳的完整链概念.它说:
如果xs0,xs1,...是具有极限xs的部分列表序列,并且P(xsn)对于所有n成立,则P(xs)也成立,则属性P被称为链完成.
作为连锁完整财产的一个例子,它说:
所有方程式e1 = e2,其中e1和e2是涉及普遍量化的自由变量的Haskell表达式,是链完整的.
我很难理解这个例子如何适合链完成的属性.并且它还表明不等式e1 =/= e2不一定是链完整的.我如何从这个链完整性的角度理解这些属性？
顺便说一句,这可能不一定是关于Haskell的问题,而是数学方面的问题.
这是一个例子.
假设您的xs_1, xs_2, ...限制列表序列越来越多xs.
对于每一个人k,我们都map id xs_k等于xs_k.
通过链完整性(AKA斯科特连续性)我们得到的map id xs是xs.
这为我们提供了一种xs通过仅对其近似值进行验证来证明极限列表上的属性的方法,这些极限列表可能是无限的xs_k.
这里的直觉是,为了xs成为限制列表,每个xs_k必须等于xs或更短的形式前缀x1:x2:...:xn:undefined.注意未定义的尾部,表示循环计算(例如无限递归).正因为如此,如果我们比较f xs_k和f xs,我们发现,后者必须至少与终止,因为前者.这里的一般想法是,如果我们传递更多或定义的输入,我们得到更多或定义的输出.在数学上,这个概念是通过斯科特订购的单调性捕获的.
斯科特欧米茄的连续性或链条完整性更进一步.它告诉我们f xs序列的极限是完全相同的f xs_k.最终结果近似于近似值的结果f.粗略地说,您可以通过使输入收敛来使输出收敛.
不平等不能以连锁完整的方式运作.实际上,将其xs = [0..]视为无限列表和近似值xs_k = 0:...:k:undefined.很明显,对于每个人xs_k来说都不等于.但我们并没有采取不平等的限制,这种不平等会说明不等于.xskxsxs
总结来说,这里的主题非常广泛.如果您有兴趣,我建议您阅读有关指称语义的内容,例如阅读Winskel的书.