MDA之路

MDA,UML,XML,Eclipse及Java相关的Blog
posts - 53, comments - 494, trackbacks - 0, articles - 2
  BlogJava :: 首页 :: 新随笔 :: 联系 :: 聚合  :: 管理

Lambda演算学习笔记

Posted on 2005-05-15 20:53 wxb_nudt 阅读(19908) 评论(42)  编辑  收藏 所属分类: 技术杂谈

前言

blog好久没有更新了,上次更新还是428号。这段时间实在是很忙,4月的最后一周为了赶一篇论文,累死累活,最后在tom的帮助下总算在430号截稿之前完成了。429号的晚上一直改到了第二天凌晨3点才睡。

430号下午回家,可是没有料到长沙的八一路修路,路上堵车。打的从学校到火车站花了40分钟,平时只要15分钟的。于是在最后10分钟一路狂奔,终于在开车前1分钟上车了。

五一长假的第一天去了双峰山,云雾缭绕之中真的颇有几分气势,可惜数码照片全部都拍得很模糊,早知道我就自己动手好了。五一归来马上开始整理软件工程相关资料,一共花了3天时间,还剩软件标准化的部分没有整理完毕。

接下来的三天,一直在学习lambda演算的相关内容,由于资料不全,学习的过程很是痛苦。国内的大学好像基本上不开设Functional Programming课程,因此FP的基础知识lambda演算也讲得很少。不过好歹在网上找到了一些资料,加上数理逻辑中的少量介绍,明白了一个大致。相关资料网址会列在最后。

Lamda演算简介

Wikipedia(维基百科全书)中关于lambda演算的解释如下:

The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what a computable function is. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.

Lambda演算是一个形式系统,它被设计出来用来研究函数定义,函数应用和递归。它是在二十世纪三十年代由Alonzo Church Stephen Cole Kleene发明的。Church1936年使用lambda演算来证明了判定问题是没有答案的。Lambda演算可以用来清晰的定义什么是一个可计算的函数。两个lambda演算表达式是否相等的问题不能够被一个通用的算法解决,这是第一个问题,它甚至排在停机问题之前。为了证明停机问题是没有答案的,不可判定性能够被证明。Lambda演算对于函数式编程语言(例如lisp)有重大的影响。

同时,数理逻辑中对于lambda演算的介绍就简单得多:

λ-演算可以说是最简单、最小的一个形式系统。它是在二十世纪三十年代由Alonzo Church Stephen Cole Kleene发明的。至今,在欧洲得到了广泛的发展。可以说,欧洲的计算机科学是从λ-演算开始的,而现在仍然是欧洲计算机科学的基础,首先它是函数式程序理论的基础,而后,在λ-演算的基础上,发展起来的π-演算、χ-演算,成为近年来的并发程序的理论工具之一,许多经典的并发程序模型就是以π-演算为框架的。

这里不由得想起一位我尊敬的老师的博士毕业论文就是关于π-演算的,可惜这位老师已经去别的学校了。

Lambda演算表达了两个计算机计算中最基本的概念“代入”和“置换”。“代入”我们一般理解为函数调用,或者是用实参代替函数中的形参;“置换”我们一般理解为变量换名规则。后面会讲到,“代入”就是用lambda演算中的β-归约概念。而“替换”就是lambda演算中的α-变换。

Lambda演算系统的形式化定义

维基百科全书上面的对于lambda演算的定义不是很正规,但是说明性的文字较多。而数理逻辑中的定义很严密,不过没有说明不容易理解。我尽可能把所有资料结合起来说明lambda演算系统的定义。

字母表

lambda演算系统中合法的字符如下:

1.         x1x2x3变元(变元的数量是无穷的,不能在有限步骤内穷举,这个很重要,后面有定理是根据这一点证明的)

2.         à 归约

3.         等价

4.         λ,(,)  (辅助工具符号,一共有三个,λ和左括号右括号)

所有能够在lambda演算系统中出现的合法符号只有以上四种,其他符号都是非法的。例如λx.x+2,如果没有其他对于+符号的说明,那么这就是一个非法的λ演算表达式。

λ-

λ-项在一些文章中也称为λ表达式(lambda expression),它是由上面字母表中的合法字符组成的表达式,合法的表达式组成规则如下:

