more edits for clarity

doc/bool.ott

@@ -15,27 +15,33 @@ v :: 'v_' ::=
   | Bool                  ::   :: TyBool 
   | True                  ::   :: LitTrue
   | False                 ::   :: LitFalse
-  | if ne then a else b    ::   :: If
 
 neutral , ne :: 'n_' ::=
   | if ne then a else b    ::   :: If
 
+nf :: 'nf_' ::= 
+  | Bool                  ::   :: TyBool 
+  | True                  ::   :: LitTrue
+  | False                 ::   :: LitFalse
+  | if ne then a else b    ::   :: If
+
+
 defns 
 Jwhnf :: '' ::= 
 
 defn
-whnf a ~> v ::    :: whnf :: 'whnf_' 
+whnf a ~> nf ::    :: whnf :: 'whnf_' 
 by
 
 whnf a ~> True
-whnf b1 ~> v
+whnf b1 ~> nf
 --------------------------- :: if_true
-whnf if a then b1 else b2 ~> v
+whnf if a then b1 else b2 ~> nf
 
 whnf a ~> False
-whnf b2 ~> v
+whnf b2 ~> nf
 ------------------------------- :: if_false
-whnf if a then b1 else b2 ~> v
+whnf if a then b1 else b2 ~> nf
 
 ----------------- :: bool
 whnf Bool ~> Bool

doc/data.ott

@@ -29,11 +29,15 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }}
 v :: 'v_' ::= 
    | K args       ::     :: TCon
    | T args       ::     :: DCon 
-   | case ne of { </ pati -> ai // i /> } ::     :: Case 
 
 neutral, ne :: 'n_' ::=
    | case ne of { </ pati -> ai // i /> } ::     :: Case 
 
+nf :: 'nf_' ::= 
+   | K args       ::     :: TCon
+   | T args       ::     :: DCon 
+   | case ne of { </ pati -> ai // i /> } ::     :: Case 
+
 
 args {{ tex \overline{a} }} , bs {{ tex \overline{b} }} :: '' ::= 
    |              ::     :: Nil
@@ -78,7 +82,7 @@ defns
 Jwhnf :: '' ::= 
 
 defn
-whnf a ~> v ::    :: whnf :: 'whnf_' 
+whnf a ~> nf ::    :: whnf :: 'whnf_' 
 by
 
 -------------------- :: tcon
@@ -88,9 +92,9 @@ whnf T args ~> T args
 whnf K args ~> K args
 
 match (K args) (pati -> ai) ~> b
-whnf b ~> v
+whnf b ~> nf
 ---------------------------------------------------------------------- :: case
-whnf case (K args) of { </ pati -> ai // i /> } ~> v
+whnf case (K args) of { </ pati -> ai // i /> } ~> nf
 
 a ~> ne
 ------------------------------------------------------------------------------- :: case_cong

doc/epsilon.ott

@@ -43,7 +43,7 @@ defns
 Jwhnf :: '' ::= 
 
 defn
-whnf a ~> v ::    :: whnf :: 'whnf_' 
+whnf a ~> nf ::    :: whnf :: 'whnf_' 
 by
 
 defns

doc/oplss.mng

@@ -1251,7 +1251,8 @@ The main idea is that we will:
 
 \item
   Figure out how to revise the \emph{algorithmic} version of our type
-  system so that it supports the above rule.
+  system so that it supports the above rule, deferring to an algorithmic 
+  version of equality.
 \end{itemize}
 
 What is a good definition of equality? We have implicitly started with a very
@@ -1333,6 +1334,8 @@ $\Pi$-type, then we can access its subcomponents.
 has already been reduced to normal form. This will allow \rref{c-lambda} to
 match against a literal function type.
 
+\[ \drule[width=4in]{c-whnf} \]
+
 \end{itemize}
 
 \begin{figure}
@@ -1345,19 +1348,20 @@ match against a literal function type.
 
 The following judgment (shown in Figure~\ref{fig:whnf})
 %
-\[ \fbox{$[[whnf a ~> v]]$} \]
+\[ \fbox{$[[whnf a ~> nf]]$} \]
 %
-describes when a term $[[a]]$ reduces to some result $[[v]]$ in \emph{weak
+describes when a term $[[a]]$ reduces to some result $[[nf]]$ in \emph{weak
   head normal form (whnf)}.  For closed terms, these rules correspond to a
 big-step evaluation relation and produce a value (i.e. abstraction or type
-form).  For open terms, the rules could also produce terms that are some
+form).  For open terms, the rules could also produce terms that are a
 sequence of applications headed by a variable.  In this case, we call the term
 a \emph{neutral} term, and use the metavariable $[[ne]]$ to refer to it.
 
 \[ 
 \begin{array}{llcl}
-\textit{value}     & [[v]] & ::= & [[Type]]\ |\ [[\x.a]]\ |\ [[(x:A) -> B]]\ |\ [[()]]\ |\ [[Unit]]\ |\ [[ne]] \\
+\textit{value}     & [[v]] & ::= & [[\x.a]]\ [[Type]]\ |\ [[(x:A) -> B]]\ \\
 \textit{neutral terms} & [[ne]] & ::= & [[x]]\ |\ [[ne a]] \\
+\textit{weak-head normal form} & [[nf]] & ::= & [[v]]\ |\ [[ne]] \\
 \end{array}
 \]
 
@@ -1429,11 +1433,17 @@ of \texttt{inferType}
 \subsection{Implementing definitional equality (see Equal.hs)}
 \label{sec:equate}
 
+\begin{figure}
+\drules[eq]{$[[G |- A <=> B]]$}{Algorithmic equality}{refl,whnf,abs,pi,app}
+\caption{Algorithmic equality for core \pif}
+\label{fig:algeq}
+\end{figure}
+
+
 The rules for $[[G |- a = b ]]$ \emph{specify} when terms should be equal, but
 they are not an algorithm. But how do we implement its algorithmic analogue
 $[[G |- a <=> b]]$?
 
-
 There are several ways to do so.
 
 The easiest one to explain is based on reduction---for \texttt{equate} to
@@ -1450,8 +1460,11 @@ One way to do this is with the following algorithm:
 \end{verbatim}
 
 However, we can do better.  Sometimes we can find out that terms are
-equivalent without fully reducing them. Because reduction can be expensive (or
-even nonterminating) we would like to only reduce as much as necessary.
+equivalent without fully reducing them. For example, if we observe that the
+two terms are already $\alpha$-equavalent, then we already know that they are
+equal---no need to reduce them first. Because reduction can be expensive (or
+even nonterminating) we would like to only reduce as much as we need to find
+out whether the terms can be identified.
 
 Therefore, the implementation of \cd{equate} has the following form.
 \begin{verbatim}
@@ -1474,35 +1487,39 @@ Therefore, the implementation of \cd{equate} has the following form.
         -- | head forms don't match throw an error
         (_,_) -> Env.err ...
 \end{verbatim}
-Above, we first check whether the terms are already alpha-equivalent. If they
-are, we do not need to do anything else, we can return immediately
+Above, we first check for alpha-equivalence. If they
+are, we do not need to do anything else. Instead, the function returns immediately
 (i.e., without throwing an error, which is what the function does when it
 decides that the terms are not equal). The next step is to reduce both terms
 to their weak head normal forms.  If two terms have different head forms, then
 we know that they must be different terms, so we can throw an error. If they have
 the same head forms, then we can call the function recursively on analogous
 subcomponents until the function either terminates or finds a mismatch.
 
+This algorithm is summarized in Figure~\ref{fig:algeq}.
+
 Why do we use weak head reduction vs.~full reduction?
 
 \begin{itemize}
-\item
-  We can implement deferred substitutions for variables. Note that when
-  comparing terms we need to have their definitions available. That way we
-  can compute that \texttt{(plus\ 3\ 1)} weak head normalizes to 4, by
-  looking up the definition of \texttt{plus} when needed. However, we
-  don't want to substitute all variables through eagerly---not only does
-  this make extra work, but error messages can be extremely long.
+\item We can extend this algorithm to implement deferred substitutions for
+  variables. Note that when comparing terms we need to have their definitions
+  available. That way we can compute that \texttt{(plus\ 3\ 1)} weak head
+  normalizes to 4, by looking up the definition of \texttt{plus} when
+  needed. However, we don't want to substitute all variables through
+  eagerly---not only does this make extra work, but error messages can be
+  extremely long.
 \item Furthermore, we allow recursive definitions in \pif, so normalization
   may just fail completely if we unfold recursive definitions inside
   functions before they are applied. In contrast, the definition based on
   \texttt{whnf} only unfolds recursive definitions when they stand in the way
   of equivalence, so avoids some infinite loops in the type checker.
-
-  Note that we don't have a complete treatment of equality. There will always
-  be terms that can cause \texttt{equate} to loop forever.
 \end{itemize}
 
+Note that equality is not decidable in \texttt{pi-forall}. There will always
+be terms that could cause \texttt{equate} to loop forever. However, the
+algorithm is sound. If it says that two terms are equal, then there is some
+derivation using the rules of Figure~\ref{fig:defeq} that the terms are equal.
+
 \section{Dependent pattern matching and propositional equality}
 \label{sec:pattern-matching}
 
@@ -1755,9 +1772,13 @@ with an equivalent type.
 
 \[ \drule[width=4in]{t-subst-simple} \]
 
-How can we implement this rule? For simplicity, we will play the same trick that
-we did with booleans, requiring that one of the sides of the equality be a
-variable.
+How can we implement this rule? For simplicity in these lecture notes, we will
+play the same trick that we did with booleans, requiring that one of the sides
+of the equality be a variable.\footnote{The \pif implementation implements a more 
+expressive rule that uses \emph{unification} to determine the substitution to apply 
+to $A$. Unification means that if we have an equality type such as
+$[[(x, True) = ( (), y)]]$ 
+then we can produce the substitution of $[[()]]$ for $[[x]]$ and $[[True]]$ for $[[y]]$.}
 
 \[ \drule[width=4in]{c-subst-left-simple} \]
 \[ \drule[width=4in]{c-subst-right-simple} \]
@@ -1885,21 +1906,22 @@ evaluate to \texttt{Refl} we could erase it.
 We need to make sure that an irrelevant variable is not ``used'' in the
 relevant parts of the body of a $\lambda$-abstraction. How can we do so?
 
-The key idea is that we mark variables in the context with an $[[ep]]$
-annotation, which is either $[[Rel]]$ (relevant) or $[[Irr]]$ (irrelevant).
-``Normal'' variables, introduced by $\lambda$-expressions, will always be
-marked as relevant, and only relevant variables can be used in terms.  As a
-result, we revise the variable typing rule to require the relevant annotation.
-In the \texttt{version3} implementation, type signatures in the environment now
-include an \cd{Epsilon} tag, and the function \cd{checkStage} ensures that this
-tag is $[[Rel]]$ when the variable is used in the term.
+The key idea is that we mark variable assumptions in the context with an
+$\epsilon$ annotation, which is either $[[Rel]]$ (relevant) or $[[Irr]]$
+(irrelevant).  and only relevant variables can be used in terms. (``Normal''
+variables, introduced by $\lambda$-expressions, will always be marked as
+relevant.) As a result, we revise the variable typing rule to require the
+relevant annotation.  In the \texttt{version3} implementation, type signatures
+in the environment now include an \cd{Epsilon} tag, and the function
+\cd{checkStage} ensures that this tag is $[[Rel]]$ when the variable is used
+in the term.
 
 \[
 \drule{t-evar}
 \]
 
 An irrelevant abstraction introduces its variable into the context tagged with
-the irrelevant annotation. Because of the $[[Irr]]$ tag, such variables are
+the irrelevant annotation. Because of the $[[Irr]]$ tag, these variables are
 inaccessible in the body of the function.
 
 \[
@@ -1916,8 +1938,8 @@ in the \rref{t-eapp} rule below.
 \]
 
 This operation on the context, called \emph{resurrection}, converts all
-$[[Irr]]$ tags on variables to be $[[Rel]]$. It represents a shift in our
-perspective: because we have entered an irrelevant part of the term, the
+``$[[Irr]]$'' tags on variables to be ``$[[Rel]]$''. It represents a shift in
+our perspective: because we have entered an irrelevant part of the term, the
 variables that were not visible before are now available after this context
 modification.
 
@@ -1951,7 +1973,7 @@ arguments are now tagged with their relevance, and when we compare arguments
 that are tagged as irrelevant, we do nothing. In fact, what we are doing is
 actually \emph{defining} equality over just the computationally relevant parts
 of the term instead of the entire term. And we have been doing this in a limited
-form from the beginning---recall that \texttt{version1} of \pif \pif already
+form from the beginning---recall that \texttt{version1} of \pif already
 ignores type annotations. Just as type annotations do not affect computation
 and can be ignored, the same reasoning holds for irrelevant arguments.