summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/lazylist
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/latex/lazylist')
-rw-r--r--Master/texmf-dist/doc/latex/lazylist/lazylist.tex1156
1 files changed, 1156 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/lazylist/lazylist.tex b/Master/texmf-dist/doc/latex/lazylist/lazylist.tex
new file mode 100644
index 00000000000..9173ed7e789
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lazylist/lazylist.tex
@@ -0,0 +1,1156 @@
+% Filename: lazylist.tex
+% Author: Alan Jeffrey
+% Last modified: 11 May 1990
+% Modified: 24 July 2003 by Robin Fairbairns, for file name changes
+% and use with LaTeX 2e
+%
+% Copyright (c) 1990 Alan Jeffrey. Permission is granted to Tugboat
+% to publish any or all of this.
+%
+% A keyboard check:
+%
+% @ # $ % ^ & * ~ at hash dollar percent caret ampersand asterisk tilde
+% : ; , . colon semicolon comma period
+% ? ! question-mark exclamation-mark
+% " ' ` double-quote apostrophe back-quote
+% ( ) { } [ ] parentheses braces square-brackets
+% - + = / \ minus plus equals forward-slash backslash
+% _ | < > underscore vertical-bar less-than greater-than
+%
+
+\documentclass{ltugboat}
+\usepackage{lazylist}
+
+% This document defines a whole load of extra commands, some of which
+% over-ride how LaTeX normally lays things out. For example, ~ is
+% redefined to give a hairspace in math mode. This whole document
+% should probably be put in a group to stop it getting in the way
+% of other articles' macros.
+
+\title{Lists in \TeX's Mouth}
+
+\author{Alan Jeffrey}
+
+\address{Programming Research Group\\
+ Oxford University\\
+ 11 Keble Road\\
+ Oxford OX1 3QD}
+
+\netaddress{Alan.Jeffrey@uk.ac.oxford.prg}
+
+\makeatletter
+
+% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
+% generate text italic rather than math italic by default. This makes
+% multi-letter names look neater. The mathcode for character 'c'
+% is set to "7000 (variable family) + "400 (text italic) + c.
+%
+% This neat bit of code is due to Mike Spivey.
+%
+% \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
+% \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
+% \advance\count0 by1 \advance\count1 by1 \repeat}}
+%
+% \@setmcodes{`A}{`Z}{"7441}
+% \@setmcodes{`a}{`z}{"7461}
+
+% however, for all its neatness, the code doesn't actually work in 2e;
+% the following looks even neater (if you don't consider what goes on
+% behind the scenes), and does the specified job
+
+\DeclareSymbolFont{letters} {OT1}{cmr} {m}{it}
+
+
+\def\Number#1{\csname Number-#1\endcsname}
+\def\Label#1{\csname Label-#1\endcsname}
+
+\newcount\Lastnum
+
+\def\Forward#1%
+ {\global\advance\Lastnum by 1
+ \csnameafter\xdef{Number-#1}%
+ {\the\Lastnum}%
+ \csnameafter\xdef{Label-\the\Lastnum}%
+ {\@currentlabel}}
+
+\def\csnameafter#1#2%
+ {\expandafter#1\csname#2\endcsname}
+
+\def\Bylist#1%
+ {\Map\Label
+ {\Insertsort\Lessthan
+ {\Map\Number{#1}}}}
+
+\def\By{\Show\Bylist}
+
+\let\bindspace=~
+\def~{\ifmmode \, \else \bindspace \fi}
+
+\def\start#1{\lefteqn{#1}\quad\\}
+
+\def\nil{[\,\,]}
+
+\newtheorem{fact}{Fact}
+\def\thefact{\@roman\c@fact}
+
+\def\cstok#1{\leavevmode\thinspace\hbox{\vrule\vtop{\vbox{\hrule\kern1pt
+ \hbox{\vphantom{\tt/}\thinspace{\tt#1}\thinspace}}%
+ \kern1pt\hrule}\vrule}\thinspace}
+
+\begingroup \catcode `|=0 \catcode `[= 1
+\catcode`]=2 \catcode `\{=12 \catcode `\}=12
+\catcode`\\=12 |gdef|@xTeXcode#1\end{TeXcode}[#1|end[TeXcode]]
+|endgroup
+
+\def\TeXcode
+ {\@verbatim \smallskip\hrule\medskip \frenchspacing\@vobeyspaces \@xTeXcode}
+\def\endTeXcode
+ {\medskip\hrule\smallskip\endtrivlist}
+
+\makeatother
+
+\begin{document}
+
+\maketitle
+
+\section{Why lists?}
+
+Originally, I wanted lists in \TeX\ for
+a paper I was writing which contained a lot of facts.
+\begin{fact}
+\Forward{Fac-cows}
+ Cows have four legs.
+\end{fact}
+\begin{fact}
+\Forward{Fac-people}
+ People have two legs.
+\end{fact}
+\begin{fact}
+\Forward{Fac-yawn}
+ Lots of facts in a row can be dull.
+\end{fact}
+These are generated with commands like
+\begin{verbatim}
+\begin{fact}
+\Forward{Fac-yawn}
+ Lots of facts in a row can be dull.
+\end{fact}
+\end{verbatim}
+I can then refer to these facts by saying
+\begin{verbatim}
+\By[Fac-yawn,Fac-cows,Fac-people]
+\end{verbatim}
+to get
+\By[Fac-yawn,Fac-cows,Fac-people].
+And as if by magic, the facts come out sorted, rather than in
+the jumbled order I typed them. This is very useful, as I can
+reorganize my document to my heart's content, and not have to worry
+about getting my facts straight.
+
+Originally I tried programming this sorting routine in \TeX's
+list macros, from Appendix~D of \TB, but I soon ran into trouble.
+The problem is that all the Appendix~D macros work by assigning
+values to macros. For example:
+\begin{verbatim}
+\concatenate\foo=\bar\baz
+\end{verbatim}
+expands out to
+\begin{verbatim}
+\ta=\expandafter{\bar}
+\tb=\expandafter{\baz}
+\edef\foo{\the\ta\the\tb}
+\end{verbatim}
+which assigns the macro \verb|\foo| the contents of \verb|\bar|
+followed by the contents of \verb|\baz|. Programming sorting routines
+(which are usually recursive) in terms of these lists became rather
+painful, as I was constantly having to watch out for local variables,
+worrying about what happened if a local variable had the same name
+as a global one, and generally having a hard time.
+
+Then I had one of those ``flash of light'' experiences ---
+``You can do lambda-calculus in \TeX,'' I thought,
+and since you can do lists directly in lambda calculus,
+you should be able to do lists straightforwardly in \TeX. And so you
+can. Well, fairly straightforwardly anyway.
+
+So I went and did a bit of mathematics, and derived the \TeX\ macros
+you see here. They were formally verified, and worked first time
+(modulo typing errors, of which there were two).
+
+\section{\TeX's mouth and \TeX's stomach}
+
+\TeX's programming facilities come in two forms --- there are \TeX's
+{\em macros\/} which are expanded in its mouth, and some additional
+{\em assignment\/} operations like \verb|\def| which take place in the
+stomach. \TeX\ can often spring surprises on you as exactly what
+gets evaluated where.
+For example, in \LaTeX\ I can put down a
+label by saying \verb|\label{Here}|.
+\label{Here}
+Then I can refer back to that label by saying
+\verb|Section~\ref{Here}|, which
+produces Section~\ref{Here}. Unfortunately, \verb|\ref{Here}| does
+{\em not\/} expand out to {\tt\ref{Here}}! Instead, it expands out to:
+\begin{verbatim}
+\edef\@tempa{\@nameuse{r@Here}}
+\expandafter\@car\@tempa\@nil\null
+\end{verbatim}
+This means that I can't say
+\begin{verbatim}
+\ifnum\ref{Here}<4 Hello\fi
+\end{verbatim}
+and hope that this will expand out to Hello. Instead I
+get an error message. Which is rather a pity, as \TeX's mouth is
+quite a powerful programming language (as powerful as a Turing Machine in
+fact).
+
+\section{Functions}
+
+A {\em function\/} is a mathematical object that takes in an argument
+(which could well be another function) and returns some other mathematical
+object. For example the function $Not$ takes in a boolean and returns
+its complement. I'll write function application without brackets,
+so $Not~b$ is the boolean complement of $b$.
+
+Function application
+binds to the left, so $f~a~b$ is $(f~a)~b$ rather than $f~(a~b)$.
+For example, $Or~a~b$ is the boolean or of $a$ and $b$, and
+$Or~True$ is a perfectly good function that takes in a boolean
+and returns $True$.
+
+The obvious equivalents of functions in \TeX\ are macros ---
+if I define a function $Foo$ to be:
+\begin{eqnarray*}
+ Foo~x & = & True
+\end{eqnarray*}
+then it can be translated into \TeX\ as:
+\begin{verbatim}
+\def\Foo#1{\True}
+\end{verbatim}
+So where $Foo$ is a function that takes in one argument, \verb|\Foo|
+is a macro that takes in one parameter. Nothing has changed except
+the jargon and the font. \TeX\ macros can even be partially applied,
+for example if we defined:
+\begin{eqnarray*}
+ Baz & = & Or~True
+\end{eqnarray*}
+then the \TeX\ equivalent would be
+\begin{verbatim}
+\def\Baz{\Or\True}
+\end{verbatim}
+Once \verb|\Baz| is expanded, it will expect to be given a parameter,
+but when we are defining things, we can go around partially applying
+them all we like.
+
+Here, I'm using $=$ without formally defining it, which is rather
+naughty. If I say $x = y$, this means
+``given enough parameters, $x$ and $y$ will eventually
+expand out to the same thing.'' For example $Foo = Baz$, because
+for any $x$,
+\begin{eqnarray*}
+ \start{Foo~x}
+ & = & True \\
+ & = & Or~True~x \\
+ & = & Baz~x
+\end{eqnarray*}
+Normally, functions have to {respect equality\/} which means that:
+\begin{itemize}
+\item if $x = y$ then $f~x = f~y$, and
+\item if $x$ respects equality, then $f~x$ respects equality.
+\end{itemize}
+However, some \TeX\ control sequences don't obey this. For example,
+\verb|\string\Foo| and \verb|\string\Baz| are different, even though
+$Foo = Baz$. Hence $string$ doesn't respect equality.
+Unless otherwise stated, we won't assume functions respect equality,
+although all the functions defined here do.
+
+All of our functions have capital letters, so that their \TeX\ equivalents
+(\verb|\Not|, \verb|\Or| and so on) don't clash with standard \TeX\ or
+\LaTeX\ macros.
+
+\subsection{Identity}
+
+The simplest function is the {\em identity\/} function, called
+$Identity$ funnily enough, which is defined:
+\begin{eqnarray*}
+ Identity~x & = & \Identity{x}
+\end{eqnarray*}
+This, it must be admitted, is a pretty dull function, but
+it's a useful basic combinator. It can be implemented
+in \TeX\ quite simply.
+\begin{TeXcode}
+\def\Identity#1{#1}
+\end{TeXcode}
+The rules around this definition mean that it is actually part of
+\verb|Lambda.sty| and not just another example.
+
+\subsection{Error}
+
+Whereas $Identity$ does nothing in a fairly pleasant sort of way,
+$Error$ does nothing in a particularly brutal and harsh fashion.
+Mathematically, $Error$ is the function that destroys everything
+else in front of it. It is often written as $\perp$.
+\begin{eqnarray*}
+ Error~x & = & Error
+\end{eqnarray*}
+In practice, destroying the entire document when we hit one error
+is a bit much, so we'll just print out an error message.
+The user can carry on past an error at their own risk, as the code
+will no longer be formally verified.
+\begin{TeXcode}
+\def\Error
+ {\errmessage{Abandon verification all
+ ye who enter here}}
+\end{TeXcode}
+Maybe this function ought to return a more useful error message \ldots
+
+\subsection{First and Second}
+
+Two other basic functions are $First$ and $Second$, both of which
+take in two arguments, and do the obvious thing. They are defined:
+\begin{eqnarray*}
+ First~x~y & = & x \\
+ Second~x~y & = & y
+\end{eqnarray*}
+We could, in
+fact, define $Second$ in terms of $Identity$ and $First$.
+For any $x$ and $y$,
+\begin{eqnarray*}
+ \start{First~Identity~x~y}
+ & = & Identity~y \\
+ & = & y \\
+ & = & Second~x~y
+\end{eqnarray*}
+So $First~Identity = Second$. This means that anywhere in our \TeX\ code
+we have \verb|\First\Identity| we could replace it by \verb|\Second|.
+This is perhaps not the most astonishing \TeX\ fact known to humanity,
+but this sort of proof did enable more complex bits of \TeX\ to be
+verified before they were run.
+
+The \TeX\ definitions of \verb|\First| and \verb|\Second| are pretty
+obvious.
+\begin{TeXcode}
+\def\First#1#2{#1}
+\def\Second#1#2{#2}
+\end{TeXcode}
+Note that in \TeX\, \verb|\First\foo\bar| expands out to
+\verb|\foo| {\em without\/} expanding out \verb|\bar|.
+This is very useful, as we can write macros that would take
+forever and a day to run if they expanded all their arguments,
+but which actually terminate quite quickly. This is called
+{\em lazy evaluation\/} by the functional programming community.
+
+\subsection{Compose}
+
+Given two functions $f$ and $g$ we would like to be able to {\em compose\/}
+them to produce a function that first applies $g$ then applies $f$.
+Normally, this is written as $f \circ g$, but unfortunately \TeX\ doesn't
+have infix functions, so we'll have to write it $Compose~f~g$.
+\begin{eqnarray*}
+ Compose~f~g~x & = & f~(g~x)
+\end{eqnarray*}
+>From this definition, we can deduce that $Compose$ is associative:
+\begin{eqnarray*}
+ \start{Compose~(Compose~f~g)~h}
+ & = & Compose~f~(Compose~g~h)
+\end{eqnarray*}
+and $Identity$ is the left unit of $Compose$:
+\begin{eqnarray*}
+ Compose~Identity~f & = & f
+\end{eqnarray*}
+The reader may wonder why $Identity$ is called a {\em left\/} unit
+even though it occurs on the right of the $Compose$ --- this is a side-effect
+of using prefix notations where infix is more normal. The infix version
+of this equation is:
+\begin{eqnarray*}
+ Identity \circ f & = & f
+\end{eqnarray*}
+so $Identity$ is indeed on the left of the composition.
+
+$Compose$ can be implemented in \TeX\ as
+\begin{TeXcode}
+\def\Compose#1#2#3{#1{#2{#3}}}
+\end{TeXcode}
+
+\subsection{Twiddle}
+
+Yet another useful little function is $Twiddle$, which takes in
+a function and reverses the order that function takes its (first two)
+arguments.
+\begin{eqnarray*}
+ Twiddle~f~x~y & = & f~y~x
+\end{eqnarray*}
+Again, there aren't many immediate uses for such a function, but it'll
+come in handy later on. It satisfies the properties
+\begin{eqnarray*}
+ Twiddle~First & = & Second \\
+ Twiddle~Second & = & First \\
+ Compose~Twiddle~Twiddle & = & Identity
+\end{eqnarray*}
+Its \TeX\ equivalent is
+\begin{TeXcode}
+\def\Twiddle#1#2#3{#1{#3}{#2}}
+\end{TeXcode}
+This function is called ``twiddle'' because it is sometimes written
+$\widetilde f$ (and $\sim$ is pronounced ``twiddle'').
+It also twiddles its arguments around,
+which is quite nice if your sense of humour runs to appalling puns.
+
+\section{Booleans}
+
+As we're trying to program a sorting routine, it would be nice to
+be able to define orderings on things, and to do this we need some
+representation of boolean variables. Unfortunately \TeX\ doesn't have a type
+for booleans, so we'll have to invent our own. We'll
+implement a boolean as a function $b$ of the form
+\begin{eqnarray*}
+ b~x~y &
+ = &
+ \left\{
+ \begin{array}{ll}
+ x & \mbox{if $b$ is true} \\
+ y & \mbox{otherwise}
+ \end{array}
+ \right.
+\end{eqnarray*}
+More formally, a
+boolean $b$ is a function which respects equality,
+such that for all $f$, $g$ and $z$:
+\begin{eqnarray*}
+ b~f~g~z & = & b~(f~z)~(g~z)
+\end{eqnarray*}
+and for all $f$ and $g$ which respect equality,
+\begin{eqnarray*}
+ b~(f~b)~(g~b) & = & b~(f~First)~(g~Second)
+\end{eqnarray*}
+All the functions in this section satisfy these properties. Surprisingly
+enough, so does $Error$, which is quite useful, as it allows us to
+reason about booleans which ``go wrong''.
+
+\subsection{True, False and Not}
+
+Since we are implementing booleans as functions, we already have the
+definitions of $True$, $False$ and $Not$.
+\begin{eqnarray*}
+ True & = & First \\
+ False & = & Second \\
+ Not & = & Twiddle
+\end{eqnarray*}
+So for free we get the following results:
+\begin{eqnarray*}
+ Not~True & = & False \\
+ Not~False & = & True \\
+ Compose~Not~Not & = & Identity
+\end{eqnarray*}
+The \TeX\ implementation is not exactly difficult:
+\begin{TeXcode}
+\let\True=\First
+\let\False=\Second
+\let\Not=\Twiddle
+\end{TeXcode}
+
+\subsection{And and Or}
+
+The definitions of $And$ and $Or$ are:
+\begin{eqnarray*}
+ And~a~b &
+ = &
+ \left\{
+ \begin{array}{ll}
+ b & \mbox{if $a$ is true} \\
+ False & \mbox{otherwise}
+ \end{array}
+ \right.
+ \\
+ Or~a~b &
+ = &
+ \left\{
+ \begin{array}{ll}
+ True & \mbox{if $a$ is true} \\
+ b & \mbox{otherwise}
+ \end{array}
+ \right.
+\end{eqnarray*}
+With our definition of what a boolean is, this is just the same as
+\begin{eqnarray*}
+ And~a~b & = & a~b~False \\
+ Or~a~b & = & a~True~b
+\end{eqnarray*}
+>From these conditions, we can show that $And$ is associative, and
+has left unit $True$ and left zeros $False$ and $Error$:
+\begin{eqnarray*}
+ And~(And~a~b)~c & = & And~a~(And~b~c) \\
+ And~True~b & = & b \\
+ And~False~b & = & False \\
+ And~Error~b & = & Error
+\end{eqnarray*}
+$Or$ is associative, has left unit $False$ and left zeros $True$ and $Error$:
+\begin{eqnarray*}
+ Or~(Or~a~b)~c & = & Or~a~(Or~b~c) \\
+ Or~False~b & = & b \\
+ Or~True~b & = & True \\
+ Or~Error~b & = & Error
+\end{eqnarray*}
+De~Morgan's laws hold:
+\begin{eqnarray*}
+ Not~(And~a~b) & = & Or~(Not~a)~(Not~b) \\
+ Not~(Or~a~b) & = & And~(Not~a)~(Not~b)
+\end{eqnarray*}
+and $And$ and $Or$ left-distribute through one another:
+\begin{eqnarray*}
+ Or~a~(And~b~c) & = & And~(Or~a~b)~(Or~a~c) \\
+ And~a~(Or~b~c) & = & Or~(And~a~b)~(And~a~c)
+\end{eqnarray*}
+$And$ and $Or$ are {\em not\/} commutative, though. For example,
+\begin{eqnarray*}
+ \start{Or~True~Error}
+ & = & True~True~Error \\
+ & = & True
+\end{eqnarray*}
+but
+\begin{eqnarray*}
+ \start{Or~Error~True}
+ & = & Error~True~True \\
+ & = & Error
+\end{eqnarray*}
+This is actually quite useful since there are some booleans that
+need to return an error occasionally. If $a$ is $True$ when $b$
+is safe (i.e.\ doesn't become $Error$) and is $False$ otherwise, we can
+say $Or~a~b$ and know we're not going to get an error. This is handy
+for things like checking for division by zero, or trying to get the
+first element of an empty list.
+
+Similarly, because of the possibility of $Error$,
+$And$ and $Or$ don't right-distribute through each other,
+as
+\begin{eqnarray*}
+ \start{Or~(And~False~Error)~True}
+ & \ne & And~(Or~False~True)~(Or~Error~True)
+\end{eqnarray*}
+As errors shouldn't crop up, this needn't worry us too much.
+\begin{TeXcode}
+\def\And#1#2{#1{#2}\False}
+\def\Or#1#2{#1\True{#2}}
+\end{TeXcode}
+
+\subsection{Lift}
+
+Quite a lot of the time we won't be dealing with booleans, but with
+{\em predicates}, which are just functions that return a boolean.
+For example, the predicate $Lessthan$ is defined below so that
+$Lessthan~i~j$ is true whenever $i<j$.
+Given a predicate $p$ we would like to be able to
+{\em lift\/} it to $Lift~p$, defined:
+\begin{eqnarray*}
+ Lift~p~f~g~x & = & p~x~f~g~x
+\end{eqnarray*}
+For example, $Lift~(Lessthan~0)~f~g$ takes in a number and applies
+$f$ to it if it is positive and $g$ to it otherwise. This is quite
+useful for defining functions.
+\begin{TeXcode}
+\def\Lift#1#2#3#4{#1{#4}{#2}{#3}{#4}}
+\end{TeXcode}
+
+\subsection{Lessthan and \TeX if}
+
+Finally, we would like to be able to use \TeX's built-in booleans
+as well as our own. For example, we would like a predicate
+$Lessthan$ such that:
+\begin{eqnarray*}
+ Lessthan~i~j &
+ = &
+ \left\{
+ \begin{array}{ll}
+ True & \mbox{if } i < j \\
+ False & \mbox{if } i \ge j \\
+ Error & \mbox{otherwise}
+ \end{array}
+ \right.
+\end{eqnarray*}
+The $Error$ condition happens if we try applying $Lessthan$ to something
+that isn't a number --- $Lessthan~True~False$ is $Error$%
+\footnote
+ {Actually, that's a little white lie --- trying to persuade \TeX\ to
+ do run-time type checking isn't much fun. So the \TeX\ implementation
+ of this is actually a {\em refinement\/} where the $Error$ condition
+ has been replaced by whatever it is \TeX\ does if you try doing
+ {\tt\string\ifnum $x$ < $y$} when $x$ and $y$ aren't numbers}.
+This is fine as a mathematical definition, but how will
+we implement it? If we assume we have a macro \verb|\TeXif|,
+which converts \TeX\ if-statements into booleans, we could just
+define:
+\begin{TeXcode}
+\def\Lessthan#1#2{\TeXif{\ifnum#1<#2 }}
+\end{TeXcode}
+So the question is just how to define \verb|\TeXif|.
+Unfortunately, the ``obvious'' code does not work:
+\begin{verbatim}
+\def\TeXif#1#2#3{#1#2\else#3\fi}
+\end{verbatim}
+For example, \verb|\TeXif\iftrue\True\True| doesn't expand out to
+\verb|\True|. Instead, it expands as:
+\begin{verbatim}
+\TeXif\iftrue\True\True
+ = \iftrue\True\else\True\fi
+ = \True\else\True\fi
+ = \else\fi
+ =
+\end{verbatim}
+Another common \TeX nique is to use a macro \verb|\next| to
+be the expansion text:
+\begin{verbatim}
+\def\TeXif#1#2#3%
+ {#1\def\next{#2}\else\def\next{#3}\fi
+ \next}
+\end{verbatim}
+However, this uses \TeX's stomach to do the \verb|\def|, and we are
+trying to do this using only the mouth. One (slightly tricky) solution
+is to use pattern-matching to gobble up the offending \verb|\else| and/or
+\verb|\fi|.
+\begin{TeXcode}
+\def\gobblefalse\else\gobbletrue\fi#1#2%
+ {\fi#1}
+\def\gobbletrue\fi#1#2%
+ {\fi#2}
+\def\TeXif#1%
+ {#1\gobblefalse\else\gobbletrue\fi}
+\end{TeXcode}
+So if the \TeX\ if-statement is true, \verb|\gobblefalse| gobbles
+up the false-text, otherwise \verb|\gobbletrue| gobbles up the
+true-text. For example,
+\begin{verbatim}
+\TeXif\iftrue\True\True
+ = \iftrue\gobblefalse\else
+ \gobbletrue\fi\True\True
+ = \gobblefalse\else
+ \gobbletrue\fi\True\True
+ = \fi\True
+ = \True
+\end{verbatim}
+Phew. And so we have booleans.
+
+\section{Lists}
+
+A list is a (possibly infinite) sequence of values. For example,
+the list $[1,2,3]$ contains three numbers, the list $\nil$ contains
+none, and the list $[1,2,3,\ldots]$ contains infinitely many.
+A list is either {\em empty\/} (written $\nil$) or is comprised
+of a {\em head\/}
+$x$ and a {\em tail\/} $xs$ (in which case it's written $x:xs$).
+For example, $1:2:3:\nil$ is $[1,2,3]$.
+
+In a similar fashion to the implementation of booleans,
+a list $xs$ is implemented as a function of the form
+\begin{eqnarray*}
+ xs~f~e &
+ = &
+ \left\{
+ \begin{array}{ll}
+ e & \mbox{if $xs$ is empty} \\
+ f~y~ys & \mbox{if $xs$ has head $y$ and tail $ys$}
+ \end{array}
+ \right.
+\end{eqnarray*}
+Again, we are implementing a datatype as a function, a quite powerful
+trick, just not one usually seen in \TeX. We will assume that
+whenever a list $x:xs$ is applied to $f$ and $e$, $f~x$ respects equality.
+This allows us to assume that if $xs = ys$ then $x:xs = x:ys$,
+which is handy.
+
+\subsection{Nil, Cons, Stream and Singleton}
+
+The simplest list is $Nil$, the empty list which we have been writing
+$\nil$.
+\begin{eqnarray*}
+ Nil & = & Second
+\end{eqnarray*}
+The other possible list is $Cons~x~xs$, which has head $x$ and tail $xs$.
+\begin{eqnarray*}
+ Cons~x~xs~f~e & = & f~x~xs
+\end{eqnarray*}
+Every list can be constructed using these functions.
+The list $[1,2,3]$ is $Cons~1~(Cons~2~(Cons~3~Nil))$, and the
+list $[a,a,a,\ldots]$ is $Stream~a$ where $Stream$ is defined:
+\begin{eqnarray*}
+ Stream~a & = & Cons~a~(Stream~a)
+\end{eqnarray*}
+There's even at least one application for infinite lists,
+as we'll see in Section~\ref{outputroutines}.
+
+The singleton list $[a]$ is $Singleton~a$, defined as:
+\begin{eqnarray*}
+ Singleton~a & = & Cons~a~Nil
+\end{eqnarray*}
+These all have straightforward \TeX\ definitions.
+\begin{TeXcode}
+\let\Nil=\Second
+\def\Cons#1#2#3#4{#3{#1}{#2}}
+\def\Stream#1{\Cons{#1}{\Stream{#1}}}
+\def\Singleton#1{\Cons{#1}\Nil}
+\end{TeXcode}
+
+\subsection{Head and Tail}
+
+So, we can construct any list we like, but we still can't get any information
+out of it. To begin with, we'd like to be able to get the head
+and tail of a list.
+\begin{eqnarray*}
+ Head~xs & = & xs~First~Error \\
+ Tail~xs & = & xs~Second~Error
+\end{eqnarray*}
+For example, the tail of $x:xs$ is
+\begin{eqnarray*}
+ \start{Tail~(Cons~x~xs)}
+ & = & Cons~x~xs~Second~Error \\
+ & = & Second~x~xs \\
+ & = & \Tail{\Cons{x}{xs}}
+\end{eqnarray*}
+The tail of $\nil$ is, as one would expect,
+\begin{eqnarray*}
+ \start{Tail~Nil}
+ & = & Nil~Second~Error \\
+ & = & Error
+\end{eqnarray*}
+And the head of $Stream~a$ is
+\begin{eqnarray*}
+ \start{Head~(Stream~a)}
+ & = & Stream~a~First~Error \\
+ & = & Cons~a~(Stream~a)~First~Error \\
+ & = & First~a~(Stream~a) \\
+ & = & \Head{\Stream{a}}
+\end{eqnarray*}
+So we can get the head of an infinite list in finite time. This is
+fortunate, as otherwise there wouldn't be much point in allowing
+infinite objects.
+\begin{TeXcode}
+\def\Head#1{#1\First\Error}
+\def\Tail#1{#1\Second\Error}
+\end{TeXcode}
+
+\subsection{Foldl and Foldr}
+
+Using $Head$ and $Tail$ we can get at the beginning of any non-empty list,
+but in general we need more information than that. Rather than write
+a whole bunch of recursive functions on lists, I'll implement two
+fairly general functions, with which we can implement (almost) everything
+else.
+
+$Foldl$ and $Foldr$ both take in functions and apply them recursively
+to a list. $Foldl$ starts at the left of the list, and $Foldr$
+starts at the right. For example,
+\begin{eqnarray*}
+ Foldl~f~e~[1,2,3] & = & f~(f~(f~e~1)~2)~3 \\
+ Foldr~f~e~[1,2,3] & = & f~1~(f~2~(f~3~e))
+\end{eqnarray*}
+These functions will be used a lot later on. $Foldl$ can be defined:
+\begin{eqnarray*}
+ Foldl~f~e~xs & = & xs~(Foldl'~f~e)~e \\
+ Foldl'~f~e~x~xs & = & Foldl~f~(f~e~x)~xs
+\end{eqnarray*}
+So $Foldl~f~e~\nil$ is
+\begin{eqnarray*}
+ \start{Foldl~f~e~Nil}
+ & = & Nil~(Foldl'~f~e)~e \\
+ & = & \Foldl{f}{e}\Nil
+\end{eqnarray*}
+And $Foldl~f~e~(x:xs)$ is
+\begin{eqnarray*}
+ \start{Foldl~f~e~(Cons~x~xs)}
+ & = & Cons~x~xs~(Foldl'~f~e)~e \\
+ & = & Foldl'~f~e~x~xs \\
+ & = & Foldl~f~(f~e~x)~xs
+\end{eqnarray*}
+For example, $Foldl~f~e~[1,2,3]$ is
+\begin{eqnarray*}
+ \start{Foldl~f~e~[1,2,3]}
+ & = & Foldl~f~(f~e~1)~[2,3] \\
+ & = & Foldl~f~(f~(f~e~1)~2)~[3] \\
+ & = & Foldl~f~(f~(f~(f~e~1)~2)~3)~\nil \\
+ & = & f~(f~(f~e~1)~2)~3
+\end{eqnarray*}
+as promised. Similarly, we can define $Foldr$ as
+\begin{eqnarray*}
+ Foldr~f~e~xs & = & xs~(Foldr'~f~e)~e \\
+ Foldr'~f~e~x~xs & = & f~x~(Foldr~f~e~xs)
+\end{eqnarray*}
+For $Foldr~f$ to respect equality, $f~x$ should respect equality.
+
+When we do the unfolding, we discover that
+\begin{eqnarray*}
+ Foldr~f~e~\nil & = & e \\
+ Foldr~f~e~(x:xs) & = & f~e~(Foldr~f~e~xs)
+\end{eqnarray*}
+$Foldr$ tends to be more efficient than $Foldl$, because $Foldl$
+has to run along the entire list before it can start applying $f$,
+whereas $Foldr$ can apply $f$ straight away. If $f$ is a lazy function,
+this can make quite a difference. $Foldl$ on infinite lists, anyone?
+\begin{TeXcode}
+\def\Foldl#1#2#3%
+ {#3{\Foldl@{#1}{#2}}{#2}}
+\def\Foldl@#1#2#3#4%
+ {\Foldl{#1}{#1{#2}{#3}}{#4}}
+\def\Foldr#1#2#3%
+ {#3{\Foldr@{#1}{#2}}{#2}}
+\def\Foldr@#1#2#3#4%
+ {#1{#3}{\Foldr{#1}{#2}{#4}}}
+\end{TeXcode}
+
+\subsection{Cat}
+
+Given two lists, we would like to be able to stick them together,
+which is what $Cat$ (short for ``concatenate'')
+does. For example, $Cat~[1,2]~[3,4]$ is
+$[1,2,3,4]$. It can be defined using $Foldr$:
+\begin{eqnarray*}
+ Cat~xs~ys & = & Foldr~Cons~ys~xs
+\end{eqnarray*}
+So
+\begin{eqnarray*}
+ \start{Cat~[1,2]~[3,4]}
+ & = & Foldr~Cons~[3,4]~[1,2] \\
+ & = & Cons~1~(Foldr~Cons~[3,4]~[2]) \\
+ & = & Cons~1~(Cons~2~(Foldr~Cons~[3,4]~\nil)) \\
+ & = & Cons~1~(Cons~2~[3,4]) \\
+ & = & \Unlistize{\Cat{\Listize[1,2]}{\Listize[3,4]}}
+\end{eqnarray*}
+The \TeX\ code for \verb|\Cat| is suspiciously similar to its mathematical
+definition.
+\begin{TeXcode}
+\def\Cat#1#2{\Foldr\Cons{#2}{#1}}
+\end{TeXcode}
+
+\subsection{Reverse}
+
+We can reverse any list with the function $Reverse$, defined using
+$Foldl$:
+\begin{eqnarray*}
+ Reverse & = & Foldl~(Twiddle~Cons)~Nil
+\end{eqnarray*}
+For example, $Reverse~[1,2,3]$ can be calculated:
+\begin{eqnarray*}
+ \start{Reverse~[1,2,3]}
+ & = & Foldl~(Twiddle~Cons)~Nil~[1,2,3] \\
+ & = & Twiddle~Cons \\
+ & & \quad (Twiddle~Cons~(Twiddle~Cons~Nil~1)~2)~3 \\
+ & = & Cons~3~(Cons~2~(Cons~1~Nil)) \\
+ & = & \Show\Reverse[1,2,3]
+\end{eqnarray*}
+The \TeX\ code for \verb|\Reverse| doesn't even take in any parameters.
+\begin{TeXcode}
+\def\Reverse{\Foldl{\Twiddle\Cons}\Nil}
+\end{TeXcode}
+
+\subsection{All, Some and Isempty}
+
+Given a predicate $p$, we can find out if all the elements of
+a list satisfy $p$ with $All~p$. Similarly we can find if something
+in the list satisfies $p$ with $Some~p$. For example,
+\begin{eqnarray*}
+ All~(Lessthan~1)~[1,2,3]
+ & = & \All{\Lessthan 1}{\Listize[1,2,3]}{True}{False} \\
+ Some~(Lessthan~1)~[1,2,3]
+ & = & \Some{\Lessthan 1}{\Listize[1,2,3]}{True}{False}
+\end{eqnarray*}
+These can be defined
+\begin{eqnarray*}
+ All~p & = & Foldr~(Compose~And~p)~True \\
+ Some~p & = & Foldr~(Compose~Or~p)~False
+\end{eqnarray*}
+For example, $Isempty$ can be defined
+\begin{eqnarray*}
+ Isempty & = & All~(First~False)
+\end{eqnarray*}
+This is probably not the most efficient check in the world, but we
+hardly ever need it --- $Foldl$ or $Foldr$ will normally do the job.
+\begin{TeXcode}
+\def\All#1{\Foldr{\Compose\And{#1}}\True}
+\def\Some#1{\Foldr{\Compose\Or{#1}}\False}
+\def\Isempty{\All{\First\False}}
+\end{TeXcode}
+
+\subsection{Filter}
+
+$Filter$ takes a predicate $p$ and a list $xs$, and returns a list
+containing only those elements of $xs$ that satisfy $p$. For example,
+\begin{eqnarray*}
+ Filter~(Lessthan~1)~[1,2,3] & = & \Show\Filter{\Lessthan 1}[1,2,3]
+\end{eqnarray*}
+$Filter$ can be defined as a $Foldr$:
+\begin{eqnarray*}
+ Filter~p & = & Foldr~(Lift~p~Cons~Second)~Nil
+\end{eqnarray*}
+Another easy bit of \TeX:
+\begin{TeXcode}
+\def\Filter#1%
+ {\Foldr{\Lift{#1}\Cons\Second}\Nil}
+\end{TeXcode}
+
+\subsection{Map}
+
+$Map$ takes a function $f$ and a list $xs$ and applies $f$ to every
+element of $xs$. For example,
+\begin{eqnarray*}
+ Map~f~[1,2,3] & = & \Show\Map{f~}[1,2,3]
+\end{eqnarray*}
+This is another job for $Foldr$.
+\begin{eqnarray*}
+ Map~f & = & Foldr~(Compose~Cons~f)~Nil
+\end{eqnarray*}
+We shall see $Map$ used later on, to convert from a list of
+names such as \Show\Map{\Compose\mbox\tt}[Fac-yawn,Fac-cows], to a list of
+labels such as \By[Fac-yawn,Fac-cows].
+\begin{TeXcode}
+\def\Map#1{\Foldr{\Compose\Cons{#1}}\Nil}
+\end{TeXcode}
+
+\subsection{Insert}
+
+The only function we need which isn't easily defined as a reduction
+is $Insert$, which inserts an element into a sorted list. For example,
+\begin{eqnarray*}
+ Insert~Lessthan~3~[1,2,4,5] & = & \Show\Insert\Lessthan3[1,2,4,5]
+\end{eqnarray*}
+$Insert$ takes in an ordering as its first parameter, so we're not stuck
+with one particular order. It is defined directly in terms of the
+definition of lists.
+\begin{eqnarray*}
+ Insert~o~x~xs & = & xs~(Insert'~o~x)~(Singleton~x) \\
+ Insert'~o~x~y~ys & = & o~x~y \\
+ & & \quad (Cons~x~(Cons~y~ys)) \\
+ & & \quad (Cons~y~(Insert~o~x~ys))
+\end{eqnarray*}
+We can then define the function all this has been leading up to,
+$Insertsort$ which takes an ordering and a list, and insert-sorts the
+list according to the ordering. For example,
+\begin{eqnarray*}
+ Insertsort~Lessthan~[2,3,1,2] & = & \Show\Insertsort\Lessthan[2,3,1,2]
+\end{eqnarray*}
+We can implement this as a fold:
+\begin{eqnarray*}
+ Insertsort~o & = & Foldr~(Insert~o)~Nil
+\end{eqnarray*}
+And so we've got sorted lists.
+\begin{TeXcode}
+\def\Insert#1#2#3%
+ {#3{\Insert@{#1}{#2}}{\Singleton{#2}}}
+\def\Insert@#1#2#3#4%
+ {#1{#2}{#3}%
+ {\Cons{#2}{\Cons{#3}{#4}}}%
+ {\Cons{#3}{\Insert{#1}{#2}{#4}}}}
+\def\Insertsort#1{\Foldr{\Insert{#1}}\Nil}
+\end{TeXcode}
+Interestingly, as we have implemented unbounded lists in \TeX's mouth,
+this means we can implement a Turing Machine. So, if you believe
+the Church-Turing thesis, \TeX's mouth is as powerful as any
+computer anywhere. Isn't that good to know?
+
+\section{Sorting reference lists}
+\label{thissection}
+
+So, these are the macros I've got to play with --- how do we apply them to
+sorting lists of references? Well, I'm using \LaTeX, which keeps the
+current reference in a macro called \verb|\@currentlabel|, which
+is~\ref{thissection} at the moment, as this is Section~\ref{thissection}.
+So I just need to store the value of \verb|\@currentlabel| somehow.
+
+Fortunately, I'm only ever going to be making references to facts
+earlier on in the document, in order to make sure I'm not proving
+any results in terms of themselves. So I don't need to play around
+with auxiliary files, and can just do everything in terms of
+macros.
+
+\subsection{Number and Label}
+
+Each label in the document is given a unique number, in the order
+the labels were put down. So the number of \verb|Fac-cows|
+is \verb|\Number{Fac-cows}|, which expands out to~\Number{Fac-cows},
+the number of \verb|Fac-people| is~\Number{Fac-people}, and so on.
+
+Each number has an associated label with it. For example,
+the first label is \verb|\Label{1}|, which is~\Label{1},
+the second label is~\Label{2} and so on. So to find the label for
+\verb|Fac-cows|, we say \verb|\Label{\Number{Fac-cows}}| which expands
+out to~\Label{\Number{Fac-cows}}.
+
+These numbers and labels are kept track of in macros. For example,
+the number of \verb|Fac-cows| is kept in \cstok{Number-Fac-cows}.
+Similarly, the first label is kept in \cstok{Label-1}.
+As these macros have dashes in their names, they aren't likely to
+be used already.
+
+So the \TeX\ code for \verb|\Number| and \verb|\Label| is pretty
+simple.
+\begin{verbatim}
+\def\Number#1{\csname Number-#1\endcsname}
+\def\Label#1{\csname Label-#1\endcsname}
+\end{verbatim}
+
+\subsection{Lastnum and Forward}
+
+The number of the most recent label is kept in \verb|\Lastnum|.
+\begin{verbatim}
+\newcount\Lastnum
+\end{verbatim}
+To put down a label \verb|Foo|, I type \verb|\Forward{Foo}|.
+\Forward{Foo}
+This increments the counter
+\verb|\Lastnum|, and \verb|\xdef|s \cstok{Number-Foo}
+to be the value of
+\verb|\Lastnum|, which is now~\the\Lastnum. So
+\verb|\Number{Foo}| now expands to~\Number{Foo}.
+Similarly, it \verb|\xdef|s \cstok{Label-\Number{Foo}} to be
+\verb|\@currentlabel|, which is currently~\Label{\Number{Foo}}.
+So \verb|\Label{\Number{Foo}}| now expands to~\Label{\Number{Foo}}.
+\begin{verbatim}
+\def\Forward#1%
+ {\global\advance\Lastnum by 1
+ \csnameafter\xdef{Number-#1}%
+ {\the\Lastnum}%
+ \csnameafter\xdef{Label-\the\Lastnum}%
+ {\@currentlabel}}
+\end{verbatim}
+This uses \verb|\csnameafter\foo{bar}|, which expands out to
+\verb|\foo\bar|.
+\begin{verbatim}
+\def\csnameafter#1#2%
+ {\expandafter#1\csname#2\endcsname}
+\end{verbatim}
+
+\subsection{Listize, Unlistize and Show}
+
+At the moment, lists have to be built up using \verb|\Cons| and
+\verb|\Nil|, which is rather annoying. Similarly, we can't actually
+do anything with a list once we've built it. We'd like some way
+of converting lists in the form \verb|[a,b,c]| to and from the
+form $[a,b,c]$. This is done with \verb|\Listize| and \verb|\Unlistize|.
+So \verb|\Listize[a,b,c]| expands to
+\begin{verbatim}
+\Cons{a}{\Cons{b}{\Cons{c}{\Nil}}}
+\end{verbatim}
+Similarly, \verb|\Unlistize| takes the list $[a,b,c]$ and expands out
+to \verb|[a, b, c]|. \verb|\Unlistize| is done with a $Foldr$.
+\begin{TeXcode}
+\def\Unlistize#1{[#1\Unlistize@{}]}
+\def\Unlistize@#1{#1\Foldr\Commaize{}}
+\def\Commaize#1#2{, #1#2}
+\end{TeXcode}
+The macro \verb|\Listize| is just a \TeX\ hack with pattern matching.
+It would have been nice to use \verb|\@ifnextchar| for this, but
+that uses \verb|\futurelet|, which doesn't expand in the mouth. Oh well.
+\begin{TeXcode}
+\def\Listize[#1]%
+ {\Listize@[#1,\relax]}
+\def\Listize@#1,#2]%
+ {\TeXif{\ifx\relax#2}%
+ {\Singleton{#1}}%
+ {\Cons{#1}{\Listize@#2]}}
+\end{TeXcode}
+This only works for nonempty lists --- \verb|\Listize[]| produces the
+singleton list \verb|\Singleton{}|. It also uses \verb|\relax| as its
+end-of-list character, so lists with \verb|\relax| in them have to
+be done by hand. You can't win them all. So
+\begin{verbatim}
+$\Unlistize{\Listize[a,b,c]}$
+\end{verbatim}
+produces
+$\Unlistize{\Listize[a,b,c]}$. This is such a common construction
+that I've defined a macro \verb|\Show| such that
+\verb|\Show\foo[a,b,c]| expands out to
+\begin{verbatim}
+\Unlistize{\foo{\Listize[a,b,c]}}
+\end{verbatim}
+For example, the equation
+\begin{eqnarray*}
+ Filter\,(Lessthan\,1)\,[1,2,3]
+ &=& \Show\Filter{\Lessthan 1}[1,2,3]
+\end{eqnarray*}
+was generated with
+\begin{verbatim}
+\begin{eqnarray*}
+ Filter\,(Lessthan\,1)\,[1,2,3]
+ &=& \Show\Filter{\Lessthan 1}[1,2,3]
+\end{eqnarray*}
+\end{verbatim}
+Many of the examples in this article were typeset this way.
+\begin{TeXcode}
+\def\Show#1[#2]%
+ {\Unlistize{#1{\Listize[#2]}}}
+\end{TeXcode}
+
+\subsection{By}
+
+Given these macros, we can now sort any list of references with $Bylist$,
+defined
+\begin{eqnarray*}
+ Bylist~xs & = & Map~Label \\
+ & & \quad (Insertsort~Lessthan \\
+ & & \quad\quad (Map~Number~xs))
+\end{eqnarray*}
+This takes in a list of label names like \verb|Fac-yawn|,
+converts it into a list of numbers with $Map~Number$,
+sorts the resulting list with $Insertsort~Lessthan$,
+and finally converts all the numbers into labels like
+\Label{\Number{Fac-yawn}} with $Map~Label$. For example,
+\begin{eqnarray*}
+ \start{Bylist~\Show\Map{\Compose\mbox\tt}[Fac-yawn,Fac-cows]}
+ & = & Map~Label~(Insertsort~Lessthan \\
+ & & \quad (Map~Number~
+ \Show\Map{\Compose\mbox\tt}[Fac-yawn,Fac-cows])) \\
+ & = & Map~Label~(Insertsort~Lessthan~
+ \Show\Map\Number[Fac-yawn,Fac-cows]) \\
+ & = & Map~Label~\Show\Compose{\Insertsort\Lessthan}{\Map\Number}
+ [Fac-yawn,Fac-cows] \\
+ & = & \Show\Bylist[Fac-yawn,Fac-cows]
+\end{eqnarray*}
+The \TeX\ code for this is
+\begin{verbatim}
+\def\Bylist#1%
+ {\Map\Label
+ {\Insertsort\Lessthan
+ {\Map\Number{#1}}}}
+\end{verbatim}
+So we can now stick all this together, and define the macro \verb|\By|
+that prints out lists of references. It is
+\begin{verbatim}
+\def\By{\Show\Bylist}
+\end{verbatim}
+So \verb|\By[Fac-yawn,Fac-cows]| is~\By[Fac-yawn,Fac-cows].
+Which is quite nice.
+
+\section{Other applications}
+\label{outputroutines}
+
+Is all this worth it? Well, I've managed to get my lists of facts in
+order, but that's not the world's most astonishing application.
+There are other things that these lists are useful for, though.
+
+For example, Damian Cugley has a macro package under development for
+laying out magazines. {\sc Mag}\TeX's output routine needs to be quite
+smart, as magazines often have gaps where illustrations or photographs
+are going to live. In general, each block of text needs to be output
+in a different fashion from every other block of text.
+This will be handled by keeping an infinite list of output
+routines. Each time a box is cut off the scroll to be output,
+the head of the list is chopped off and is used as the output routine
+for that box. That way, quite complex page shapes can be built up.
+
+Mainly, though, these macros were written just as a challenge.
+I learned quite a lot about \TeX\ and needed some \TeX niques I'd
+never seen before. It was also quite pleasing to see that \TeX\ code
+can be formally verified, albeit in a rather noddy way. Without
+some sort of abstract view of lists, these \TeX\ macros could
+not have been written.
+
+\section{Acknowledgements}
+
+Thanks to Jeremy Gibbons for letting me bounce ideas off him
+and spotting the duff ones,
+to Damian Cugley for saying ``Do you really think \TeX\ is meant
+to do this?'', and to the Problem Solving Club for hearing me out.
+This work was sponsored by the Science and Engineering
+Research Council and Hewlett Packard.
+
+\makesignature
+
+\end{document}
+