突発簡単チュートリアル２：λ計算の操作的意味論

（5/24追記：「λ式とは何か」「β簡約とは何か」あたりは前提知識としています。その部分については、自己引用ですみませんが授業のレジュメや、はてなキーワードのyoriyukiさんによるλ計算についてのエントリなどをば。）

ちょー間が空いてしまいましたが、突然再開。λ式

M ::= x | λx.M | M1 M2

の操作的意味論というと、

(λx.M1)M2 → [M2/x]M1
M1→M1'ならばM1 M2 → M1' M2
M2→M2'ならばM1 M2 → M1 M2'
M→M'ならばλx.M → λx.M'

という帰納的定義によるsmall-step reductionが「普通」です。プログラミング言語を意識して、閉じた式かつ（たとえば）call-by-valueに限ると

V ::= λx.M
M ::= V | x | M1 M2

(λx.M)V → [V/x]M
M1→M1'ならばM1 M2 → M1' M2
M2→M2'ならばM1 M2 → M1 M2'

のようになります。さらにleft-to-rightに限るなら、3番目は「M→M'ならばV M → V M'」となります。

しかし、これだと１ステップごとにパターンマッチして書き換えないといけないので、インタプリタの実装などにはあまり適していません（かつ、定義が式の構造に従った再帰になっていないので美しくありません）。そこで、「式Mを評価したら値Vになる」というbig-step evaluationの関係「M⇒V」を直接定義することにします。（この⇒は普通は $\Downarrow$ と表記しますが、はてなでは入力するのが面倒なので…）

λx.M ⇒ λx.M
M1⇒λx.MかつM2⇒Wかつ[W/x]M⇒Vならば、M1 M2 ⇒ V

この定義を逆に読むと、「λx.Mを評価した値としては、λx.Mそのものを返せばよい」「M1 M2を評価した値としては、M1を評価した値をλx.M、M2を評価した値をW、[W/x]Mを評価した値をVとして、Vを返せばよい」となります。この⇒ではエラーと無限ループの区別がつきませんが、それについてはまたいつか…

しかし、これでもまだ[W/x]Mという代入を毎回計算するあたりが無駄です（代入自身の定義も考慮すると二重再帰になっている）。そこで、前回の環境の概念を利用して、以下のように「環境εの下で式Mを評価すると値Vになる」という関係「ε├ M ⇒ V」を定義します。

M ::= x | λx.M | M1 M2
V ::= Closure(x,M,ε)

ε├ x ⇒ ε(x)
ε├ λx.M ⇒ Closure(x,M,ε)
ε├ M1 ⇒ Closure(x,M,ε')かつε├ M2 ⇒ Wかつε'∪{(x,W)}├ M ⇒ Vならば、ε├ M1 M2 ⇒ V （ただしxがすでにε'に現れていたらε'∪{(x,W)}では「上書き」されるものとする）

この関係「ε├ M ⇒ V」が環境と式から値への関数になっていることに注意して、（たとえば）OCamlで実装すると

type var = string
type exp =
  | Var of var
  | Lam of var * exp
  | App of exp * exp
type env = (string * value) list
and value =
  | Closure of var * exp * env
    
let rec eval e = function
  | Var x -> List.assoc x e
  | Lam(x, m) -> Closure(x, m, e)
  | App(m1, m2) ->
      let Closure(x, m, e') = eval e m1 in
      let w = eval e m2 in
      eval ((x, w) :: e') m

# #use "eval.ml";;
type var = string
type exp = Var of var | Lam of var * exp | App of exp * exp
type env = (string * value) list
and value = Closure of var * exp * env
val eval : env -> exp -> value = <fun>
# let s = Lam("x", Lam("y", Lam("z", App(App(Var "x", Var "z"), App(Var "y", Var "z"))))) ;;
val s : exp =
  Lam ("x",
   Lam ("y", Lam ("z", App (App (Var "x", Var "z"), App (Var "y", Var "z")))))
# let k = Lam("x", Lam("y", Var "x")) ;;
val k : exp = Lam ("x", Lam ("y", Var "x"))
# let i = App(App(s, k), k) ;;
val i : exp =
  App
   (App
     (Lam ("x",
       Lam ("y",
        Lam ("z", App (App (Var "x", Var "z"), App (Var "y", Var "z"))))),
     Lam ("x", Lam ("y", Var "x"))),
   Lam ("x", Lam ("y", Var "x")))
# eval [] (App(i, Lam("a", Var "a"))) ;;
- : value = Closure ("a", Var "a", [])
#

のようになります。それ以前のsmall-step reductionや、環境ではなく代入によるbig-step evaluationもすべてちゃんと実装して比較できれば、関数型言語のモデルとしての（型なし）λ計算の初歩をちょっと理解したといえるかも。

ここから言語を充実させて、環境だけでなくストアや継続も扱えるようにして、lexerとparserも作れば、立派な実用的言語処理系が誕生します。