Λ演算
| Λ演算 |
λ演算（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展，以變量綁定和替換的規則，來研究函數如何抽象化定義、函數如何被應用以及遞歸的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。lambda演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函數，而任何可計算函數都能以這種形式表達和求值，它能模擬單一磁帶圖靈機的計算過程；儘管如此，lambda演算強調的是變換規則的運用，而非實現它們的具體機器。
目錄
簡介
λ演算（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展，以變量綁定和替換的規則，來研究函數如何抽象化定義、函數如何被應用以及遞歸的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。lambda演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函數，而任何可計算函數都能以這種形式表達和求值，它能模擬單一磁帶圖靈機的計算過程；儘管如此，lambda演算強調的是變換規則的運用，而非實現它們的具體機器。lambda演算可比擬是最根本的編程語言，它包括了一條變換規則（變量替換）和一條將函數抽象化定義的方式。因此普遍公認是一種更接近軟件而非硬件的方式。對函數式編程語言造成很大影響，比如Lisp、ML語言和Haskell語言。在1936年邱奇利用λ演算給出了對於判定性問題（Entscheidungsproblem）的否定：關於兩個lambda表達式是否等價的命題，無法由一個「通用的算法」判斷，這是不可判定性能夠證明的頭一個問題，甚至還在停機問題之先。
評價
頭兩條規則用來生成函數，而第三條描述了函數是如何作用在參數上的。通常，lambda抽象（規則2）和函數作用（規則3）中的括弧在不會產生歧義的情況下可以省略。如下假定保證了不會產生歧義：（1）函數的作用是左結合的，和（2）lambda操作符被綁定到它後面的整個表達式。例如，表達式 (λx.x x)(λy.y) 可以簡寫成λ(x.x x) λy.y 。類似λx.(x y)這樣的lambda表達式並未定義一個函數，因為變量y的出現是自由的，即它並沒有被綁定到表達式中的任何一個λ上。一個lambda表達式的自由變量的集合是通過下述規則（基於lambda表達式的結構歸納地）定義的：在表達式V中，V是變量，則這個表達式里自由變量的集合只有V。在表達式λV .E中（V是變量，E是另一個表達式），自由變量的集合是E中自由變量的集合減去變量V。因而，E中那些V被稱為綁定在λ上。在表達式 (E E')中，自由變量的集合是E和E'中自由變量集合的並集。例，對於表達式λx.x（我們將第一個x視作變量，第二個x視作表達式），其中表達式x中，由1，它的自由變量集合是x，又由2，表達式λx.x的自由變量的集合是表達式x的自由變量集合減去變量x。所以對於表達式λx.x，它的自由變量集合是空。例，對於表達式λx.x x由形式化描述的第3點，我們把它看作((λx.x)(x))，(λx.x)和(x)分別為表達式，由上一例知道(λx.x)的自由變量集合為空，表達式(x)的變量集合為變量x，所以對於λx.x x，它的自由變量集合為x與空的並，即x。在lambda表達式的集合上定義了一個等價關係(在此用==標註)，「兩個表達式其實表示的是同一個函數」這樣的直覺性判斷即由此表述，這種等價關係是通過所謂的「alpha-變換規則」和「beta-歸約規則」。。[1]