\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-soln}{Quiz 1 Solutions}{9 October 1996}

\medskip

\problem(20) 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{align}
\qrule[(1)]
        && \Code{0 + (-0)}  & \opCode{=} \Code{-0} \\
\qrule[(2)]  && \Code{0 + (-0)}  & \opCode{=} \Code{0} \\
\qrule[(1)]  && \Code{-0}        & \opCode{=} \Code{0 + (-0)} \\
\qrule[(3) (2)]
        && \Code{-0}        & \opCode{=} \Code{0} \\
\qrule[(5)]  && \Code{0}         & \opCode{<=} \Code{1} \\
\qrule[(5)]  && \Code{-1}        & \opCode{<=} \Code{-0} \\
\qrule[(6) (4.5)]  && \Code{-1}        & \opCode{<=} \Code{0} \\
\qrule[(7)]  && \Code{-1 + $e$}  & \opCode{<=} \Code{0 + $e$} \\
\qrule[(9)]  && \Code{0 + $e$}   & \opCode{=} e \\
\qrule[(8) (9.5)]  && \Code{-1 + $e$}  & \opCode{<=} e
\end{align}

Correction made in class: insert lines
\begin{align*}
\qrule[(4)]
        && \hspace{1.3in} \Code{-0}        & \opCode{<=} \Code{0} \hspace{2.4in} (4.5)\\
\qrule[(9)]  && \Code{0 + $e$}   & \opCode{<=} e \hspace{2.4in} (9.5)
\end{align*}

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

\begin{quotation}\noindent
All the axioms are valid over the real numbers, \reals, and the inference
rules all preserve validity over \reals, so all provable inequalities must
be valid over \reals.  But the inequality above is not valid over \reals,
e.g., it fails for $\Code{x} = 1/2$, and hence it is not provable in our
system.
\end{quotation}

\newpage
\problem(30)
\subproblem(15)
\[\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.
\begin{quotation}\noindent
We claim that if $\ple \Code{($e$ <= $f$)}$ and $\ple
\Code{($g$ <= $h$)}$, then\\
$\ple \Code{( ($e$ + $g$) <= ($f$ +$h$) )}$.  So any use of the
(\Code{++}-\Code{<=}-congruence) rule in a proof could be replaced by an
ordinary $\ple$-proof of its consequent, and there is no need ever to use
this rule.

To prove the claim, note that from $\ple \Code{($e$ <= $f$)}$, we
can conclude that 
\[\ple \Code{( ($e$ + $g$) <= ($f$ + $g$) )}\]
by (\Code{+}-\Code{<=}-congruence).  From $\ple
\Code{($g$ <= $h$)}$, we
can conclude that $\ple \Code{( ($g$ + $f$) <= ($h$ + $f$) )}$ by 
(\Code{+}-\Code{<=}-congruence) again, and then
\[\ple \Code{( ($f$ + $g$) <= ($f$ + $h$) )}\]
by (+-commutativity), ($\leq$-reflexivity), and
($\leq$-transitivity).  A final application of the ($\leq$-transitivity) rule
to the displayed equations shows that
\[\ple \Code{( ($e$ + $g$) <= ($f$ + $h$) )}\]
as required.
\end{quotation}

\subproblem(15)  Explain why deleting the rule \mbox{($\leq$-antisymmetry)}
will not change the set of provable inequalities.
\begin{quotation}\noindent
The consequent of the rule is an equation, so any use of the
\mbox{($\leq$-antisymmetry)} rule in a proof could be replaced by
inserting a purely equational proof of the consequent.  Such an
equational proof always exists by {\em completeness} of our equational
system.
\end{quotation}

\problem(15)
\begin{quote}
\Code{\underline{(define l 1)}}\footnote{Technically, the {\em whole body}
is the redex of the garbage collection rule, but this particular definition is the
part of the redex which gets erased.}\\
\Code{(define m 2)}\\
\Code{(define n 3)}\\
\Code{(define add\_n (lambda (m) (+ m \underline{n})))}\\
\Code{(define mul\_m\_add5+n (lambda (n) (+ (2 3) (\underline{add\_n} (* \underline{m} n)))))}\\
\Code{(\underline{mul\_m\_add5+n} \underline{( (lambda (m) (+ m \underline{n}))  5 )})}
\end{quote}

\subproblem(5)  Underline {\em all} the redexes in this body.
\begin{quotation}
There are seven in all: 1 G, 1 L, and 5 I.
\end{quotation}


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

\begin{quote}
\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{(define m\_1 5)}\\
\Code{(mul\_m\_add5+n (+ m\_1 n))}
\end{quote}

\problem(15)  Give an example of a functional kernel Scheme body that is
\subproblem(5) an \ival\ that is not terminated.
\[\Code{(lambda (x) $M$)}\] where $M$ is {\em any} body which is not
terminated, e.g.,
\[\Code{(lambda (x) (+ 0 1))}\]

\subproblem(5) a terminated expression that is not an \ival.
\[\Code{(2 3)}\] or any other such ``error-causing'' primitive
application.

\subproblem(5) a body that {\em cannot} reach a terminated body by repeated rewriting.
\[\Code{(define f (lambda (x) (f x))) (f 1)}\]
\[\Code{( (lambda (x) (x x)) (lambda (x) (x x)) )}\]
are representative examples.

\end{document}
