lab14: impl small step semantics

lab14/typed-semantics.typ

@@ -1,8 +1,30 @@
-// ============================================================
-// Operational Semantics for BoolInt* Language — Typst version
-// ============================================================
-//
-// ----- helper functions -------------------------------------
+/*
+In this lab, you will develop evaluation rules and typing rules for a small language.
+
+Our language is an extended version of the one discussed in class:
+
+e ::= true
+| false
+| i (Integers)
+| s (Strings)
+| succ e
+| pred e
+| iszero e
+| if e then e else e
+| concat e e
+| isemptystr e
+| strlen e
+
+Our types must therefore include:
+
+T ::= Bool
+| Int
+| String
+
+First, write the evaluation order rules (using small-step semantics) for the expressions in the language.
+
+Next, define the typing rules for these expressions. Be sure that your typing rules guarantee both progress and preservation. (For ways of formally guaranteeing these properties, see Chapter 8 of Ben Pierce's "Types and Programming Languages").
+*/
 
 // Language keywords rendered in monospace
 #let kw(body) = text(font: "DejaVu Sans Mono", size: 0.85em, body)
@@ -12,81 +34,66 @@
 #let ife(e1, e2, e3) = [#kw[if] #e1 #kw[then] #e2 #kw[else] #e3]
 #let suc(e) = [#kw[succ] #e]
 #let prd(e) = [#kw[pred] #e]
-#let sec(e) = [#kw[secret] #e]
+#let iszero(e) = [#kw[iszero] #e]
+#let concat(e1, e2) = [#kw[concat] #e1 #h(0.2em) #e2]
+#let isemptystr(e) = [#kw[isemptystr] #e]
+#let strlen(e) = [#kw[strlen] #e]
 
-// Security labels
-#let lH = $upright(H)$
-#let lL = $upright(L)$
-#let ljoin = $union.sq$
-
-// Labeled value: (v, ℓ)
-#let lval(v, l) = $(#v, #l)$
-
-// Big-step evaluation relation: e ⇓ (v, ℓ)
-#let bstep(e, v) = $#e arrow.b.double #v$
+// Small-step evaluation relation: e -> e'
+#let sstep(e, ee) = $#e -> #ee$
 
 // Rule name label in small-caps
 #let rel(name) = text(size: 0.9em, smallcaps[\[#name\]])
 
-// Big-step rule: fraction with name on the left
+// Small-step rule: fraction with name on the left
 // premises (content), conclusion (content)
-#let bsrule(name, premises, conclusion) = {
+#let ssrule(name, premises, conclusion) = {
   grid(
     columns: (auto, auto),
     column-gutter: 1em,
     align: (right + horizon, left + horizon),
-    rel(name), math.equation(block: true, numbering: none, math.frac(premises, conclusion)),
+    rel(name),
+    box(stroke: 0.5pt, inset: 4pt, math.equation(
+      block: true,
+      numbering: none,
+      // if premises != "" {
+      math.frac(premises, conclusion),
+      // } else { conclusion },
+    )),
   )
   v(0.4em)
 }
 
