如何在 OCaml 中实现 lambda 演算？

Question

在 OCaml 中，“fun”对我来说似乎是绑定运算符。OCaml 有内置替换吗？如果有，如何实施？是使用de Bruijn索引实现的吗？

只是想知道如何在 OCaml 中实现非类型化 lambda 演算，但没有找到这样的实现。

Answer 1

作为 Bromind，我也不太明白你所说的“OCaml 有内置替换吗？”是什么意思？

\n\n

关于 lambda 演算，我不太明白，但是，如果您谈论编写某种 lambda 演算解释器，那么您需要首先定义您的“语法”：

\n\n

(* Bruijn index *)\ntype index = int\n\ntype term =\n  | Var of index\n  | Lam of term\n  | App of term * term\n

\n\n

我们的语法中的 and(\xce\xbbx.x) y也是如此。(\xce\xbb 0) 1App(Lam (Var 0), Var 1)

\n\n

现在你需要实施你的减少、替代等。例如你可能有这样的东西：

\n\n

(* identity substitution: 0 1 2 3 ... *)\nlet id i = Var i\n\n(* particular case of lift substitution: 1 2 3 4 ... *)\nlet lift_one i = Var (i + 1)\n\n(* cons substitution: t \xcf\x83(0) \xcf\x83(1) \xcf\x83(2) ... *)\nlet cons (sigma: index -> term) t = function\n  | 0 -> t\n  | x -> sigma (x - 1)\n\n(* by definition of substitution:\n       1)  x[\xcf\x83] = \xcf\x83(x)\n       2)  (\xce\xbb t)[\xcf\x83] = \xce\xbb(t[cons(0, (\xcf\x83; lift_one))])\n               where (\xcf\x831; \xcf\x832)(x) = (\xcf\x831(x))[\xcf\x832]\n       3)  (t1 t2)[\xcf\x83] = t1[\xcf\x83] t2[\xcf\x83]\n*)\nlet rec apply_subs (sigma: index -> term) = function\n  | Var i -> sigma i\n  | Lam t -> Lam (apply_subs (function\n                              | 0 -> Var 0\n                              | i -> apply_subs lift_one (sigma (i - 1))\n                             ) t)\n  | App (t1, t2) -> App (apply_subs sigma t1, apply_subs sigma t2)\n

\n\n

正如你所看到的，OCaml 代码只是直接重写定义。

\n\n

现在小步减少：

\n\n

let is_value = function\n  | Lam _ | Var _ -> true\n  | _ -> false\n\nlet rec small_step = function\n  | App (Lam t, v) when is_value v ->\n     apply_subs (cons id v) t\n  | App (t, u) when is_value t ->\n     App (t, small_step u)\n  | App (t, u) ->\n     App (small_step t, u)\n  | t when is_value t ->\n     t\n  | _ -> failwith "You will never see me"\n\nlet rec eval = function\n  | t when is_value t -> t\n  | t -> let t\' = small_step t in\n         if t\' = t then t\n         else eval t\'\n

\n\n

例如您可以评估(\xce\xbbx.x) y：

\n\n

eval (App(Lam (Var 0), Var 1))\n- : term = Var 1\n

\n