安全等于进展加保持

16:26 2006-6-24
安全等于进展加保持。

进展:一个良类型系统不会受阻(要么它是一个值,要么它根据求值规则作下一步)
保持:如果一个良类型项做进一步求值,那么所得到的项也是良类型的。

我对此的一个奇怪的理解是,一个良类型系统的值构成一组基,由它的运算所组成的表达式构成一个群。它对其运算保持封闭,具有群的一切"稳定性"。

对于进展,我们只能理解为,它不会到达一个意外的受阻状态。并非所有的项都可以规约为值。例如
(λx. x x)(λx. x x)。不过这个是一个无穷的递归,与我们所要讨论的类型系统无关。

说到这里,我觉得ocaml很特别的一点就是可以定义一个无穷项的数组,例如1,-1,1,-1...,然后对其操作。编译器当然不会为这样的数组的每个元素真的去划分空间,肯定是以某种方式将其递归定义暗地存了起来。例如这种数组本来就是对自己递归定义的。

可是这样的数组有什么用呢?我暂时没有想到。我们可以利用其构造一个数学意义上的数列,然后对其取任何一项。但是我们并不能对其所有项求和。也许这样做仅仅是能让我们以一种简单的方式可以获取其第n项。也许我们可以把fibnacci函数封装在一个类体里然后重载operator[]可以达到同样的视觉效果。然后呢?我们可以把这个operator作为一个functor在构造的时候传入,并作为private成员存储,然后我们还可以定义operator+,operator-,operator*,operator/,方式就是用原有的两个operator[]构造一个新的functor,利用STL现有的functor就可以很简单的完成这个组合。然后呢?这样意义上的数组有什么用?

不知道,哈哈!

嗯,或许我们可以利用这个,加上误差估计技术,将一个函数用某种级数展开,然后进行某种运算例如逐项求导,然后利用误差估计技术,选其前N项求和,然后得到我们要的答案,精确到10^-n次方的一个解。或许吧。

跑题了,我本来是想感叹下lamda演算的伟大呢。
谁能告诉我lamda演算是什么?我的理解就是反复的项的代入替换规约。可是并非如此,对于代入替换,lamda演算有自己的定义。lamda演算本身并不是代入替换。它是什么?它太奇妙了。我们可以用它来模拟无类型数值演算,利用lamda演算的奇妙特性定义Church数值和Bool常数,定义递归函数。OMG~

不会lamda演算的人也会用Functional Programming
Language写程序。这究竟是语言抽象的利呢,还是弊?我们在学一门语言的时候并不用去关心它深厚的理论设计原理。(不过貌似C语言这样的东西没有什么太深奥的可言)

OMG,我觉得我还是对lamda演算一无所知,还是老老实实继续看书吧,不唠叨了,据说关于可计算性理论的书上讲的有这个,我去图书馆找找先。

此博客中的热门博文

少写代码,多读别人写的代码

在windows下使用llvm+clang

tensorflow distributed runtime初窥