\documentclass{handout}
\usepackage{6044}
%\documentclass[11pt]{article}
%\usepackage{6001}
\usepackage{time,fullpage}
\usepackage{amsmath}

\textheight 8.5in

\oddsidemargin 11pt
\evensidemargin \oddsidemargin
\marginparwidth 0.5in

\advance\textwidth by -2\oddsidemargin

\newdimen\tablewidth
\tablewidth=\textwidth
\advance \tablewidth by -11pt

\parindent 0.0in
\parskip \medskipamount

\newcommand{\twiddle}{\char`\~}

\let\to\rightarrow
\let\union\cup
\let\cross\times

%\newcommand{\subst}[3]{#1[#2 := #3]}

\def\SI{\mbox{Scheme-Integer}}
\def\SNI{\mbox{Scheme-Nonneg-Integer}}
\def\SN{\mbox{Sch-\-Num}}
\def\SB{\mbox{Sch-Bool}}
\def\Empty{\mbox{Empty}}
\def\SI{\mbox{Sch-Int}}
\def\SNI{\mbox{Sch-Nonneg-Int}}


\makeatletter

\def\DefineBNFAbbrev#1#2{%
    \expandafter\newcommand\expandafter{\csname#1\endcsname}{\@bnfabbrev{#2}}%
}

\def\@bnfabbrev#1{%
    \@ifnextchar _{\@subabbrev{#1}}{\@plainabbrev{#1}}%
}

\def\@subabbrev#1_#2{\hbox{\normalfont$\langle\mbox{#1}_{#2}\rangle$}}

\def\@plainabbrev#1{\hbox{\normalfont$\langle\mbox{#1}\rangle$}}

% \def\exp{\hbox{$\bnf <expression>$}}

\DefineBNFAbbrev{idfr}{identifier}
\DefineBNFAbbrev{expr}{expression}
\DefineBNFAbbrev{define}{define}
%\DefineBNFAbbrev{defines}{defines}
\DefineBNFAbbrev{vrbl}{variable}
\DefineBNFAbbrev{bod}{body}
\DefineBNFAbbrev{init}{init}
%\DefineBNFAbbrev{val}{value}
\DefineBNFAbbrev{ival}{immediate\ value}
\DefineBNFAbbrev{sval}{syntactic\ value}
\DefineBNFAbbrev{lsval}{list value}
\DefineBNFAbbrev{prval}{pair value}
\DefineBNFAbbrev{test}{test}
\DefineBNFAbbrev{orsf}{or}
\DefineBNFAbbrev{andsf}{and}
\DefineBNFAbbrev{pridfr}{procedure\ identifier}
%\DefineBNFAbbrev{rspidfr}{rule-specified\ procedure\ id}
%\DefineBNFAbbrev{ppridfr}{primitive\ procedure\ id}
\DefineBNFAbbrev{lamexp}{lambda\ expression}
\DefineBNFAbbrev{beginsf}{begin}
\DefineBNFAbbrev{letform}{let\ form}
\DefineBNFAbbrev{letrec}{letrec}
\DefineBNFAbbrev{ccntxt}{control\ context}
\DefineBNFAbbrev{hole}{hole}
\DefineBNFAbbrev{proc}{procedure}

\makeatletter


\def\fbox#1{%
  \vtop{\vbox{\hrule%
     \hbox{\vrule\kern3pt%
 \vtop{\vbox{\kern3pt#1}\kern3pt}%
 \kern3pt\vrule}}%
 \hrule}}


\begin{document}
\handout{syntax}{Scheme Syntax in BNF}
{October 28, 1998 (final section added 11/5/98)}

The following Backus-Naur Form (BNF) grammars describe the main constructs
of Scheme\footnote{For the official, full Scheme grammar, see the
\RFVS\ Manual available on the web at:
\begin{center}
\texttt{http://www-swiss.ai.mit.edu/\twiddle jaffer/r5rs\_toc.html}
\end{center}}
as well as some of the syntactic concepts needed in a rewriting
``Substitution Model'' for Scheme, namely, \emph{syntactic values} and
\emph{control contexts}.

In these grammars, superscript ``$^{*}$'' indicates zero or more occurrences
of a grammatical phrase, and superscript ``$^{+}$'' indicates one or more
occurrences.

\section{The Functional Kernel}
\begin{bnf}
\begin{eqnarray*}
\expr &::=& <self-evaluating> | <symbol> | <nil> | \vrbl\\
        && {} | \proc | \letform | <if> | <combination>\\
\\
<self-evaluating>  &::=& <numeral> | <boolean> | <string> \ \dots\\
<numeral>   &::=&   "0" | "-1" | "3.14159" | \dots\\
<boolean>   &::=&   "#t" | "#f" \\
<string>   &::=&   \hbox{\Code{"hello there"}} | \dots \\
\\
<symbol> &::=& "(quote"\: \idfr")"\\
\idfr &::=& \hbox{identifiers which are not } <self-evaluating>\\
<nil>  &::=&  "'()"\\
\vrbl &::=& \hbox{identifiers which are neither } <self-evaluating>,\\
      & &   {} \quad \pridfr, \hbox{ nor }<keyword>\\
\\
<keyword>   &::=&  "quote" | "lambda" | <let keyword> | "if"\\
\\
\proc &::=& \pridfr | \lamexp\\
\pridfr  &::=& "+" | "-" | "*" | "/" | "=" | "<" | "atan" | "call/cc" | \dots\\
         && {} | "number?" | "symbol?" | "procedure?" | "eq?" | \dots\\
         && {} | "cons" | "car" | "cdr" | "list" | "apply" | "null?" | "pair?"\\
         && {} \hbox{(Note: No ``side-effect'' procedures such as
               \Code{display}, \Code{set-car!}.)}\\
\lamexp &::=&  "(lambda ("<formals>")"\: \expr")"\\
         && {} | "(lambda " \vrbl\: \expr")"\\
<formals>  &::=& \vrbl^{*}   \qquad \hbox{(Note: all \vrbl's must be distinct.)}
\end{eqnarray*}
\end{bnf}

\begin{bnf}
\begin{eqnarray*}
\letform &::=& "("<let keyword> "("<binding>^{*}")"\: \expr ")"\\
        && {} \qquad \hbox{(Note: all \Code{let}form-bound variables must be distinct.)}\\
<let keyword> &::=& "letrec"\\
<binding> &::=& "("\vrbl\: <init>")"\\
<init> &::=& \expr\\
\\
<if> &:=& "(if"\: <test> <consequent> <alternative>")" \\
<test>   &::=&   \expr\\
<consequent>   &::=&   \expr\\
<alternative>   &::=&   \expr\\
\\
<combination>   &::=&   "("<operator> <operand>^{*}")"\\
<operator> &::=& \expr\\
<operand>  &::=& \expr
\end{eqnarray*}
\end{bnf}

\section{The Full Kernel}

\begin{bnf}
\begin{eqnarray*}
\define &::=& "(define"\: \vrbl \expr ")"\\
\\
\expr &::=& \dots | \beginsf | <assignment>\\
\\
<keyword>   &::=& \dots | "define" | "begin" | "set!"\\
\\
\pridfr  &::=& \dots | "set-car!" | "set-cdr!" | "display" | "newline" | \dots\\
\\
<begin> &::=& "(begin " \expr^{+}")"\\
\\
<assignment> &::=& "(set!"\: \vrbl\: \expr")"
\end{eqnarray*}
\end{bnf}

\section{Derived Syntax}

\begin{bnf}
\begin{eqnarray*}
\define &::=& \dots | "(define ("\vrbl <formals>")"\: \bod")"\\
\bod  &::=& <internal defines> \expr^{+}\\
<internal defines> &::=& \define^* \qquad \hbox{(Note: all defined variables must be distinct.)}\\
\\
\expr &::=& \dots | <cond> | \andsf | \orsf | <quoted>\\
\\
<keyword>  &::=&  \ \dots\, | "cond" | "else" | "and" | "or" | "quasiquote"\\
\\
\letform &::=& \dots | "("<let keyword> "("<binding>^{*}")"\: \bod")" \\
<let keyword> &::=& \dots | "let" | "let*"\\
\\
\lamexp &::=& \dots | "(lambda ("<formals>")"\: \bod")"\\
         && {} | "(lambda " \vrbl\: \bod")"\\
\\
<cond> &::=& "(cond"\: <clause> <clause>^{*}")"\\
<clause> &::=& "("<test> \expr^*")" | "(else"\: \expr^+")"\\
\andsf &::=& "(and "\expr^{*}")"\\
\orsf &::=& "(or "\expr^{*}")"\\
\\
<quoted> &::=& "(quote"\: <s-expression>")" | "(quasiquote"\: <s-expression>")" \\
<s-expression> &::=& \idfr | <self-evaluating> | "("<s-expression>^*")"
\end{eqnarray*}
\end{bnf}

\section{Syntactic Values}

\begin{bnf}
\begin{eqnarray*}
\sval &::=& \ival | \prval | \lsval\\
\ival &::=&  <self-evaluating> | <symbol> | \proc\\
\prval &::=& "(cons " \sval\: \prval")"\\
           && {} |  "(cons " \sval\: \ival ")"\\
\lsval &::=& <nil> | "(list " \sval^{+} ")"\\
\end{eqnarray*}
\end{bnf}

\section{Control Contexts for Kernel Scheme}
\begin{bnf}
\begin{eqnarray*}
\ccntxt &::=& \hole\\
     && {} | "(if "\ccntxt\: \expr\: \expr")"\\
     && {} | "(begin "\ccntxt\: \expr^*")"\\
     && {} | "(set! "\vrbl\: \ccntxt")"\\
     && {} | "("<let keyword>\\
     && {} \qquad "("<value binding>^*\: "("\vrbl\: \ccntxt")"\: <binding>^*")"\\
     && {} \quad \qquad \expr")"\\
     && {} | "("\sval^*\: \ccntxt\: \expr^*")"\\
\hole  &::=& \Code{  < >}\\
<value binding> &::=& "("\vrbl\: \sval")"
\end{eqnarray*}
\end{bnf}

\section{Immediate Redexes for Kernel Scheme}

\begin{bnf}
\begin{eqnarray*}
<immediate redex> &::=& \vrbl\\
     && {} | "(if "\sval\: \expr\: \expr")"\\
     && {} | "(begin "\expr")"\\
     && {} | "(begin "\sval\: \expr^*")"\\
     && {} | "(set! "\vrbl\: \sval")"\\
     && {} | "("<let keyword> "("<value binding>^*")" \expr")"\\
     && {} | "("\sval^+")"\\
     && {} | "(define "\vrbl\: \expr")"
\end{eqnarray*}
\end{bnf}

\begin{lemma*} (\textbf{Unique Matching})
If a Scheme expression, $E$, is not a syntactic value, then there is a
unique control context, $C$, and a unique immediate redex, $R$, such that
$E = \subst{C}{\Code{< >}}{R}$.  Moreover, if $B$ is a sequence of value
bindings (of distinct variables), then there is at most one Scheme
Substitution Model rewrite rule whose pattern matches
\Code{(letrec\,(\mbox{$B$})\,\mbox{$E$})}, and if there is such a rewrite
rule, its match is unique.
\end{lemma*}

\end{document}
