144 lines
4.1 KiB
Typst
144 lines
4.1 KiB
Typst
/*
|
|
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").
|
|
*/
|
|
|
|
#set page(columns: 2)
|
|
|
|
// Language keywords rendered in monospace
|
|
#let kw(body) = text(font: "DejaVu Sans Mono", size: 0.85em, body)
|
|
|
|
#let tr = kw[true]
|
|
#let fl = kw[false]
|
|
#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 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]
|
|
|
|
// Type keywords
|
|
#let bool = kw[Bool]
|
|
#let int = kw[Int]
|
|
#let string = kw[String]
|
|
|
|
// Small-step evaluation relation: e -> e'
|
|
#let sstep(e, ee) = $#e -> #ee$
|
|
|
|
// Typing relation: e : T
|
|
#let tstep(e, T) = $#e : #T$
|
|
|
|
// Rule name label in small-caps
|
|
#let rel(name) = text(size: 0.9em, smallcaps[\[#name\]])
|
|
|
|
// Rule: fraction with name on the left
|
|
// premises (content), conclusion (content)
|
|
#let rule(name, premises, conclusion) = {
|
|
stack(
|
|
dir: ttb,
|
|
spacing: 0.4em,
|
|
rel(name),
|
|
box(stroke: 0.5pt, inset: 4pt, math.equation(
|
|
block: true,
|
|
numbering: none,
|
|
math.frac(premises, conclusion),
|
|
)),
|
|
)
|
|
v(0.8em)
|
|
}
|
|
|
|
= Evaluation Rules
|
|
|
|
#v(0.6em)
|
|
|
|
#rule("E-Succ-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#suc[$e$]][#suc[$e'$]]$)
|
|
#rule("E-Succ", "", $#sstep[#suc[$i$]][$i + 1$]$)
|
|
|
|
#rule("E-Pred-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#prd[$e$]][#prd[$e'$]]$)
|
|
#rule("E-Pred", "", $#sstep[#prd[$i$]][$i - 1$]$)
|
|
|
|
#rule("E-IsZero-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#iszero[$e$]][#iszero[$e'$]]$)
|
|
#rule("E-IsZero-Zero", "", $#sstep[#iszero[0]][true]$)
|
|
#rule("E-IsZero-NonZero", $i != 0$, $#sstep[#iszero[#suc[$i$]]][false]$)
|
|
|
|
#rule("E-If-Ctx", $#sstep[$e_1$][$e'_1$]$, $#sstep[#ife[$e_1$][$e_2$][$e_3$]][#ife[$e'_1$][$e_2$][$e_3$]]$)
|
|
#rule("E-If-True", "", $#sstep[#ife[true][$e_2$][$e_3$]][$e_2$]$)
|
|
#rule("E-If-False", "", $#sstep[#ife[false][$e_2$][$e_3$]][$e_3$]$)
|
|
|
|
#rule("E-Concat-Ctx1", $#sstep[$e_1$][$e'_1$]$, $#sstep[#concat[$e_1$][$e_2$]][#concat[$e'_1$][$e_2$]]$)
|
|
#rule("E-Concat-Ctx2", $#sstep[$e_2$][$e'_2$]$, $#sstep[#concat[$s_1$][$e_2$]][#concat[$s_1$][$e'_2$]]$)
|
|
#rule("E-Concat", $s_3 = s_1 + s_2$, $#sstep[#concat[$s_1$][$s_2$]][$s_3$]$)
|
|
|
|
#rule("E-IsEmptyStr-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#isemptystr[$e$]][#isemptystr[$e'$]]$)
|
|
#rule("E-IsEmptyStr-Empty", "", $#sstep[#isemptystr[`""`]][true]$)
|
|
#rule("E-IsEmptyStr-NonEmpty", [$s !=$ `""`], $#sstep[#isemptystr[$s$]][false]$)
|
|
|
|
#rule("E-StrLen-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#strlen[$e$]][#strlen[$e'$]]$)
|
|
#rule("E-StrLen-Zero", "", $#sstep[#strlen[`""`]][0]$)
|
|
#rule("E-StrLen-NonZero", [c is a single char, $s = c + s'$], $#sstep[#strlen[$s$]][#suc[#strlen[$s'$]]]$)
|
|
|
|
#pagebreak()
|
|
= Typing Rules
|
|
|
|
#v(0.6em)
|
|
|
|
#rule("T-True", "", $#tstep[true][#bool]$)
|
|
#rule("T-False", "", $#tstep[false][#bool]$)
|
|
#rule("T-Int", "", $#tstep[n][#int]$)
|
|
#rule("T-String", "", $#tstep[s][#string]$)
|
|
|
|
#rule("T-Succ", $#tstep[$e$][#int]$, $#tstep[#suc[$e$]][#int]$)
|
|
#rule("T-Pred", $#tstep[$e$][#int]$, $#tstep[#prd[$e$]][#int]$)
|
|
#rule("T-IsZero", $#tstep[$e$][#int]$, $#tstep[#iszero[$e$]][#bool]$)
|
|
#rule(
|
|
"T-If",
|
|
[
|
|
$#tstep[$e_1$][#bool]$,
|
|
$#tstep[$e_2$][$T$]$,
|
|
$#tstep[$e_3$][$T$]$
|
|
],
|
|
$#tstep[#ife[$e_1$][$e_2$][$e_3$]][T]$,
|
|
)
|
|
#rule(
|
|
"T-Concat",
|
|
[
|
|
$#tstep[$e_1$][$#string$]$,
|
|
$#tstep[$e_2$][$#string$]$
|
|
],
|
|
$#tstep[#concat[$e_1$][$e_2$]][#string]$,
|
|
)
|
|
#rule(
|
|
"T-IsEmptyStr",
|
|
$#tstep[$e$][$#string$]$,
|
|
$#tstep[#isemptystr[$e$]][#bool]$,
|
|
)
|
|
#rule(
|
|
"T-StrLen",
|
|
$#tstep[$e$][$#string$]$,
|
|
$#tstep[#strlen[$e$]][#int]$,
|
|
)
|