-// Definition head: "e ::= ..." with label
-#let mydefhead(lhs, label) = {
-  grid(
-    columns: (auto, auto),
-    column-gutter: 1fr,
-    [#lhs], emph(label),
-  )
-}
-
-// Definition case: indented alternative with description
-#let mydefcase(alt, desc) = {
-  grid(
-    columns: (2em, auto, auto),
-    column-gutter: 1fr,
-    [], [#alt], [#desc],
-  )
-}
-
-
-// ----- Figure 2: big-step semantics -------------------------
-
-#figure(
-  box(width: 85%, inset: (left: 1em))[
-    #set align(left)
-    #text(weight: "bold")[Evaluation Rules:#h(1em)]#box(stroke: 0.5pt, inset: 4pt, $#bstep[$e$][$#lval[$v$][$ell$]$]$)
+== Operational Semantics Rules
 
 #v(0.6em)
 
-    #bsrule("B-Value", "", $#bstep[$v$][$#lval[$v$][$#lL$]$]$)
+#ssrule("E-Succ-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#suc[$e$]][#suc[$e'$]]$)
+#ssrule("E-Succ", "", $#sstep[#suc[$i$]][$i + 1$]$)
 
-    #bsrule("B-Secret", $#bstep[$e$][$#lval[$v$][$ell$]$]$, $#bstep[#sec[$e$]][$#lval[$v$][$#lH$]$]$)
+#ssrule("E-Pred-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#prd[$e$]][#prd[$e'$]]$)
+#ssrule("E-Pred", "", $#sstep[#prd[$i$]][$i - 1$]$)
 
-    #bsrule(
-      "B-IfTrue",
-      $#bstep[$e_1$][$#lval[$#tr$][$ell_1$]$] #h(2em) #bstep[$e_2$][$#lval[$v$][$ell_2$]$]$,
-      $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$#lval[$v$][$ell_1 #ljoin ell_2$]$]$,
-    )
+#ssrule("E-IsZero-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#iszero[$e$]][#iszero[$e'$]]$)
+#ssrule("E-IsZero-Zero", "", $#sstep[#iszero[0]][true]$)
+#ssrule("E-IsZero-NonZero", $i != 0$, $#sstep[#iszero[#suc[$i$]]][false]$)
 
-    #bsrule(
-      "B-IfFalse",
-      $#bstep[$e_1$][$#lval[$#fl$][$ell_1$]$] #h(2em) #bstep[$e_3$][$#lval[$v$][$ell_3$]$]$,
-      $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$#lval[$v$][$ell_1 #ljoin ell_3$]$]$,
-    )
+#ssrule("E-If-Ctx", $#sstep[$e_1$][$e'_1$]$, $#sstep[#ife[$e_1$][$e_2$][$e_3$]][#ife[$e'_1$][$e_2$][$e_3$]]$)
+#ssrule("E-If-True", "", $#sstep[#ife[true][$e_2$][$e_3$]][$e_2$]$)
+#ssrule("E-If-False", "", $#sstep[#ife[false][$e_2$][$e_3$]][$e_3$]$)
 
-    #bsrule("B-Succ", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#suc[$e$]][$#lval[$i + 1$][$ell$]$]$)
+#ssrule("E-Concat-Ctx1", $#sstep[$e_1$][$e'_1$]$, $#sstep[#concat[$e_1$][$e_2$]][#concat[$e'_1$][$e_2$]]$)
+#ssrule("E-Concat-Ctx2", $#sstep[$e_2$][$e'_2$]$, $#sstep[#concat[$s_1$][$e_2$]][#concat[$s_1$][$e'_2$]]$)
+#ssrule("E-Concat", $s_3 = s_1 + s_2$, $#sstep[#concat[$s_1$][$s_2$]][$s_3$]$)
 
-    #bsrule("B-Pred", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#prd[$e$]][$#lval[$i - 1$][$ell$]$]$)
-  ],
-  caption: [Big-step semantics for BoolInt\* with information flow],
-) <fig:bigstep>
+#ssrule("E-IsEmptyStr-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#isemptystr[$e$]][#isemptystr[$e'$]]$)
+#ssrule("E-IsEmptyStr-Empty", "", $#sstep[#isemptystr[`""`]][true]$)
+#ssrule("E-IsEmptyStr-NonEmpty", [$s !=$ `""`], $#sstep[#isemptystr[$s$]][false]$)
+
+#ssrule("E-StrLen-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#strlen[$e$]][#strlen[$e'$]]$)
+#ssrule("E-StrLen-Zero", "", $#sstep[#strlen[`""`]][0]$)
+#ssrule("E-StrLen-NonZero", [c is a single char, $s = c + s'$], $#sstep[#strlen[$s$]][#suc[#strlen[$s'$]]]$)
+
+== Typing Rules
+
+#v(0.6em)