相信點開這篇文章的你或多或少地聽説過函數式編程這個名詞。在摩爾定律失效的今天，對多核處理器的充分利用成為了一種越發重要的程序優化方法，而函數式編程也因為其並行運算親和的特點在大眾視野中越發頻繁地出現。究其原因，離不開它從其理論上的祖先之一—Lambda演算那裏所繼承的特徵。

而Lambda演算這一起源於20世紀30年代，出自圖靈導師阿隆佐·邱奇之手的形式系統如今已經發展成了蔚為大觀的一個大家族，本文將展示其中最基礎的一種：無類型Lambda演算（這也是最早阿隆佐·邱奇提出的那種）。

無類型Lambda演算的基本規則

無類型Lambda演算中能做的事情只有定義Lambda（經常稱為Abstraction）和調用Lambda（經常稱為Application），它們也是Lambda演算中的基礎表達式。

由於函數式編程範式對主流編程語言的影響，大多數程序員對Lambda表達式這個名字已經不會感到陌生了。不過，無類型Lambda演算中的Lambda要比主流編程語言簡單一些。一個Lambda通常看起來就像這樣：λx.x x ， 其中x是它的參數（每個Lambda只能有一個參數），.是分隔參數與表達式具體定義的分隔符，後面的x x便是它的定義了。

也有些材料的記法不寫空格，上面的例子要改寫成λx.xx

上面的x x如果換成x(x)，可能更符合我們在一般語言中見到的函數調用。但在Lambda演算較常見的寫法中，調用一個Lambda只需要在它和它的參數中間寫個空格。此處我們調用x所給出的參數就是x自己。

以上兩種表達式和定義Lambda時引入的變量加在一起合稱Lambda項，我們在MoonBit裏用一個enum類型來表示它。

enum Term {
  Var(String) // 變量
  Abs(String, Term) // 定義lambda，變量用字符串表示
  App(Term, Term) // 調用lambda
}

我們在日常編程中所接觸的概念諸如布爾值、if表達式、自然數算術乃至遞歸都可以通過Lambda表達式實現，但這並非本文內容的重心所在，有興趣的讀者可以參閲：

• 程序語言理論與實現
• Programming with Nothing

要實現一個無類型Lambda演算的解釋器，我們所需要了解的基本就只有兩條規則：Alpha轉換與Beta歸約。

Alpha轉換所描述的事實是，Lambda的結構是重點，變量名叫什麼沒那麼重要。λx.x和λfoo.foo可以互相替換。對於某些有重複變量名的嵌套Lambda例如λx.(λx.x) x，重命名時不能把內層的變量也重命名了，例如上面的例子可以通過Alpha轉換寫成λy.(λx.x) y。

Beta歸約則專注於處理Lambda的調用，還是舉一個例子：

(λx.(λy.x)) (λs.(λz.z))

在無類型Lambda演算中，調用Lambda之後所需要做的事情僅僅是對參數進行替換(substitution)，上面這個例子裏就需要把變量x替換成(λs.(λz.z))，得到的結果是:

(λy.(λs.(λz.z)))

想看更多的例子可以參見：程序語言理論與實現

自由變量與變量捕獲

一個Lambda項中的變量如果在它所處的上下文中沒有定義，那麼我們叫它自由變量。例如(λx.(λy.fgv h))這個Lambda項中變量fgv和h就沒有對應的Lambda定義。

在進行Beta歸約時，如果用於替換變量的那個Lambda項中含有自由變量，可能會導致一種被稱為“變量捕獲“的行為：

(λx.(λy.x)) (λz.y)

上面這個表達式在替換後會變成：

λy.λz.y

λz.y中的自由變量被當成了某個Lambda的參數，這顯然不是我們想要的。

變量捕獲問題在編寫解釋器時的常見解決方案是在替換前遍歷表達式得到一個自由變量的集合，做替換時遇到內層Lambda就判斷一下變量名在不在這個自由變量集合裏面：

// (λx.E) T => E.subst(x, T)
fn subst(self : Term, var : String, term : Term) -> Term {
  let freeVars : Set[String] = term.get_free_vars()
  match self {
    Abs(variable, body) => {
      if freeVars.contains(variable) {
        //自由變量集合中有當前這個內層lambda的參數名，即會發生變量捕獲
        abort("subst(): error while encountering \(variable)")
      } else {
        ......
      }
    }
    ......
  }
}

接下來我們介紹一種較少見但具有一定便利性的方法：de Bruijn index（德布朗係數）。

de Bruijin index（德布朗係數）

de Bruijn index（德布朗指數）是一種用整數表示Lambda項中變量的技術，具體地説，它用變量所在位置和原先引入它的位置中間有幾層Lambda來替換特定變量。

λx.(λy.x (λz.z z))

λ.(λ.1 (λ.0 0))

上面的例子中，變量x和引入它的地方λx中間有一個λy，於是將x替換為1，而z和定義它的位置中間沒有夾雜其他的Lambda，於是直接用0替換。某種程度上説，德布朗指數的值描述的是變量與對應Lambda的相對距離，此處的距離衡量標註就是中間嵌套的Lambda層數。

