1 files changed, 38 insertions, 0 deletions

diff --git a/theories/lambda/operational.v b/theories/lambda/operational.v
new file mode 100644
index 0000000..b0fa366
--- /dev/null
+++ b/theories/lambda/operational.v
@@ -0,0 +1,38 @@
+From mininix Require Export utils.
+From stdpp Require Import options.
+
+Module Import lambda.
+
+Inductive expr :=
+  | EString (s : string)
+  | EId (x : string)
+  | EAbs (x : string) (e : expr)
+  | EApp (e1 e2 : expr).
+
+Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
+  match e with
+  | EString s => EString s
+  | EId x => if ds !! x is Some d then d else EId x
+  | EAbs x e => EAbs x (subst (delete x ds) e)
+  | EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
+  end.
+
+Reserved Infix "-->" (right associativity, at level 55).
+Inductive step : expr → expr → Prop :=
+  | Sβ x e1 e2 : EApp (EAbs x e1) e2 --> subst {[x:=e2]} e1
+  | SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
+where "e1 --> e2" := (step e1 e2).
+
+Infix "-->*" := (rtc step) (right associativity, at level 55).
+
+Definition final (e : expr) : Prop :=
+  match e with
+  | EString _ => True
+  | EAbs _ _ => True
+  | _ => False
+  end.
+
+Definition stuck (e : expr) : Prop :=
+  nf step e ∧ ¬final e.
+
+End lambda.