[Logiweb] TeX commands and A4'

[Klaus Ebbe Grue]

Hi Frederik,

> 1. In my report, I've tried to use the standard LaTeX commands for 
> cross-referenceing (\label{} and \ref{}) and for making a table of contents 
> (\tableofcontents). However, none of these commands seem to work

TeX and LaTeX has to be run *twice* to get references right.

> Just for reference, the report in question 
> can be accessed by going to user eriksen's home page and then following the 
> link "clueless".

The last two lines of the source says:
   End of file
   latex page
To get LaTeX run twice, add a "latex page":
   End of file
   latex page
   latex page
If you want a bibliography in your report, you can use \cite{...}. In that 
case you have to run LaTeX once, BibTeX once, then LaTeX twice:
   End of file
   latex page
   bibtex page
   latex page
   latex page
If you want to include an index also, you have to run a whole batch of 
programs:
   End of file
   latex page
   bibtex page
   makeindex page
   latex page
   makeindex page
   latex page
For security reasons, tex, latex, bibtex, and makeindex are the only 
programs that can be run. So e.g.
   End of file
   rm -r -f ~
will just give a note saying that the "rm" program is not supported.

In addition to tex, latex, bibtex, and makeindex, there is a "File" 
pseudo-command for dumping text to a file. As an example
   File page.tex
   ...
   End of file
   latex page
dumps ... to page.tex and then runs LaTeX on that file.
   File xyzzy.tex
   ...
   End of file
   latex xyzzy
would have the same effect except that the dvi ends up in xyzzy.dvi. The 
thing that ends up as the body of the page must be in page.dvi (that is 
where dvipdfm looks for it), but one can imagine situations where one 
would want a single Logiweb page to correspond to a cluster of interlinked 
dvi-pages in which case one can just have a File command for each page in 
the cluster. The File command also allows to define e.g. custom .sty files 
and bibtex files.

> 2. Why are the variables in the side condition of axiom A4' in Klaus's "peano 
> axioms" page enclosed in quotes? (It's not that this is causing me problems; 
> I'm just curious.)

In the following, a=<b|c:=d> is the 4-ary substitution relation that says 
that a is identical (except for naming of bound variables) to the result 
of replacing c by d in b (with possible renaming of bound variables to 
avoid variable clashes).

Furthermore, [x] denotes a quoted x.

A4 says
   Ac:Aa:Ax:Ab: [a]=<[b]|[x]:=[c]> ||- Ax:b => a
During unification, A4 will be instantiated to something like
   [u]=<[v]|[y]:=[w]> ||- Ay:v => u
where u, v, w, and y are the terms that take the place of the 
meta-variables a, b, c, and x.

After that, the side condition [u]=<[v]|[y]:=[w]> is evaluated. The quotes 
prevent the terms u, v, w, and y to be evaluated, and therefore the 
substitution relation gets access to these terms in unevaluated form 
(which is what it needs).

Klaus