\documentclass{handout}
\usepackage{6044}
\usepackage{time,fullpage}
\usepackage{amsmath}

\begin{document}

\handout{95-lecture-outline}{Outline of Fall 1995 Lectures}{14 September 1995}

\begin{enumerate}
%1
\item (Wed, 9/6) Administration.  Definition of ``halting'' Scheme
expressions, and statement of non-existence of Scheme procedure {\tt halts?}.

%2
\item (Wed, 9/8) Proof of noncomputability of {\tt halts?}  Diagonal
arguments.  Countability of ASCII strings and Scheme procedures.

%3
\item (Mon, 9/11) Scheme expression halting depends on store and environment.
Extension of halting problem undecidiablity to arbitrary properties of
values.  End with question: what is a Scheme ``value''?

%4
\item (Wed, 9/13) Relevance to other languages.  Scheme interpreter for C
implies C can't solve Scheme halting problem either.  Paradox from
self-application.

(Fri, 9/15) Cancelled

%5
\item (Mon, 9/18) Rewriting model for Scheme; primitive, conditional and
instantiation rules. Uniqueness.

%6
\item (Wed, 9/20) lambda application rule; renaming for static scope.
Adding syntactic sugar.

%7
\item (Fri, 9/21) state possible simulation of numbers, lists,
conditional, even defines by ``pure'' applicative Scheme.  State Hilbert's
10th to illustrate how numbers may cause problems.

(Mon, 9/25) no classes

%8
\item (Wed, 9/27)  Equational reasoning about Church numerals.

%9
\item (Fri, 9/29) Translation of function Scheme into pure applicative
Scheme.  Understanding recursion as finding fixed points.

%10
\item (Mon, 10/2) Y operator

(Wed, 10/4) cancelled (Yom Kippur)

%11
\item (Fri, 10/6) Observational congruence

(Mon, 10/9) Columbus Day

%12
\item (Wed, 10/11) Observational congruence

\item (Fri 10/13)
\item (Mon 10/16)
\item (Wed 10/18)\\
 Equational proofs.  The proof system $\fe$.  Decidable iff
half-decidable and co-half-decidable.  Provable equations are
half-decidable.

\item (Fri 10/20) car(decidable) is half-decidable.

\item (Mon 10/23) repair lacuna: car(decidable) is half-decidable requires
a symbol enumerator.  remark: car(half-decidable) is still half-decidable.
Thm: Provable equations are half-decidable.  Thm: (proof for Wed) True $\fe$
equations are not half-decidable.  Cor: Incompleteness of sound proof
systems.

\item (Wed 10/25) \Code{($M$ = (spin))} $\in \mbox{True}_{\it func}$ iff
$M \in$ complement(Halts).  set containment versus decidability.  many-one
reducibility.

\item (Fri 10/27) Review, mainly of PS4.
\end{enumerate}

\end{document}
