{ Logiweb, a system for electronic distribution of mathematics Copyright (C) 2004 Klaus Grue This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 USA Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen, Denmark, grue@diku.dk, http://yoa.dk/, http://www.diku.dk/~grue/ Logiweb is a system for distribution of mathematical definitions, lemmas, and proofs. For more on Logiweb, consult http://yoa.dk/. } {See the pyk source of the 'base' page for explanations of the format of the present file} PAGE check BIBLIOGRAPHY base: "http:base/latest/vector/page.lgw" PREASSOCIATIVE base: bracket * end bracket, propositional calculus, propositional a one, propositional a two, propositional a three, propositional modus ponens, propositional identity PREASSOCIATIVE base: * sub * end sub, * factorial PREASSOCIATIVE base: unicode start of text * end unicode text PREASSOCIATIVE base: * apply * PREASSOCIATIVE base: * times * PREASSOCIATIVE base: * plus * PREASSOCIATIVE base: * term plus * end plus POSTASSOCIATIVE base: * raw pair * POSTASSOCIATIVE base: * comma * PREASSOCIATIVE base: * boolean equal * PREASSOCIATIVE base: not * PREASSOCIATIVE base: * and * PREASSOCIATIVE base: * or * POSTASSOCIATIVE base: * macro imply *, * imply * POSTASSOCIATIVE base: * guard * PREASSOCIATIVE base: * select * else * end select PREASSOCIATIVE base: lambda * dot * PREASSOCIATIVE base: * init PREASSOCIATIVE base: * at * POSTASSOCIATIVE base: * infer * PREASSOCIATIVE base: all * indeed * POSTASSOCIATIVE base: * rule plus * POSTASSOCIATIVE base: * cut * PREASSOCIATIVE base: * proves * PREASSOCIATIVE base: locally define * as * end line * POSTASSOCIATIVE base: * then * PREASSOCIATIVE base: * tab * PREASSOCIATIVE base: * row * BODY "File page.tex \documentclass [fleqn]{article} % Make \rm the default font in math mode. This makes rendering of strings % easier and TeX source for rendering of strings easier to read. % Furthermore, \rm is the default font in all pages generated from scratch % by Logiweb so the body of a page (the thing defined from 'BODY' above to % the end of the present file) should also declare \rm to be the default % font to ensure that all constructs are rendered consistently on all pages. \everymath{\rm} % Include latexsym to make symbols like \rhd available. The line below % also occurs on automatically generated pages so that one can use % e.g. \rhd in the tex and tex name aspects of symbols. \usepackage{latexsym} % Enable use of hyperlinks. The lines below also occur on automatically % generated pages, possibly with other values for parameters. \usepackage[dvipdfm=true]{hyperref} \hypersetup{pdfpagemode=none} \hypersetup{pdfstartpage=1} \hypersetup{pdfstartview=FitBH} \hypersetup{pdfpagescrop={120 130 490 730}} \hypersetup{pdftitle=Introduction to Logiweb} \hypersetup{colorlinks=true} % The following definitions affect the TeX rendering of the body of % a page (the TeX rendering includes the dvi and pdf versions). The % definitions also affect the TeX rendering of the macro expanded % version of the body. % % One should not refer to the definitions below from the tex % and tex name aspects of Logiweb symbols since those aspects are % also used by Logiweb for generating documents like the bibliography, % dictionary, and codex of a page, and the defintions below are not % available when generating those documents. % % One could think of more flexible ways of generating TeX source. But % the long term goal is to port TeX to the Logiweb programming language % and avoid generating TeX source alltogether. % % Unfortunately, I have violated the rules above myself until I find % a better solution. But when I violate the rules I only do so in tex % aspects and always ensure there is an associated tex name aspect in % which the rules are not violated. And I never use constructs that % violate the rules in the right hand side of definitions. That makes % things work tolerably. % Ensure that overfull paragraphs are marked \setlength {\overfullrule }{1mm} % Include Logiweb-generated file that defines something like the following. % \gdef\today{GRD-2005-06-30.UTC:06:41:25.303814} % \gdef\lgwlgt{LGT-4626830517303814e-6} % \gdef\lgwmjdtai{MJD-53551.TAI:06:41:57.303814} % \gdef\lgwgrdutc{GRD-2005-06-30.UTC:06:41:25.303814} % \gdef\lgwmantissa{4626830517303814} % \gdef\lgwexponent{6} % \gdef\lgwfraction{303814} % \gdef\lgwsecond{25} % \gdef\lgwminute{41} % \gdef\lgwhour{06} % \gdef\lgwday{30} % \gdef\lgwmonth{06} % \gdef\lgwyear{2005} % % In addition, the file defines something like the following for each % bibliographic entry (including reference zero: the page itself). % % \gdef\lgwMapKana{nani ...} % \gdef\lgwMapHex{01 ...} % \gdef\lgwMapDec{001 ...} % \gdef\lgwMapUrl{http://ydun.yoa.dk/logiweb/server/relay/go/01...} % % A reference to a page with name 'my page' gives rise to definitons of % \lgwMyPageKana, \lgwMyPageHex, \lgwMyPageDec, and \lgwMyPageUrl. \input{lgwinclude} % Prepare for making an index. % % The page.sty included below is defined later in the present source. % % The \intro and \indexintro commands support a style where introduced % concepts are put in italics and entered in the index. % % The \back command is used when maintaining a visually straight left % margin in which formulas start at the left margin but the initial left % bracket of formulas is placed in the margin. This is used in the index. \usepackage{makeidx} \usepackage{page} \makeindex \newcommand{\intro}[1]{\emph{#1}} \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} \newlength{\bracketwidth} \settowidth{\bracketwidth}{$[{}$} \newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}} % Prepare for making a bibliography \bibliographystyle{plain} % \tex{foo} writes foo to page.otx for later inclusion % \test{foo} writes foo to page.tst for later inclusion \newtoks\toktex \newwrite\outex \newwrite\outest \immediate\openout\outex=page.otx \immediate\openout\outest=page.tst \newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}} \newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}} % Save current \parindent. \newlength{\docparindent} \setlength{\docparindent}{\parindent} % To be included after each \section, \subsection, etc. \newcommand{\sect}[1]{\label{section:#1}\setlength{\parindent}{\docparindent}} % The document itself \begin {document} \title {Introduction to Logiweb} \author {Klaus Grue} \maketitle \tableofcontents "[ ragged right expansion ]" \section{Introduction}\sect{Introduction} Logiweb \cite{logiweb} is a system for distribution of mathematical definitions, lemmas, and proofs. More precisely, the Logiweb standard comprises a format, a semantics, and a protocol for storage, interpretation, and transmission of formal mathematics. A ``clean'' implementation of Logiweb comprises a Logiweb server, a Logiweb client, and an authoring tool. The Logiweb standard governs the server, the client, and the backend of the authoring tool. Logiweb allows a user to submit Logiweb pages that contain formal formal mathematics. To submit a page, the user must first produce the page using the authoring tool and then make the page available on the ordinary World Wide Web (WWW) under some Hyper Text Transport Protocal Uniform Resource Locator (http URL). Then the authoring tool must notify the nearest Logiweb server about the submission. Each Logiweb page has a Logiweb reference which essentially is a global hash key computed on the basis of the contents of the page. Logiweb pages are addressed using Logiweb references but retrieved from WWW using their http URL. The main task of the mesh of Logiweb servers is to translate Logiweb references to http URLs. A single Logiweb server cannot do the translation from Logiweb reference to http URL alone. Rather, the Logiweb servers form a mesh that cooperate on indexing all Logiweb pages in the world. \subsection{References}\sect{References} The reference of the present page is "[ display "{\tt\lgwCheckHex}" end display ]" when expressed in \indexintro{mixed endian hexadecimal}. ``Mixed endian'' indicates that the reference is written in network byte order but each byte is written with the most significant digit first as in dot-notation for ip-addresses. When written in mixed endian Kana, the reference of the present page reads "[ display "{\tt\lgwCheckKana}" end display ]" In the Kana notation, ``n'', ``t'', ``s'', ``k'' represent 00, 01, 10, and 11, respectively. Also, ``a'', ``i'', ``u'', ``e'' represent 00, 01, 10, and 11, respectively. So ``11000100 11000000'' translates to ``kata kana'' and ``00 01 10 11 11 10 01 00'' translates to ``nise kuta''. The Kana format is useful if one has to pronounce a reference. \subsection{Bibliographies}\sect{Bibliographies} Each Logiweb page contains a bibliography which is a list of references to other Logiweb pages. As an example the present page references a page named \href {\lgwBaseUrl}{base}. As mentioned, the reference of a page depends on the contents of the page and one cannot change a page without affecting its reference. For that reason, an author of a Logiweb page can safely refer to another Logiweb page without fearing that that other page will change. Furthermore, if an author references a Logiweb page, then the author may copy and resubmit that page and in that way ensure that the referenced Logiweb page will not disappear from Logiweb. The \href {\lgwBaseUrl}{base} page referenced by the present page contains loads of definitions of computing machinery, macro expansion machinery, proof checking machinery, and many other things. The present page states a proof that has been machine checked by Logiweb plus a some other examples of the merits of Logiweb. \subsection{Programming}\sect{Programming} Logiweb supports programming. As an example,% % \test{"[ math test zero factorial tagged equal one end test end math ]"}% % \test{"[ math test one factorial tagged equal one end test end math ]"}% % \test{"[ math test two factorial tagged equal two end test end math ]"}% % "[ display math value define var n factorial as open if var n tagged equal zero then one else var n times parenthesis var n minus one end parenthesis factorial end define end math intro var n factorial pyk "* factorial" tex "#1."n\char33" end intro end display ]" The footnote of the definition above states what one should type on a keyboard or say in a microphone to enter the factorial function. Appendix \ref{section:TexDefinitions} states how Logiweb should render the factorial function using \TeX. Enclosing formulas in brackets is a stylistic choice of the author, not something enforced by Logiweb. \subsection{Evaluation}\sect{Evaluation} Logiweb supports evaluation, compilation, and test of programs. As an example, "[ display math test three factorial tagged equal six end test end math end display ]" tests that "[ bracket three factorial end bracket ]" evaluates to "[ bracket six end bracket ]". Logiweb has checked the test case above as can be seen from the ``After verifying: The page is correct'' in the Logiweb main menu of the present page (The name of the present page is ``check'' for historical reasons). For further test cases see Section \ref{section:Test}. \subsection{Theories}\sect{Theories} Logiweb supports formal mathematics. As an example, propositional calculus "[ bracket propositional calculus end bracket ]" as defined in \cite{mendelson} reads: "[ display math theory propositional calculus end theory end math intro propositional calculus index "L" pyk "propositional calculus" tex ""nL" end intro end display ]" "[ display math in theory propositional calculus rule propositional a one says all meta a indeed all meta b indeed meta a imply meta b imply meta a end rule end math intro propositional a one index "A1" pyk "propositional a one" tex ""nA1" end intro end display ]" "[ display math in theory propositional calculus rule propositional a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a imply meta b imply meta c end parenthesis imply parenthesis meta a imply meta b end parenthesis imply meta a imply meta c end rule end math intro propositional a two index "A2" pyk "propositional a two" tex ""nA2" end intro end display ]" "[ display math in theory propositional calculus rule propositional a three says all meta a indeed all meta b indeed parenthesis not meta b imply not meta a end parenthesis imply parenthesis not meta b imply meta a end parenthesis imply meta b end rule end math intro propositional a three index "A3" pyk "propositional a three" tex ""nA3" end intro end display ]" "[ display math in theory propositional calculus rule propositional modus ponens says all meta a indeed all meta b indeed meta a infer meta a imply meta b infer meta b end rule end math intro propositional modus ponens index "MP" pyk "propositional modus ponens" tex ""nMP" end intro end display ]" The construct "[ bracket var x imply var y end bracket intro var x imply var y pyk "* imply *" tex "#1."n\Rightarrow #2." end intro ]" is post-associative (i.e.\ right associative in text that runs left to right, c.f.\ Appendix \ref{section:PriorityTable}). The construct "[ bracket not var x end bracket ]" is introduced on the \href {\lgwBaseUrl}{base} page and has higher associativity than "[ bracket var x imply var y end bracket ]". Parentheses "[ bracket parenthesis var x end parenthesis end bracket ]" are macro defined on the \href {\lgwBaseUrl}{base} page. Parentheses affect the structure of parse trees but are macro expanded away before e.g.\ the proof checker sees the terms they occur in. \subsection{Proof checking}\sect{Proof checking} Logiweb supports proof checking. As an example, Lemma "[ bracket propositional identity end bracket ]" below says that "[ bracket meta a imply meta a end bracket ]" holds for all terms "[ bracket meta a end bracket ]" in propositional calculus: "[ display math in theory propositional calculus lemma propositional identity says all meta a indeed meta a imply meta a end lemma end math intro propositional identity index "I" pyk "propositional identity" tex ""nI" end intro end display ]" We have chosen to render meta-quantification as "[ bracket all meta a indeed meta b end bracket ]". When formalizing first order predicate calculus which has an object-quantifier, it may be more convenient to pick another name for the meta-quantifier. That is possible to do since Logiweb offers complete notational freedom. A proof of the statement above could read: "[ statement math propositional calculus proof of propositional identity reads arbitrary meta a end line line ell a because propositional a one indeed meta a imply parenthesis meta a imply meta a end parenthesis imply meta a end line line ell b because propositional a one indeed meta a imply meta a imply meta a end line line ell c because propositional a two indeed parenthesis meta a imply parenthesis meta a imply meta a end parenthesis imply meta a end parenthesis imply macro newline parenthesis meta a imply meta a imply meta a end parenthesis imply parenthesis meta a imply meta a end parenthesis end line line ell d because propositional modus ponens modus ponens ell a modus ponens ell c indeed parenthesis meta a imply meta a imply meta a end parenthesis imply parenthesis meta a imply meta a end parenthesis end line because propositional modus ponens modus ponens ell b modus ponens ell d indeed meta a imply meta a qed end math end statement ]" Logiweb has checked the proof above as can be seen from the ``After verifying: The page is correct'' in the Logiweb main menu of the present page. \subsection{Logiweb and copyright}\sect{LogiwebAndCopyright} Once a Logiweb page is submitted to Logiweb it is understood that anybody is allowed to make verbatim copies of the page and resubmit them to Logiweb. Resubmitted copies have the same Logiweb reference as the original but a different http URL. For this reason, each Logiweb page may have many http URLs but only one Logiweb reference. To Logiweb, all copies of a Logiweb page are equal, and the original (i.e.\ the first copy submitted to Logiweb) has no special priviledges. A Logiweb page continues to exist as long as there is at least one copy of it on Logiweb. Hence, a Logiweb page may continue to exist even if the original is deleted. Copyright notices on Logiweb pages may restrict human readers in what they do with the pages, such as modifying them or exporting them to other media than Logiweb. But copyright notices cannot prevent verbatim copying inside Logiweb: verbatim copying is what Logiweb does to submitted pages. To avoid verbatim copying of your page, don't submit it to Logiweb. \subsection{Logiweb and trade marks}\sect{LogiwebAndTradeMarks} The word ``Logiweb'' is a good one and, hence, it is used as a trademark and a registered trademark for many different things. But when used for a format, a semantics, and a protocol for exchange of mathematics via the internet, ``Logiweb'' is a trademark of the author of the present paper. The purpose is to force incompatible versions of Logiweb to pick other names. Furthermore, the blue ``Logiweb and stribes'' logo is a trademark of the author. \subsection{Further reading}\sect{FurtherReading} For further information, read \cite{logiweb}, the \href {\lgwBaseUrl}{base} page, and ``help'' text. To play with Logiweb, download it from http://yoa.dk/. Have fun. \appendix \section{Chores}\sect{Chores} \subsection{The name of the page}\sect{TheNameOfThePage} This defines the name of the page: "[ display math pyk define check as "check" end define end math end display ]" \subsection{\TeX\ definitions}\sect{TexDefinitions} \begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}} \immediate\closeout\outex \input{./page.otx} \end{list} \subsection{Test}\sect{Test} \begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}} \immediate\closeout\outest \input{./page.tst} \end{list} \subsection{Priority table}\sect{PriorityTable} "[ flush left math priority table Priority end table end math end left ]" \section{Index}\sect{Index} \newcommand\myidxitem{\par\noindent} \renewenvironment{theindex}{\let\item\myidxitem}{} \printindex \section{Bibliography}\sect{Bibliography} \bibliography{./page} \end{document} End of file File page.bib @article {berline97, author = {C. Berline and K. Grue}, title = {A $\kappa$-denotational semantics for {M}ap {T}heory in {ZFC+SI}}, journal = TCS, year = {1997}, volume = {179}, number = {1--2}, pages = {137--202}, month = {jun}} @book {church41, author = {A. Church}, title = {The Calculi of Lambda-Conversion}, publisher = {Princeton University Press}, year = {1941}} @Article {godel, author = {K. G{\"!o}del}, title = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re \mbox{S\"!at}\-ze der \mbox{Prin}\-ci\-pia \mbox{Mathe}\-ma\-ti\-ca und ver\-wand\-ter \mbox{Sys}\-teme \mbox{I}}, journal = {Mo\-nats\-hef\-te f{\"!u}r Mathe\-ma\-tik und Phy\-sik}, year = {19\-31}, volume = {12}, number = {\mbox{XXXVIII}}, pages = {173-198}} @book {Gordon79, author = {M. J. Gordon, A. J. Milner, C. P. Wadsworth}, title = {Edinburgh {LCF}, A mechanised logic of computation}, publisher = {Springer-Verlag}, year = {1979}, volume = {78}, series = {Lecture Notes in Computer Science}} @article {grue92, author = {K. Grue}, title = {Map Theory}, journal = TCS, year = {1992}, volume = {102}, number = {1}, pages = {1--133}, month = {jul}} @inproceedings{Logiweb, author = {K. Grue}, title = {Logiweb}, editor = {Fairouz Kamareddine}, booktitle = {Mathematical Knowledge Management Symposium 2003}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {93}, year = {2004}, pages = {70--101}} @article {mccarthy60, author = {J. McCarthy}, title = {Recursive functions of symbolic expressions and their computation by machine}, journal = {Communications of the ACM}, year = {1960}, pages = {184--195}} @book {mendelson, author = {E. Mendelson}, title = {Introduction to Mathematical Logic}, publisher = {Wadsworth and Brooks}, year = {1987}, edition = {3.}} @book {TeXbook, author = {D. Knuth}, title = {The TeXbook}, publisher = {Addison Wesley}, year = {1983}} End of file File page.sty % thebibliography environment from % /usr/share/texmf/tex/latex/base/book.cls % with \chapter removed \renewenvironment{thebibliography}[1] {\list{\@biblabel{\@arabic\c@enumiv}}% {\settowidth\labelwidth{\@biblabel{#1}}% \leftmargin\labelwidth \advance\leftmargin\labelsep \@openbib@code \usecounter{enumiv}% \let\p@enumiv\@empty \renewcommand\theenumiv{\@arabic\c@enumiv}}% \sloppy \clubpenalty4000 \@clubpenalty \clubpenalty \widowpenalty4000% \sfcode`\.\@m} {\def\@noitemerr {\@latex@warning{Empty `thebibliography' environment}}% \endlist} End of file latex page makeindex page bibtex page latex page makeindex page latex page dvipdfm page"