Skip to content

Instantly share code, notes, and snippets.

@dhilst
Created August 22, 2022 03:00
Show Gist options
  • Save dhilst/61535e0377487bb294996d5399cd595a to your computer and use it in GitHub Desktop.
Save dhilst/61535e0377487bb294996d5399cd595a to your computer and use it in GitHub Desktop.
(**
* 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);
()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment