Skip to content

Instantly share code, notes, and snippets.

@DanielAugusto191

DanielAugusto191/lambCalc.sml

Last active June 9, 2024 20:57
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save DanielAugusto191/5bb378cca5fb2f64ab3884e5db9e1730 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save DanielAugusto191/5bb378cca5fb2f64ab3884e5db9e1730 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
lambCalc.sml
(* (λx.x)a→a *)
(* (λx.λy.x)ab→(λy.a)b→a *)
(* (λx.xx)a→aa *)
(* (λx.λy.xy)a→λy.ay *)
datatype Term
= Var of string
| Abs of string*Term
| App of Term*Term
fun freshVar base used =
let
fun fresh n =
let
val newVar = base ^ Int.toString n
in
if List.exists (fn x => x = newVar) used then fresh (n+1) else newVar
end
in
fresh 0
end
fun collectVars (Var x) = [x]
| collectVars (Abs (x, t)) = x :: collectVars t
| collectVars (App (t1, t2)) = collectVars t1 @ collectVars t2
fun subst (x: string, s: Term, t: Term): Term =
let
fun alphaConvert (t: Term, usedVars: string list) =
case t of
Var v => (Var v, usedVars)
| Abs (v, t1) =>
let
val newV = freshVar v usedVars
val (newT1, newUsedVars) = alphaConvert (subst (v, Var newV, t1),newV:: usedVars)
in
(Abs (newV, newT1), newUsedVars)
end
| App (t1, t2) =>
let
val (newT1, newUsedVars1) = alphaConvert (t1, usedVars)
val (newT2, newUsedVars2) = alphaConvert (t2, newUsedVars1)
in
(App (newT1, newT2), newUsedVars2)
end
(*Substitute x for s on t*)
fun subst' (x: string, s: Term, t: Term): Term =
case t of
Var y => if x = y then s else t
| Abs (y, t1) =>
if x = y then t
else if List.exists (fn z => z = y) (collectVars s) then
let
val (newAbs, _) = alphaConvert(Abs (y, t1), collectVars t @
collectVars s)
in
subst (x, s, newAbs)
end
else Abs (y, subst (x,s,t1))
| App (t1, t2) => App (subst (x, s, t1), subst(x, s, t2))
in
subst' (x, s, t)
end
fun eval (t: Term): Term =
case t of
Var _ => t
| Abs (_, _) => t
| App (Abs (x, t1), t2) => eval (subst (x, t2, t1))
| App (t1, t2) =>
let
val t1' = eval t1
val t2' = eval t2
in
case t1' of
Abs (_, _) => eval (App (t1', t2'))
| _ => App (t1', t2')
end
fun termToString t =
case t of
Var x => x
| Abs (x, t1) => "\\lambda " ^ x ^ ". " ^ termToString t1
| App (t1, t2) => "(" ^ termToString t1 ^ " " ^ termToString t2 ^ ")"
(* (λx.x)a→a *)
val term0 = App (Abs ("x", Var "x"), Var "a")
val ans0 = eval term0
val ts0 = termToString term0;
val _ = print "\n"
(* (λx.λy.x)ab→(λy.a)b→a *)
val term1 = App (App(Abs("x", Abs ("y", Var "x")), Var "a"), Var "b")
val ans1 = eval term1
val ts1 = termToString term1;
val _ = print "\n"
(* (λx.xx)a→aa *)
val term2 = App (Abs ("x", App (Var "x", Var "x")), Var "a")
val ans2 = eval term2
val ts2 = termToString term2;
val _ = print "\n"
(* (λx.λy.xy)a→λy.ay *)
val term3 = App (Abs ("x", Abs ("y", App (Var "x", Var "y"))), Var "a")
val ans3 = eval term3
val ts3 = termToString term3;
val _ = print "\n"
val zero = Abs ("f", Abs ("x", Var "x"))
val ezero = eval zero
val one = Abs ("f", Abs ("x", App (Var "f", Var "x")))
val eone = eval one
val succ = Abs ("n", Abs("f", Abs("x", App(Var "f", App(App(Var "n", Var "f"),
Var "x")))))
val r = App (succ, zero);
val _ = (print (termToString (eval one) ^ " = one\n"))
Raw
millet.toml
version = 1
workspace.root = "source.mlb"
Raw
source.mlb
lambCalc.sml
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment