diff --git a/lab14/typed-semantics.pdf b/lab14/typed-semantics.pdf index 1a6206c..0af14b4 100644 Binary files a/lab14/typed-semantics.pdf and b/lab14/typed-semantics.pdf differ diff --git a/lab14/typed-semantics.typ b/lab14/typed-semantics.typ index fb6159a..fcd4aa5 100644 --- a/lab14/typed-semantics.typ +++ b/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), - ) -} +== Operational Semantics Rules -// Definition case: indented alternative with description -#let mydefcase(alt, desc) = { - grid( - columns: (2em, auto, auto), - column-gutter: 1fr, - [], [#alt], [#desc], - ) -} +#v(0.6em) +#ssrule("E-Succ-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#suc[$e$]][#suc[$e'$]]$) +#ssrule("E-Succ", "", $#sstep[#suc[$i$]][$i + 1$]$) -// ----- Figure 2: big-step semantics ------------------------- +#ssrule("E-Pred-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#prd[$e$]][#prd[$e'$]]$) +#ssrule("E-Pred", "", $#sstep[#prd[$i$]][$i - 1$]$) -#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$]$]$) +#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]$) - #v(0.6em) +#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-Value", "", $#bstep[$v$][$#lval[$v$][$#lL$]$]$) +#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-Secret", $#bstep[$e$][$#lval[$v$][$ell$]$]$, $#bstep[#sec[$e$]][$#lval[$v$][$#lH$]$]$) +#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]$) - #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-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'$]]]$) - #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$]$]$, - ) +== Typing Rules - #bsrule("B-Succ", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#suc[$e$]][$#lval[$i + 1$][$ell$]$]$) - - #bsrule("B-Pred", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#prd[$e$]][$#lval[$i - 1$][$ell$]$]$) - ], - caption: [Big-step semantics for BoolInt\* with information flow], -) +#v(0.6em)