如何在 OCaml 中实现 lambda 演算？

Question

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

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

Answer 1

我不太明白你所说的 "Does OCaml have built-in substitution? ..." 是什么意思，但是关于如何在 OCaml 中实现 lambda 演算，你确实可以使用 fun ：只需替换所有的 lambdas通过 fun，例如：对于教堂数字：你知道 zero = \f -> (\x -> x)、one = \f -> (\x -> f x)，所以在 Ocaml 中，你会有

let zero = fun f -> (fun x -> x)
let succ = fun n -> (fun f -> (fun x -> f (n f x)))

和 succ zero 给你 one 正如你所期望的那样，即 fun f -> (fun x -> f x) （要突出显示它，你可以例如尝试 (succ zero) (fun s -> "s" ^ s) ("0") 或 (succ zero) (fun s -> s + 1) (0) ).

据我所知，你可以玩let和fun来改变评估策略，但有待确认...

N.B.: 我把所有的括号都加进去只是为了清楚，也许有些可以去掉。

Answer 2

作为Bromind，我也不太明白你说的"Does OCaml have built-in substitution?"

是什么意思

关于 lambda-calculus 我不是很了解，但是，如果你谈论编写某种 lambda-calculus 解释器，那么你需要首先定义你的 "syntax":

(* Bruijn index *)
type index = int

type term =
  | Var of index
  | Lam of term
  | App of term * term

所以 (λx.x) y 将是 (λ 0) 1 并且在我们的语法中 App(Lam (Var 0), Var 1).

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

(* identity substitution: 0 1 2 3 ... *)
let id i = Var i

(* particular case of lift substitution: 1 2 3 4 ... *)
let lift_one i = Var (i + 1)

(* cons substitution: t σ(0) σ(1) σ(2) ... *)
let cons (sigma: index -> term) t = function
  | 0 -> t
  | x -> sigma (x - 1)

(* by definition of substitution:
       1)  x[σ] = σ(x)
       2)  (λ t)[σ] = λ(t[cons(0, (σ; lift_one))])
               where (σ1; σ2)(x) = (σ1(x))[σ2]
       3)  (t1 t2)[σ] = t1[σ] t2[σ]
*)
let rec apply_subs (sigma: index -> term) = function
  | Var i -> sigma i
  | Lam t -> Lam (apply_subs (function
                              | 0 -> Var 0
                              | i -> apply_subs lift_one (sigma (i - 1))
                             ) t)
  | App (t1, t2) -> App (apply_subs sigma t1, apply_subs sigma t2)

如您所见，OCaml 代码只是直接重写定义。

现在小步减少：

let is_value = function
  | Lam _ | Var _ -> true
  | _ -> false

let rec small_step = function
  | App (Lam t, v) when is_value v ->
     apply_subs (cons id v) t
  | App (t, u) when is_value t ->
     App (t, small_step u)
  | App (t, u) ->
     App (small_step t, u)
  | t when is_value t ->
     t
  | _ -> failwith "You will never see me"

let rec eval = function
  | t when is_value t -> t
  | t -> let t' = small_step t in
         if t' = t then t
         else eval t'

例如，您可以评估 (λx.x) y:

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

Answer 3

OCaml 不执行正常顺序归约，而是使用按值调用语义。 Some terms of lambda calculus have a normal form than cannot be reached with this evaluation strategy.

见The Substitution Model of Evaluation, as well as How would you implement a beta-reduction function in F#?。

如何在 OCaml 中实现 lambda 演算？

how to implement lambda-calculus in OCaml?

ocaml

lambda-calculus