CaZzzer/cs-252
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

lab03: update docs in semantics.tex

Browse Source
This commit is contained in:
Yura
2026-02-08 17:33:05 -08:00
parent b900e95d09
commit 802f99b8ba
2 changed files with 26 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files

BIN
lab03/semantics.pdf
View File

Binary file not shown.

69
lab03/semantics.tex
View File

@@ -13,7 +13,7 @@
% Commands for language expressions and values % Commands for language expressions and values
\newcommand{\true}{\mbox{\tt true}} \newcommand{\true}{\mbox{\tt true}}
\newcommand{\false}{\mbox{\tt false}}\title{Operational Semantics for Bool* Language} \newcommand{\false}{\mbox{\tt false}}\title{Operational Semantics for BoolInt* Language}
\newcommand{\ife}[3]{\mbox{\tt if}~{#1}~\mbox{\tt then}~{#2}~\mbox{\tt else}~{#3}} \newcommand{\ife}[3]{\mbox{\tt if}~{#1}~\mbox{\tt then}~{#2}~\mbox{\tt else}~{#3}}
\newcommand{\suc}[1]{\mbox{\tt succ}~{#1}} \newcommand{\suc}[1]{\mbox{\tt succ}~{#1}}
\newcommand{\prd}[1]{\mbox{\tt pred}~{#1}} \newcommand{\prd}[1]{\mbox{\tt pred}~{#1}}
@@ -48,13 +48,13 @@
\begin{abstract} \begin{abstract}
In this paper, we will provide a review of the big-step operational semantics In this paper, we will provide a review of the big-step operational semantics
for the Bool* language we discussed in class. for the BoolInt* language we discussed in class.
\end{abstract} \end{abstract}
%%%% %%%%
%\section{Introduction} %\section{Introduction}
Bool* is a very minimal language that allows us to experiment with operational semantics. BoolInt* is a very minimal language that allows us to experiment with operational semantics.
First, we define the valid expressions in our language. First, we define the valid expressions in our language.
These expressions dictate the possibilities of what expressions These expressions dictate the possibilities of what expressions
@@ -64,23 +64,27 @@ Statements might not evaluate to a value;
expressions always will.) expressions always will.)
\begin{figure} \begin{figure}
\caption{The Bool* language} \caption{The BoolInt* language}
\label{fig:lang} \label{fig:lang}
\[ \[
\begin{array}{ll@{\qquad\qquad}l} \begin{array}{ll@{\qquad\qquad}l}
\mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions} \mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
\mydefcase{\true}{true value} \mydefcase{\true}{true value}
\mydefcase{\false}{false value} \mydefcase{\false}{false value}
\mydefcase{i}{integers}
\mydefcase{\ife e e e}{conditional expressions} \mydefcase{\ife e e e}{conditional expressions}
\mydefcase{\suc e}{successor}
\mydefcase{\prd e}{predecessor}
\\ \\
\mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values} \mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
\mydefcase{\true}{true value} \mydefcase{\true}{true value}
\mydefcase{\false}{false value} \mydefcase{\false}{false value}
\mydefcase{i}{integers}
\end{array} \end{array}
\] \]
\end{figure} \end{figure}
Figure~\ref{fig:lang} shows the list of expressions and values for the Bool* language. Figure~\ref{fig:lang} shows the list of expressions and values for the BoolInt* language.
Expressions can be the value $\true$, the value $\false$, Expressions can be the value $\true$, the value $\false$,
or the conditional expression $\ife e e e$. or the conditional expression $\ife e e e$.
Note that conditional expressions have a recursive structure, Note that conditional expressions have a recursive structure,
@@ -89,7 +93,7 @@ with 3 sub-expressions.
After evaluating a program, we should be able to produce a value in this language. 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; (In other languages, we might hit a bad situation and need to crash instead;
that won't happen in this language.) that won't happen in this language.)
The valid values for Bool* are $\true$ and $\false$. The valid values for BoolInt* are $\true$, $\false$, and $i$.
With our expressions and values defined, With our expressions and values defined,
we can now specify the semantics for our language. we can now specify the semantics for our language.
@@ -102,7 +106,7 @@ To do so, we will use the following big-step evaluation relation:
The above line should be read as ``the expression $e$ evaluates to the value $v$''. The above line should be read as ``the expression $e$ evaluates to the value $v$''.
\begin{figure} \begin{figure}
\caption{Big-step semantics for Bool*} \caption{Big-step semantics for BoolInt*}
\label{fig:bigstep} \label{fig:bigstep}
{\bf Evaluation Rules:~~~ \fbox{$\bstep{e}{v}$}} \\ {\bf Evaluation Rules:~~~ \fbox{$\bstep{e}{v}$}} \\
\[ \[
@@ -122,13 +126,23 @@ The above line should be read as ``the expression $e$ evaluates to the value $v$
}{ }{
\bstep{\ife{e_1}{e_2}{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}
}
\end{array} \end{array}
\] \]
\end{figure} \end{figure}
Figure~\ref{fig:bigstep} shows the big-step evaluation rules for the Bool* language. Figure~\ref{fig:bigstep} shows the big-step evaluation rules for the BoolInt* language.
Of course, there are additional possible rules. Of course, there are additional possible rules.
The \rel{B-Value} rule applies when the expression (to the left of ``$\Downarrow$'') The \rel{B-Value} rule applies when the expression (to the left of ``$\Downarrow$'')
@@ -147,41 +161,10 @@ and $e_2$ evaluates to some value $v$.
If the premise holds, then the result of evaluating the expression is the 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. The structure of \rel{B-IfFalse} is similar.
We also have rules for handling the integer operations.
\section*{Exercise} 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$.
Let's extend the language with new features. Similarly, \rel{B-Pred} evaluates $\prd e$ to $i-1$ if $e$ evaluates to $i$.
Our new language will be called BoolInt*.
The valid expressions and values are shown below:
%\begin{figure}
%\caption{The BoolInt* language}
%\label{fig:lang2}
\[
\begin{array}{ll@{\qquad\qquad}l}
\mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
\mydefcase{\true}{true value}
\mydefcase{\false}{false value}
\mydefcase{i}{integers}
\mydefcase{\ife e e e}{conditional expressions}
\mydefcase{\suc e}{successor}
\mydefcase{\prd e}{predecessor}
\\
\mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
\mydefcase{\true}{true value}
\mydefcase{\false}{false value}
\mydefcase{i}{integers}
\end{array}
\]
%\end{figure}
In addition to integers, our expanded language has the ability to increment an integer ($\suc e$)
and decrement an integer ($\prd e$).
Using LaTeX, write the evaluation rules for these additional constructs.
If necessary, revise any existing rules.
Then, add these new constructs to the Haskell interpreter that we have been working with.
\end{document} \end{document}