type var = string type exp = VAR of var | LAM of var * exp | APP of exp * exp | SUCC | ZERO;; let subst (e: exp) (v: var) : exp -> exp = let rec f (e2: exp) : exp = match e2 with | VAR w -> if v=w then e else e2 | LAM(w,e3) -> if v=w then e2 else LAM(w, f e3) | APP(e1,e2) -> APP(f e1, f e2) | SUCC -> SUCC | ZERO -> ZERO in f;; let rec reduce (e: exp) : exp = match e with | APP (LAM (v,e1), e2) -> subst e2 v e1 | APP (e1, e2) -> APP (reduce e1, reduce e2) | _ -> e;; let twice = LAM("f", LAM("x", APP(VAR "f", (APP (VAR "f", VAR "x")))));; let exp1 = APP(APP(twice, (APP (twice, SUCC))), ZERO);; type exp' = LAM of (exp' -> exp') | APP of exp' * exp' | SUCC | ZERO;; let rec reduce (e: exp') : exp' = match e with | APP (LAM f, e) -> reduce (f e) | APP (e1, e2) -> APP (reduce e1, reduce e2) | _ -> e;; let twice' = LAM(fun f -> LAM(fun x -> APP(f, (APP (f, x)))));; let exp1' = APP(APP(twice', (APP (twice', SUCC))), ZERO);;