\documentclass[11pt]{handout}

\usepackage{6044}
\usepackage{time}
\usepackage[fleqn]{amsmath}
\usepackage{prooftree}
\setlength{\textheight}{8in}
\setlength{\textwidth}{5.5in}
\setlength{\oddsidemargin}{.4in} 
\setlength{\evensidemargin}{0in} 
\parindent0in
\parskip\medskipamount

\newcommand{\ple}{\ensuremath{\vdash_\le\,}}

\def\f={\mathop{\Code{=}}}
\newcommand{\eqtn}[2]{\Code{( #1 = #2 )}}
\newcommand{\peqtn}[2]{\fortext{\proves \eqtn{#1}{#2}}}
\newcommand{\etrm}[1]{\Code{ = #1}}
\newcommand{\leqtn}[2]{\Code{( #1 <= #2 )}}
\newcommand{\aeqv}{\fortext{\mathrel{=_{\alpha}}}}

\newcommand{\qrule}[1][]{%
    \ifx!#1!\else
        \rlap{\hbox to 4em{\hss#1\hss}}%
    \fi
    \vrule width 4em height -2.1pt depth 2.5pt\relax
}

\def\opCode#1{\mathbin{\Code{#1}}}

\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{pval}{primitive\ value}
\DefineBNFAbbrev{ival}{immediate\ value}
\DefineBNFAbbrev{test}{test}
\DefineBNFAbbrev{orsf}{or}
\DefineBNFAbbrev{andsf}{and}
\DefineBNFAbbrev{prvar}{procedure\ variable}
\DefineBNFAbbrev{rspvar}{rule-specified\ procedure\ variable}
\DefineBNFAbbrev{pprvar}{primitive\ procedure\ variable}
\DefineBNFAbbrev{lamexp}{lambda\ expression}
%\DefineBNFAbbrev{beginsf}{begin}

\makeatletter


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

\makeatletter
\renewenvironment{description}
               {\list{}{\labelwidth\z@
                        \leftmargin1em
                        \itemindent-\leftmargin
                        \let\makelabel\descriptionlabel}}
               {\endlist}
\makeatother

\renewcommand*\descriptionlabel[1]{\hspace\labelsep
                                {\normalfont\bfseries #1}:}


\begin{document}
\handout{q1}{Quiz 1}{7 October 1996}

\medskip

\problem For any arithmetic expression $e$, the sequence of equalities and
inequalities below is a proof in our formal system for proving
inequalities.  (The Appendix contains all the rules of the system.)  For
each line, write the line numbers of its antecedents in the space to its
left; if a line is an axiom, write its own line number.  For example, the
required antecedent numbers for lines (1) and (4) have been filled in for
you.

%%  \begin{eqnarray}
%%  \Code{\underline{\quad{\rm (1)}\quad} 0 + (-0)} & \Code{=} & \Code{-0}\\
%%  \Code{\underline{\qquad\qquad} 0 + (-0)} & \Code{=} & \Code{0}\\
%%  \underline{\qquad\qquad}\Code{       -0} & \Code{=} & \Code{0 + (-0)}\\
%%  \Code{\underline{ {\rm (3) (2)}  }       -0} & \Code{=} & \Code{0}\\
%%  \Code{\underline{\qquad\qquad}        0} & \Code{\:<=\:} & \Code{1}\\
%%  \Code{\underline{\qquad\qquad}       -1} & \Code{\:<=\:} & \Code{-0}\\
%%  \Code{\underline{\qquad\qquad}       -1} & \Code{\:<=\:} & \Code{0}\\
%%  \Code{\underline{\qquad\qquad}  -1 + $e$} & \Code{\:<=\:} & \Code{0 + $e$}\\
%%  \Code{\underline{\qquad\qquad}   0 + $e$} & \Code{=} & e\\
%%  \Code{\underline{\qquad\qquad}  -1 + $e$} & \Code{\:<=\:} & e
%%  \end{eqnarray}

\begin{align}
\qrule[(1)]
        && \Code{0 + (-0)}  & \opCode{=} \Code{-0} \\
\qrule  && \Code{0 + (-0)}  & \opCode{=} \Code{0} \\
\qrule  && \Code{-0}        & \opCode{=} \Code{0 + (-0)} \\
\qrule[(3) (2)]
        && \Code{-0}        & \opCode{=} \Code{0} \\
\qrule  && \Code{0}         & \opCode{<=} \Code{1} \\
\qrule  && \Code{-1}        & \opCode{<=} \Code{-0} \\
\qrule  && \Code{-1}        & \opCode{<=} \Code{0} \\
\qrule  && \Code{-1 + $e$}  & \opCode{<=} \Code{0 + $e$} \\
\qrule  && \Code{0 + $e$}   & \opCode{=} e \\
\qrule  && \Code{-1 + $e$}  & \opCode{<=} e
\end{align}

\problem Explain why \Code{( x <= (x * x) )} is not provable in our formal
system.

\newpage

\problem
\subproblem Here is a useful inference rule for inequalities:
\[\prooftree
    \Code{($e$ <= $f$)}, \quad \Code{($g$ <= $h$)}
\justifies
    \Code{( ($e$ + $g$) <= ($f$ + $h$) )}
\using
    \mbox{\ \ (\Code{++}-\Code{<=}-congruence)}
\endprooftree\]

Explain why adding the rule (\Code{++}-\Code{<=}-congruence) to our
proof system will not change the set of provable inequalities.

\vspace{3in}

\subproblem  Explain why deleting the rule \mbox{($\leq$-antisymmetry)}
will not change the set of provable inequalities.

\vspace{3in}


\problem Here is a body from our functional kernel of Scheme:
\begin{quote}
\Code{(define l 1)}\\
\Code{(define m 2)}\\
\Code{(define n 3)}\\
\Code{(define add\_n (lambda (m) (+ m n)))}\\
\Code{(define mul\_m\_add5+n (lambda (n) (+ (2 3) (add\_n (* m n)))))}\\
\Code{(mul\_m\_add5+n ( (lambda (m) (+ m n))  5 ))}
\end{quote}

\subproblem  Underline {\em all} the redexes in this body.

\subproblem Write out the body that results from one rewriting at the
lambda application redex followed by all possible applications of the
garbage collection rule.

\vspace{2in}

\newpage

\problem  Give an example of a functional kernel Scheme body that is
\subproblem an \ival\ that is not terminated.

\vspace{.7in}

\subproblem a terminated expression that is not an \ival.

\vspace{.7in}

\subproblem a body that {\em cannot} reach a terminated body by repeated rewriting.

\vspace{1in}


\newpage

\subsubsection*{Appendix}
\begin{table}[!h]

\parindent0pt

\caption{Standard Equational Inference Rules.}\small
%\label{steqrules}}
\[\begin{array}{|c|} \hline
\\
\prooftree
\justifies
    e = e
\using
    \mbox{(reflexivity)}
\endprooftree
\qquad\quad
\prooftree
    e = f
\justifies
    f = e
\using
    \mbox{(symmetry)}
\endprooftree
\qquad\quad
\prooftree
     e = f, \quad f = g
\justifies
    e = g
\using
    \mbox{(transitivity)}
\endprooftree\\
\\
\prooftree
    e_{1} = e_{2}, \quad f_{1} = f_{2}
\justifies
    e_1 + f_1 = e_2 + f_2
\using
    \mbox{($+$-congruence)}
\endprooftree
\quad
\prooftree
    e_{1} = e_{2}, \quad f_{1} = f_{2}
\justifies
    e_1 * f_1 = e_2 * f_2
\using
    \mbox{($*$-congruence)}
\endprooftree
\quad
\prooftree
    e = f
\justifies
   -e = -f
\using
    \mbox{($-$-congruence)}
\endprooftree\\
\\ \hline
\end{array}\]
%%  \end{table}


%%  \begin{table}[h]
\caption{Equational Axioms for Arithmetic%\label{eqaxarith}
}\small
\[\begin{array}{|rcll|}
\hline
(e + f) + g &=& e + (f + g) & \mbox{(associativity of $+$)}\\
(e * f) * g &=& e * (f * g) & \mbox{(associativity of $*$)}\\
e + f &=& f + e & \mbox{(commutativity of $+$)}\\
e * f &=& f * e & \mbox{(commutativity of $*$)}\\
0 + e &=& e  & \mbox{(identity for $+$)}\\
1 * e &=& e  & \mbox{(identity for $*$)}\\
e + (-e) &=& 0  & \mbox{(inverse for $+$)}\\
e * (f + g) &=& (e * f) + (e * g) & \mbox{(distributivity)}\\
\hline
\end{array}\]
%%  \end{table}

%%  \begin{table}[h]
\caption{Inference Rules for Inequalities.}\small
% \label{ineq}}\small
\[\begin{array}{|c|} \hline
\\
\prooftree
    e = f
\justifies
    e \leq f
\using
    \mbox{($\leq$-reflexivity)}
\endprooftree
\quad
\prooftree
    e \leq f, \quad f \leq e
\justifies
    f = e
\using
    \mbox{($\leq$-antisymmetry)}
\endprooftree
\quad
\prooftree
     e \leq f, \quad f \leq g
\justifies
    e \leq g
\using
    \mbox{($\leq$-transitivity)}
\endprooftree\\
\\
\prooftree
    e \leq f
\justifies
    e + g \leq f + g
\using
    \mbox{($+$-$\leq$-congruence)}
\endprooftree
\quad
\prooftree
    e \leq f, \quad 0 \leq g
\justifies
    e * g \leq f * g
\using
    \mbox{($*$-$\leq$-congruence)}
\endprooftree
\quad
\prooftree
    e \leq f
\justifies
    -f \leq -e
\using
    \mbox{($-$-$\leq$-congruence)}
\endprooftree\\
\\
0 \leq 1 \quad\mbox{($01$-axiom)}\\
\\ \hline
\end{array}\]
\end{table}

\end{document}



\iffalse

term-sequence proof iff equation-sequence proof

diamond lemma--say uniqueness for simple exps plus non-immediate defines.

\fi
