从Lisp到Lambda演算,再到用Lisp写个Web记事栏
笔记罗马已死,但现今的合众国与共和国都闪耀着罗马的光辉,Lisp也是
初遇Lisp
从前端和cpp
中了解到的匿名函数与lambda
表达式,作为一名React
的爱好与使用者,对于Hook
已经是非常熟悉的了。
在React
目前热门且主流的Hook
声明式写法中,存在一个非常有名的公式如下:
$$ UI = f(state) $$
这个公式,可以说是典型的函数式编程,它的意思是,UI
是一个函数,它的参数是state
,返回值是UI
。在使用Hook
多个月后,笔者对这个清晰简单的写法产生了很大的兴趣,在使用其时,在框架上的心智负担非常大小,不需要详细记住很多的生命周期函数/副作用函数,只需要建立好Hook
的抽象思维即可,关于Hook
与声明式编程,有兴趣的同学可以去直接查阅React
文档以及Flutter
文档,其中有很清晰的介绍。
于是笔者去了解了函数式编程,看到了王垠大佬对相关编程语言的赞誉,于是笔者找到了Lisp
这门古老的语言,当年看黑客与画家
时 又名“Lisp是世界上最好的语言(” ,就已经有所好奇 可惜并没有坚持看下去 ,感觉现在是时候认真的深入学习下了。
最开始直接去看Lisp
文档时,几乎是一脸懵,括号语言?什么鬼?习惯了过程式、命令式以及面向对象编程的程序员几乎很难一下子适应,所以笔者先去了解了下函数式编程的一个核心思想,Lambda Calculus
,即Lambda演算。
Lambda演算
Lambda
是一个纯净的函数,只由函数的input
和ouput
来表示,Lambda
符号$\lambda$只是一个标识特征,.
是一个分隔符,前面是input
,后面是output
,函数主要的逻辑与运算都在ouput
中。所以也可以表示如$\lambda , input , . , ouput$。
一个典型的Lambda表达式
如下,就如$E = mc^2$一样优雅且简洁,并且其演算形式已经被证明是图灵完备的,即能能用纯函数实现一个while
循环,存在停机问题,这个后文会加以说明。
$$ \lambda x . (x+1) $$
理论
学会了Lambda
的表示与思想,就能瞬间学会很多语言的匿名函数或者说Lambda
特性。不过不同语言对于Lambda
的实现特性存在差异。比如Python
的Lambda
是一个严格的实现,其ouput
体内仅仅允许单一的表达式,像javascript
与cpp
的实现则可以包含多条计算。
$\lambda$ 到普通函数的形式化变换如下:
$$ \lambda x . (x+1) \quad \hArr \quad f(x)=x+1 \quad \hArr \quad x+1=f(x) $$
上面的例子同样可以用c
语言定义如下,不过Lambda
函数计算中全是匿名的,即无法用 变量/标识符 进行 引用/表示 :
int lambda(int x){
return x+1;
}
看了上文的同学可能会疑惑,这不就是一个几乎所有高级语言都有的基本特性,定义一个函数么?这怎么实现一个while
循环,乃至实现一个图灵机,证明图灵完备?不要着急,下面开始进行解释。
首先,有三个法则需要我们作为前置知识进行了解,分别是:$\alpha - \text{变换}$、$\beta - \text{规约}$、$\eta - \text{规约}$,简单来分别是变量等效替换、代入推导,函数等效替换。
他们的公式表达如下:
$\alpha-$变换
$$ \lambda x.\lambda y.2 * x+y \quad \hArr \quad \lambda y.\lambda x. 2 * y+x $$
$\beta-$规约
函数中的自由变量(即ouput
中不由当前对应的input
声明的变量),可以被其上文中的变量的值代入替换,即化简规约。公式样例如下,其中$\lambda y.2*x+y$中的自由变量为$x$,可以被值为3
的$x$规约:
$$ \lambda x.\lambda y. 2 * x + y \quad 3 \quad 2\quad \rArr \quad \lambda y.2 * 3+y \quad 2 \quad \hArr \quad \lambda x.2 * 3 +x \quad 2 \ \rArr 2*3+2 \rArr 8 $$
上文公式先进行关于 $x$ 的 $\beta$ 规约,再进行 $\alpha$ 变换,最后进行关于 $y$ 或者说 $x$ 的 $\beta$ 变换。
再解释下,对于$\lambda x . (x+1)$,需要输入一个$x$作为实际参数才能规约,即实际能够规约的表示为$\lambda , x . (,x + 1)\quad 3$,规约最终结果为$3+1$即$4$。
$\eta-$规约
如果定义域区间上,函数g
和函数f
的等效,那么g
就可以被规约为f
,这个规约的公式如下:
$$ if \quad g(x) \equiv f(x) \quad \forall x \ then \quad \lambda x.g(x) \quad \hArr \quad \lambda x.f(x) $$
假设如果有读者坚持看完上文还没睡着且理解了的话,那么就可以开始进行后续最精彩 无聊且难 的部分了,Y算子的实现。
对于上面如何用函数实现一个while
循环,关键就是靠Y算子。Y算子的定义如下:
$$ \lambda f.(\lambda x. f(x , x)) , (\lambda x. f(x , x)) $$
Y算子可以接收一个待接收一个函数的的函数H,即表达式$Y H$,并根据情况来规约成$H , \text{target function}$还是$H$加上$Y H$自身即$H (Y H)$,以此来产生递归,即循环,具体推导可以见下方参考文献。
Lambda代码
接下来我们开始用Lambda
思想编写javascript
,其中包括了Y算子的JavaScript实现。要读懂下面的代码,首先建议了解下currying,即柯里化。首先是完成一个递归计算阶乘的函数的完全体Overview(概览)。
// factorial function
const fac = n => (n == 0 ? 1 : n * fac(n - 1))
// fac = H fac .1
const H = f => n => (n == 0 ? 1 : n * f(n - 1))
// fac = Y H .2
// Y H = H fac .3=1+2
// Y H = H (Y H) .4=3+2
const Y = f => (x => f(v => x(x)(v)))(x => f(v => x(x)(v)))
console.log({ fac_result: fac(10) })
console.log({ fac_result: H(fac)(10) })
console.log({ result: Y(H)(10) })
console.log({
result:
(f => (x => f(v => x(x)(v)))(x => f(v => x(x)(v))))
(f => n => (n == 0 ? 1 : n * f(n - 1)))
(10)
})
// 上述代码放到浏览器/nodejs环境中执行,结果如下x3:
// { result: 3628800 }
// 是不是很神奇?特别是对于第三个log的结果
任何的递归均有一个等价的循环实现,也就是一个while
的实现,进而可以实现一个图灵机,证明图灵完备。
当然这里可能还会有个疑惑,用while
实现的递归,是不是更加的慢?而且由于嵌套的函数调用栈的存在,内存占用等也会极高,比如一个100的循环,那么就会有100个保存的调用栈?那栈复杂度不是会约等于时间复杂度???
哈哈哈,函数式当然有自己的解决方案,那就是大名鼎鼎的尾调用(Tail Calls),就是把下一个函数的调用放当前函数的最后,直接弹出当前栈,弹入调用栈,这样就可以避免函数调用栈的增加,这样就可以达到更好的性能。可惜ECMAScript
对于Syntactic Tail Calls (STC)的提案2016
年pendding至今2022-02-26
,看issue讨论好像是不方便开发调试时的现场定位。
函数式编程
继续以上面的javascript
代码为例子做展开,比如上面提到的$\lambda x . (x+1)$,就可以编写如下:
x => x + 1
// or
(x) => { return x + 1; }
Lambda
的计算过程,其实就是规约的过程,需要有实际的参数输入,那么我们来表示 $\lambda x . (x+1) \quad 3 $ 如下:
(x => x + 1)(3)
// or
((x) => { return x + 1; })(3)
上面的代码都是可以在浏览器/nodejs环境下运行的哦,当然其他语言也有类似的实现。
后续更多的代码细节推荐查阅这篇博客:ES6函数与Lambda演算 | 小蘿蔔丁
Lisp Coding
那么到现在,已经具备理论基础了,可以去看Common Lisp
文档及其相关的库啦,当然这里笔者还参考了他人的最佳实践。
下面这是一个用Common Lisp
编写的Web记录应用,可以创建、检索、删除记录,并且可以持久化数据。
具体代码及其介绍与参考,见Github: https://github.com/Kingfish404/web-notes-lisp
好了,Lisp函数式之旅到这里暂以告落了,计算机科学的世界非常有趣,旅途愉快,下次见~