同一個變量在不同的地方可能會用不同的整數來替換

我們定義一個新類型TermDBI來表示使用德布朗指數的Lambda項：

enum TermDBI {
  Var(String, Int)
  Abs(String, TermDBI)
  App(TermDBI, TermDBI)
}

不過直接編寫以及閲讀德布朗指數形式的Lambda很痛苦，所以我們需要編寫一個將Term轉換成TermDBI的函數bruijn() - 這也是TermDBI類型定義中仍有String的原因，保留原變量名可用於它的to_string方法，這樣就可以方便地用println打印求值結果查看了。

fn to_string(self : TermDBI) -> String {
  match self {
    Var(name, _) => name
    Abs(name, body) => "(\\\(name).\(body))"
    App(t1, t2) => "\(t1) \(t2)"
  }
}

為了簡化實現，如果輸入的Term中含有自由變量，bruijn()函數會直接報錯。MoonBit將會在標準庫中提供Result[V, E]類型，它有Ok(V)和Err(E)兩個構造器，分別代表計算成功與失敗。不過，目前我們還是得自己定義一下：

enum Result[V, E] {
  Ok(V)
  Err(E)
}

使用過Rust語言的讀者應該會感到熟悉

fn bruijn(self : Term) -> Result[TermDBI, String]

我們採取一種笨辦法來保存變量名與相關聯的嵌套深度，首先定義Index類型：

struct Index {
  name : String
  depth : Int
}

然後寫一個從List[Index]中根據特定name查找對應depth的輔助函數：

// 查找環境中第一個varname對應的整數
fn find(map : List[Index], varname : String) -> Result[Int, String] {
  match map {
    Nil => Err(varname) // abort("variable \'\(varname)\' not found")
    Cons(i, rest) => {
      if i.name == varname {
        Ok(i.depth)
      } else {
        find(rest, varname)
      }
    }
  }
}

現在可以補全bruijn()函數了。

• Var的處理最簡單，只需要查表尋找對應depth即可。
• Abs稍微複雜一點，首先對列表中所有index的depth加一（因為Lambda嵌套加深了一層），然後在列表的開頭加上{ name : varname, depth : 0 }
• App在兩個子項都能轉換時成功，否則返回一個Err

fn go(m : List[Index], t : Term) -> Result[TermDBI, String] {
    match t {
      Var(name) => {
        let idx = find(m, name)
        match idx {
          Err(name) => Err(name)
          Ok(idx) => Ok(Var(name, idx))
        }
      }
      Abs(varname, body) => {
        let m = m.map(fn (index){
          { name : index.name, depth : index.depth + 1 }
        }).cons({ name : varname, depth : 0 })
        let res = go(m, body)
        match res {
          Err(name) => Err(name)
          Ok(term) => Ok(Abs(varname, term))
        }
      }
      App(e1, e2) => {
        match (go(m, e1), go(m, e2)) {
          (Ok(e1), Ok(e2)) => Ok(App(e1, e2))
          (Err(name), _) => Err(name)
          (_, Err(name)) => Err(name)
        }
      }
    }
  }
  go(Nil, self)

在TermDBI上做歸約

歸約主要處理的是App，即調用：

fn eval(self : TermDBI) -> TermDBI {
  match self {
    App(t1, t2) => {
      match (eval(t1), eval(t2)) {
        (Abs(_, t1), t2) => eval(subst(t1, t2))
        (t1, t2) => App(t1, t2)
      }
    }
    Abs(_) => self
    otherwise => abort("eval(): \(otherwise) ")
    // eval應該不會遇到自由變量才對
  }
}

首先對兩個子項嘗試歸約，然後看eval(t1)得到的是否是一個Lambda，如果是，就執行一步變量替換（通過subst函數）然後繼續化簡。對於Lambda(即Abs)，直接原樣返回即可。

subst函數的實現在不用考慮自由變量的情況下簡單了許多，只要記錄遞歸到當前位置的深度並且與遇到的變量進行比對，大小相等就是需要替換的目標變量。

fn subst(t1 : TermDBI, t2 : TermDBI) -> TermDBI {
  fn go(t1 : TermDBI, t2 : TermDBI, depth : Int) -> TermDBI {
    match t1 {
      Var(name, d) => {
        if d == depth {
          t2
        } else {
          t1
        }
      }
      Abs(name, t) => {
        Abs(name, go(t, t2, depth + 1))
      }
      App(tl, tr) => {
        App(go(tl, t2, depth), go(tr, t2, depth))
      }
    }
  }
  go(t1, t2, 0)
}

完整代碼實現

改進

我們在保存變量名到索引的對應關係時使用了List[Index]類型，並且在每增加一層Lambda時更新整個列表，但是這其實是個很笨的辦法。相信聰明且注意力集中的你們很快就能發現，其實只需要保存一個List[String]就夠了，大家如果有興趣也可以自己試着做一做。