MinCaml読解ノート: β簡約

MinCamlでβ簡約と呼んでいるのは、変数の定義が単に別の変数のコピーであるような変数を元の変数で置き換えることである。 つまり let y = x in ... のような変数yを使う箇所を全て元の変数xで置き換える。

変数を別の変数に置き換えるという処理はα変換と似通っており、コードもほとんど同じである。 違いはletのときに変数の値を与える式が変数(KNormal.Var)である場合に限り変換を登録する点等である。

let rec g env = function
  | Add(x, y) -> Add(find x env, find y env)
  | Sub(x, y) -> Sub(find x env, find y env)
  | [...]
  | Let((x, t), e1, e2) ->
      (match g env e1 with
      | Var(y) ->
	  Format.eprintf "beta-reducing %s = %s@." x y;
	  g (M.add x y env) e2
      | e1' ->
	  let e2' = g env e2 in
	  Let((x, t), e1', e2'))
  | [...]