semantics-1: typst pt. 1
This commit is contained in:
2827
semantics-1/semantics-typst.pdf
Normal file
2827
semantics-1/semantics-typst.pdf
Normal file
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,197 @@
|
||||
// ============================================================
|
||||
// Operational Semantics for BoolInt* Language — Typst version
|
||||
// ============================================================
|
||||
|
||||
// ----- page setup (fullpage equivalent) ---------------------
|
||||
#set page(margin: 1in)
|
||||
#set text(size: 11pt)
|
||||
#set par(justify: true)
|
||||
|
||||
// ----- helper functions -------------------------------------
|
||||
|
||||
// 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]
|
||||
|
||||
// Big-step evaluation relation: e ⇓ v
|
||||
#let bstep(e, v) = $#e arrow.b.double #v$
|
||||
|
||||
// Rule name label in small-caps
|
||||
#let rel(name) = text(size: 0.9em, smallcaps[\[#name\]])
|
||||
|
||||
// Big-step rule: fraction with name on the left
|
||||
// premises (content), conclusion (content)
|
||||
#let bsrule(name, premises, conclusion) = {
|
||||
grid(
|
||||
columns: (auto, 1fr),
|
||||
column-gutter: 1em,
|
||||
align: (right + horizon, left + horizon),
|
||||
rel(name),
|
||||
math.equation(block: true, numbering: none,
|
||||
math.frac(premises, conclusion)
|
||||
),
|
||||
)
|
||||
v(0.4em)
|
||||
}
|
||||
|
||||
// Definition head: "e ::= ..." with label
|
||||
#let mydefhead(lhs, label) = {
|
||||
grid(
|
||||
columns: (1fr, auto),
|
||||
[#lhs],
|
||||
emph(label),
|
||||
)
|
||||
}
|
||||
|
||||
// Definition case: indented alternative with description
|
||||
#let mydefcase(alt, desc) = {
|
||||
grid(
|
||||
columns: (2em, 1fr, auto),
|
||||
[], [#alt], [#desc],
|
||||
)
|
||||
}
|
||||
|
||||
// ----- title block ------------------------------------------
|
||||
|
||||
#align(center)[
|
||||
#text(size: 17pt, weight: "bold")[Operational Semantics for BoolInt\* Language]
|
||||
|
||||
#v(0.8em)
|
||||
|
||||
Yuri Tatishchev \
|
||||
San José State University \
|
||||
iurii.tatishchev\@sjsu.edu
|
||||
]
|
||||
|
||||
#v(1em)
|
||||
|
||||
// ----- abstract ---------------------------------------------
|
||||
|
||||
#align(center)[
|
||||
#block(width: 85%)[
|
||||
#set text(size: 10pt)
|
||||
*Abstract.* In this paper, we will provide a review of the big-step operational semantics
|
||||
for the BoolInt\* language we discussed in class.
|
||||
]
|
||||
]
|
||||
|
||||
#v(0.5em)
|
||||
|
||||
// ----- body text --------------------------------------------
|
||||
|
||||
BoolInt\* is a very minimal language that allows us to experiment with operational semantics.
|
||||
|
||||
First, we define the valid expressions in our language.
|
||||
These expressions dictate the possibilities of what expressions
|
||||
we may have in our source programs.
|
||||
(Note that other language might also have _statements_.
|
||||
Statements might not evaluate to a value;
|
||||
expressions always will.)
|
||||
|
||||
// ----- Figure 1: language definition ------------------------
|
||||
|
||||
#figure(
|
||||
block(inset: (left: 2em))[
|
||||
#set align(left)
|
||||
#mydefhead[$e ::=$ #h(6em)][Expressions]
|
||||
#mydefcase(tr, [true value])
|
||||
#mydefcase(fl, [false value])
|
||||
#mydefcase($i$, [integers])
|
||||
#mydefcase(ife[$e$][$e$][$e$], [conditional expressions])
|
||||
#mydefcase(suc[$e$], [successor])
|
||||
#mydefcase(prd[$e$], [predecessor])
|
||||
|
||||
#v(0.5em)
|
||||
|
||||
#mydefhead[$v ::=$ #h(6em)][Values]
|
||||
#mydefcase(tr, [true value])
|
||||
#mydefcase(fl, [false value])
|
||||
#mydefcase($i$, [integers])
|
||||
],
|
||||
caption: [The BoolInt\* language],
|
||||
) <fig:lang>
|
||||
|
||||
@fig:lang shows the list of expressions and values for the BoolInt\* language.
|
||||
Expressions can be the value $#tr$, the value $#fl$,
|
||||
or the conditional expression $#ife[$e$][$e$][$e$]$.
|
||||
Note that conditional expressions have a recursive structure,
|
||||
with 3 sub-expressions.
|
||||
|
||||
After evaluating a program, we should be able to produce a value in this language.
|
||||
(In other languages, we might hit a bad situation and need to crash instead;
|
||||
that won't happen in this language.)
|
||||
The valid values for BoolInt\* are $#tr$, $#fl$, and $i$.
|
||||
|
||||
With our expressions and values defined,
|
||||
we can now specify the semantics for our language.
|
||||
To do so, we will use the following big-step evaluation relation:
|
||||
|
||||
$ #bstep[$e$][$v$] $
|
||||
|
||||
The above line should be read as "the expression $e$ evaluates to the value $v$".
|
||||
|
||||
// ----- Figure 2: big-step semantics -------------------------
|
||||
|
||||
#figure(
|
||||
block(inset: (left: 1em))[
|
||||
#set align(left)
|
||||
#text(weight: "bold")[Evaluation Rules:#h(1em)]#box(stroke: 0.5pt, inset: 4pt, $#bstep[$e$][$v$]$)
|
||||
|
||||
#v(0.6em)
|
||||
|
||||
#bsrule("B-Value",
|
||||
$emptyset$,
|
||||
$#bstep[$v$][$v$]$,
|
||||
)
|
||||
|
||||
#bsrule("B-IfTrue",
|
||||
$#bstep[$e_1$][$#tr$] #h(2em) #bstep[$e_2$][$v$]$,
|
||||
$#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$,
|
||||
)
|
||||
|
||||
#bsrule("B-IfFalse",
|
||||
$#bstep[$e_1$][$#fl$] #h(2em) #bstep[$e_3$][$v$]$,
|
||||
$#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$,
|
||||
)
|
||||
|
||||
#bsrule("B-Succ",
|
||||
$#bstep[$e$][$i$]$,
|
||||
$#bstep[#suc[$e$]][$i + 1$]$,
|
||||
)
|
||||
|
||||
#bsrule("B-Pred",
|
||||
$#bstep[$e$][$i$]$,
|
||||
$#bstep[#prd[$e$]][$i - 1$]$,
|
||||
)
|
||||
],
|
||||
caption: [Big-step semantics for BoolInt\*],
|
||||
) <fig:bigstep>
|
||||
|
||||
@fig:bigstep shows the big-step evaluation rules for the BoolInt\* language.
|
||||
Of course, there are additional possible rules.
|
||||
|
||||
The #rel("B-Value") rule applies when the expression (to the left of "$arrow.b.double$")
|
||||
is also a value, as defined in @fig:lang.
|
||||
There are no premises for this rule (above the line),
|
||||
meaning that it is an _axiom_.
|
||||
This rule states that a value evaluates to itself,
|
||||
so that #tr evaluates to #tr and #fl evaluates to #fl.
|
||||
|
||||
Two different rules are needed for handling conditional expressions.
|
||||
Which rule applies depends on the premises.
|
||||
|
||||
For the #rel("B-IfTrue") rule,
|
||||
the premise states that $e_1$ evaluates to #tr
|
||||
and $e_2$ evaluates to some value $v$.
|
||||
If the premise holds, then the result of evaluating the expression is the value $v$.
|
||||
The structure of #rel("B-IfFalse") is similar.
|
||||
|
||||
We also have rules for handling the integer operations.
|
||||
The #rel("B-Succ") rule states that if the operand $e$ evaluates to an integer $i$,
|
||||
then the expression $#suc[$e$]$ evaluates to $i + 1$.
|
||||
Similarly, #rel("B-Pred") evaluates $#prd[$e$]$ to $i - 1$ if $e$ evaluates to $i$.
|
||||
|
||||
Reference in New Issue
Block a user