1. 程式人生 > >函數語言程式設計之根-拉姆達運算/演算(λ-calculus)

函數語言程式設計之根-拉姆達運算/演算(λ-calculus)

1930s初,普林斯頓大學的邏輯學家阿倫佐·丘奇 (Alonzo Church,1903-1995) 開發出了一種新的形式系統(formal system),即拉姆達運算/演算 (λ-calculus 、lambda calculus ,lambda即希臘字母λ)

λ運算的核心是λ表示式,以此形成函式定義、函式應用和遞迴的形式系統。當使用λ表示式定義出布林值、數值和各種基本操作符等語言元素後,就能夠形成一種程式語言,所以,λ運算是函數語言程式設計語言共同的祖先,典型代表是Lisp(Scheme)、ML、Haskell和Erlang等等。

由於任何一個可計算函式都能用λ運算來表達和求值,因而它等價於圖靈機。

λ運算決定或形成了函數語言程式設計正規化。

下面的內容,將作為學習函數語言程式設計的大圖(big map)/鳥瞰圖,以便在學習過程中知道自己身在何處。


0.1.1 λ表示式

普通的數學函式如f(x)=x+1,功能是給其引數x加上1。為了將數學函式表示成計算機程式中常用的表示式,可以換一種寫法:

λx.( x+1),讀成“對於引數x,x+1”(假定操作符+已經被定義)。丘奇選擇了λ,因此各種相關計算稱為λ演算。
Lambda,λ,僅僅表達的是數學"函式"的概念

各種程式語言,也引入了λ表示式。例如:

C#語言:(x) =>{ return x+1; }

Java語言:(x) ->{ return x+1; }

Scheme語言:(lambda (x) (+ x 1))

1. λ表示式的定義

λ表示式由變數、兩個抽象符號λ和.(即點),以及括號( )組成。合法的λ表示式的遞迴定義如下:

  •  變數x是一個λ表示式。
  •  函式抽象:W是引數為變數x的λ表示式,則λx.W是λ表示式。這種表示式給出了一個函式的定義:W是函式體,形參就是變數x。
    λx.( x+1)
    λx. λy. ( x+y) ;;;表示 λx. (λy. ( x+y))
  •  函式應用:有了f(x)=x+1,自然需要計算f(2),即給函式一個(實際)引數進行求值。A、B是λ表示式,則 (A B) 也是λ表示式,表示將實參B帶入函式A中。

通常,程式語言會提供內建的基本函式,如各種操作符。操作符的應用“是一種”函式應用,從λ表示式的遞迴定義的角度,“函式應用”規則可以得更直接的一條規則:

  • 操作符和λ表示式組成的表示式,是λ表示式。如x+1

下面是一些λ表示式的例子:

最簡單的:x、y、

函式抽象:λx.x、λx.y、

函式應用:(λx.x y)、(x y)、λx. (x y)……

2.λ表示式的特點

從λ表示式的定義,可以引申出它的兩個特點:

  • 匿名函式。數學函式如f(x)=x+1或λ表示式如λx.( x+1),描述了一個計算過程;數學函式的f是函式名,而λ表示式關注計算過程,為該函式命名,變成了程式設計師的事情。
  • 每個函式只有一個輸入引數,如λn. λm.λf.λx. ((n f)  (++ m) )。程式設計時函式通常可以有一個引數列表,邏輯學家 Haskell Curry證明可以將一個擁有多個引數的函式轉化為只有一個引數的多個函式的連續呼叫,這一轉化過程稱為對擁有多個引數的函式的currying/柯里化
3.通過丘奇數,熟悉λ演算的α-變換和β簡化。