diff --git a/lab03/semantics.pdf b/lab03/semantics.pdf index 2a32692..083bbf6 100644 Binary files a/lab03/semantics.pdf and b/lab03/semantics.pdf differ diff --git a/lab03/semantics.tex b/lab03/semantics.tex index b71939d..984fd21 100644 --- a/lab03/semantics.tex +++ b/lab03/semantics.tex @@ -13,7 +13,7 @@ % Commands for language expressions and values \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{\suc}[1]{\mbox{\tt succ}~{#1}} \newcommand{\prd}[1]{\mbox{\tt pred}~{#1}} @@ -48,13 +48,13 @@ \begin{abstract} 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} %%%% %\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. These expressions dictate the possibilities of what expressions @@ -64,23 +64,27 @@ Statements might not evaluate to a value; expressions always will.) \begin{figure} -\caption{The Bool* language} +\caption{The BoolInt* language} \label{fig:lang} \[ \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} -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$, or the conditional expression $\ife e e e$. 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. (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 Bool* are $\true$ and $\false$. +The valid values for BoolInt* are $\true$, $\false$, and $i$. With our expressions and values defined, 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$''. \begin{figure} -\caption{Big-step semantics for Bool*} +\caption{Big-step semantics for BoolInt*} \label{fig:bigstep} {\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} } +\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{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. 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$. The structure of \rel{B-IfFalse} is similar. - -\section*{Exercise} - -Let's extend the language with new features. -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. +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$. \end{document}