Lambda Calculus Interpreter (beta-reduction + alpha-conversion)

lc-interpreter.ml

type term = Var of string | Abs of string * term | App of term * term

let rec to_string t =
  match t with
  | Var x -> x
  | Abs (x, body) -> "λ" ^ x ^ "." ^ to_string body
  | App (t1, t2) -> "(" ^ to_string t1 ^ " " ^ to_string t2 ^ ")"

let fresh_var =
  let counter = ref 0 in
  fun base ->
    incr counter;
    base ^ string_of_int !counter

let rec free_in x t =
  match t with
  | Var y -> y = x
  | App (t1, t2) -> free_in x t1 || free_in x t2
  | Abs (y, body) -> if y = x then false else free_in x body

let rec subst body x replacement =
  match body with
  | Var y -> if y = x then replacement else Var y
  | App (t1, t2) -> App (subst t1 x replacement, subst t2 x replacement)
  | Abs (y, t) ->
      if y = x then Abs (y, t)
      else if free_in y replacement then
        let y' = fresh_var y in
        let t' = subst t y (Var y') in
        Abs (y', subst t' x replacement)
      else Abs (y, subst t x replacement)

let rec reduce t =
  match t with
  | App (Abs (x, body), arg) -> subst body x arg
  | App (t1, t2) ->
      let t1' = reduce t1 in
      if t1 <> t1' then App (t1', t2) else App (t1, reduce t2)
  | Abs (x, body) -> Abs (x, reduce body)
  | Var _ -> t

let rec normalize t =
  let t' = reduce t in
  if t = t' then t else normalize t'