1一152期六合图库资料

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 閱讀(19213) 評論(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年前,博主是前輩了,失敬失敬...

只有注冊用戶登錄后才能發表評論。


網站導航:
 
1一152期六合图库资料 中国福利彩票3d开奖 516 金蟾捕鱼 新疆25选7预测 南通棋牌安卓版下载 福彩3d字谜图谜总汇图 浙江6+1 菲律宾中介怎么赚钱 青海快3电子板 河南快赢481客户端下载 大乐透走势图表