1.         任一个变元是一个项

2.         MN是项,则(MN)也是一个项  function application,函数应用)

3.         M是一个项,而x是一个变元,则(λx.M)也是一个项  function abstraction,函数抽象)

4.         仅仅由以上规则归纳定义得到的符号串是项

说明1λ-项是左结合的,意思就是若f x y都是λ-项,那么f x y(f x) y

说明2(λx.M)这样的λ-项被称为函数抽象,原因是它常常就是一个函数的定义,函数的参数就是变量x,函数体就是M,而函数名称则是匿名的。用一个不恰当的比喻来说,我们通常认为的函数f(x)=x+2,可以被表达为λx.x+2。因为+是未定义的,所以这个比喻只是为了方便理解而已。

说明3MN这样的λ-项被称为函数应用,原因是它表达了将M这个函数应用到N这个概念。沿用上面的例子f(x)=x+2,那么f(2)=2+2;同样的λx.x+2表达了f(x)的概念,那么(λx.x+22表达了f(2)的概念。其中Mλx.x+2N2,所以MN=(λx.x+22

说明4:注意说明3只是为了方便理解,但是还存在很多与直观理解不符合的地方。例如xy也是一个合法的λ-项,它们也是MN形式的,不过xy都仅仅是一个变量而已,谈不上函数代入。

    上面是λ-项的形式化定义,有一些是可以与函数理论直观联系的,而另一些只是说明这个λ-项是合法的,不一定有直观的字面意义。

公式

    MNλ-项,则MàNM=N是公式。

λ-项中的变量自由出现法则

在一个λ-项中,变量要么是自由出现的,要么是被一个λ符号绑定的。还是以函数的方式来理解变量的自由出现和绑定。例如f(x)=xy这个函数,我们知道x是和函数f相关的,因为它是f的形参,而y则是和f无关的。那么在λx.xy这个λ-项中,x就是被λ绑定的,而y则是自由出现的变量。

直观的理解,被绑定的变量就是作为某个函数形参的变量,而自由变量则是不作为任何函数形参的变量。

Lambda变量绑定规则:

1.         在表达式x中,如果x本身就是一个变量,那么x就是一个单独的自由出现。

2.         在表达式λ x. E中,自由出现就是E中所有的除了x的自由出现。这种情况下在E中所有x的出现都称为被表达式中x前面的那个λ所绑定。

3.         在表达式(MN )中,变量的自由出现就是MN中所有变量的自由出现。

另一种关于变量的自由出现的规则也许更直接:

1.         free(x) = x

2.         free(MN) = free(M) È free(N)

3.         free(lx • M) = free(M) {x}

为什么要花大力气来给出变量自由出现的规则,是因为后面的很多地方要用到变量的自由出现的概念。例如α-变换和β-归约。

例子:分析λf.λx.fx中变量的自由出现和绑定状况。

λf.λx.fx =λf.E, E=λx.fx

E=λx.A, A=A1A2, A1=f, A2=x

所以在Afx都是自由出现的,

所以Ex是绑定λ x

所以整个公式中f是绑定第一个λ f的。

λ x的控制域

来看两个λ-项,λx.xxλx.(xx)有何不同?根据左结合的法则,λx.xx(λx.x)x,其中第一个x是被λ绑定的,而第二个x则是自由出现的。而λx.(xx)中两个x都是被λ绑定的。这表明了两个λ-项中λx的控制域是不同的。

我们知道谓词演算中量词也是有控制域的,λx的控制域与它们类似,这里就不给出详细的定义了。其实也很直观。

α-变换(α-conversion

α-变换规则试图解释这样一个概念,λ演算中约束变量的名称是不重要的,例如λx.xλy.y是相同的函数。因此,将某个函数中的所有约束变量全部换名是可以的。但是,换名需要遵循一些约束。

首先是一个说明:如果MNλ-项,xM中有自由出现,若以N置换M中所有x的自由出现(M中可能含有x的约束出现),我们得到另一个λ-项,记为M[x/N]

α-变换规则如下:

λx.M=λy.M[x/y]  如果y没有在M中自由出现,并且只要y替换M中的x,都不会被M中的一个λ绑定。

例子:λx.( λx.x)x = λy(λx.x)y

α-变换主要用来表达函数中的变量换名规则,需要注意的是被换名的只能是M(函数体)中变量的自由出现。

β-归约

β-归约表达的是函数应用或者函数代入的概念。前面提到MN是合法的λ-项,那么MN的含义是将M应用到N,通俗的说是将N作为实参代替M中的约束变量,也就是形参。β-归约的规则如下:

(λx.M)N à M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现

β-归约是λ演算中最重要的概念和规则,它是函数代入这个概念的形式化表示。

一些例子如下:

(lx.ly.y x)(lz.u) ® ly.y(lz.u)

(lx. x x)(lz.u) ® (lz.u) (lz.u)

(ly.y a)((lx. x)(lz.(lu.u) z)) ® (ly.y a)(lz.(lu.u) z)

(ly.y a)((lx. x)(lz.(lu.u) z)) ® (ly.y a)((lx. x)(lz. z))

(ly.y a)((lx. x)(lz.(lu.u) z)) ® ((lx. x)(lz.(lu.u) z)) a

需要多加练习才能习惯这种归约。

η-变换(η-conversion

η-变换表达了“外延性”(extensionality)的概念,在这种上下文中,两个函数被认为是相等的“当且仅当”对于所有的参数,它们都给出同样的结果。我理解为,对于所有的实参,通过β-归约都能得到同样的λ-项,或者使用α-变换进行换名后得到同样的λ-项。

例如λx.fxf相等,如果x没有在f中自由出现。

λ演算的公理和规则组成

这一段来自《数理逻辑与集合论》(第二版 清华大学出版社)。还修正了其中的一个错误。

1.         (λx.M)N à M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现

2.         MàM

3.         MàN, NàL => MàL  (原书中此处错误)

4.         MàM’=>ZMàZM’

5.         MàM’=>MZàM’Z

6.         MàM’=>λx. M àλx. M’

7.         MàM’=>M=M’

8.         M=M’=>M’=M

9.         M=N,N=L=>M=L

10.     M=M’ => ZM = ZM’

11.     M=M’ => MZ = M’Z

12.     M=M’ =>λx. M =λx. M’

如果某一公式MàN或者M=N可以用以上的公理推出,则记为λ├MàNλ├MN

范式

如果一个λ-M中不含有任何形为((λx.N1)N2)的子项,则称M是一个范式,简记为n.f.。如果一个λ-M通过有穷步β-归约后,得到一个范式,则称Mn.f.,没有n.f.λ-项称为n.n.f.

    通俗的说法是,将一个λ-项进行β-归约,也就是进行实参代入形参的过程,如果通过有穷步代入,可以得到一个不能够再进行代入的λ-项,那么这就是它的范式。如果无论怎样代入,总存在可以继续代入的子项,那么它就没有范式。

例子

M = λx.(x((λy.y)x))y,则Mà y((λy.y)y) à yyM有一个n.f.

例子

M =λx.(xx) λx.(xx),则Màλx.(xx) λx.(xx)=M。注意到M的归约只有唯一的一个可能路径,所以M不可能归约到n.f.。所以Mn.n.f.

注意这个λx.(xx) λx.(xx)λ演算的协调性研究中是一个比较经典的项。((λ x. x x) (λ x. x x))被称为Ω, ((λ x. x x x) (λ x. x x x))被称为 Ω2

不动点理论

Λ表示所有的λ-项组成的集合。

定理:对于每一个F∈Λ,存在M∈Λ,使得λ├FM=M

证明:定义wλx.F(xx),又令Mww,则有λ├Mww(λx.F(xx))wF(ww)=FM

证明是非常巧妙的,对于每个F,构造出的这个ww刚好是可以通过一次β-归约得到F(ww)FM,如果再归约一次就得到F(FM),这样可以无限次的归约下去得到F(F(F(F…(FM)…)))

Church-Rosser定理及其等价定理

这两个定理告诉我们这样一个事实:如果M有一个n.f.,则这个n.f.是唯一的,任何β-归约的路径都将终止,并且终止到这个n.f.

Church-Rosser定理:如果λ├M=N,则对某一个Zλ├MàZ并且λ├NàZ

与之等价的定理如下,

Diamond Property定理:如果MàN1,MàN2,则存在某一Z,使得N1àZN2àZ

后记

最后两个定理的证明没有怎么看懂,所以没有在笔记中记下。另外,前天在网上订购的《程序设计语言:概念和结构》第二版刚刚拿到手,其中有关于λ演算的一章。应该也对我大有帮助,待看完再说。

学习λ演算的初衷是了解一些程序设计的最基本原理,没想到最后还是绕到形式系统和数理逻辑这儿来了。不过,形式化表达的λ演算更清晰。

国内大学虽然也开程序设计的课程,不过好像都是pascalc/c++之类,关于程序设计的本质基础的程序好像并不多。随着大学扩招,中国有望在很短的时间内成为世界上程序员最多的国家,如果仅仅只学命令式和面向对象的程序设计,一定是不够的。函数式和逻辑式程序设计语言也是要学学的啊。

文中肯定有很多错漏,希望看出来的人给我留言。

参考文献

School of Computer Science and Software Engineering, Faculty of Information Technology, Monash University, Australia 3800

这个大学的FP课程中的Lambda演算相关部分

http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/

wikipedialambda演算相关介绍

http://en.wikipedia.org/wiki/Lambda_calculus

《数理逻辑与集合论》第二版 清华大学出版社

 


评论

# re: Lambda演算学习笔记  回复  更多评论   

2005-05-16 07:34 by 月光乱乱
小同志 辛苦了!

# re: Lambda演算学习笔记  回复  更多评论   

2005-06-01 18:41 by oneday
blog对lamda的解释很不错。比一般教科书上的要清楚的多。对我的帮助很大,你是老师么? :)
国内有一本南大出版的巴伦德莱赫特的<lamda演算的语法和语义>,也可以作为相应的参考书。
我们开了程序语义学的课,但我认为这种类型的课目前在国内很难上好。

# re: Lambda演算学习笔记  回复  更多评论   

2005-06-02 11:14 by wxb_nudt
我不是老师,只是学生。
Lambda演算其实和我的研究方向不沾边,只不过一次和别人讨论时提起。有感于教材和网上素材不完善,因此整理了一下而已。

# re: Lambda演算学习笔记  回复  更多评论   

2005-11-12 21:45 by xephang
哪位同志有进程代数,派演算方面的书和资料?

# re: Lambda演算学习笔记  回复  更多评论   

2005-12-05 21:03 by Pesky
赞,我觉得比我们老师讲的好多了

# re: Lambda演算学习笔记  回复  更多评论   

2006-01-17 14:42 by 冰岛
我们也要学,倒来倒去,不知道有啥用处!

# re: Lambda演算学习笔记  回复  更多评论   

2006-02-03 01:55 by 李奇
我在剑桥大学学计算机,我们这里就开了functional Language Programming,感觉你说得不错,谢谢你,呵呵,感觉很有收获~~

# re: Lambda演算学习笔记  回复  更多评论   

2007-01-26 05:26 by JGG
我在法国学计算机,本学期也开了个这个课
你写的东西很有用
谢谢

# re: Lambda演算学习笔记  回复  更多评论   

2007-03-16 10:11 by 逸宇行空
最近又收集了点资料,基本上是结合楼主的这篇文章,Wiki中的介绍,再就是<<类型和程序设计语言>>,,欢迎来讨论并指正
http://blog.sina.com.cn/templarwzy

楼主你是长沙的? 科大的吧? 你说的老师是李舟军教授吗?

# re: Lambda演算学习笔记  回复  更多评论   

2007-03-16 16:46 by wxb_nudt
@逸宇行空
对,你都说对了。现在我已经毕业到北京了。

# re: Lambda演算学习笔记  回复  更多评论   

2007-03-18 02:02 by skAzurina
我手头上有一本书,叫做《计算机语言的形式语义》,科学出版社出版的,作者陆汝钤(音同钱),ISBN为7030030222。
这本书在第一章第一节就讲了λ运算,很清楚,比blog主的内容还多一点。感兴趣的可以去看看。

# re: Lambda演算学习笔记  回复  更多评论   

2007-07-14 19:24 by yujian
写得不错,以前没有看懂,今天看了你的文章,感觉非常直白,恍然大悟。

#  'β.x"  回复  更多评论   

2007-08-02 22:04 by 江顺
以后

# re: Lambda演算学习笔记  回复  更多评论   

2007-10-18 21:17 by llin_zou
大张见识~

# re: Lambda演算学习笔记[未登录]  回复  更多评论   

2007-11-11 19:14 by liu
很喜欢看你blog,写的东西都很不错!

# re: Lambda演算学习笔记[未登录]  回复  更多评论   

2008-01-18 16:11 by cy
写得不错,辛苦你了.

# re: Lambda演算学习笔记  回复  更多评论   

2008-11-02 18:08 by miles
有个地方不是很明白:
β-归约:“通俗的说是将N作为实参代替M中的约束变量”

(lx. x x)(lz.u) ® (lz.u) (lz.u)
这里面是将两个x都代替了,但由前文的“λ x的控制域”理解:第一个x是在λ的控制之下,但第二个x不是;而“β-归约”是说“以实参代替约束变量”,也就是说我不太明白为什么将第二个x,也就是自由变量也给代替掉了?
或许我还有一些没能理解透彻的地方,请指教。

# re: Lambda演算学习笔记  回复  更多评论   

2008-11-04 11:58 by miles
@miles
我自己想明白了,谢谢

# re: Lambda演算学习笔记  回复  更多评论   

2008-11-21 08:11 by 微笑的撒旦
很不错,谢谢!
但是,能不能用几句话概括一下到底什么Lambda演算?
比如:基于字母表中,通过什么方法,最后解决什么问题。有个总结性的说明,理解起来应该更容易。

# re: Lambda演算学习笔记  回复  更多评论   

2009-03-07 21:15 by Winston
博主对lambda calculus的理解有至关重要的错误。关于lambda作用域的见解是很明显的错误。lambda calculus不符合左结合的特征,即,lambda x.x x不等价于(lambda x.x) x而是等价于lambda x. (x x)。在您论述beta reduction的时候已经能清楚的看到和这一错误观点的矛盾之处了。请严谨对待之。以上。

# re: Lambda演算学习笔记  回复  更多评论   

2009-03-07 21:17 by Winston
当然,博主对lambda calculus的分析还是浅显易懂的,初学者应该可以受益匪浅。
无意冒犯,但请严谨求证,不要误人子弟。

# re: Lambda演算学习笔记  回复  更多评论   

2009-03-10 20:13 by wxb_nudt
@Winston
谢谢指教,不过这篇blog是几年前写的,都忘记了。大家看的时候注意点吧。最近忙,估计没时间更新了。

# re: Lambda演算学习笔记  回复  更多评论   

2009-06-13 12:39 by lightest
其實Lambda演算的好處是甚麼? 比起圖靈機

# re: Lambda演算学习笔记  回复  更多评论   

2009-09-14 00:07 by 陈星
lamda演算其实有很多奇怪的性质,尤其是对于递归函数的研究,应该是一种十分有利的工具,我是听人说的,自己并不明白,希望博主再努力讲讲。

# re: Lambda演算学习笔记  回复  更多评论   

2009-11-15 14:16 by sigma
比维基百科上说得好。但并不是通俗易懂。不过鉴于是作者的学习笔记,没有过多可讲,还是感谢你!

# re: Lambda演算学习笔记  回复  更多评论   

2010-07-16 17:58 by 王勃
@Winston
博主写的是对的,你理解错了

# re: Lambda演算学习笔记  回复  更多评论   

2010-07-16 21:46 by 王勃
@王勃
我错了,忽略我的评论吧

# re: Lambda演算学习笔记  回复  更多评论   

2010-10-26 10:24 by 饶高琦
楼主的帮助太大了,最近在做数理逻辑的大作业,实在感谢,如获至宝!

# re: Lambda演算学习笔记  回复  更多评论   

2011-01-19 12:14 by 长风(@wildAir)
请问“λ x的控制域”部分是不是讲错了?

在wiki中lambda calculus的Formal definition一节中,有这样的描述:“The body of an abstraction extends as far right as possible”,也就是说λx.ab 等价于 λx.(ab),而不是λ(x.a) b。
所谓的“左结合”法则,指的是应用(application),而非抽象(abstraction): M N P 等价于 (M N) P。

请核实一下,我是初学者,也不能肯定是这边出错了。
谢谢!

# re: Lambda演算学习笔记  回复  更多评论   

2011-05-10 22:42 by 游客
南京大学计算机研究生课程--计算入门。开有λ-演算

# re: Lambda演算学习笔记  回复  更多评论   

2012-07-22 14:49 by 墨燃
@长风(@wildAir) 嗯 同感 我最近刚开始学习的课程与这个有关 application binds to the left,abstraction binds to the right lambda x. x y = lambda x. (x y) 不等于 (lambda x. x) y 请核实一下 刚学 迷糊中

# re: Lambda演算学习笔记  回复  更多评论   

2012-08-28 04:04 by koven
λ-项中的变量自由出现法则 倒数第三行,我猜应该是:
“所以在A中f和x都(不)是自由出现的”

# re: Lambda演算学习笔记  回复  更多评论   

2012-08-28 04:09 by koven
α-变换(α-conversion)倒数第二行例子是否应该是:

例子:λx.( λx.x)x = λy.(λx.x)y

# re: Lambda演算学习笔记[未登录]  回复  更多评论   

2013-10-22 00:42 by young
@Winston
我也有这个疑问,过几天去问教授看看到底哪个是对的。

# re: Lambda演算学习笔记[未登录]  回复  更多评论   

2013-10-22 00:47 by young
@xephang
不知道你说的进程代数指的什么意思,我们学过一门课是关于进程模拟的,教授的教学计划中设计到PI演算,不过后来没讲这部分内容,在给出的参考资料中有一本是:D.Sangiorgi, D.Walker, The Pi-Calculus -- A Theory of Mobile Processes, Cambridge University Press, 2001不知道对你有没有用。

# re: Lambda演算学习笔记[未登录]  回复  更多评论   

2013-10-23 05:29 by young
@skAzurina
这本书现在绝版了吧。

# re: Lambda演算学习笔记  回复  更多评论   

2014-06-19 16:15 by Rogerlee
深入浅出,很好。请问一点地方:
范式一节中M = λx.(x((λy.y)x))y,则Mà y((λy.y)y) à yy。
为什么M进行规约运算之后,只有两个y。
M里面的两个x都是绑定形式的吧,那么不应该是
Mà y((λy.y)y)y à y((y)y)y à yyyy

# re: Lambda演算学习笔记  回复  更多评论   

2014-06-19 16:22 by Rogerlee
@Rogerlee
问完问题,就是容易灵光乍现。我明白了。谢谢你的博客。

# re: Lambda演算学习笔记  回复  更多评论   

2014-06-26 20:58 by 蓝鲸鸡腿
感谢楼主 对课程有所帮助

# re: Lambda演算学习笔记  回复  更多评论   

2015-04-02 03:06 by qilin
感谢博主。

# re: Lambda演算学习笔记  回复  更多评论   

2016-06-01 18:38 by 慕容渊
The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved.

博主这段翻译是有问题的,后面那个 for which 是修饰停机问题的。
正确的涵义应该是这样:
没有一个通用的算法可以解决判定两个 lambda 计算表达式是否相等的问题。这是 lambda 计算的的头号问题,甚至排在停机问题之前。(for which)停机问题的不可决定性(也就是说元图灵机无法判定给定的程序是否在给定的输入上一定停止)是可以被证明的。

而博主翻译的
“为了证明停机问题是没有答案的,不可判定性能够被证明。”
是有问题的。

当然博主的这篇文章仍然很棒,基本上正确表达了维基百科 lambda calculus 词条的前面部分。对于学习 LISP 系语言(个人认为,尤其scheme)的同学来说,博主的这篇文章是有助益的。我在搜索某个问题的时候来到了这个链接,原来是几年前的。
挖坑有理,博主勿怪^_^

# re: Lambda演算学习笔记  回复  更多评论   

2016-06-01 19:01 by 慕容渊
晕。再看了下文章发表在 05 年,居然是11年前,博主是前辈了,失敬失敬...

只有注册用户登录后才能发表评论。


网站导航: