Lambda 演算入門

1. 單個字母被稱爲變量
2. 約束變量：一個變量同時出如今函數體和函數參數中
   1. 如 λx.x ，其中 x 同時出如今了 . 字符以前函數參數中和 .字符以後的函數體
   2. 解釋爲：一個參數爲 x ，函數體也爲 x 的 函數
3. 自由變量：即變量沒有在函數體內被預先聲明
4. 一行符號被叫作表達式，或者稱爲λ項，表達式能夠包含
   1. 變量 variables
   2. 函數 function
   3. 應用 application
5. ()括號：有括號時表示期內的表達式是一個總體，沒有括號時 從左往右計算

函數

1. λ參數.函數體，. 字符以前爲參數，. 字符以後爲函數體。這樣的一個表達式稱爲函數
2. 函數能夠由一個或多個表達式構成，必須包括頭部和身體部分
   1. 頭部：.字符以前的部分，由 λ和變量開頭
   2. 身體部分： .字符以後的部分，是一個表達式

變量

1. 全部變量都是 λ 形式（即全部變量都是合法的 λ 表達式）
2. 若是，變量 x 和變量 y 都是 λ 形式，那麼 (xy) 也是 λ 形式
   1. 即一個字母是表達式，多個字母也是表達式
   2. 兩個表達式組合在一塊兒爲一個新的表達式
   3. 且 (λx.y) 也是 λ 形式
3. 這樣的話，能夠理解 (λy.xy)ab 等價於 (((λy.(x y)a))b)
   1. 表達式1 爲： (λy.xy) ，y是函數參數，xy 是函數體
   2. 表達式2 爲：ab

求值

函數在只有一個表達式的時候是不會進行任何操做的，當它有其餘的表達式，那麼這個函數就能夠被解析（resolving），即求值。

解析過程

這個過程極其相似於咱們較爲經常使用的 Ctrl + x 和 Ctrl + v

參數與函數體中有同名變量

1. 以 (λy.x(yz))(ab) 爲例
2. 要替換的變量爲函數參數 y
3. 而後將表達式2 做爲一個總體，替換至表達式1 中的身體部分
4. 刪除函數參數 y
5. 獲得結果 x(abz)

參數與函數體中沒有同名變量

1. 以 (λx.y)a爲例
2. 要替換的變量爲函數參數 x
3. 可是沒有在表達式1 即函數的身體部分 中找到同名變量
4. 那麼表達式2 會被刪除，由於至關於你 Ctrl + x 了一個變量，但沒有找到須要插入的位置
5. 刪除函數參數 x
6. 獲得結果 y

高階函數

1. 以 (λx.(λy.x))a爲例
2. () 內的總體爲函數的身體部分，即表達式1
3. 將表達式1 中的同名變量替換爲表達式2
4. 刪除函數參數 x
5. 獲得結果 λy.a