lambda-calc-debruijn.ml

(**
 *      Closed Terms Lambda Caulcus with De Bruijn Indexes 
 *      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 *)

open Format

type term = 
  | Var of int
  | Lamb of int * term
  | App of term * term

let rec term_equal t1 t2 =
  match t1, t2 with
  | App (f, arg1), App (g, arg2) ->
    term_equal f g && term_equal arg1 arg2
  | Lamb (i, body1), Lamb (j, body2) ->
    i = j && term_equal body1 body2
  | Var i, Var j -> i = j
  | _, _ -> false

let rec show_term = function
  | Var i -> sprintf "%d" i
  | Lamb (_, body) -> sprintf "λ%s" (show_term body)
  | App (f, arg) -> sprintf "(%s %s)" (show_term f) (show_term arg)

let p msg term =
  printf "%s %s\n" msg (show_term term)

type env = (int * term) list

let extend k v env =
  (k, v) :: env

let lookup k env =
  List.assoc k env

let rec subst env arg parm = function
  | Lamb (i, body) ->
    if i = arg
    then Lamb (i, body)
    else Lamb (i, subst env arg parm body)
  | App (f, arg') ->
    App (subst env arg parm f, subst env arg parm arg')
  | Var x ->
    if x = arg
    then parm
    else Var x

let rec whnf env = function
  | App (Lamb (i, body), arg) -> 
    whnf env (subst (extend i arg env) i arg body)
  | App (App (_, _) as f, arg) ->
    whnf env (App (whnf env f, arg))
  | term -> term

let rec is_norm = function
  | App (Lamb (_, _), _) ->
    false
  | App (App (_, _) as f, _) ->
    is_norm f
  | App (_, arg) ->
    is_norm arg
  | Lamb (_, body) ->
    is_norm body
  | Var _ -> true

let rec norm env  = function
  | App (f, arg)  ->
    let term = whnf env (App (f, norm env arg)) in
    if is_norm term
    then term
    else norm env term
  | Lamb (parm, body) ->
    Lamb (parm, norm env body)
  | term -> whnf env term

let () =
  let env = [] in
  let zero = Lamb (2, Lamb (1, Var 1)) in
  let succ = Lamb (3, Lamb (2, Lamb (1, (
      App (Var 2, (App (App (Var 3, Var 2), Var 1))))))) in
  let plus = Lamb (4, Lamb (3, Lamb (2, Lamb (1,
      App (App (Var 4, Var 2), App (App (Var 3, Var 2), Var 1)))))) in
  let one = App (succ, zero) in
  let two = App (succ, App (succ, zero)) in 
  let three = App (succ, two) in
  let four = App (App (plus, two), two) in
  p "one" (norm env one);
  p "two" (norm env two);
  p "three" (norm env three);
  p "four" (norm env four);
  ()