semantics-1: init

semantics-1/semantics.tex

@@ -0,0 +1,171 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+%\usepackage{citesort}
+%\usepackage{url}
+%\usepackage{listings}
+\usepackage{color}
+
+
+% Commands for formatting figures
+\newcommand{\mydefhead}[2]{\multicolumn{2}{l}{{#1}}&\mbox{\emph{#2}}\\}
+\newcommand{\mydefcase}[2]{\qquad\qquad& #1 &\mbox{#2}\\}
+
+% Commands for language expressions and values
+\newcommand{\true}{\mbox{\tt true}}
+\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}}
+
+% Big-step evaluation relation.
+% #1 is the expression.
+% #2 is the resulting value.
+\newcommand{\bstep}[2]{{#1} \Downarrow {#2}}
+
+% Command for formatting the name of the evaluation relation.
+\newcommand{\rel}[1]{ \mbox{\sc [#1]} }
+
+% Format for a big-step evaluation rule.
+% #1 is the name of the rule.
+% #2 are the premises.  Leave blank if there are none.
+% #3 is the conclusion.
+\newcommand{\bsrule}[3]{
+  \rel{#1} &
+  \frac{\strut\begin{array}{@{}c@{}} #2 \end{array}}
+       {\strut\begin{array}{@{}c@{}} #3 \end{array}}
+   \\~\\
+}
+
+\author{
+  Yuri Tatishchev \\
+  San Jos\'{e} State University \\
+  iurii.tatishchev@sjsu.edu
+}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+In this paper, we will provide a review of the big-step operational semantics
+for the BoolInt* language we discussed in class.
+\end{abstract}
+
+%%%%
+%\section{Introduction}
+
+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 {\em statements}.
+Statements might not evaluate to a value;
+expressions always will.)
+
+\begin{figure}
+\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 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,
+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 $\true$, $\false$, 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$''.
+
+\begin{figure}
+\caption{Big-step semantics for BoolInt*}
+\label{fig:bigstep}
+  {\bf Evaluation Rules:~~~ \fbox{$\bstep{e}{v}$}} \\
+\[
+\begin{array}{r@{\qquad\qquad}c}
+\bsrule{B-Value}{}{
+  \bstep{v}{v}
+}
+\bsrule{B-IfTrue}{
+  \bstep{e_1}{\true} \\
+  \bstep{e_2}{v}
+}{
+  \bstep{\ife{e_1}{e_2}{e_3}}{v}
+}
+\bsrule{B-IfFalse}{
+  \bstep{e_1}{\false} \\
+  \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}
+}
+\end{array}
+\]
+\end{figure}
+
+
+
+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$'')
+is also a value, as defined in Figure~\ref{fig:lang}.
+There are no premises for this rule (above the line),
+meaning that it is an {\em axiom}.
+This rule states that a value evaluates to itself,
+so that \true{} evaluates to \true{} and \false{} evaluates to \false{}.
+
+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 \true{}
+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$.
+
+
+\end{document}
+