как реализовать лямбда-исчисление в OCaml?

OCaml не выполняет редукции нормального порядка и использует семантику вызова по значению. Некоторые термины лямбда-исчисления имеют нормальную форму, которая не может быть достигнута с помощью этого стратегия оценки.

См. Модель оценки замещения, а также Как бы вы реализовали функцию бета-редукции в F#?.

Как Bromind, я также не совсем понимаю, что вы имеете в виду, говоря: «Есть ли в OCaml встроенная замена?»

О лямбда-исчислении еще раз я не совсем понимаю, но если вы говорите о написании какого-то интерпретатора лямбда-исчисления, вам нужно сначала определить свой «синтаксис»:

(* 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

Я не совсем понимаю, что вы имеете в виду, говоря: "Есть ли в OCaml встроенная замена?...", но относительно того, как лямбда-исчисление может быть реализовано в OCaml, вы действительно можете использовать fun : просто замените все лямбды на 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.: Я поставил все скобки просто для того, чтобы было понятно, возможно, некоторые из них можно убрать.