summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/skak/lambda.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/latex/skak/lambda.tex')
-rw-r--r--Master/texmf-dist/doc/latex/skak/lambda.tex1146
1 files changed, 0 insertions, 1146 deletions
diff --git a/Master/texmf-dist/doc/latex/skak/lambda.tex b/Master/texmf-dist/doc/latex/skak/lambda.tex
deleted file mode 100644
index 5285e9a5104..00000000000
--- a/Master/texmf-dist/doc/latex/skak/lambda.tex
+++ /dev/null
@@ -1,1146 +0,0 @@
-% Filename: Lambda.tex
-% Author: Alan Jeffrey
-% Last modified: 11 May 1990
-%
-% 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
-%
-
-\documentstyle[ltugboat,Lambda]{article}
-
-% 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}
-
-\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}
-