## Logiweb source of base

""{ Logiweb, a system for electronic distribution of mathematics
Copyright (C) 2004-2006 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://logiweb.eu/, http://www.diku.dk/~grue/

Logiweb is a system for distribution of mathematical definitions,
lemmas, and proofs. For more on Logiweb, consult http://logiweb.eu/.
}

PAGE base

BIBLIOGRAPHY

PREASSOCIATIVE
1 "" proclaim " as " end proclaim
"" empty
"" preassociative " greater than "
"" postassociative " greater than "
"" priority " equal "
"" priority " end priority
"" asterisk
"" pyk
"" Define " of " as " end define
"" math " end math
"" display math " end math
"" make math " end math
"" a
"" b
"" c
"" d
"" e
"" f
"" g
"" h
"" i
"" j
"" k
"" l
"" m
"" n
"" o
"" p
"" q
"" r
"" s
"" t
"" u
"" x
"" y
"" z
"" v
"" w
"" A
"" B
"" C
"" D
"" E
"" F
"" G
"" H
"" I
"" J
"" K
"" L
"" M
"" N
"" O
"" P
"" Q
"" R
"" S
"" T
"" U
"" V
"" W
"" X
"" Y
"" Z
"" true
"" quote " end quote
"" optimized define " of " as " end define
"" tex
"" tex name
"" priority
"" value
"" macro
"" render
"" claim
"" message
"" unpack
"" execute
"" executables
"" exampleaspect0
"" exampleaspect1
"" exampleaspect2
"" name " end name
"" macro name " end name
"" hiding name " end name
"" hide " end hide
"" array ( " ) " end array
"" left
"" center
"" right
"" %%
"" ( " )
"" < " | " := " >
"" bottom
"" false
"" define " of " as " end define
"" ...
"" ---
"" Zero
"" One
"" Two
"" Three
"" Four
"" Five
"" Six
"" Seven
"" Eight
"" Nine
"" Ten
"" Base
"" Xor ( " , " , " )
"" Carry ( " , " , " )
"" Plus ( " , " , " )
"" Borrow ( " , " , " )
"" Compare ( " , " , " )
"" Minus ( " , " , " )
"" BoolTag
"" IntTag
"" PairTag
"" ExTag
"" MapTag
"" equal1 ( " , " )
"" TheInt ( " , " )
"" int ( " )
"" plus1 ( " , " )
"" plus2 ( " , " , " , " )
"" minus1 ( " )
"" minus2 ( " , " )
"" times1 ( " , " )
"" times2 ( " , " , " , " )
"" lt1 ( " , " )
"" lt2 ( " , " , " , " )
"" reverse ( " )
"" revappend ( " , " )
"" nth ( " , " )
"" exception
"" map ( " )
"" Catch ( " )
"" catch ( " )
"" object ( " )
"" Object ( " , " , " )
"" destruct ( " )
"" 0
"" 1
"" 2
"" 3
"" 4
"" 5
"" 6
"" 7
"" 8
"" 9
"" numeral ( " )
"" num1 ( " , " , " )
"" num2 ( " , " , " )
"" evenp ( " )
"" oddp ( " )
"" half ( " )
"" small ( " )
"" double ( " , " )
"" lognot ( " )
"" logior ( " , " )
"" logxor ( " , " )
"" logand ( " , " )
"" logeqv ( " , " )
"" lognand ( " , " )
"" lognor ( " , " )
"" logandc1 ( " , " )
"" logandc2 ( " , " )
"" logorc1 ( " , " )
"" logorc2 ( " , " )
"" logtest ( " , " )
"" ash ( " , " )
"" ash+ ( " , " )
"" ash- ( " , " )
"" logbitp ( " , " )
"" logcount ( " )
"" logcount1 ( " )
"" integer-length ( " )
"" vector-empty ( " )
"" vector-head1 ( " )
"" vector-tail1 ( " )
"" vector-cons ( " , " )
"" vector ( " )
"" vector-suffix ( " , " )
"" vector-prefix ( " , " )
"" vector-subseq ( " , " , " )
"" vector-length ( " )
"" vector-index ( " , " )
"" vector-head ( " )
"" vector-tail ( " )
"" vector2byte* ( " )
"" vector2byte*1 ( " , " )
"" bt2byte* ( " )
"" bt2byte*1 ( " , " )
"" bt2vector ( " )
"" revbyte*2vector ( " , " )
"" vector-revappend ( " , " )
"" vt2byte* ( " )
"" vt2byte*1 ( " , " )
"" vt2vector ( " )
"" floor1 ( " , " )
"" ceiling1 ( " , " )
"" round1 ( " , " )
"" floor ( " , " )
"" ceiling ( " , " )
"" truncate ( " , " )
"" round ( " , " )
"" reverse quotient ( " )
"" length ( " )
"" length1 ( " , " )
"" list-prefix ( " , " )
"" list-suffix ( " , " )
"" lookup ( " , " , " )
"" zip ( " , " )
"" array1 ( " , " , " )
"" array2 ( " , " , " , " )
"" array3 ( " , " )
"" array4 ( " , " )
"" array5 ( " , " , " , " , " )
"" eval ( " , " , " )
"" eval1 ( " , " , " , " )
"" spy ( " )
"" trace ( " )
"" print ( " )
"" timer ( " )
"" test1
"" test2 ( " )
"" test3 ( " , " )
"" test3* ( " , " )
"" ttst1 ( " )
"" ftst1 ( " )
"" etst1 ( " )
"" ttst " end test
"" ftst " end test
"" etst " ; " end test
"" texname " end texname
"" testfunc1 ( " )
"" testfunc2 ( " , " )
"" testfunc3
"" testfunc4
"" testfunc5 ( " )
"" testfunc6 ( " )
"" testfunc7 ( " )
"" testfunc8 ( " , " )
"" macro1
"" macro2 ( " )
"" macro3 ( " , " , " )
"" macro3* ( " , " , " )
"" macro4 ( " )
"" macrostate0
"" stateexpand ( " , " , " )
"" stateexpand* ( " , " , " )
"" substitute ( " , " , " )
"" substitute* ( " , " , " )
"" expand ( " , " )
"" protect " end protect
"" Macro define " as " end define
"" Macrodefine ( " )
"" macro define " as " end define
"" macrodefine ( " )
"" self
"" makeself ( " )
"" root protect " end protect
"" rootprotect ( " )
"" render define " as " end define
"" tex define " as " end define
"" tex name define " as " end define
"" value define " as " end define
"" message define " as " end define
"" priority table "
"" verifier " end verifier
"" unpacker " end unpacker
"" renderer " end renderer
"" expander " end expander
"" executer " end executer
"" executables " end executables
"" ragged right
"" make macro expanded version ragged right
"" <<>>
"" << " >>
"" tuple1 ( " )
"" tuple2 ( " , " )
"" eager define " as " end define
"" eager1 ( " )
"" eager2 ( " , " , " )
"" eager message define " as " end define
"" macrolet1 ( " )
"" destructure
"" destructure define " as " end define
"" let1 ( " )
"" let2 ( " , " , " , " )
"" let3 ( " , " , " , " )
"" make-var ( " )
"" make-let ( " , " , " )
"" make-prime ( " )
"" make-head ( " )
"" make-tail ( " )
"" back " quote " end quote
"" make-root ( " , " )
"" make-pair ( " , " , " )
"" make-true ( " )
"" make-quote ( " , " )
"" make-make-root ( " , " , " )
"" backquote0 ( " )
"" backquote1 ( " , " , " )
"" backquote2 ( " , " , " , " , " )
"" backquote2* ( " , " , " , " , " )
"" text " : " end text
"" tex ( " )
"" latex ( " )
"" bibtex ( " )
"" makeindex ( " )
"" dvipdfm ( " )
"" page ( " , " ) title " bib " main text " appendix " end page
"" page1 ( " )
"" tex-file ( " , " , " )
"" tex-command ( " , " )
"" quit ( " )
"" boot ( " , " , " )
"" write ( " )
"" read ( " )
"" exec ( " , " )
"" int ( " , " )
"" extend ( " )
"" extended ( " )
"" Hello World
"" Echo
"" Echo1 ( " )
"" Eecho
"" Eecho1 ( " )

PREASSOCIATIVE
"" +"
"" -"
"" 0"
"" 1"
"" 2"
"" 3"
"" 4"
"" 5"
"" 6"
"" 7"
"" 8"
"" 9"

PREASSOCIATIVE
"" " factorial
"" " _ { " }
"" " prime
"" " %0
"" " %1
"" " %2
"" " %3
"" " %4
"" " %5
"" " %6
"" " %7
"" " %8
"" " %9
"" " tail
"" " raise
"" " catch
"" " catching maptag
"" " maptag
"" " untag
"" " boolp
"" " truep
"" " falsep
"" " intp
"" " pairp
"" " atom
"" " mapp
"" " objectp
"" " root
"" " Tail
"" " TheBool
"" " TheNat
"" " norm
"" " Tag
"" " BoolP
"" " IntP
"" " PairP
"" " ExP
"" " MapP
"" " ObjectP
"" " Sign
"" " Mag
"" " zeroth
"" " first
"" " second
"" " third
"" " fourth
"" " fifth
"" " sixth
"" " seventh
"" " eighth
"" " ninth
"" " ref
"" " idx
"" " debug
"" " [[ " ]]
"" " [[ " -> " ]]
"" " [[ " => " ]]
"" " unquote

PREASSOCIATIVE
"" " ' "
"" " apply "

PREASSOCIATIVE
"" - "
"" + "

PREASSOCIATIVE
"" " Times "
"" " * "

PREASSOCIATIVE
"" " Plus "
"" " Minus "
"" " + "
"" " - "

PREASSOCIATIVE
"" PlusTag "
"" MinusTag "

PREASSOCIATIVE
"" " div "
"" " mod "

POSTASSOCIATIVE
"" " LazyPair "
"" " Pair "
"" " NatPair "
"" " :: "

POSTASSOCIATIVE
"" " ,, "

PREASSOCIATIVE
"" " = "
"" " != "
"" " Equal "
"" " LT "
"" " < "
"" " <= "
"" " > "
"" " >= "
"" " r= "
"" " t= "
"" " t=* "

PREASSOCIATIVE
"" Not "
"" .not. "
"" notnot "

PREASSOCIATIVE
"" " And "
"" " .and. "
"" " .then. "
"" " &c "

PREASSOCIATIVE
"" " Or "
"" " .or. "

POSTASSOCIATIVE
"" " Iff "

PREASSOCIATIVE
"" " Select " else " end select
"" " IN "

PREASSOCIATIVE
"" \ " . "
"" If " then " else "
"" if " then " else "
"" newline "
"" LET " BE "
"" let " := " in "
"" let " = " in "

POSTASSOCIATIVE
"" norm "
"" " Guard "
"" " is val : "
"" " is bool : "
"" " is int : "
"" " is pair : "
"" " is map : "
"" " is object : "

PREASSOCIATIVE
"" " reduce to "
"" " == "

POSTASSOCIATIVE
"" ","
"" "[ " ]"
"" "[[ " ]]"
"" "[[[ " ]]]"

PREASSOCIATIVE
"" " linebreak "

PREASSOCIATIVE
"" " & "

PREASSOCIATIVE
"" " \\ "

BODY

text "page.html" : ""+
<title>
A Logiweb base page
</title>

<body>
<h2>
A Logiweb base page
</h2>

<p>
<a href='../index.html'>Up</a>
</p>

<p>

Contents:
<a href='page.pdf'>Main text</a>
<a href='chores.pdf'>Chores</a>
</p>

</body>
" end text ,,

text "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}}

@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}}

@techreport{chores,
author = {K. Grue},
year = {2006},
title = {A Logiweb base page - chores},
institution={Logiweb},
note = {\href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/appendix.pdf}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/appendix.pdf}}}

" end text ,,

text "page.tex" : ""+

\documentclass[fleqn]{article}

% Include definitions generated by pyk
\input{lgwinclude}

% Make latexsym characters available
\usepackage{latexsym}

% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}

% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}

% Enable generation of a bibliography
\bibliographystyle{plain}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
% (x,y)=(120,80) lower left, (x,y)=(490,730) upper right
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=A Logiweb base page}

% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}

\begin{document}
\title{A Logiweb base page}
\author{Klaus Grue}
\maketitle
\tableofcontents

"[ make macro expanded version ragged right ]"

\section{Introduction}

\indexintro{Logiweb} \cite{Logiweb} is an open source system available under GNU GPL for distribution of mathematical definitions, lemmas, and proofs.

The present document is part of a \index{page, Logiweb}\indexintro{Logiweb page}. A Logiweb page is a cluster of documents which has been submitted to the Logiweb system. Such a cluster typically consists of a main document like the present one plus a number of electronic appendices.

The present Logiweb page (i.e.\ the document cluster to which the present document belongs) is a Logiweb \index{base page}\intro{base} page. A Logiweb base page is a Logiweb page which references no other Logiweb pages. Logiweb base pages are self-contained pages which define elementary concepts.

\subsection{Electronic appendices}

The present Logiweb page comprises one html and two PDF files, located the following places:

\begin{itemize}
\item \href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/page.pdf}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/page.pdf}
\item \href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/appendix.pdf}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/appendix.pdf} \cite{chores}
\item \href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/page.html}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/page.html}
\end{itemize}

The first link points to the present paper. The second link points to an electronic appendix with definitions that would bore most readers (such as definitions of how each construct should be rendered). The second link is included in the \textsc{Bib}\TeX\ bibliography \cite{chores} for easy reference. The third link points to a table of contents.

\subsection{Proclamations}\label{sec:Proclamations}

Logiweb has a number of predefined semantic concepts. Each predefined concept has a name where a name is a string of characters.

Furthermore, Logiweb has a \indexintro{proclamation} mechanism which allows to connect syntactic constructs with semantic concepts. Some proclamations are given in the following.

\begin{statements}

\item "[[ proclaim \ x . y as "lambda" end proclaim ]]"\index{lambda} connects the syntactic construct "[[ \ x . y ]]" with the semantic concept whose name reads lambda''. This proclamation tells Logiweb that "[[ \ x . y ]]" denotes \index{abstraction, lambda}\indexintro{lambda abstraction} in the present context. The proclamation has effect on the present Logiweb page and all Logiweb pages which reference the present page.

\item "[[ proclaim x ' y as "apply" end proclaim ]]"\index{apply} proclaims "[[ x ' y ]]" to denote \index{application, functional}\indexintro{functional application}.

\item "[[ proclaim true as "true" end proclaim ]]"\index{true} proclaims "[[ true ]]" to denote \indexintro{truth}.

\item "[[ proclaim If x then y else z as "if" end proclaim ]]"\index{if} proclaims "[[ If x then y else z ]]" to denote an \index{construct, if-then-else}\indexintro{if-then-else construct}. This and the previous 3 constructs are explained in more detail in Section \ref{sec:Computation}.

\item "[[ proclaim quote x end quote as "quote" end proclaim ]]"\index{quote} proclaims "[[ quote x end quote ]]" to denote a data structure which represents the term "[[ x ]]". This is explained in more detail in Section \ref{sec:RepresentationOfTerms}.

\item "[[ proclaim proclaim x as y end proclaim as "proclaim" end proclaim ]]"\index{proclaim} proclaims "[[ proclaim x as y end proclaim ]]" to denote \indexintro{proclamation}. Each construct in Logiweb is identified by a reference and an index, both of which are integers. The reference identifies the Logiweb page which introduces the construct. If a page is a base' page in the sense that it references no other pages, then the construct with index 1 of that page is born as a proclamation construct. Such a proclamation construct can declare other constructs to be proclamation constructs. But it also has to secure itself by declaring itself as a proclamation construct as it otherwise looses its proclamation ability. The present page happens to be a base page and the construct above happens to be construct number 1 of the present page.

\item "[[ proclaim define x of y as z end define as "define" end proclaim ]]"\index{define} says that "[[ define x of y as z end define ]]" \index{definition}\intro{defines} the "[[ x ]]" \indexintro{aspect} of "[[ y ]]" to be "[[ z ]]". As an example of use, "[[ define value of x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define ]]" defines the \index{aspect, value}\indexintro{value aspect} of "[[ x factorial ]]" such that "[[ ttst 3 factorial = 6 end test ]]".

\item "[[ proclaim Define x of y as z end define as "define" end proclaim ]]" says that "[[ Define x of y as z end define ]]" means exactly the same as "[[ define x of y as z end define ]]". The difference is in how the right hand side of the definition is rendered. "[[ define x of y as z end define ]]" renders "[[ z ]]" using the \index{aspect, tex}\indexintro{tex aspect} of "[[ z ]]" whereas "[[ Define x of y as z end define ]]" uses the \index{aspect, tex name}\index{name aspect, tex}\indexintro{tex name aspect}. For more on the tex and tex name aspects see Section \ref{sec:AspectDeclarations} and see the newline construct at the end of Section \ref{sec:ElementaryDefinitions}.

\item "[[ proclaim optimized define x of y as z end define as "introduce" end proclaim ]]"\index{introduce} says that "[[ optimized define x of y as z end define ]]" means exactly the same as "[[ Define x of y as z end define ]]", except that "[[ optimized define x of y as z end define ]]" may affect CPU run time dramatically in a few, vital cases c.f.\ Section \ref{sec:ElementaryDefinitions}.

\item "[[ proclaim hide x end hide as "hide" end proclaim ]]"\index{hide} proclaims that "[[ x ]]" in "[[ name hide x end hide end name ]]" should be hidden from \indexintro{harvesting}. Harvesting is the process in which proclamations, definitions, and other Logiweb \index{revelation}\intro{revelations} are collected from a page. Hiding may be useful e.g.\ when talking about revelation constructs without wanting them to take effect. For more on hiding see Section \ref{sec:VisibilityConstructs}.

\end{statements}

Logiweb has predefined concepts with the names used above (apply, lambda, true, if, quote, proclaim, define, introduce, hide, pre, and post). Logiweb has no other predefined concepts than those. Attempts to proclaim a construct to denote some unknown concept are ignored. The \index{compiler, pyk}\indexintro{pyk compiler} (a tool for constructing Logiweb pages) issues a warning in case of unrecognized proclamations.

\subsection{Aspect declarations}\label{sec:AspectDeclarations}

On Logiweb, constructs that assign meaning to constructs always assign meaning to a particular \indexintro{aspect} of the construct. Some aspects are defined by the following \index{aspect declaration}\index{declaration, aspect}\intro{aspect declarations}.

\begin{statements}

\item "[[ Define "message" of message as "message" end define ]]"\index{message} defines "[[ message ]]" to represent the \index{aspect, message}\indexintro{message aspect}. The message aspect of a construct indicates which aspect the construct represents. For an example of use, see the next entry.

Section \ref{sec:Proclamations} proclaimed two definitions constructs, one with and one without an exclamation mark. The one with the exclamation mark renders its arguments using the tex name aspect whereas the one without renders its aspect and right hand side using the tex aspect. The tex name aspect of a string comprises the string with quotes around whereas the tex aspect of a string is the string without quotes. The exclamation mark version of the definition construct is used here to make it easy distinguish strings from non-strings.

\item "[[ Define message of value as "value" end define ]]"\index{value} defines "[[ value ]]" to represent the \index{aspect, value}\indexintro{value aspect}. As an example, the definition "[[ Define value of x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define ]]" from Section \ref{sec:Proclamations} used "[[ value ]]" to represent the value aspect. One may replace "[[ message ]]" and "[[ value ]]" by the strings they denote as in "[[ Define "message" of value as "value" end define ]]" and "[[ Define "value" of x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define ]]".

\item "[[ Define message of pyk as "pyk" end define ]]"\index{pyk} defines "[[ pyk ]]" to represent the \index{aspect, pyk}\indexintro{pyk aspect}. The pyk aspect of a construct is a plain text representation for the construct. Such a plain text representation is useful when editing Logiweb pages using an ordinary text editor. As an example, the pyk aspects of "[[ \ x . y ]]", "[[ u ]]", and "[[ v ]]" are \verb+\"!."!+, \verb+vu+, and \verb+vv+, respectively. For that reason, one may type \verb+\ u . vv+ in a text editor, run the text through a pyk'' compiler, and get a Logiweb page containing "[[ \ u . v ]]". For examples of pyk definitions see Section Pyk definitions'' in \cite{chores}.

The name pyk'' is constructed from the name Volap{\"!u}k'' in the same way that Rene Thom constructed the word versal'' from universal'': pyk'' is constructed by removing Vola'' from Volap{\"!u}k''. Volap{\"!u}k was an artificial language constructed from several other languages by simplifying their words and their grammar. As an example, the name of the language itself is constructed from Vola'' which is a simplification of World'' and p{\"!u}k'' which is a simplification of speak''. Among other, pyk is indended to be entered through a microphone.

\item "[[ Define message of tex as "tex" end define ]]"\index{tex} defines "[[ tex ]]" to represent the \index{aspect, tex}\indexintro{tex aspect}. The tex aspect of a construct indicates how the aspect should be rendered in \TeX\ when using the construct. For examples of tex definitions see Section \TeX\ definitions'' in \cite{chores}.

\item "[[ Define message of tex name as "texname" end define ]]"\index{name, tex}\index{tex name} defines "[[ tex name ]]" to represent the \index{name aspect, tex}\index{aspect, tex name}\indexintro{tex name aspect}. The tex name aspect of a construct indicates how the aspect should be rendered in \TeX\ when talking about the construct. Most constructs look the same when using them and when talking about them. For that reason, the tex name aspect defaults to the tex aspect. As an example, "[[ \ x . y ]]" has no tex name aspect so "[[ \ x . y ]]" looks the same when using lambda abstraction and when talking about lambda abstraction. Some constructs look different when using them and when talking about them, c.f.\ Section \ref{sec:VisibilityConstructs}. For examples of tex name definitions see Section \TeX\ definitions'' in \cite{chores}. For more on the use of tex and tex name aspects, see the newline construct at the end of Section \ref{sec:ElementaryDefinitions}.

\item "[[ Define message of priority as "priority" end define ]]"\index{priority} defines "[[ priority ]]" to represent the \index{aspect, priority}\indexintro{priority aspect}. The priority aspect of a Logiweb page indicates the priority and associativity of all constructs on the page itself plus all constructs on directly referenced Logiweb pages. For an example of a priority definition see Section Priority table'' in \cite{chores}.

The statement above that the priority aspect of a Logiweb page indicates the priorities is not completely true. Aspects attach to constructs, not to pages. However, each Logiweb page has a \index{construct, page}\indexintro{page construct} which represents the page (c.f.\ Section \ref{sec:RepresentationOfTerms}). The page construct of the present page reads "[[ base ]]"'' and the priority table in \cite{chores} is indeed a definition of the priority aspect of this "[[ base ]]"'' construct.

\item "[[ Define message of macro as "macro" end define ]]"\index{macro} defines "[[ macro ]]" to represent the \index{aspect, macro}\indexintro{macro aspect}. The macro aspect defines how a Logiweb page is macro expanded, c.f.\ Section \ref{sec:MacroExpansion}.

\item "[[ Define message of render as "render" end define ]]"\index{render} defines "[[ render ]]" to represent the \index{aspect, render}\indexintro{render aspect}. Logiweb has a predefined way of rendering Logiweb pages, but rendering can be modified using the render aspect.

\item "[[ Define message of claim as "claim" end define ]]"\index{claim} defines "[[ claim ]]" to represent the \index{aspect, claim}\indexintro{claim aspect}. The claim aspect defines how a Logiweb page is verified, c.f.\ Section \ref{sec:Verification}.

\item "[[ Define message of unpack as "unpack" end define ]]"\index{unpack} defines "[[ unpack ]]" to represent the \index{aspect, unpack}\indexintro{unpack aspect}. When stored on disk or transmitted over a network, Logiweb pages are stored as \index{Logiweb vector}\index{vector, Logiweb}\intro{Logiweb vectors}, i.e.\ as sequences of bytes. Logiweb has a predefined way of unpacking Logiweb vectors into Logiweb pages, but unpacking can be modified using the unpack aspect.

\item "[[ Define message of execute as "execute" end define ]]"\index{execute} defines "[[ execute ]]" to represent the \index{aspect, execute}\indexintro{execute aspect}. Logiweb has two mechanisms for letting Logiweb pages contain executable code. One mechanism is to set the execute aspect of the page construct to a computable function. When a Logiweb page is \index{execute}\intro{executed}, a Logiweb machine is started with the computable function as \index{handler, boot}\indexintro{boot handler}, c.f.\ Section \ref{sec:Interaction}.

\item "[[ Define message of executables as "executables" end define ]]"\index{executables} defines "[[ executables ]]" to represent the \index{aspect, executables}\indexintro{executables aspect}. The other mechanism for expressing executable code is to set the executables aspect of the page construct to an association list from names to functions. When rendering a page, each function is converted into a machine as described above and written to disc in a user defined directory under the given name. Hence, the difference between the "[[ execute ]]" and "[[ executables ]]" method is that the "[[ execute ]]" method defines one, nameless machine and the "[[ executables ]]" method can define any numbder of named machines. The user can execute the machine defined by the "[[ execute ]]" aspect during rendering and/or store it under a user supplied name.

\item "[[ Define message of exampleaspect0 as "example aspect/kg" end define ]]" defines "[[ exampleaspect0 ]]" to represent an aspect named example aspect/kg'. The exampleaspect0 aspect is a \index{aspect, user}\indexintro{user aspect} in the sense that Logiweb does not know about it in advance. To avoid name conflicts, one should give any user aspect a personal touch. The exampleaspect0 aspect above is represented by a string which includes the initials of the present author. In general, user aspects should contain at least one character which is not a small latin letter (a to z) and not a space. The example aspect above is ok since it contains a slash. Aspects which contain only small latin letters and spaces are reserved for future extensions of Logiweb. The only exception is the 'destructure' aspect defined later which consists of only small latin letters for historical reasons.

\item "[[ Define message of exampleaspect1 as exampleaspect2 end define ]]" defines "[[ exampleaspect1 ]]" to represent a user aspect represented by the construct "[[ exampleaspect2 ]]". "[[ exampleaspect2 ]]" is a construct introduced on the present page. Like any other Logiweb construct, it is identified by a \indexintro{reference} and an \indexintro{index}. The reference is a world-wide unique natural number which identifies the present page. The index is a natural number which distinguishes the "[[ exampleaspect2 ]]" construct from the other constructs introduced on the present page. The definition of "[[ exampleaspect1 ]]" above defines "[[ exampleaspect1 ]]" to denote an aspect which is represented by the reference and identifier of "[[ exampleaspect2 ]]". Contrary to the definition of the exampleaspect0 aspects above, there is no risk of name conflicts. On the other hand, the "[[ exampleaspect2 ]]" ceases to exist if the present page is ever deleted from Logiweb.

\item "[[ Define message of exampleaspect2 as exampleaspect2 end define ]]" defines "[[ exampleaspect2 ]]" to represent the user aspect represented by "[[ exampleaspect2 ]]" itself. Hence, "[[ exampleaspect1 ]]" and "[[ exampleaspect2 ]]" denote the same aspect.

\end{statements}

Logiweb assigns a particular semantics to the value, pyk, tex, texname, priority, macro, claim, message, unpack, execute, and executables aspects. Logiweb does not assign semantics to any other aspects, but it allows users to declare arbitrary user aspects like the example aspects above. It is up to the authors of Logiweb pages to assign semantics to user aspects. As an example, the present page declares a destructure' user aspect in Section \ref{sec:LetConstructs} and defines a destructuring let' macro such that let' uses the destructure' aspect. Apart from the destructure aspect, any user defined aspect should contain at least one character which is neither a small latin letter (a to z) nor a space.

\subsection{Definition of pre- and post-associativity}

\begin{statements}

\item "[[ Define priority of preassociative x greater than y as "pre" end define ]]"\index{pre} defines "[[ name preassociative x greater than y end name ]]" to denote \index{preassociative}\intro{preassociativity}. A preassociative construct is leftassociative in text that runs left to right, rightassociative in text that runs right to left, topassociative in text that runs from top to bottom, counter-clock-wise-associative in text written in clock-wise spirals, and so on. "[[ name preassociative x greater than y end name ]]" states that all constructs listed in the "[[ x ]]" position are preassociative and that all of them have greater priority than those listed in the "[[ y ]]" position. For a table of associativites and priorities see the chapter named Priority table'' in \cite{chores}.

\item "[[ Define priority of postassociative x greater than y as "post" end define ]]"\index{post} defines "[[ name postassociative x greater than y end name ]]" to denote \index{postassociative}\intro{postassociativity}.

\end{statements}

\subsection{The Logiweb system}\label{sec:TheLogiwebSystem}

From a standardization point of view, the Logiweb system comprises two standards, one which defines the syntax and semantics of Logiweb pages and one which defines a protocol for exchanging information about Logiweb pages.

From an implementation point of view, the current implementation of the Logiweb system comprises two programs called the \index{compiler, pyk}\indexintro{pyk compiler} and the \index{server, Logiweb}\indexintro{Logiweb server}, respectively, plus a number of auxilliary files and programs.

From a user point of view, Logiweb comprises a number of Logiweb pages which the user can browse using an ordinary web browser or search using an ordinary web search engine.

Users who merely want to read existing Logiweb pages can do with an ordinary web browser. Users will need the pyk compiler in the following cases:

\begin{enumerate}

\item\label{enum:author} when authoring and submitting new Logiweb pages.

\item\label{enum:mirror} when mirroring Logiweb pages, i.e.\ when a user wants to make a particular Logiweb page available on the users own web site.

\item\label{enum:execute} when executing computable functions on Logiweb pages (c.f.\ the execute'' aspect in Section \ref{sec:AspectDeclarations}).

\end{enumerate}

In general, users will not be aware of Logiweb servers. All Logiweb servers in the world cooperate on indexing all Logiweb pages in the world, which is needed in connection with the internal referencing system of Logiweb. When searching for Logiweb pages, users should use an ordinary web search engine.

Even though Logiweb has several components and even though one can view Logiweb from several points of view, the only piece of Logiweb software users will typically meet is the pyk compiler. Typically, when the present paper states that Logiweb is able to perform various tasks, those tasks are actually undertaken by the pyk compiler.

Note that the pyk compiler is just one, possible implementation of Logiweb. A wysiwyg Logiweb browser/editor was once implemented but is not currently maintained, but one may foresee other tools than the pyk compiler for viewing, authoring, mirroring, and executing Logiweb pages.

\section{Computation}\label{sec:Computation}

Logiweb (i.e.\ the pyk compiler, c.f.\ Section \ref{sec:TheLogiwebSystem}) is able to \indexintro{reduce} computable terms to \index{form, normal}\indexintro{normal form}. It does so using the \index{computing engine, Logiweb}\index{engine, Logiweb computing}\indexintro{Logiweb computing engine}.

The Logiweb engine is just a computing engine; it has no facilities for communicating with the outside world. The Logiweb machine (c.f.\ Section \ref{sec:Interaction}) contains the Logiweb engine and also contains facilities for input/output.

\subsection{Reduction system}\label{sec:ReductionSystem}

The engine reduces terms according to the following reduction system:

"[[[ array ( left,left,left )

( \ x . y ) ' z & %% reduce to %% & < y | x := z > \\

true ' z & %% reduce to %% & true \\

If true then u else v & %% reduce to %% & u \\

If \ x . y then u else v & %% reduce to %% & v

end array ]]]"

\noindent "[[ < x | y := z > ]]" denotes the result of replacing all free occurrences of the variable "[[ y ]]" in the term "[[ x ]]" by the term "[[ z ]]", possibly renaming bound variables as needed.

\subsection{Normal forms}\label{sec:NormalForms}

We shall say that a term "[[ z ]]" is on \index{normal form}\indexintro{truth normal form} if the term "[[ z ]]" is identical to "[[ true ]]". We shall say that a term "[[ z ]]" is on \indexintro{function normal form} if the term "[[ z ]]" has form "[[ \ x . y ]]" where "[[ x ]]" is a variable and "[[ y ]]" is a term. We shall say that a term is on \indexintro{root normal form} if the term is on truth or function normal form.

When given a term, the Logiweb engine starts reducing the term using leftmost reduction. The Logiweb engine stops again when the term reaches root normal form, if ever.

We shall say that a term is a \indexintro{true term} if the engine reduces it to a truth normal form and that a term is a \indexintro{function term} if the engine reduces it to a function normal form. We shall say that a term is a \indexintro{bottom term} if the engine reduces the term forever without reaching a root normal form.

\subsection{Maps}\label{sec:Maps}

The reduction system above is pure lambda calculus extended with an uhr-element "[[ true ]]" and an if-then-else construct which can test for equality to "[[ true ]]". It is out of the scope of the present page to explain why that extension is vital.

It is possible to reason about lambda calculus extended with "[[ true ]]" and "[[ If x then y else z ]]" using \index{theory, map}\indexintro{map theory} \cite{berline97}. Using the terminology of \cite{berline97} we shall refer to values of terms built from "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]" as \index{map}\intro{maps}.

Map theory defines a notion of equality named "[[ x == y ]]". We shall use "[[ x = y ]]" to denote that "[[ x ]]" and "[[ y ]]" are equal modulo identifications whereas we use "[[ x == y ]]" to denote genuine equality.

In other words, we use a sign with two horizontal bars, "[[ x = y ]]" to denote that "[[ x ]]" and "[[ y ]]" are very much equal and one with 3 horizontal bars, "[[ x == y ]]" to denote that "[[ x ]]" and "[[ y ]]" are even more equal.

The use of "[[ x = y ]]" to denote an equivalence relation (equality modulo identifications) and "[[ x == y ]]" to denote equality is apparently opposite to normal mathematical use. In practice, the use of "[[ x = y ]]" to denote equality modulo identification is very much in line with mathematical litterature. As an example, if one identifies the bidual of a Hilbert space with the Hilbert space itself, then it is common practice to use "[[ x = y ]]" between members of the bidual and members of the Hilbert space.

Anyone who can come up with a better name than "[[ x == y ]]" for true, identification disrespecting equality is welcome to contact the author.

Note that "[[ x == y ]]" has much lower priority than "[[ x = y ]]" according to the priority table in \cite{chores}. As an example, "[[ \ x . x = x == y ]]" means "[[ ( \ x . ( x = x ) ) == y ]]".

The reduction rules of Section \ref{sec:ReductionSystem} correspond to the following axioms of map theory:

"[[[ array ( left,left,left )

( \ x . y ) ' z & %% == %% & < y | x := z > \\

true ' z & %% == %% & true \\

If true then u else v & %% == %% & u \\

If \ x . y then u else v & %% == %% & v

end array ]]]"

\subsection{Full reduction system}\label{sec:FullReductionSystem}

The reduction system in Section \ref{sec:ReductionSystem} gives a good description of the Logiweb engine from a theoretical point of view, but a more complete description is given in the following:

\begin{itemize}

\item The engine reduces constructs proclaimed to denote lambda abstraction, functional application, truth, and if-then-else as indicated in Section \ref{sec:ReductionSystem}. Section \ref{sec:Proclamations} proclaimed "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]" to denote these concepts, respectively.

\item The engine reduces constructs proclaimed to denote quoting to the value described in Section \ref{sec:RepresentationOfTerms}. Section \ref{sec:Proclamations} proclaimed "[[ quote x end quote ]]" to denote quoting. "[[ quote x end quote ]]" reduces to a term built up from "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]". The value of "[[ quote x end quote ]]" represents the term "[[ x ]]".

\item The engine reduces constructs that have a value definition according to that definition, c.f. Section \ref{sec:ElementaryDefinitions}.

\item The engine reduces page constructs to terms which (in principle) are built up from "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]". The value of a page construct is called the \indexintro{cache} of the given page. The cache of a page is a huge data structure which represents a lot of information about the given page and all its transitively referenced pages. Among other, the cache contains the page before and after macro expansion, a structure which contains all definitions harvested from the page, and a structure which contains compiled versions of all value definitions.

\item The engine reduces all other constructs (non-page constructs that are neither proclaimed nor defined) to "[[ true ]]". This rather arbitrary convention is made to make the behaviour of the engine well-defined in all cases.

\item The engine would be rediculously slow if it wasn't for the optimizations explained in Section \ref{sec:ElementaryDefinitions}.

\end{itemize}

\subsection{Elementary definitions}\label{sec:ElementaryDefinitions}

Consider the following definitions:

\begin{statements}

\item "[[ define value of x LazyPair y as \ z . If z then x else y end define ]]". The engine reduces "[[ x LazyPair y ]]" to the function normal form "[[ \ z . If z then x else y ]]". As we shall see, it is possible to extract "[[ x ]]" and "[[ y ]]" from the return value, so the return value is a \indexintro{pairing} construct.

\item "[[ optimized define value of false as true LazyPair true end define ]]". The engine reduces "[[ false ]]" to the function normal form "[[ \ x . If x then true else true ]]". We shall use "[[ false ]]" to represent \indexintro{falsehood} as opposed to "[[ true ]]" which we use to represent truth.

\item "[[ define value of x Head as x ' true end define ]]". We have "[[[ array ( left )

( u LazyPair v ) Head == %% \\

( \ x . If x then u else v ) Head == %% \\

( \ x . If x then u else v ) ' true == %% \\

If true then u else v == %% \\

u

end array ]]]" Hence, "[[ ( u LazyPair v ) Head == u ]]" whenever "[[ u ]]" and "[[ v ]]" differ from "[[ bottom ]]".

\item "[[ define value of x Tail as x ' false end define ]]". Like above, we have that "[[ ( u LazyPair v ) Tail == v ]]" whenever "[[ u ]]" and "[[ v ]]" differ from "[[ bottom ]]". This supports the claim above that "[[ x LazyPair y ]]" is a pairing construct.

\item "[[ define value of x Guard y as If x then y else y end define ]]". The engine reduces "[[ x Guard y ]]" by reducing "[[ x ]]", discarding the value, reducing "[[ y ]]", and returning the value of "[[ y ]]". Hence "[[ x Guard y ]]" has the following properties:

\begin{itemize}

\item "[[ true Guard y == y ]]"

\item "[[ \ u . v Guard y == y ]]"

\item "[[ bottom Guard y == bottom ]]".

\end{itemize}

"[[ bottom ]]" above is defined in Section \ref{sec:Bottom}. "[[ bottom ]]" is a bottom term, i.e.\ a term which the engine reduces forever without reaching a root normal form (c.f.\ Section \ref{sec:NormalForms}).

\item "[[ define value of x Pair y as x Guard y Guard x LazyPair y end define ]]". The engine reduces "[[ x Pair y ]]" by reducing "[[ x ]]", discarding the value, reducing "[[ y ]]", discarding the value, and then returning the function normal form "[[ \ z . If z then x else y ]]". "[[ x Pair y ]]" is \indexintro{eager} or \indexintro{strict} in the sense that

\begin{itemize}

\item "[[ bottom Pair y == bottom ]]"

\item "[[ x Pair bottom == bottom ]]"

\end{itemize}

\item "[[ protect optimized define value of ( x ) as x end define end protect ]]". This definition says that a parenthesis does not affect the value of its contents. Section \ref{sec:Parentheses} macro defines parentheses such that they disappear during macro expansion which is another way of saying that a parenthesis does not affect the value of its contents. The purpose of the value definition above is to ensure that "[[ ( x ) == x ]]" even in situations where "[[ ( x ) ]]" is not macro expanded. The definition above is itself protected against macro expansion with the "[[ protect x end protect ]]" construct which is defined in Section \ref{sec:ElementaryMacros}. Without that protection, the left hand side of the definition above would be macro expanded from "[[ ( x ) ]]" to "[[ x ]]" so that the definition would define "[[ x ]]" to be equal to itself. Due to the minimal semantics convention, that would define "[[ x ]]" to be equal to "[[ bottom ]]".

\item "[[ protect optimized define value of newline x as x end define end protect ]]". This construct leaves its argument unaffected just like parentheses do; and it is macro defined in Section \ref{sec:Parentheses} just like parentheses are. But the newline construct is rendered differently. When talking about the construct, it is rendered as above. But when using it as in the formula "[[ 2 + newline 3 ]]" it affects line breaking. In the formula, the newline construct appears right after the plus sign. This effect is acheived by definitions in \cite{chores}. In \cite{chores}, the 'tex name' definition of the newline construct defines how the construct should be rendered when it occurs in the left hand side of a definition or some other context where the construct is talked about. Furthermore, the 'tex' definition of the newline construct in \cite{chores} defines how the newline construct should be rendered when it is used rather than talked about. Finally, in \cite{chores}, the 'tex' definition of the definition construct specifies that the left hand side of a definition should be rendered using the 'tex name' definition rather than the 'tex' definition.

\end{statements}

The definition of "[[ false ]]" above is an example of an introduction''. Formally, an introduction has exactly the same meaning as a definition. However, each implementation of Logiweb is supposed so contain a finite list of functions which have been hand-coded for efficiency. The nulary function "[[ false ]]" is one such function.

For each hand-coded function, the implementation must contain a definition for an equivalent function expressed solely using the reduction system in \ref{sec:ReductionSystem} plus quoting. When the implementation sees an introduction, it runs through the list of equivalent functions to see if the right hand side matches one of them. If a match is found then the introduced construct is translated into the associated hand-coded function. If no match is found then the introduction is treated as an ordinary definition. As long as implementors are careful to ensure equivalence between hand-coded functions and equivalent functions, this ensures portability of code between different implementations of Logiweb.

Matching of right hand sides against equivalent functions is quite strict: One may change names of variables and names of functions, but apart from that, an exact match is required. It is decidable (and fast to decide) whether two functions match.

\subsection{Booleans}

\begin{statements}

\item "[[ proclaim x Select y else z end select as "if" end proclaim ]]"

\item "[[ define value of Not x as If x then false else true end define ]]"

\item "[[ define value of x And y as x Select If y then true else false else If y then false else false end select end define ]]"

\item "[[ define value of x Or y as x Select If y then true else true else If y then true else false end select end define ]]"

\item "[[ define value of x Iff y as x Select If y then true else false else If y then false else true end select end define ]]"

\item "[[ define value of x TheBool as If x then true else false end define ]]"

\item "[[ define value of x Equal y as If x then newline If y then true else false else newline If y then false else x Head Equal y Head And x Tail Equal y Tail end define ]]"

\end{statements}

\subsection{Naturals}\label{sec:Naturals}

We shall refer to the \index{number, natural}\index{natural number}\intro{natural numbers} 0, 1, 2, and so on as \indexintro{naturals}. We shall say that a list "[[ b _ { 0 } Pair b _ { 1 } Pair ... Pair b _ { n } Pair true ]]" is an \index{representation, untagged}\indexintro{untagged representation} of the natural $\sum_{i=0}^{n} 2^i c_i$ where "[[ c _ { i } ]]" is zero or one when "[[ b _ { i } ]]" is true or false, respectively. When a list is used as an untagged representation of a natural, we shall refer to the list as an \index{natural, untagged}\indexintro{untagged natural}. The following functions apply to untagged naturals.

\begin{statements}

\item "[[ define value of Zero as true end define ]]"

\item "[[ define value of x NatPair y as If x And y then Zero else x TheBool Pair y end define ]]"

\item "[[ define value of x TheNat as If x then Zero else x Head NatPair x Tail TheNat end define ]]"

\item "[[ define value of One as false Pair Zero end define ]]"

\item "[[ define value of Two as true Pair One end define ]]"

\item "[[ define value of Three as false Pair One end define ]]"

\item "[[ define value of Four as true Pair Two end define ]]"

\item "[[ define value of Five as false Pair Two end define ]]"

\item "[[ define value of Six as true Pair Three end define ]]"

\item "[[ define value of Seven as false Pair Three end define ]]"

\item "[[ define value of Eight as true Pair Four end define ]]"

\item "[[ define value of Nine as false Pair Four end define ]]"

\item "[[ define value of Ten as true Pair Five end define ]]"

\item "[[ define value of Xor ( x , y , c ) as x Head Iff y Head Iff c end define ]]"

\item "[[ define value of Carry ( x , y , c ) as If x Head then y Head Or c else y Head And c end define ]]"

\item "[[ define value of Plus ( x , y , c ) as If x And y And c then Zero else Xor ( x , y , c ) NatPair Plus ( x Tail , y Tail , Carry ( x , y , c ) ) end define ]]"

\item "[[ define value of x Plus y as Plus ( x , y , true ) end define ]]"

\item "[[ define value of Borrow ( x , y , b ) as If x Head then y Head And b else y Head Or b end define ]]"

\item "[[ define value of Compare ( x , y , b ) as If x And y then b else Compare ( x Tail , y Tail , Borrow ( x , y , b ) ) end define ]]"

\item "[[ define value of x LT y as Compare ( y , x , false ) end define ]]"

\item "[[ define value of Minus ( x , y , b ) as If x And y then Zero else Xor ( x , y , b ) NatPair Minus ( x Tail , y Tail , Borrow ( x , y , b ) ) end define ]]"

\item "[[ define value of x Minus y as Minus ( x , y , true ) end define ]]"

\item "[[ define value of x Times y as If x then Zero else ( If x Head then Zero else y ) Plus ( true Pair x Tail Times y ) end define ]]"

\end{statements}

\subsection{Bottom}\label{sec:Bottom}

\begin{statements}

\item "[[ optimized define value of bottom as ( \ x . x ' x ) ' ( \ x . x ' x ) end define ]]"

Optimized bottom is a peculiar optimized function. Evaluation of the right hand side above takes forever. So the semantics of "[[ bottom ]]" is that it does not return a value. Optimized bottom is faithful to that: it never returns a value. What it does do is that it prints and error message and kills its caller. So the user can sit comfortably one step further away and watch the caller being killed.

One could suggest some bessermachen'' and suggest some sort of catcher which allows to test whether or not some computation results in a call to optimized bottom. That, however, will give grave portability problems and grave problems for reasoning about programs. What you need if you think of this bessermachen'' are the exceptions described in Section \ref{sec:TaggedValues}.

It should be noted that not only users can sit comfortably one step away and see a caller being killed by "[[ bottom ]]". Also computers can do that. In the Logiweb machine described in Section \ref{section:Interaction}, a handler could use its interface to the outside world to look into the machine itself and inspect the fate of a subordinate process.

\end{statements}

\section{Tagged values}\label{sec:TaggedValues}

\subsection{Tags}\label{sec:Tags}

\index{tagged value}\index{value, tagged}\intro{Tagged values} have form "[[ t LazyPair v ]]" where "[[ t ]]" is a \indexintro{tag} which identifies the type of the value and "[[ v ]]" represents the value itself.

Tags have form "[[ r Pair i ]]" where "[[ r ]]" and "[[ i ]]" are untagged naturals. We shall refer to "[[ r ]]" and "[[ i ]]" as the \indexintro{reference} and \indexintro{index} of the tag, respectively.

The reference of a tag is supposed to be either zero or to be the reference of a Logiweb page. The former case is used for the \index{predefined type}\index{type, predefined}\intro{predefined} types listed later. Individual users who want to introduce their own types should use tags of form "[[ r Pair i ]]" where "[[ r ]]" is the reference of a Logiweb page they have published.

The predefined types are: \index{Boolean type}\index{type, boolean}\intro{Booleans}, \index{integer type}\index{type, integer}\intro{integers}, \index{pair type}\index{type, pair}\intro{pairs}, \index{exception type}\index{type, exception}\intro{exceptions}, and \index{map type}\index{type, map}\intro{maps}. Maps are just arbitrary values with a tag on.

The tags of the predefined types are:

\begin{statements}

\item "[[ define value of BoolTag as Zero Pair Zero end define ]]"

\item "[[ define value of IntTag as Zero Pair One end define ]]"

\item "[[ define value of PairTag as Zero Pair Two end define ]]"

\item "[[ define value of ExTag as Zero Pair Three end define ]]"

\item "[[ define value of MapTag as Zero Pair Four end define ]]"

\end{statements}

\subsection{Tag querying}\label{sec:TagQuerying}

\begin{statements}

\item "[[ define value of x Tag as x Head Head TheNat Pair x Head Tail TheNat end define ]]"

\item "[[ define value of x BoolP as x Tag Equal BoolTag end define ]]"

\item "[[ define value of x IntP as x Tag Equal IntTag end define ]]"

\item "[[ define value of x PairP as x Tag Equal PairTag end define ]]"

\item "[[ define value of x ExP as x Tag Equal ExTag end define ]]"

\item "[[ define value of x MapP as x Tag Equal MapTag end define ]]"

\item "[[ define value of x ObjectP as Not ( x BoolP Or x IntP Or x PairP Or x ExP Or x MapP ) end define ]]"

\end{statements}

\subsection{Guards}

\begin{statements}

\item "[[ optimized define value of x is val : y as If x norm ExP then x else y end define ]]"

\item "[[ optimized define value of x .then. y as If x norm ExP then x else y end define ]]"

\item "[[ optimized define value of x is bool : y as x is val : y is val : If x norm BoolP then y else exception end define ]]"

\item "[[ optimized define value of x is int : y as x is val : y is val : If x norm IntP then y else exception end define ]]"

\item "[[ optimized define value of x is pair : y as x is val : y is val : If x norm PairP then y else exception end define ]]"

\item "[[ optimized define value of x is map : y as x is val : y is val : If x norm MapP then y else exception end define ]]"

\item "[[ optimized define value of x is object : y as x is val : y is val : If x norm ObjectP then y else exception end define ]]"

\end{statements}

\subsection{Normalization}\label{sec:Normalization}

\begin{statements}

\item "[[ optimized define value of x norm as newline

If x BoolP then x TheBool else newline

If x IntP then int ( x Tail ) else newline

If x PairP then x Tail Head :: x Tail Tail else newline

If x ExP then x Tail raise else newline

If x MapP then map ( x Tail ) else newline

x Tag Pair x Tail norm end define ]]"

\item "[[ optimized define value of norm x as x norm end define ]]"

\end{statements}

\subsection{Booleans}\label{sec:OperationsOnBooleans}

\begin{statements}

\item "[[ optimized define value of x boolp as x is val : x BoolP end define ]]"

\item "[[ optimized define value of if x then y else z as x is val : If norm x then y else z end define ]]"

\item "[[ optimized define value of .not. x as norm x is val : if x then false else true end define ]]"

\item "[[ optimized define value of notnot x as norm x is val : if x then true else false end define ]]"

\item "[[ optimized define value of x .and. y as If x norm then y norm else x norm end define ]]"

\item "[[ optimized define value of x .or. y as if x norm then true else y norm end define ]]"

\item "[[ optimized define value of x = y as norm x is val : y is val : equal1 ( x norm , y norm ) end define ]]"

\item "[[ define value of equal1 ( x , y ) as newline

if x boolp then x Equal y else newline

if x intp then x Equal y else newline

if x pairp then y pairp .and. x head = y head .and. x tail = y tail else newline

if x mapp then y mapp else newline

x Tag Equal y Tag .and. x Tail = y Tail end define ]]"

\item "[[ define value of x != y as norm x is val : y is val : .not. x = y end define ]]"

\item "[[ define value of x truep as x is val : x boolp .and. notnot x end define ]]"

\item "[[ define value of x falsep as x is val : x boolp .and. .not. x end define ]]"

\end{statements}

\subsection{Integers}\label{sec:Integers}

\begin{statements}

\item "[[ optimized define value of x intp as norm x is val : x IntP end define ]]"

\item "[[ define value of int ( x ) as TheInt ( x Head TheBool , x Tail TheNat ) end define ]]"

\item "[[ define value of PlusTag x as TheInt ( true , x ) end define ]]"

\item "[[ define value of MinusTag x as TheInt ( false , x ) end define ]]"

\item "[[ define value of x Sign as x Tail Head end define ]]"

\item "[[ define value of x Mag as x Tail Tail end define ]]"

\item "[[ optimized define value of + x as norm x is val : x is int : x end define ]]"

\item "[[ optimized define value of +x as + x end define ]]"

\end{statements}

\begin{statements}

\item "[[ define value of TheInt ( s , v ) as IntTag Pair ( s Or v ) Pair v end define ]]"

\item "[[ optimized define value of x + y as norm x is val : y is val : plus1 ( x norm , y norm ) end define ]]"

\item "[[ define value of plus1 ( x , y ) as x is int : y is int : plus2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]"

\item "[[ define value of plus2 ( s , t , x , y ) as

s Select ""; x>0

t Select ""; x>0, y>0

PlusTag x Plus y

else ""; x>0, y<0

x LT y Select ""; x>0, y<0, |x|<|y|

MinusTag y Minus x

else ""; x>0, y<0, |x|>|y|

PlusTag x Minus y end select end select

else ""; x<0

t Select ""; x<0, y>0

x LT y Select ""; x<0, y>0, |x|<|y|

PlusTag y Minus x

else ""; x<0, y>0, |x|>|y|

MinusTag x Minus y end select

else ""; x<0, y<0

MinusTag x Plus y end select end select end define ]]"

\end{statements}

\subsection{Integer subtraction}\label{sec:IntegerSubtraction}

\begin{statements}

\item "[[ optimized define value of - x as norm x is val : minus1 ( x norm ) end define ]]"

\item "[[ optimized define value of -x as - x end define ]]"

\item "[[ define value of minus1 ( x ) as x is int : minus2 ( x Sign , x Mag ) end define ]]"

\item "[[ define value of minus2 ( s , x ) as TheInt ( Not s , x ) end define ]]"

\item "[[ optimized define value of x - y as norm x is val : y is val : x + - y end define ]]"

\end{statements}

\subsection{Integer multiplication}\label{sec:IntegerMultiplication}

\begin{statements}

\item "[[ optimized define value of x * y as norm x is val : y is val : times1 ( x norm , y norm ) end define ]]"

\item "[[ define value of times1 ( x , y ) as x is int : y is int : times2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]"

\item "[[ define value of times2 ( s , t , x , y ) as TheInt ( s Iff t , x Times y ) end define ]]"

\end{statements}

\subsection{Integer comparison}\label{sec:IntegerComparison}

\begin{statements}

\item "[[ optimized define value of x < y as norm x is val : y is val : x is int : y is int : lt1 ( x norm , y norm ) end define ]]"

\item "[[ define value of lt1 ( x , y ) as lt2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]"

\item "[[ define value of lt2 ( s , t , x , y ) as

s Select ""; x>0

t Select ""; x>0, y>0

x LT y

else ""; x>0, y<0

false end select

else ""; x<0

t Select ""; x<0, y>0

true

else ""; x<0, y<0

y LT x end select end select end define ]]"

\item "[[ optimized define value of x > y as norm x is val : y is val : x is int : y is int : y < x end define ]]"

\item "[[ optimized define value of x <= y as norm x is val : y is val : x is int : y is int : .not. x > y end define ]]"

\item "[[ optimized define value of x >= y as norm x is val : y is val : x is int : y is int : .not. x < y end define ]]"

\end{statements}

\subsection{Integer construction}\label{sec:IntegerConstruction}

An integer like "[[ %% %1 %2 %3 ]]" can be expressed as an invisible zero followed by three suffix operators "[[ x %1 ]]", "[[ x %2 ]]", and "[[ x %3 ]]". The suffix operators multiply "[[ x ]]" by ten and add one, two, and three, respectively.

\begin{statements}

\item "[[ optimized define value of Base as norm PlusTag Ten end define ]]"

\item "[[ optimized define value of %% as norm PlusTag Zero end define ]]"

Invisible zero.

\item "[[ optimized define value of x %0 as norm x is val : x * Base end define ]]"

\item "[[ optimized define value of x %1 as norm x is val : x * Base + PlusTag One end define ]]"

\item "[[ optimized define value of x %2 as norm x is val : x * Base + PlusTag Two end define ]]"

\item "[[ optimized define value of x %3 as norm x is val : x * Base + PlusTag Three end define ]]"

\item "[[ optimized define value of x %4 as norm x is val : x * Base + PlusTag Four end define ]]"

\item "[[ optimized define value of x %5 as norm x is val : x * Base + PlusTag Five end define ]]"

\item "[[ optimized define value of x %6 as norm x is val : x * Base + PlusTag Six end define ]]"

\item "[[ optimized define value of x %7 as norm x is val : x * Base + PlusTag Seven end define ]]"

\item "[[ optimized define value of x %8 as norm x is val : x * Base + PlusTag Eight end define ]]"

\item "[[ optimized define value of x %9 as norm x is val : x * Base + PlusTag Nine end define ]]"

\item "[[ define value of 0 as norm %% %0 end define ]]"

\item "[[ define value of 1 as norm %% %1 end define ]]"

\item "[[ define value of 2 as norm %% %2 end define ]]"

\item "[[ define value of 3 as norm %% %3 end define ]]"

\item "[[ define value of 4 as norm %% %4 end define ]]"

\item "[[ define value of 5 as norm %% %5 end define ]]"

\item "[[ define value of 6 as norm %% %6 end define ]]"

\item "[[ define value of 7 as norm %% %7 end define ]]"

\item "[[ define value of 8 as norm %% %8 end define ]]"

\item "[[ define value of 9 as norm %% %9 end define ]]"

\end{statements}

\subsection{Logical operations on integers}

\begin{statements}

\item "[[ optimized define value of evenp ( x ) as norm x is val : x is int : x Mag Head TheBool end define ]]"

\item "[[ define value of oddp ( x ) as norm x is val : x is int : .not. evenp ( x ) end define ]]"

\item "[[ optimized define value of half ( x ) as norm x is val : x is int : norm If x Sign then PlusTag x Mag Tail else MinusTag ( x Plus One ) Mag Tail end define ]]"

\item "[[ define value of small ( x ) as norm x is val : norm x is int : -1 <= x .and. x <= 0 end define ]]"

\item "[[ define value of double ( b , i ) as norm b is val : i is val : b is bool : i is int : if b then 1 + 2 * i else 2 * i end define ]]"

\item "[[ optimized define value of lognot ( x ) as norm x is val : x is int : -1 - x end define ]]"

\item "[[ optimized define value of logior ( x , y ) as norm x is val : y is val : x is int : y is int : newline

if x = -1 then -1 else if y = -1 then -1 else newline

if x = 0 then y else if y = 0 then x else double ( oddp ( x ) .or. oddp ( y ) , logior ( half ( x ) , half ( y ) ) ) end define ]]"

\item "[[ optimized define value of logxor ( x , y ) as norm x is val : y is val : x is int : y is int : newline

if x = -1 then lognot ( y ) else if y = -1 then lognot ( x ) else newline

if x = 0 then y else if y = 0 then x else double ( oddp ( x ) != oddp ( y ) , logxor ( half ( x ) , half ( y ) ) ) end define ]]"

\item "[[ optimized define value of logand ( x , y ) as norm x is val : y is val : x is int : y is int : newline

if x = -1 then y else if y = -1 then x else newline

if x = 0 then 0 else if y = 0 then 0 else double ( oddp ( x ) .and. oddp ( y ) , logand ( half ( x ) , half ( y ) ) ) end define ]]"

\item "[[ optimized define value of logeqv ( x , y ) as norm x is val : y is val : x is int : y is int : lognot ( logxor ( x , y ) ) end define ]]"

\item "[[ optimized define value of lognand ( x , y ) as norm x is val : y is val : x is int : y is int : lognot ( logand ( x , y ) ) end define ]]"

\item "[[ optimized define value of lognor ( x , y ) as norm x is val : y is val : x is int : y is int : lognot ( logior ( x , y ) ) end define ]]"

\item "[[ optimized define value of logandc1 ( x , y ) as norm x is val : y is val : x is int : y is int : logand ( lognot ( x ) , y ) end define ]]"

\item "[[ optimized define value of logandc2 ( x , y ) as norm x is val : y is val : x is int : y is int : logand ( x , lognot ( y ) ) end define ]]"

\item "[[ optimized define value of logorc1 ( x , y ) as norm x is val : y is val : x is int : y is int : logior ( lognot ( x ) , y ) end define ]]"

\item "[[ optimized define value of logorc2 ( x , y ) as norm x is val : y is val : x is int : y is int : logior ( x , lognot ( y ) ) end define ]]"

\item "[[ optimized define value of logtest ( x , y ) as norm x is val : y is val : x is int : y is int : logand ( x , y ) != 0 end define ]]"

\item "[[ optimized define value of ash ( i , c ) as norm i is val : c is val : i is int : c is int : if c >= 0 then ash+ ( i , c ) else ash- ( i , - c ) end define ]]"

\item "[[ define value of ash+ ( i , c ) as norm i is val : c is val : i is int : c is int : if c = 0 then i else ash+ ( 2 * i , c - 1 ) end define ]]"

\item "[[ define value of ash- ( i , c ) as norm i is val : c is val : i is int : c is int : if c = 0 then i else ash- ( half ( i ) , c - 1 ) end define ]]"

\item "[[ optimized define value of logbitp ( x , i ) as norm x is val : i is val : x is int : i is int : if x < 0 then exception else oddp ( ash ( i , - x ) ) end define ]]"

\item "[[ optimized define value of logcount ( x ) as norm x is val : x is int : if x < 0 then logcount1 ( lognot ( x ) ) else logcount1 ( x ) end define ]]"

\item "[[ define value of logcount1 ( x ) as norm x is val : x is int : if x = 0 then 0 else logcount1 ( half ( x ) ) + if evenp ( x ) then 0 else 1 end define ]]"

\item "[[ optimized define value of integer-length ( x ) as norm x is val : x is int : if small ( x ) then 0 else 1 + integer-length ( half ( x ) ) end define ]]"

\end{statements}

\subsection{Vector operations}

A byte is an integer in the range 0..255. We shall represent sequences of bytes as \index{vector}\emph{vectors} as follows: Given a sequence of bytes, add the number "[[ 1 ]]" at the end of the sequence, then interpret the sequence little endian base 256. In that way, sequences of bytes are represented by cardinals (positive integers). As an example, the sequence "[[ << 65 ,, 66 >> ]]" is represented by the number "[[ 65 + 256 * 66 + 256 * 256 * 1 ]]".

Strings like "[[ name "AB" end name ]]" are treated as vectors. The value of "[[ name "AB" end name ]]" is "[[ 65 + 256 * 66 + 256 * 256 * 1 ]]" because A and B have unicode 65 and 66, respectively. Strings are encoded using UTF-8 so strings are always sequences of bytes even when characters in the strings have unicodes above 255.

If a number like "[[ 65 + 256 * 66 + 256 * 256 * 2 ]]" is interpreted as a vector, it represents the vector consisting of the bytes 65 and 66. Hence, when translating integers to vectors, the stop byte can have any, non-zero value.

We define the following functions on vectors:

\begin{statements}

\item "[[ vector ( x ) ]]". Normalize the vector (change the stop byte to a one-byte).

\item "[[ vector-suffix ( x , b ) ]]". Return the subvector beginning at byte number "[[ b ]]" (where the first byte is byte number zero): "[[ vector-suffix ( name "ABCD" end name , 2 ) = name "CD" end name ]]".

\item "[[ vector-prefix ( x , e ) ]]". Return the subvector ending before byte number "[[ e ]]": "[[ vector-prefix ( name "ABCD" end name , 2 ) = name "AB" end name ]]".

\item "[[ vector-subseq ( x , b , e ) ]]". Return the subvector beginning at "[[ b ]]" and ending before "[[ e ]]": "[[ vector-subseq ( name "ABCD" end name , 1 , 3 ) = name "BC" end name ]]".

\item "[[ vector-length ( x ) ]]". Return the length of the vector: "[[ vector-length ( name "ABCD" end name ) = 4 ]]".

\item "[[ vector-index ( x , i ) ]]". Return the i'th byte: "[[ vector-index ( name "ABCD" end name , 1 ) = 66 ]]".

\item "[[ eager define vector-head ( x ) as vector-index ( x , 0 ) end define ]]".

\item "[[ eager define vector-tail ( x ) as vector-suffix ( x , 1 ) end define ]]".

\end{statements}

We shall represent byte sequences in four ways:

\begin{description}

\item[byte*] A list of bytes.

\item[vector] An integer which encodes the list little endian base 256 with a stop byte at the end.

\item[bt] A \index{byte tree}\index{tree, byte}\emph{byte tree}, i.e.\ a structure built up from bytes and conses. To convert it to a sequence, scan the tree root to leaf, left to right, and collect all bytes found. Ignore anything which is not a byte.

\item[t] A \index{vector tree}\index{tree, vector}\emph{byte vector}, i.e.\ a structure built up from vectors and conses. To convert it to a sequence, scan the tree root to leaf, left to right, and append all vectors (integers) found. Ignore anything which is not a vector.

\end{description}

\noindent The following functions convert between the representations. Examples:

$\begin{array}{lll} "[ vector2byte* ( name "ABC" end name ) ]" & = & "[ << 65 ,, 66 ,, 67 >> ]" \\ "[ bt2byte* ( ( 65 :: 66 ) :: - 1 :: 256 :: true :: 67 :: false :: 68 ) ]" & = & "[ << 65 ,, 66 ,, 67 ,, 68 >> ]" \\ "[ bt2vector ( ( 65 :: 66 ) :: - 1 :: 256 :: true :: 67 :: false :: 68 ) ]" & = & "[ name "ABCD" end name ]" \\ "[ vt2byte* ( ( name "A" end name :: name "BC" end name ) :: - 1 :: name "" end name :: false :: name "D" end name ) ]" & = & "[ << 65 ,, 66 ,, 67 ,, 68 >> ]" \\ "[ vt2vector ( ( name "A" end name :: name "BC" end name ) :: - 1 :: name "" end name :: false :: name "D" end name ) ]" & = & "[ name "ABCD" end name ]" \\ \end{array}$

\noindent In the implementations, care is taken to make the functions tail recursive. Furthermore, whenever tail recursion had to favor either recursion in the head or in the tail of pairs, recursion in the tail has been favored. For that reason, the functions can handle very long lists without stack overflow. This is done at the cost of having to reverse lists occasionally.

\noindent The definitions read:

\begin{statements}

\item "[[ define value of vector-mask as norm %% %2 %5 %5 end define ]]"

\item "[[ optimized define value of vector-empty ( x ) as norm x is val : x <= vector-mask end define ]]"

\item "[[ define value of vector-head1 ( x ) as norm x is val : logand ( vector-mask , x ) end define ]]"

\item "[[ define value of vector-tail1 ( x ) as norm x is val : ash ( x , -8 ) end define ]]"

\item "[[ define value of vector-cons ( x , y ) as norm x is val : y is val : logior ( x , ash ( y , 8 ) ) end define ]]"

\item "[[ optimized define value of vector ( x ) as norm x is val : if vector-empty ( x ) then "" else vector-cons ( vector-head1 ( x ) , vector ( vector-tail1 ( x ) ) ) end define ]]"

\item "[[ optimized define value of vector-suffix ( x , b ) as norm x is val : b is val : if b <= 0 then vector ( x ) else vector-suffix ( vector-tail1 ( x ) , b - 1 ) end define ]]"

\item "[[ optimized define value of vector-prefix ( x , e ) as norm x is val : e is val : if vector-empty ( x ) .or. e <= 0 then "" else vector-cons ( vector-head1 ( x ) , vector-prefix ( vector-tail1 ( x ) , e - 1 ) ) end define ]]"

\item "[[ optimized define value of vector-subseq ( x , b , e ) as norm x is val : b is val : e is val : if b <= 0 then vector-prefix ( x , e ) else vector-subseq ( vector-tail1 ( x ) , b - 1 , e - 1 ) end define ]]"

\item "[[ optimized define value of vector-length ( x ) as norm x is val : if vector-empty ( x ) then 0 else 1 + vector-length ( vector-tail1 ( x ) ) end define ]]"

\item "[[ optimized define value of vector-index ( x , i ) as if i < 0 .or. vector-length ( x ) <= i then exception else vector-head1 ( vector-suffix ( x , i ) ) end define ]]"

\item "[[ optimized define value of vector2byte* ( x ) as norm x is val : vector2byte*1 ( x , true ) end define ]]"

\item "[[ define value of vector2byte*1 ( x , r ) as norm x is val : r is val : newline

if vector-empty ( x ) then reverse ( r ) else newline

vector2byte*1 ( vector-tail1 ( x ) , vector-head1 ( x ) :: r ) end define ]]"

\item "[[ optimized define value of bt2byte* ( x ) as norm x is val : reverse ( bt2byte*1 ( x , true ) ) end define ]]"

\item "[[ define value of bt2byte*1 ( x , r ) as norm x is val : r is val : newline

if x pairp then bt2byte*1 ( x tail , bt2byte*1 ( x head , r ) ) else newline

if x intp .and. 0 <= x .and. x <= vector-mask then x :: r else r end define ]]"

\item "[[ optimized define value of bt2vector ( x ) as norm x is val : revbyte*2vector ( bt2byte*1 ( x , true ) , name "" end name ) end define ]]"

\item "[[ define value of revbyte*2vector ( x , r ) as norm x is val : r is val : newline

if x atom then r else newline

revbyte*2vector ( x tail , vector-cons ( x head , r ) ) end define ]]"

Reverse the list "[[ x ]]" of bytes, revappend them to the vector "[[ r ]]", and return them as a vector.

\item "[[ define value of vector-revappend ( x , y ) as norm x is val : y is val : newline

if vector-empty ( x ) then y else newline

vector-revappend ( vector-tail1 ( x ) , vector-head1 ( x ) :: y ) end define ]]"

Convert the vector "[[ x ]]" to a sequence of bytes and revappend it to the sequence "[[ y ]]" of bytes.

\item "[[ optimized define value of vt2byte* ( x ) as norm x is val : reverse ( vt2byte*1 ( x , true ) ) end define ]]"

\item "[[ define value of vt2byte*1 ( x , r ) as norm x is val : r is val : newline

if x pairp then vt2byte*1 ( x tail , vt2byte*1 ( x head , r ) ) else newline

if x intp then vector-revappend ( x , r ) else r end define ]]"

\item "[[ optimized define value of vt2vector ( x ) as norm x is val : revbyte*2vector ( vt2byte*1 ( x , true ) , name "" end name ) end define ]]"

\end{statements}

\subsection{Division}

The division routines in the following return quotient/remainder pairs of form "[[ q :: r ]]" where "[[ q ]]" is the quotient and "[[ r ]]" is the remainder. When dividing the dividend "[[ x ]]" by the divisor "[[ y ]]", the resulting quotient/remainder pair satisfies "[[ x = q * y + r ]]". The differences between the various kinds of divisions lie in the direction in which the quotient is rounded and, hence, the possible interval for the remainder.

There is general agreement about how negative dividends "[[ x ]]" should be handled. But there is no similar agreement about the handling of negative divisors "[[ y ]]". For that reason, we simply proclaim division by negative numbers to be as undefined as division by zero.

We now define four division routines, "[[ floor ( x , y ) ]]", "[[ ceiling ( x , y ) ]]", "[[ truncate ( x , y ) ]]", and "[[ round ( x , y ) ]]", one for each kind of rounding defined by the IEEE floating point standard. These division routines raise an exception in case of division by zero or division by a negative number. The names of the division routines are inspired by Common Lisp, c.f.\ the Common Lisp Hyperspec, which is available on the World Wide Web.

We consider "[[ floor ( x , y ) ]]", which does rounding towards minus infinity, to be the most useful integer division routine, and introduce "[[ x div y ]]" and "[[ x mod y ]]" to denote the quotient and remainder, respectively, returned by "[[ floor ( x , y ) ]]".

To define division, we first define restricted forms of division "[[ floor1 ( x , y ) ]]", "[[ ceiling1 ( x , y ) ]]", and "[[ round1 ( x , y ) ]]" which can handle positive arguments. We also introduce a construct "[[ reverse quotient ( p ) ]]" for changing the sign of both quotient and remainder in a quotient/remainder pair. The restricted division routines may loop indefinitely when the input values are out of range.

\begin{statements}

\item "[[ define value of floor1 ( x , y ) as newline

if x < y then 0 :: x else newline

LET floor1 ( x , 2 * y ) BE z IN newline

if z tail < y then 2 * z head :: z tail else 2 * z head + 1 :: z tail - y end define ]]"

Divide the natural "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards minus infinity.

\item "[[ define value of ceiling1 ( x , y ) as newline

LET floor1 ( x , y ) BE z IN newline

if z tail = 0 then z else z head + 1 :: z tail - y end define ]]"

Divide the positive integer "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards plus infinity and return af pair "[[ q :: r ]]" of quotient "[[ d ]]" and remainder "[[ r ]]".

\item "[[ define value of round1 ( x , y ) as newline

LET floor1 ( x , y ) BE z IN newline

if z tail * 2 < y then z else newline

if z tail * 2 > y then z head + 1 :: z tail - y else newline

if evenp ( z head ) then z else newline z head + 1 :: z tail - y end define ]]"

Divide the natural "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards nearest/even, c.f.\ the IEEE floating point standard or the Common Lisp Hyperspec.

\item "[[ define value of reverse quotient ( p ) as - p head :: - p tail end define ]]"

Negate both quotient and remainder of a quotient/remainder pair.

\item "[[ optimized define value of truncate ( x , y ) as newline

if y <= 0 then exception else newline

if 0 <= x then floor1 ( x , y ) else newline

reverse quotient ( floor1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards zero.

\item "[[ optimized define value of floor ( x , y ) as newline

if y <= 0 then exception else newline

if 0 <= x then floor1 ( x , y ) else newline

reverse quotient ( ceiling1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards minus infinity.

\item "[[ optimized define value of ceiling ( x , y ) as newline

if y <= 0 then exception else newline

if 0 < x then ceiling1 ( x , y ) else newline

reverse quotient ( floor1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards plus infinity.

\item "[[ optimized define value of round ( x , y ) as newline

if y <= 0 then exception else newline

if 0 < x then round1 ( x , y ) else newline

reverse quotient ( round1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards nearest/even, c.f.\ the IEEE floating point standard or the Common Lisp Hyperspec.

\item "[[ optimized define value of x div y as floor ( x , y ) head end define ]]"

\item "[[ optimized define value of x mod y as floor ( x , y ) tail end define ]]"

\end{statements}

\subsection{Pairs}\label{sec:Pairs}

\begin{statements}

\item "[[ optimized define value of x pairp as norm x is val : x PairP end define ]]"

\item "[[ define value of a atom as norm a is val : norm a is val : .not. a pairp end define ]]"

\item "[[ optimized define value of x :: y as norm x is val : y is val : PairTag Pair x norm Pair y norm end define ]]"

\item "[[ optimized define value of x head as norm x is val : if x atom then x norm else x norm Tail Head end define ]]"

\item "[[ optimized define value of x tail as norm x is val : if x atom then x norm else x norm Tail Tail end define ]]"

\item "[[ define value of reverse ( x ) as norm x is val : revappend ( x , true ) end define ]]"

\item "[[ define value of revappend ( x , y ) as norm x is val : y is val : newline

if x atom then y else revappend ( x tail , x head :: y ) end define ]]"

\item "[[ define value of nth ( n , x ) as norm n is val : x is val : newline

if n <= 0 then x head else nth ( n - 1 , x tail )

end define ]]"

\item "[[ eager define length ( x ) as length1 ( x , 0 ) end define ]]".

Compute length of list.

\item "[[ eager define length1 ( x , r ) as if x atom then r else length1 ( x tail , r + 1 ) end define ]]".

Compute the sum of the integer "[[ r ]]" and the length of the list "[[ x ]]".

\item "[[ eager define list-prefix ( l , n ) as newline

if n = 0 then true else l head :: list-prefix ( l tail , n - 1 ) end define ]]"

Return the first "[[ n ]]" elements of the list "[[ l ]]".

\item "[[ eager define list-suffix ( l , n ) as newline

if n = 0 then l else list-suffix ( l tail , n - 1 ) end define ]]"

Remove the first "[[ n ]]" elements from the list "[[ l ]]".

\end{statements}

\subsection{Exceptions}\label{sec:Exceptions}

\begin{statements}

\item "[[ optimized define value of x raise as norm x is val : ExTag Pair x norm end define ]]"

\item "[[ optimized define value of exception as norm true raise end define ]]"

\item "[[ optimized define value of catch ( x ) as Catch ( x norm ) end define ]]"

\item "[[ optimized define value of x catch as Catch ( x norm ) end define ]]"

\item "[[ define value of Catch ( x ) as If x ExP then true :: x Tail else false :: x end define ]]"

\end{statements}

\subsection{Maps}\label{sec:TaggedMaps}

\begin{statements}

\item "[[ optimized define value of x mapp as norm x is val : x MapP end define ]]"

\item "[[ optimized define value of map ( x ) as MapTag LazyPair x end define ]]"

\item "[[ optimized define value of x catching maptag as map ( x norm ) end define ]]"

\item "[[ optimized define value of x maptag as norm x is val : x catching maptag end define ]]"

\item "[[ optimized define value of x untag as norm x is val : x is map : x Tail norm end define ]]"

\item "[[ optimized define value of x apply y as norm x is val : y is val : x is map : y is map : map ( x Tail ' y Tail ) end define ]]"

\item "[[ optimized define value of x root as norm x is val : x is map : x Tail TheBool end define ]]"

\end{statements}

\subsection{Objects}\label{sec:Objects}

\begin{statements}

\item "[[ optimized define value of x objectp as norm x is val : x ObjectP end define ]]"

\item "[[ optimized define value of object ( x ) as norm x is val : Object ( x head head , x head tail , x tail ) end define ]]"

\item "[[ define value of Object ( x , y , z ) as x is int : y is int : z is val : if x < 0 .or. y < 0 .or. x = 0 .and. y <= %% %4 then exception else x head head Mag Pair x head tail Mag Pair x tail end define ]]"

\item "[[ optimized define value of destruct ( x ) as norm x is val : x is object : ( ( PlusTag ( x Head Head ) :: PlusTag ( x Head Tail ) ) :: x Tail ) norm end define ]]"

\end{statements}

\section{Evaluation}

\subsection{Let construct}

"[[ optimized define value of LET x BE y as x is val : y ' x end define ]]"

"[[ proclaim x IN y as "lambda" end proclaim ]]"

\subsection{Simple accessors}

\begin{statements}

\item "[[ define value of x zeroth as norm x is val : x head end define ]]"

\item "[[ define value of x first as norm x is val : x tail zeroth end define ]]"

\item "[[ define value of x second as norm x is val : x tail first end define ]]"

\item "[[ define value of x third as norm x is val : x tail second end define ]]"

\item "[[ define value of x fourth as norm x is val : x tail third end define ]]"

\item "[[ define value of x fifth as norm x is val : x tail fourth end define ]]"

\item "[[ define value of x sixth as norm x is val : x tail fifth end define ]]"

\item "[[ define value of x seventh as norm x is val : x tail sixth end define ]]"

\item "[[ define value of x eighth as norm x is val : x tail seventh end define ]]"

\item "[[ define value of x ninth as norm x is val : x tail eighth end define ]]"

\end{statements}

\subsection{Representation of terms}\label{sec:RepresentationOfTerms}

Section \ref{sec:Proclamations} proclaimed "[[ quote x end quote ]]" to denote \indexintro{quoting}. The value of "[[ quote x end quote ]]" is a structure which represents the term "[[ x ]]". As an example, the value of "[[ quote u + 2 end quote ]]" represents the plus construct applied to the "[[ u ]]" construct and the "[[ 2 ]]" construct.

As mentioned in Section \ref{sec:AspectDeclarations}, every Logiweb construct is represented by a \indexintro{reference} and an \indexintro{index}. The reference is a world-wide unique natural number which identifies the \index{page, home}\indexintro{home page} of the construct, i.e.\ the page on which the construct is introduced. The index is a natural number which distinguishes the construct from the other constructs introduced on that home page.

The value of "[[ quote u + 2 end quote ]]" has form "[[[ ( r :: i :: d ) :: x :: y :: true ]]]" where "[[ r ]]" and "[[ i ]]" are the reference and index, respectively, of the plus construct. "[[ x ]]" and "[[ y ]]" represent the terms "[[ u ]]" and "[[ 2 ]]" respectively. "[[ d ]]" is \index{information, debugging}\index{debugging information}.

The purpose of debugging information is to allow users to locate the source of errors. When a user receives an error message saying e.g.\ that a particular proof is in error, then the error message is likely to contain a term from the macro expanded version of the page. On the present page, the debugging information of a term indicates the location a term had before macro expansion. Users have control over the debugging information through the unpacking and macro expansion machinery.

On the present page, the debugging information of a term has form "[[[ ( p _ { n } :: --- :: p _ { 1 } :: r prime :: true ) :: true ]]]" where "[[ r prime ]]" is the reference of the page on which the term occurs and "[[ p _ { n } ,, ... ,, p _ { 1 } ]]" indicate that before macro expansion, the term was subtree number "[[ p _ { n } ]]" of subtree number "[[ p _ { n - 1 } ]]" and so on of the root of the page.

Strings are represented in a particular way in that they have form "[[[ ( r :: i :: d ) :: true ]]]" where "[[ r ]]" is zero and "[[ i ]]" is a natural number which represents the string. "[[ i ]]" is constructed thus: write the string as a sequence of bytes using Unicode and UTF-8 encoding (a \indexintro{byte} is a natural number between 0 and 255, inclusive). Then add a byte with value "[[ 1 ]]" at the end. Finally, convert the sequence of bytes to a natural number using little endian radix 256 representation.

On many occasions, there is a need to assign aspects to a page. As an example, Section \ref{sec:Verification} assigns a claim' aspect to the present page. As another example, Section \ref{sec:MacroExpansion} assigns a macro' aspect to the present page. Formally, definitions can only assign aspects to constructs and not to pages. That problem is solved by the convention that every page has a \index{construct, page}\indexintro{page construct} which represents the page. The page construct of a page has index zero and aspects of the page construct should be interpretted as aspects of the page. As examples, the "[[ pyk ]]" and "[[ tex name ]]" aspects of a page symbol define the name of the page expressed in pyk and \TeX, respectively.

The following constructs allows to access the reference, index, and debugging information of a term "[[ x ]]"

\begin{statements}

\item "[[ define value of x ref as norm x is val : x head head end define ]]"

\item "[[ define value of x idx as norm x is val : x head tail head end define ]]"

\item "[[ define value of x debug as norm x is val : x head tail tail end define ]]"

\end{statements}

\subsection{Tree equality}

\begin{statements}

\item "[[ define value of x t= y as norm x is val : y is val : x ref = y ref .and. x idx = y idx .and. x tail t=* y tail end define ]]" True if the terms "[[ x ]]" and "[[ y ]]" are equal modulo differences in debugging information. As an example, "[[ quote z end quote = quote z end quote ]]" is false because the two instances of "[[ z ]]" occur different places on the page whereas "[[ quote z end quote t= quote z end quote ]]" because the "[[ %% t= %% ]]" operation disregards debugging information.

\item "[[ define value of x t=* y as norm x is val : y is val : if x atom then y atom else if y atom then false else x head t= y head .and. x tail t=* y tail end define ]]" Coordinatewise application of "[[ u t= v ]]" to the lists "[[ x ]]" and "[[ y ]]" of terms.

\item "[[ define value of x r= y as norm x is val : y is val : x ref = y ref .and. x idx = y idx end define ]]" True if the roots of terms "[[ x ]]" and "[[ y ]]" are equal modulo differences in debugging information.

\item "[[ define value of lookup ( x , s , d ) as norm x is val : s is val : d is val : if s atom then d else if x t= s head head then s head tail else lookup ( x , s tail , d ) end define ]]" Look up the term "[[ x ]]" in the stack "[[ s ]]". A \indexintro{stack} is an association list which associates terms to values. When the term "[[ x ]]" is not found in the stack "[[ s ]]", the default "[[ d ]]" is returned.

\item "[[ define value of zip ( x , y ) as norm x is val : y is val : newline

if x atom .or. y atom then true else newline

( x head :: y head ) :: zip ( x tail , y tail ) end define ]]" Zip the list "[[ x ]]" of terms and the list "[[ y ]]" of values into a stack (may of course be used for arbitrary lists).

\end{statements}

\subsection{Arrays}

\begin{statements}

\item "[[ define value of a [[ i ]] as norm a is val : i is val : i is int : array1 ( a , i , 0 ) end define ]]"

\item "[[ define value of array1 ( a , i , x ) as norm a is val : i is val : x is val : i is int : x is int : newline

if a atom then true else newline

if a head intp then if i = a head then a tail else true else newline

array1 ( if logbitp ( x , i ) then a tail else a head , i , x + 1 )

end define ]]"

\item "[[ define value of a [[ i -> v ]] as norm a is val : i is val : v is val : i is int : array2 ( a , i , v , 0 ) end define ]]"

\item "[[ define value of array2 ( a , i , v , x ) as norm a is val : i is val : v is val : x is val : i is int : x is int : newline

if a atom then array3 ( i , v ) else newline

if a head intp then newline

if i = a head then newline

array3 ( i , v ) else newline

array5 ( a head , a tail , i , v , x ) else newline

if logbitp ( x , i ) then newline

array4 ( a head , array2 ( a tail , i , v , x + 1 ) ) else newline

array4 ( array2 ( a head , i , v , x + 1 ) , a tail )

end define ]]"

\item "[[ define value of array3 ( i , v ) as norm i is val : v is val : i is int : if v = true then true else i :: v end define ]]"

";\item "[[ define value of array4 ( a , b ) as norm a is val : b is val : if a = true .and. b = true then true else a :: b end define ]]"

\item "[[ define value of array4 ( a , b ) as norm a is val : b is val : newline

if a atom then newline

if b atom then true else if b head intp then b else a :: b else newline

if b atom .and. a head intp then a else a :: b end define ]]"

\item "[[ define value of array5 ( i , v , j , w , x ) as norm i is val : v is val : j is val : w is val : x is val : i is int : j is int : x is int : newline

if logbitp ( x , i ) then newline

if logbitp ( x , j ) then newline

true :: array5 ( i , v , j , w , x + 1 ) else newline

( j :: w ) :: ( i :: v ) else newline

if logbitp ( x , j ) then newline

( i :: v ) :: ( j :: w ) else newline

array5 ( i , v , j , w , x + 1 ) :: true end define ]]"

\item "[[ define value of a [[ i => v ]] as norm a is val : i is val : v is val : if i atom then v else a [[ i head -> a [[ i head ]] [[ i tail => v ]] ]] end define ]]"

\end{statements}

\subsection{Evaluator}

\begin{statements}

\item "[[ define value of eval ( t , s , c ) as norm t is val : s is val : c is val : newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if r = 0 then i maptag else newline

if i = 0 then if r = c [[ 0 ]] then c maptag else c [[ c [[ 0 ]] ]] [[ "cache" ]] [[ r ]] maptag else newline

LET c [[ r ]] [[ "code" ]] [[ i ]] BE f IN newline

if f mapp then eval1 ( f , t tail , s , c ) else newline

if f = true then lookup ( t , s , map ( true ) ) else newline

if f = 1 then t first maptag else newline

map ( \ t . \ s . \ c . \ x . eval ( t second , ( t first :: map ( x ) ) :: s , c ) Tail ) apply t maptag apply s maptag apply c maptag

end define ]]"

\item "[[ define value of eval1 ( f , t , s , c ) as norm f is val : t is val : s is val : c is val : f is map : newline

if t atom then f else newline

eval1 ( f apply eval ( t head , s , c ) , t tail , s , c ) end define ]]"

\end{statements}

\subsection{Debugging aids}

\begin{statements}

\item "[[ optimized define value of spy ( x ) as norm x is val : "spy" end define ]]"

\item "[[ optimized define value of trace ( x ) as norm x is val : "trace" end define ]]"

\item "[[ optimized define value of print ( x ) as norm x is val : "print" end define ]]"

\item "[[ optimized define value of timer ( x ) as norm x is val : "timer" end define ]]"

\end{statements}

"[[ spy ( x ) ]]" is faithful to the definition above in that it discards "[[ x ]]" and returns "[[ "spy" ]]". As a side effect, however, it sets a variable named *spy* to the value of "[[ x ]]". It is possible to inspect that variable in several ways: One may ask the pyk compiler to print it out using the spy flag. Or one may use the quit flag to enter a read-eval-print loop in which one may issue commands like (spy), (spycd $\ldots$), (spyls $\ldots$), (spy/), (spy..), and (spypwd) to navigate and inspect the value of the *spy* variable. The *spy* variable is set by all test constructs so that if a test case makes the computer loop indefinitely then one has a chance of finding out which one by inspection of the *spy* variable.

"[[ trace ( x ) ]]" is like "[[ spy ( x ) ]]" but prints out the value of "[[ x ]]" to standard output. To get output from a "[[ trace ( x ) ]]", the construct has to be executed, which may happen during testing, macro expansion, custom unpacking, or custom rendering. The easiest way to get output from trace is to include it in a test construct.

"[[ print ( x ) ]]" is like "[[ trace ( x ) ]]" but prints "[[ x ]]" without newlines and indentation.

"[[ timer ( x ) ]]" returns the string timer'' and is thus easy to recognize from the other ones. The timer construct is supposed to be used as the "[[ x ]]" in the "[[ x .then. y ]]" construct which discards "[[ x ]]" and returns "[[ y ]]". Whenever "[[ timer ( x ) ]]" is evaluated, the timer associated with "[[ x ]]" starts counting. If no timer is associated with "[[ x ]]", then one is created. The timer counts until a call of "[[ timer ( y ) ]]" which causes the timer associated with "[[ x ]]" to stop and the one associated with "[[ y ]]" to start counting. Just before the pyk compiler exits, it prints the values of all timers except the one associated with "[[ true ]]". Hence, "[[ timer ( true ) ]]" effectively stops counting. Note that the active timer keeps counting until the timer values are reported.

\subsection{Verification}\label{sec:Verification}

\begin{statements}

\item "[[ define claim of base as test1 end define ]]"

\item "[[ define value of x &c y as \ c . x ' c .and. y ' c end define ]]"

\item "[[ define value of test1 as \ c . test2 ( c ) end define ]]"

\item "[[ define value of test2 ( c ) as norm c is val : newline

LET test3 ( c [[ c [[ 0 ]] ]] [[ "expansion" ]] , c ) catch BE p IN newline

if p tail != true then p tail else newline

if p head then quote exception end quote else true

end define ]]"

\item "[[ define value of test3 ( t , c ) as norm t is val : c is val : newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if r = 0 .or. i = 0 then true else newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "claim" ]] BE d IN newline

if d pairp then ( eval ( d third , true , c ) apply ( t :: c :: true ) maptag ) untag else newline

if c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "definition" ]] != true then true else test3* ( t tail , c ) end define ]]"

\item "[[ define value of test3* ( t , c ) as norm t is val : c is val : if t atom then true else test3 ( t head , c ) .and. test3* ( t tail , c ) end define ]]"

\item "[[ define value of make math x end math as norm x is val : ( name quote math x end math end quote end name ref :: name quote math x end math end quote end name idx :: x debug ) :: x :: true end define ]]"

\item "[[ define claim of ttst u end test as \ x . ttst1 ( x ) end define ]]"

\item "[[ define value of ttst1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE c IN spy ( t ) .then. if eval ( t first , true , c ) untag catch = false :: true then true else make math t end math end define ]]"

\item "[[ define claim of ftst u end test as \ x . ftst1 ( x ) end define ]]"

\item "[[ define value of ftst1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE c IN spy ( t ) .then. if eval ( t first , true , c ) untag catch = false :: false then true else make math t end math end define ]]"

\item "[[ define claim of etst u ; v end test as \ x . etst1 ( x ) end define ]]"

\item "[[ define value of etst1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE c IN spy ( t ) .then. if eval ( t first , true , c ) untag catch = eval ( t second , true , c ) untag catch then true else make math t end math end define ]]"

\item "[[ ttst true end test ]]"

\item "[[ ftst false end test ]]"

\item "[[ etst 2 ; 2 end test ]]"

\item "[[ etst 2 raise ; 2 raise end test ]]"

\end{statements}

\subsection{Idiosyncrasies}

Logiweb reacts in a predictable way to definitions, even if they are stated foolishly:

\begin{statements}

\item "[[ value define testfunc1 ( x ) as x + 3 end define ]]" This is an ordinary definition: "[[ etst testfunc1 ( 2 ) ; 5 end test ]]".

\item "[[ value define testfunc2 ( x , x ) as x end define ]]" When parameters are repeated, the first one is used: "[[ etst testfunc2 ( 2 , 3 ) ; 2 end test ]]". In the codex, the definition is recorded as it is: "[[ ttst self [[ quote testfunc2 ( 2 , 3 ) end quote ref ]] [[ "codex" ]] [[ quote testfunc2 ( 2 , 3 ) end quote ref ]] [[ quote testfunc2 ( 2 , 3 ) end quote idx ]] [[ 0 ]] [[ "value" ]] t= hide quote value define testfunc2 ( x , x ) as x end define end quote end hide end test ]]".

\item "[[ value define testfunc3 as 2 end define ]]" and "[[ value define testfunc3 as 3 end define ]]" When a definition is stated more than once, then the rightmost one counts: "[[ etst testfunc3 ; 3 end test ]]". The codex always contains the definition that counts.

\item "[[ value define testfunc4 as quote value define testfunc4 as 2 end define end quote end define ]]" When a page is harvested, all functions that occur inside other functions are disregarded: "[[ ttst testfunc4 t= name hide quote value define testfunc4 as 2 end define end quote end hide end name end test ]]". Without the use of "[[ name hide x end hide end name ]]" above, the definition of "[[ testfunc4 ]]" inside the test case would override the first definition of "[[ testfunc4 ]]".

\item "[[ value define testfunc5 ( x ) as y end define ]]" Unbound variables equal "[[ true ]]": "[[ etst testfunc5 ( 2 ) ; true end test ]]". "[[ y ]]" is a variable because its root has no value definition: "[[ etst self [[ quote y end quote ref ]] [[ "code" ]] [[ quote y end quote idx ]] ; true end test ]]"

\item "[[ value define testfunc6 ( 2 ) as 2 end define ]]" One may foolishly use non-variables as parameters, but it is impossible to get access to their values since their value definitions takes precedence over their dynamic bindings: "[[ etst testfunc6 ( 3 ) ; 2 end test ]]"

\item "[[ value define testfunc7 ( x _ { 4 } ) as x _ { 4 } + 3 end define ]]" Compound variables work: "[[ etst testfunc7 ( 2 ) ; 5 end test ]]". The variable "[[ x _ { 4 } ]]" consists of a binary subscript operator applied to "[[ x ]]" and "[[ 4 ]]". "[[ x _ { 4 } ]]" is a variable because the subscript operator has no value definition. When deciding whether or not a term is a variable, only the root of the term matters. The fact that "[[ 4 ]]" does have a value definition has no influence here.

\item "[[ value define testfunc8 ( x _ { 2 + 2 } , x _ { 4 } ) as x _ { 2 + 2 } + x _ { 4 } end define ]]" "[[ x _ { 2 + 2 } ]]" and "[[ x _ { 4 } ]]" are distinct variables: "[[ etst testfunc8 ( 2 , 3 ) ; 5 end test ]]". "[[ x _ { 2 + 2 } ]]" and "[[ x _ { 4 } ]]" are distinct variables because they are distinct trees: "[[ etst quote x _ { 2 + 2 } end quote t= quote x _ { 4 } end quote ; false end test ]]". The fact that "[[ 2 + 2 = 4 ]]" has no influence here.

\end{statements}

\section{Macro expansion}\label{sec:MacroExpansion}

\subsection{Macro expansion engine}

\begin{statements}

\item "[[ define macro of base as macro1 end define ]]"

\item "[[ define value of macro1 as \ c . macro2 ( c ) end define ]]"

\item "[[ define value of macro2 ( c ) as norm c is val : newline

macro3 ( c [[ c [[ 0 ]] ]] [[ "body" ]] , macrostate0 , c ) end define ]]"

\item "[[ define value of macro3 ( t , s , c ) as norm t is val : s is val : c is val : newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if r = 0 then t else newline

if i = 0 then t else newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "macro" ]] BE d IN newline

if d = true then t head :: macro3* ( t tail , s , c ) else newline

( eval ( d third , true , c ) apply ( t :: s :: c :: true ) maptag ) untag end define ]]"

\item "[[ define value of macro3* ( t , s , c ) as norm t is val : s is val : c is val : newline

if t atom then true else

macro3 ( t head , s , c ) :: macro3* ( t tail , s , c )

end define ]]"

\item "[[ define value of macro4 ( x ) as norm x is val : macro3 ( x zeroth , x first , x second ) end define ]]"

\item "[[ define value of macrostate0 as norm map ( \ x . macro4 ( x ) ) :: true end define ]]"

\item "[[ define value of stateexpand ( t , s , c ) as norm t is val : s is val : c is val : ( s head apply ( t :: s :: c :: true ) maptag ) untag end define ]]"

\item "[[ define value of stateexpand* ( t , s , c ) as norm t is val : s is val : c is val : newline

if t atom then true else newline

stateexpand ( t head , s , c ) :: stateexpand* ( t tail , s , c ) end define ]]"

\end{statements}

\subsection{Backquoting}

\begin{statements}

\item "[[ define value of substitute ( r , t , s ) as norm r is val : t is val : s is val : newline

LET lookup ( t , s , true ) BE d IN newline

if d = true then ( t ref :: t idx :: r debug ) :: substitute* ( r , t tail , s ) else d end define ]]" Replace subterms of "[[ t ]]" according to the stack "[[ s ]]". Set the debugging information of nodes taken from "[[ t ]]" to the debugging information of the root of "[[ r ]]"

\item "[[ define value of substitute* ( r , t , s ) as norm r is val : t is val : s is val : newline

if t atom then true else newline

substitute ( r , t head , s ) :: substitute* ( r , t tail , s ) end define ]]" Coordinatwise application of substitute to the elements of the list "[[ t ]]".

\item "[[ define value of expand ( d , x ) as norm d is val : x is val : newline

LET x zeroth BE t IN LET zip ( d first tail , t tail ) BE s IN newline

stateexpand ( substitute ( t , d second , s ) , x first , x second ) end define ]]"

"[[ x ]]" is supposed to have form "[[ t :: s :: c :: true ]]". Expand the term "[[ t ]]" accoding the the macro definition "[[ d ]]", then macro expand the result as specified by "[[ x ]]". The macro definition is supposed to have form "[[ hide macro define x as y end define end hide ]]" where the root of "[[ x ]]" equals the root of "[[ t ]]".

\end{statements}

\subsection{Elementary macros}\label{sec:ElementaryMacros}

\begin{statements}

\item "[[ protect define macro of protect u end protect as \ x . x zeroth first end define end protect ]]"

The "[[ protect x end protect ]]" construct protects "[[ x ]]" against macro expansion. During macro expansion, the protection construct itself disappears. Note that the protection construct is used to protect the definition itself. Otherwise the left hand side of the definition would be macro expanded!

\item "[[ protect define macro of Macro define u as v end define as \ x . Macrodefine ( x ) end define end protect ]]"

The "[[ hide Macro define u as v end define end hide ]]" construct macro expands into "[[ hide protect define macro of u as v end define end protect end hide ]]". Thus it allows to state a macro definition which is itself protected against macro definition.

\item "[[ define value of Macrodefine ( x ) as norm x is val : newline

if x = true then quote true end quote else newline

LET x zeroth BE t IN newline

LET t first BE u IN LET t second BE v IN newline

LET ( quote u end quote :: u ) :: ( quote v end quote :: v ) :: true BE s IN newline

substitute ( t , quote protect define macro of u as v end define end protect end quote , s ) end define ]]"

This function performs the actual work of the "[[ hide Macro define u as v end define end hide ]]" macro. If "[[ x ]]" equals "[[ true ]]" then we are probably at a stage of codification where the argument has not yet get a sensible value. In this case just return a valid term. Otherwise, the argument "[[ x ]]" is supposed to have form "[[ t :: s :: c :: true ]]" where "[[ t ]]" is the term to be expanded, "[[ s ]]" is the macro state, and "[[ c ]]" is the cache of the page on which that term occurs. "[[ Macrodefine ( x ) ]]" does not need the state and cache but extracts the term "[[ t ]]" from "[[ x ]]". The term has form "[[ hide Macro define u as v end define end hide ]]" where "[[ u ]]" and "[[ v ]]" are the actual left and right hand sides of the macro definition. "[[ Macrodefine ( x ) ]]" extracts these two terms end forms a stack "[[ s ]]" which maps the variables "[[ u ]]" and "[[ v ]]" to their respective values. Then "[[ Macrodefine ( x ) ]]" calls "[[ substitute ( t , quote --- end quote , s ) ]]" to construct "[[ hide protect define macro of u as v end define end protect end hide ]]". The debugging information of the latter is set to the debugging information of the original term "[[ t ]]" so that one can locate where the macro expanded term came from.

\item "[[ Macro define macro define u as v end define as \ x . macrodefine ( x ) end define ]]"

This construct allows to state simple macro definitions in which a left hand side is macro expanded into a right hand side by simple substitution.

\item "[[ define value of macrodefine ( x ) as norm x is val : newline

LET x zeroth BE t IN newline

LET t first BE u IN newline

LET ( quote t end quote :: t ) :: ( quote u end quote :: u ) :: true BE s IN newline

substitute ( t , quote define macro of u as \ x . expand ( quote t end quote , x ) end define end quote , s ) end define ]]"

This construct is similar to "[[ Macrodefine ( x ) ]]".

\item "[[ Macro define self as \ x . makeself ( x ) end define ]]" The "[[ self ]]" construct expands into the page symbol of the page on which the "[[ self ]]" construct occurs.

\item "[[ define value of makeself ( x ) as norm x is val : newline

LET x zeroth BE t IN LET x second BE c IN newline

LET t debug BE d IN LET c [[ 0 ]] BE r IN newline

( ( r :: 0 :: d ) :: true ) end define ]]"

The "[[ makeself ( x ) ]]" extracts the term "[[ t ]]" of form "[[ self ]]" as well as the cache "[[ c ]]" of the page on which "[[ self ]]" occurs. Then "[[ makeself ( x ) ]]" extracts the debugging information "[[ d ]]" from "[[ t ]]" and extracts the reference "[[ r ]]" of the page on which "[[ self ]]" occurs. Finally, "[[ makeself ( x ) ]]" constructs a tree with reference "[[ r ]]", index "[[ 0 ]]", debugging information "[[ d ]]", and no subtrees.

\item "[[ Macro define root protect u end protect as \ x . rootprotect ( x ) end define ]]"

The "[[ root protect u end protect ]]" construct protects the root of the term "[[ u ]]" against macro expansion but does allow the subtrees of "[[ u ]]" to be expanded.

\item "[[ define value of rootprotect ( x ) as norm x is val : newline

LET x zeroth BE t IN LET t first BE u IN newline

LET u ref BE r IN LET u idx BE i IN LET t debug BE d IN newline

( r :: i :: d ) :: stateexpand* ( u tail , x first , x second ) end define ]]"

\end{statements}

\subsection{Definition macros}

\begin{statements}

\item "[[ macro define render define x as y end define as Define render of root protect x end protect as y end define end define ]]"

Define the render aspect of a construct. The construct itself is protected against macro expansion.

\item "[[ macro define tex define x as y end define as Define tex of root protect x end protect as y end define end define ]]"

Define the tex aspect of a construct. The construct itself is protected against macro expansion.

\item "[[ macro define tex name define x as y end define as Define tex name of root protect x end protect as y end define end define ]]"

\item "[[ macro define value define x as y end define as define value of root protect x end protect as y end define end define ]]"

\item "[[ macro define message define x as y end define as define message of root protect x end protect as y end define end define ]]"

\item "[[ macro define priority table x as define priority of self as protect x end protect end define end define ]]"

Define the priority table of the page.

\item "[[ macro define verifier x end verifier as define claim of self as x end define end define ]]"

Define the claim of the page.

\item "[[ macro define unpacker x end unpacker as define unpack of self as x end define end define ]]"

Define the unpacker of the page.

\item "[[ macro define renderer x end renderer as define render of self as x end define end define ]]"

Define the renderer of the page.

\item "[[ macro define expander x end expander as define macro of self as x end define end define ]]"

Define the macro expansion engine of the page.

\item "[[ macro define executer x end executer as define execute of self as x end define end define ]]"

Define the thing to be executed when executing the page as a program.

\item "[[ macro define executables x end executables as define executables of self as x end define end define ]]"

Define an association list from names to programs.

\item "[[ protect proclaim tex define x as y end define as "hide" end proclaim end protect ]]"

Ensure that the tex definition construct can be used on the present page. If a tex definition construct is used to define the tex aspect of a revelation construct (e.g. a definition or proclamation construct) and if the tex definition construct is not macro expanded (e.g. early in the codification process where the macro expander is not yet operational) then the hiding specified above ensures that the revelation construct in the left hand side of the tex definition has no effect.

\item "[[ protect proclaim tex name define x as y end define as "hide" end proclaim end protect ]]"

Ensure that the tex name definition construct can be used on the present page.

\item "[[ protect proclaim priority table x as "hide" end proclaim end protect ]]"

Ensure that the priority table construct can be used on the present page.

\item "[[ protect proclaim macro define x as y end define as "hide" end proclaim end protect ]]"

Ensure that macro definitions can expand into definitions without causing trouble at early stages of codification.

\end{statements}

\subsection{Parentheses}\label{sec:Parentheses}

\begin{statements}

\item "[[ macro define ( x ) as x end define ]]"

\item "[[ macro define newline x as x end define ]]"

\end{statements}

\subsection{Numerals}\label{sec:Numerals}

As mentioned in Section \ref{sec:IntegerConstruction}, an integer like "[[ %% %1 %2 %3 ]]" can be expressed as an invisible zero followed by three suffix operators "[[ x %1 ]]", "[[ x %2 ]]", and "[[ x %3 ]]". The pyk source of "[[ %% %1 %2 %3 ]]" reads \verb+%% %1 %2 %3+ where \verb+%%+ is the invisible zero and \verb+%1+, \verb+%2+, and \verb+%3+ are the three suffix operators. This way of entering numbers is rather inconvenient, however.

It is more convenient to enter a number like "[[ 123 ]]" as \verb+123+ where \verb+3+ is a nulary operator and \verb+1+ and \verb+2+ are prefix operators. Macros which support that are given in the following. The macros defined in the following convert \verb+123+ into \verb+%% %1 %2 %3+.

Seen in isolation, it would be much easier to treat \verb+123+ as a nulary operator \verb+1+ followed by suffix operators \verb+2+ and \verb+3+. Doing so, however, is a waste of good names. As an example, it is convenient to have constructs named things like \verb+myname+ and \verb+myname2+ in pyk files. If we introduced a suffix \verb+2+, however, \verb+myname2+ could be interpreted either as the \verb+myname+ construct followed by a suffix \verb+2+ or as the \verb+myname2+ construct. This is why numerals are constructed by prefix operators and why the burden of reversing the digit lists is left to the macro expander.

\begin{statements}

\item "[[ Macro define 0x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 1x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 2x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 3x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 4x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 5x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 6x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 7x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 8x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 9x as \ x . numeral ( x ) end define ]]"

\item "[[ define value of numeral ( x ) as norm x is val : num1 ( x zeroth , x zeroth , substitute ( x zeroth , quote %% end quote , true ) ) end define ]]"

\item "[[ protect define value of num1 ( r , t , u ) as norm r is val : t is val : u is val : newline

if t tail then num2 ( r , t , u ) else newline

LET ( quote x end quote :: u ) :: true BE s IN newline

if t r= quote 0x end quote then num1 ( r , t first , substitute ( r , quote x %0 end quote , s ) ) else newline

if t r= quote 1x end quote then num1 ( r , t first , substitute ( r , quote x %1 end quote , s ) ) else newline

if t r= quote 2x end quote then num1 ( r , t first , substitute ( r , quote x %2 end quote , s ) ) else newline

if t r= quote 3x end quote then num1 ( r , t first , substitute ( r , quote x %3 end quote , s ) ) else newline

if t r= quote 4x end quote then num1 ( r , t first , substitute ( r , quote x %4 end quote , s ) ) else newline

if t r= quote 5x end quote then num1 ( r , t first , substitute ( r , quote x %5 end quote , s ) ) else newline

if t r= quote 6x end quote then num1 ( r , t first , substitute ( r , quote x %6 end quote , s ) ) else newline

if t r= quote 7x end quote then num1 ( r , t first , substitute ( r , quote x %7 end quote , s ) ) else newline

if t r= quote 8x end quote then num1 ( r , t first , substitute ( r , quote x %8 end quote , s ) ) else newline

if t r= quote 9x end quote then num1 ( r , t first , substitute ( r , quote x %9 end quote , s ) ) else newline

substitute ( r , quote exception end quote , true ) end define end protect ]]"

\item "[[ define value of num2 ( r , t , u ) as norm r is val : t is val : u is val : newline

LET ( quote x end quote :: u ) :: true BE s IN newline

if t r= quote 0 end quote then substitute ( r , quote x %0 end quote , s ) else newline

if t r= quote 1 end quote then substitute ( r , quote x %1 end quote , s ) else newline

if t r= quote 2 end quote then substitute ( r , quote x %2 end quote , s ) else newline

if t r= quote 3 end quote then substitute ( r , quote x %3 end quote , s ) else newline

if t r= quote 4 end quote then substitute ( r , quote x %4 end quote , s ) else newline

if t r= quote 5 end quote then substitute ( r , quote x %5 end quote , s ) else newline

if t r= quote 6 end quote then substitute ( r , quote x %6 end quote , s ) else newline

if t r= quote 7 end quote then substitute ( r , quote x %7 end quote , s ) else newline

if t r= quote 8 end quote then substitute ( r , quote x %8 end quote , s ) else newline

if t r= quote 9 end quote then substitute ( r , quote x %9 end quote , s ) else newline

substitute ( r , quote exception end quote , true ) end define ]]"

\end{statements}

\subsection{Formating of the expansion}

\begin{statements}

\item "[[ macro define make macro expanded version ragged right as ragged right end define ]]"

\end{statements}

\subsection{Visibility constructs}\label{sec:VisibilityConstructs}

The following constructs affect \indexintro{visibility}:

\begin{statements}

\item "[[ name name x end name end name ]]" renders the constructs in "[[ x ]]" using the tex name aspect.

\item "[[ name macro name x end name end name ]]" is similar to "[[ name name x end name end name ]]" but also macro expands like parentheses so that it disappears in the expansion of the page.

\item "[[ name hide x end hide end name ]]" hides "[[ x ]]" from harvesting, c.f. Section \ref{sec:Proclamations}.

\item "[[ name hiding name x end name end name ]]" renders the constructs in "[[ x ]]" using the tex name aspect, protects "[[ x ]]" from macro expansion, and and hides "[[ x ]]" from harvesting.

\end{statements}

All constructs above are themselves invisible when rendered using the tex aspect. They are visible above because they are all enclosed in a "[[ name name x end name end name ]]" construct. The properties of the constructs are declared in the following:

\begin{statements}

\item "[[ optimized define value of name x end name as x end define ]]"

\item "[[ macro define macro name x end name as x end define ]]"

\item "[[ optimized define value of hide x end hide as x end define ]]"

\item "[[ proclaim hide x end hide as "hide" end proclaim ]]"

\item "[[ optimized define value of hiding name x end name as x end define ]]"

\item "[[ macro define hiding name x end name as protect hiding name x end name end protect end define ]]"

\item "[[ proclaim hiding name x end name as "hide" end proclaim ]]"

\end{statements}

\subsection{Tuples}

\begin{statements}

\item "[[ value define <<>> as norm true end define ]]"

\item "[[ Macro define << u >> as \ x . tuple1 ( x ) end define ]]"

\item "[[ define value of tuple1 ( x ) as norm x is val : stateexpand ( tuple2 ( x zeroth , x zeroth first ) , x first , x second ) end define ]]"

\item "[[ define value of tuple2 ( t , u ) as norm t is val : u is val : newline

if .not. u r= quote x ,, y end quote then newline

substitute ( t , quote u :: <<>> end quote , ( quote u end quote :: u ) :: true ) else newline

substitute ( t , quote x :: y end quote , ( quote x end quote :: u first ) :: ( quote y end quote :: tuple2 ( t , u second ) ) :: true ) end define ]]"

\end{statements}

\subsection{Eager definitions}

\begin{statements}

\item "[[ Macro define eager define u as v end define as \ x . eager1 ( x ) end define ]]"

\item "[[ define value of eager1 ( x ) as norm x is val : newline

LET x zeroth BE t IN newline

LET t first BE u IN LET t second BE v IN newline

LET ( quote u end quote :: u ) :: ( quote w end quote :: eager2 ( t , u tail , v ) ) :: true BE s IN newline

stateexpand ( substitute ( t , quote define value of u as norm w end define end quote , s ) , x first , x second ) end define ]]"

\item "[[ define value of eager2 ( t , p , v ) as norm t is val : p is val : v is val : newline

if p atom then v else newline

LET ( quote x end quote :: p head ) :: ( quote v end quote :: eager2 ( t , p tail , v ) ) :: true BE s IN newline

substitute ( t , quote x is val : v end quote , s ) end define ]]"

\item "[[ macro define eager message define x as y end define as message define x as y end define,eager define x as y end define end define ]]"

\end{statements}

\subsection{Let constructs}\label{sec:LetConstructs}

\begin{statements}

\item "[[ Macro define let u := v in w as \ x . macrolet1 ( x ) end define ]]"

\item "[[ define value of macrolet1 ( x ) as norm x is val : newline

LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN newline

LET t first BE u IN LET t third BE w IN newline

LET u ref BE r IN LET u idx BE i IN newline

LET c [[ r :: "codex" :: r :: i :: 0 :: "macro" :: true => macrodefine ( x ) ]] BE c IN newline

stateexpand ( w , s , c ) end define ]]"

\item "[[ define message of destructure as "destructure" end define ]]"

\item "[[ macro define destructure define x as y end define as define destructure of root protect x end protect as y end define end define ]]"

\item "[[ destructure define u :: v as ( if asterisk atom then asterisk else asterisk head ) :: ( if asterisk atom then asterisk else asterisk tail ) :: true end define ]]"

\item "[[ Macro define let u = v in w as \ x . let1 ( x ) end define ]]"

\item "[[ define value of let1 ( x ) as norm x is val : newline

LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN newline

LET t first BE u IN LET t second BE v IN LET t third BE w IN newline

LET stateexpand ( u , s , c ) BE u IN newline

LET stateexpand ( v , s , c ) BE v IN newline

LET stateexpand ( w , s , c ) BE w IN newline

LET make-prime ( make-var ( t ) ) BE x IN newline

LET let2 ( x , u , w , c ) BE w IN newline

make-let ( quote asterisk end quote , v , w )

end define ]]"

\item "[[ define value of let2 ( x , p , w , c ) as norm x is val : p is val : w is val : c is val : newline

LET p ref BE r IN LET p idx BE i IN newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] BE c prime IN newline

LET c prime [[ "destructure" ]] BE d IN newline

if d = true then newline

if c prime [[ "value" ]] != true then w else make-let ( p , quote asterisk end quote , w ) else newline

LET let3 ( x , p tail , w , c ) BE w IN newline

make-let ( x , d third , w )

end define ]]"

\item "[[ define value of let3 ( x , p prime , w , c ) as norm x is val : p prime is val : w is val : c is val : newline

if p prime = true then w else newline

LET p prime head BE p IN LET p prime tail BE p prime IN newline

LET let3 ( x , p prime , w , c ) BE w IN newline

LET let2 ( make-prime ( x ) , p , w , c ) BE w IN newline

LET make-let ( x , make-tail ( x ) , w ) BE w IN newline

make-let ( quote asterisk end quote , make-head ( x ) , w ) end define ]]"

\item "[[ define value of make-var ( t ) as norm t is val : newline

substitute ( t , quote asterisk end quote , true ) end define ]]"

\item "[[ define value of make-let ( u , v , w ) as norm u is val : v is val : w is val : newline

LET ( quote u end quote :: u ) :: ( quote v end quote :: v ) :: ( quote w end quote :: w ) :: true BE s IN newline

substitute ( u , quote LET v BE u IN w end quote , s ) end define ]]"

\item "[[ define value of make-prime ( x ) as norm x is val : newline

LET ( quote x end quote :: x ) :: true BE s IN newline

substitute ( x , quote x prime end quote , s ) end define ]]"

\item "[[ define value of make-head ( x ) as norm x is val : newline

LET ( quote x end quote :: x ) :: true BE s IN newline

substitute ( x , quote x head end quote , s ) end define ]]"

\item "[[ define value of make-tail ( x ) as norm x is val : newline

LET ( quote x end quote :: x ) :: true BE s IN newline

substitute ( x , quote x tail end quote , s ) end define ]]"

\end{statements}

\subsection{Backquoting}

\begin{statements}

\item "[[ Macro define back u quote v end quote as \ x . backquote0 ( x ) end define ]]"

\item "[[ define value of make-root ( t , x ) as norm t is val : x is val : x ref :: x idx :: t debug end define ]]"

\item "[[ define value of make-pair ( t , x , y ) as norm t is val : x is val : y is val : make-root ( t , quote true :: true end quote ) :: x :: y :: true end define ]]"

\item "[[ define value of make-true ( t ) as norm t is val : make-root ( t , quote true end quote ) :: true end define ]]"

\item "[[ define value of make-quote ( t , x ) as norm t is val : x is val : make-root ( t , quote quote true end quote end quote ) :: x :: true end define ]]"

\item "[[ define value of make-make-root ( t , x , y ) as norm t is val : x is val : y is val : make-root ( t , quote make-root ( true , true ) end quote ) :: x :: y :: true end define ]]"

\item "[[ define value of backquote0 ( x ) as norm x is val : backquote1 ( x zeroth , x first , x second ) end define ]]"

\item "[[ define value of backquote1 ( t , s , c ) as norm t is val : s is val : c is val : backquote2 ( t , stateexpand ( t first , s , c ) , stateexpand ( t second , s , c ) , s , c ) end define ]]"

\item "[[ define value of backquote2 ( t , u , v , s , c ) as norm t is val : u is val : v is val : s is val : c is val : newline

if v r= quote true unquote end quote then v first else newline

make-pair ( t , make-make-root ( t , u , make-quote ( t , v ) ) , backquote2* ( t , u , v tail , s , c ) ) end define ]]"

\item "[[ define value of backquote2* ( t , u , v , s , c ) as norm t is val : u is val : v is val : s is val : c is val : newline

if v atom then make-true ( t ) else newline

make-pair ( t , backquote2 ( t , u , v head , s , c ) , backquote2* ( t , u , v tail , s , c ) ) end define ]]"

\end{statements}

\subsection{Rendering}

We define a number of constructs for rendering. To see how most of them are used, consult the source of the present Logiweb page.

\begin{statements}

\item "[[ name text x : y end text end name ]]". Store the text "[[ y ]]" in a file named "[[ x ]]".

\item "[[ name latex ( x ) end name ]]". Run latex on the file named "[[ x ]]".

\item "[[ name bibtex ( x ) end name ]]". Run bibtex on the file named "[[ x ]]".

\item "[[ name makeindex ( x ) end name ]]". Run makeindex on the file named "[[ x ]]".

\item "[[ name dvipdfm ( x ) end name ]]". Run dvipdfm on the file named "[[ x ]]".

\item "[[ name tex-file ( c , x , y ) end name ]]". Equivalent to "[[ name text x : y end text end name ]]" when "[[ c ]]" is the string text''.

\item "[[ name tex-command ( c , x ) end name ]]". Equivalent to "[[ name latex ( x ) end name ]]", "[[ name bibtex ( x ) end name ]]", "[[ name makeindex ( x ) end name ]]", and "[[ name dvipdfm ( x ) end name ]]", respectively, when "[[ c ]]" is one of the strings latex'', bibtex'', makeindex'', and dvipdfm''.

\item "[[ name page ( x , y ) title t bib b main text m appendix a end page end name ]]". A construct for defining a document with title "[[ t ]]", bib-file "[[ b ]]", main text "[[ m ]]", and appendix "[[ a ]]". The main text is processed by latex, bibtex, makeindex, latex, and latex. The appendix is processed by latex three times. "[[ x ]]" and "[[ y ]]" must be Pyk and Priority, respectively, where the pyk compiler expands the two into pyk and priority definitions, respectively.

\end{statements}

Only the page' construct needs a definition here. All the other ones just have tex definitions which are stated later.

\begin{statements}

\item "[[ Macro define page ( x , y ) title t bib b main text m appendix a end page as \ z . page1 ( z ) end define ]]"

\item "[[ define value of page1 ( z ) as norm z is val : newline

LET z zeroth BE t IN newline

LET z first BE s IN newline

LET z second BE c IN newline

LET name quote protect priority table x end protect end quote end name BE p IN newline

LET ( p ref :: p idx :: t debug ) :: t second :: true BE y IN newline

LET stateexpand ( y , s , c ) BE y IN newline

LET stateexpand ( t fifth , s , c ) BE m IN newline

LET stateexpand ( t sixth , s , c ) BE a IN newline

LET name quote protect page ( x , y ) title t bib b main text m appendix a end page end protect end quote end name BE p IN newline

( p ref :: p idx :: t debug ) :: t first :: y :: t third :: t fourth :: m :: a :: true end define ]]"

\end{statements}

\section{The Logiweb machine}\label{section:Interaction}

A \index{machine, Logiweb}\indexintro{Logiweb machine} is an abstract machine which consists of

\begin{itemize}

\item a Logiweb computing engine,

\item an \indexintro{interface},

\item a \index{handler, boot}\indexintro{boot handler}, and

\item a \indexintro{cache}.

\end{itemize}

\noindent The engine and interface comprise the hardware' of the abstract machine whereas the handler and cache comprise software which is preloaded on the machine.

Each Logiweb page may define one or more Logiweb machines. When a Logiweb page is rendered, all machines defined on the page (if any) are output as executable files. The cache of each machine equals the cache of the page defining the machine whereas each machine has its own, individual handler.

The interface of a Logiweb machine performs an input-eval-output-loop in which it converts input to a list of \index{input event}\index{event, index}\intro{input events} and applies the handler to that input list. The return value is supposed to be a list of \index{output event}\index{event, output}\intro{output events} which the interface executes.

The interface has the ability to load code dynamically into the running machine. Such code can improve the efficiency of the engine and can add new abilities to the interface. A Logiweb machine is {\em virgin} from it starts and until first time it loads code. The virgin Logiweb machine has very few abilities.

\subsection{Events}\label{section:Events}

The virgin Logiweb machine knows the following output events:

$"[ array ( left ) value define quit ( x ) as << << 0 ,, "quit" >> ,, x >> end define \\ value define write ( s ) as << << 0 ,, "write" >> ,, s >> end define \\ value define exec ( p , h ) as << << 0 ,, "exec" >> ,, p ,, h >> end define \\ value define extend ( s ) as << << 0 ,, "extend" >> ,, s >> end define end array ]"$

\noindent And the following input events:

$"[ array ( left ) value define boot ( a , e , c ) as << << 0 ,, "boot" >> ,, a ,, e ,, c >> end define \\ value define read ( c ) as << << 0 ,, "read" >> ,, c >> end define \\ value define int ( i , p ) as << << 0 ,, "int" >> ,, i ,, p >> end define \\ value define extended ( x ) as << << 0 ,, "extd" >> ,, x >> end define end array ]"$

\subsection{Machine invocation}

A user may start a Logiweb machine by typing its name followed by arguments on a command line. The machine then forms the term "[[ t = h apply << boot ( a , e , c ) >> ]]" where "[[ h ]]" is the boot handler, "[[ a ]]" is \verb+argv+, "[[ e ]]" is the current environment, and "[[ c ]]" is the cache. Then the machine enters an input-eval-output-loop.

\subsection{Input-eval-output-loop}

When the machine enters the input-eval-output-loop, the interface asks the engine to reduce "[[ t ]]". The result of that is supposed to be a list of output events. The interface then executes the output events one at a time as follows:

A "[[ quit ( x ) ]]" makes the machine exit immediately with return code "[[ x ]]".

A "[[ write ( s ) ]]" makes the interface write the strings in "[[ s ]]" to standard output. If "[[ s ]]" is a cardinal then the cardinal is interpretted as a list of bytes encoded little endian base 256. Bytes with values 32-255 are written to standard output, bytes with values 0--9 and 11--31 are discarded, and bytes with a value of 10 are converted to a newline sequence of the underlying system. Standard output is supposed to support UTF-8. If "[[ s ]]" has form "[[ u :: v ]]" then the interface recursively outputs first "[[ u ]]" and then "[[ v ]]". If "[[ s ]]" is neither a cardinal nor a pair then it is ignored.

An "[[ extend ( s ) ]]" makes the interface treat "[[ s ]]" as a piece of source code which the interface compiles and loads. The details are system dependent. Each Extend event results in an "[[ extended ( x ) ]]" input event where the semantics of "[[ x ]]" is system dependent.

An "[[ exec ( p , h ) ]]" makes the machine discard all events following the Exec and asks the engine to reduce "[[ p ]]". During execution of "[[ p ]]" there is an upper, system dependent limit on the time and memory the engine may use. Reduction of "[[ p ]]" may stop because of timeout, memory overflow, or external interupts. Reduction may also stop because the engine succeeds to reduce "[[ p ]]". We shall refer to the latter situation as an {\em exit} interrupt so that reduction of "[[ p ]]" always ends with an interrupt. Then the interface forms the term

$"[ t = h apply << int ( << i ,, a _ { 1 } ,, "\ldots" ,, a _ { m } >> , p ) ,, e _ { 1 } ,, "\ldots" ,, e _ { n } >> ]"$

\noindent where "[[ i ]]" identifies the interrupt, "[[ a _ { 1 } ,, "\ldots" ,, a _ { m } ]]" are possible interrupt parameters, and "[[ e _ { 1 } ,, "\ldots" ,, e _ { n } ]]" are input events that have occurred since last. Then the interface reenters the input-eval-output-loop.

On the virgin machine, the input events comprise one Extended event for each Extend output event plus zero or one Read events. The input events comprise no Read events if no input is ready on standard input. Otherwise, the interface reads one character or one newline sequence from standard input and generates an input event of form "[[ read ( c ) ]]". The value of "[[ c ]]" is a cardinal which represents the character or newline sequence as a string. If the input is a newline sequence then the value of "[[ c ]]" is "[[ 10 + %% %2 %5 %6 ]]". If the input is a character then the character is encoded as a string of bytes using UTF-8.

\subsection{Handlers and processes}

The "[[ exec ( p , h ) ]]" event makes the machine evaluate the {\em process} "[[ p ]]" and, when that is interrupted, the {\em handler} "[[ h ]]". Hence, "[[ h ]]" corresponds to an interrupt handler and "[[ p ]]" corresponds to a less privileged user, operating system, or driver process. The handler "[[ h ]]" has full control over the machine in that it receives all input, generates all output, and cannot be interrupted.

\subsection{Hello World}

A machine with "[[ value define Hello World as map ( \ x . << write ( "Hello World" ) >> ) end define ]]" as boot handler writes Hello World'' and exits. The example abuses the high privilege boot handler to do the writing. In the absence of Exec and Quit events, the machine quits with return code 0 after writing Hello World'.

\subsection{Echo}

A machine with "[[ Echo ]]" below as boot handler echos all characters typed except that it quits when the user types q':

\begin{quote}

\noindent "[[ value define Echo as map ( \ x . Echo1 ( x ) ) end define ]]"

\noindent "[[ value define Echo1 ( x ) as

if x atom then << exec ( true , Echo ) >> else newline

LET x head BE e IN newline

LET Echo1 ( x tail ) BE r IN newline

if .not. e head = << 0 ,, "read" >> then r else newline

if e first = "q" then << quit ( 0 ) >> else

write ( e first ) :: r end define ]]"

\end{quote}

\subsection{Eecho}

A machine with "[[ Eecho ]]" below as boot handler echos all characters typed twice except that it quits when the user types q':

\begin{quote}

\noindent "[[ value define Eecho as map ( \ x . Eecho1 ( x ) ) end define ]]"

\noindent "[[ value define Eecho1 ( x ) as

if x atom then << exec ( true , Eecho ) >> else newline

LET x head BE e IN newline

LET Eecho1 ( x tail ) BE r IN newline

if .not. e head = << 0 ,, "read" >> then r else newline

if e first = "q" then << quit ( 0 ) >> else

write ( e first :: e first ) :: r end define ]]"

\end{quote}

\subsection{Execution constructs}

Logiweb has two mechanisms for producing Logiweb machines. One is to set the execute' aspect of the page symbol to a handler. As an example, "[[ executer Eecho end executer ]]" macro expands into a definition which defines the execute aspect of the present page to be "[[ Eecho ]]".

If one \index{execute}\intro{executes} the present page then a Logiweb machine is run with "[[ Eecho ]]" as handler and the cache of the present page as cache. The "[[ Eecho ]]" handler is useful e.g.\ for automated testing of Logiweb.

As an example of use, one may express a Java virtual machine as a handler and register that handler as the execute aspect of the page. If done properly, then Logiweb will be able to execute any Java code on the page.

"[[ executables << "hello" :: Hello World ,, "echo" :: Echo >> end executables ]]" uses the other mechanism for producing Logiweb machines. It specifies "[[ Hello World ]]" and "[[ Echo ]]" to be stored to disc in a user defined directory under the names hello'' and echo'', respectively.

\printindex

\bibliography{./page}

\end{document}
" end text ,,

latex ( "page" ) ,,
makeindex ( "page" ) ,,
bibtex ( "page" ) ,,
latex ( "page" ) ,,
makeindex ( "page" ) ,,
latex ( "page" ) ,,
dvipdfm ( "page" ) ,,

text "chores.tex" : ""+

\documentclass[fleqn]{article}

% Include definitions generated by pyk
\input{lgwinclude}

% Make latexsym characters available
\usepackage{latexsym}

% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}

% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}

% Enable generation of a bibliography
\bibliographystyle{plain}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=A Logiweb base page - chores}

% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}

\begin{document}
\title{A Logiweb base page - chores}
\author{Klaus Grue}
\maketitle
\tableofcontents

\section{\TeX\ definitions}

\begin{statements}

\item "[[ tex define proclaim x as y end proclaim as "
[ "[ texname x end texname ]"
\bowtie "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define empty as "" end define ]]"

\item "[[ tex name define empty as "empty" end define ]]"

\item "[[ tex define preassociative x greater than y as "
\newline \mathbf {Preassociative} \newline "[ x ]"
; "[ y ]"" end define ]]"

\item "[[ tex name define preassociative x greater than y as "
\mathbf{Preassociative}\,"[ x ]"
; "[ y ]"" end define ]]"

\item "[[ tex define postassociative x greater than y as "
\newline\mathbf{Postassociative} \newline "[ x ]"
; "[ y ]"" end define ]]"

\item "[[ tex name define postassociative x greater than y as "
\mathbf{Postassociative}\,"[ x ]"
; "[ y ]"" end define ]]"

\item "[[ tex define priority x equal y as "
["[ texname x end texname ]"
] , \linebreak [0] "[ y ]"" end define ]]"

\item "[[ tex name define priority x equal y as "
["[ x ]"
] , \linebreak [0] "[ y ]"" end define ]]"

\item "[[ tex define priority x end priority as "
["[ texname x end texname ]"
]" end define ]]"

\item "[[ tex name define priority x end priority as "
priority \ "[ x ]"
\ end" end define ]]"

\item "[[ tex define asterisk as "
\ast " end define ]]"

\item "[[ tex define pyk as "
pyk" end define ]]"

\item "[[ tex define define x of y as z end define as "
[ "[ texname y end texname ]"
\stackrel{"[ x ]"
}{\rightarrow}"[ z ]"
]" end define ]]"

\item "[[ tex define math x end math as "$"[ x ]"$" end define ]]"

\item "[[ tex name define math x end math as "
\ \$"[ x ]"\$\linebreak[0]\ " end define ]]"

\item "[[ tex define display math x end math as "$$"[ x ]"$$" end define ]]"

\item "[[ tex name define display math x end math as "
\ \$\$"[ x ]"\$\$\linebreak[0]\ " end define ]]"

\item "[[ tex define a as "
\mathit{a}" end define ]]"

\item "[[ tex define b as "
\mathit{b}" end define ]]"

\item "[[ tex define c as "
\mathit{c}" end define ]]"

\item "[[ tex define d as "
\mathit{d}" end define ]]"

\item "[[ tex define e as "
\mathit{e}" end define ]]"

\item "[[ tex define f as "
\mathit{f}" end define ]]"

\item "[[ tex define g as "
\mathit{g}" end define ]]"

\item "[[ tex define h as "
\mathit{h}" end define ]]"

\item "[[ tex define i as "
\mathit{i}" end define ]]"

\item "[[ tex define j as "
\mathit{j}" end define ]]"

\item "[[ tex define k as "
\mathit{k}" end define ]]"

\item "[[ tex define l as "
\mathit{l}" end define ]]"

\item "[[ tex define m as "
\mathit{m}" end define ]]"

\item "[[ tex define n as "
\mathit{n}" end define ]]"

\item "[[ tex define o as "
\mathit{o}" end define ]]"

\item "[[ tex define p as "
\mathit{p}" end define ]]"

\item "[[ tex define q as "
\mathit{q}" end define ]]"

\item "[[ tex define r as "
\mathit{r}" end define ]]"

\item "[[ tex define s as "
\mathit{s}" end define ]]"

\item "[[ tex define t as "
\mathit{t}" end define ]]"

\item "[[ tex define u as "
\mathit{u}" end define ]]"

\item "[[ tex define v as "
\mathit{v}" end define ]]"

\item "[[ tex define w as "
\mathit{w}" end define ]]"

\item "[[ tex define x as "
\mathit{x}" end define ]]"

\item "[[ tex define y as "
\mathit{y}" end define ]]"

\item "[[ tex define z as "
\mathit{z}" end define ]]"

\item "[[ tex define A as "
\mathit{A}" end define ]]"

\item "[[ tex define B as "
\mathit{B}" end define ]]"

\item "[[ tex define C as "
\mathit{C}" end define ]]"

\item "[[ tex define D as "
\mathit{D}" end define ]]"

\item "[[ tex define E as "
\mathit{E}" end define ]]"

\item "[[ tex define F as "
\mathit{F}" end define ]]"

\item "[[ tex define G as "
\mathit{G}" end define ]]"

\item "[[ tex define H as "
\mathit{H}" end define ]]"

\item "[[ tex define I as "
\mathit{I}" end define ]]"

\item "[[ tex define J as "
\mathit{J}" end define ]]"

\item "[[ tex define K as "
\mathit{K}" end define ]]"

\item "[[ tex define L as "
\mathit{L}" end define ]]"

\item "[[ tex define M as "
\mathit{M}" end define ]]"

\item "[[ tex define N as "
\mathit{N}" end define ]]"

\item "[[ tex define O as "
\mathit{O}" end define ]]"

\item "[[ tex define P as "
\mathit{P}" end define ]]"

\item "[[ tex define Q as "
\mathit{Q}" end define ]]"

\item "[[ tex define R as "
\mathit{R}" end define ]]"

\item "[[ tex define S as "
\mathit{S}" end define ]]"

\item "[[ tex define T as "
\mathit{T}" end define ]]"

\item "[[ tex define U as "
\mathit{U}" end define ]]"

\item "[[ tex define V as "
\mathit{V}" end define ]]"

\item "[[ tex define W as "
\mathit{W}" end define ]]"

\item "[[ tex define X as "
\mathit{X}" end define ]]"

\item "[[ tex define Y as "
\mathit{Y}" end define ]]"

\item "[[ tex define Z as "
\mathit{Z}" end define ]]"

\item "[[ tex define true as "
\mathsf{T}" end define ]]"

\item "[[ tex define quote x end quote as "
\lceil "[ x ]"
\rceil " end define ]]"

\item "[[ tex define optimized define x of y as z end define as "
["[ texname y end texname ]"
\stackrel {"[ x ]"
}{\rightarrow\rightarrow }"[ z ]"
]" end define ]]"

\item "[[ tex define tex as "
tex" end define ]]"

\item "[[ tex define tex name as "
name" end define ]]"

\item "[[ tex define priority as "
prio" end define ]]"

\item "[[ tex define value as "
val" end define ]]"

\item "[[ tex define macro as "
macro" end define ]]"

\item "[[ tex define claim as "
claim" end define ]]"

\item "[[ tex define message as "
msg" end define ]]"

\item "[[ tex define name x end name as ""[ texname x end texname ]"" end define ]]"

\item "[[ tex name define name x end name as "
name("[ x ]"
)" end define ]]"

\item "[[ tex define macro name x end name as ""[ texname x end texname ]"" end define ]]"

\item "[[ tex name define macro name x end name as "
macroname("[ x ]"
)" end define ]]"

\item "[[ tex define hiding name x end name as ""[ texname x end texname ]"" end define ]]"

\item "[[ tex name define hiding name x end name as "
hidename("[ x ]"
)" end define ]]"

\item "[[ tex define hide x end hide as x end define ]]"

\item "[[ tex name define hide x end hide as "
hide("[ x ]"
)" end define ]]"

\item "[[ tex define array ( x ) y end array as "
\begin{array}{"[ x ]"}
"[ y ]"
\end{array}" end define ]]"

\item "[[ tex name define array ( x ) y end array as "
array("[ x ]"
)\{"[ y ]"
\}" end define ]]"

\item "[[ tex define left as "l" end define ]]"

\item "[[ tex define center as "c" end define ]]"

\item "[[ tex define right as "r" end define ]]"

\item "[[ tex define %% as "" end define ]]"

\item "[[ tex name define %% as "\{\}" end define ]]"

\item "[[ tex define ( x ) as "
("[ x ]"
)" end define ]]"

\item "[[ tex define < x | y := z > as "
\langle "[ x ]"
\,{|}"[ y ]"
{:=}\,"[ z ]"
\rangle " end define ]]"

\item "[[ tex define bottom as "
\bot " end define ]]"

\item "[[ tex define false as "
\mathsf{F}" end define ]]"

\item "[[ tex define Define x of y as z end define as "
[ "[ texname y end texname ]"
\stackrel{"[ texname x end texname ]"
!}{\rightarrow}"[ texname z end texname ]"
]" end define ]]"

\item "[[ tex define ... as "
\ldots " end define ]]"

\item "[[ tex define --- as "
\cdots " end define ]]"

\item "[[ tex define exception as "
\bullet " end define ]]"

\item "[[ tex define 0 as "
0" end define ]]"

\item "[[ tex define 1 as "
1" end define ]]"

\item "[[ tex define 2 as "
2" end define ]]"

\item "[[ tex define 3 as "
3" end define ]]"

\item "[[ tex define 4 as "
4" end define ]]"

\item "[[ tex define 5 as "
5" end define ]]"

\item "[[ tex define 6 as "
6" end define ]]"

\item "[[ tex define 7 as "
7" end define ]]"

\item "[[ tex define 8 as "
8" end define ]]"

\item "[[ tex define 9 as "
9" end define ]]"

\item "[[ tex define protect x end protect as "
protect("[ x ]"
)" end define ]]"

\item "[[ tex define root protect x end protect as "
root\ protect( "[ x ]"
)" end define ]]"

\item "[[ tex define render define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{render}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define tex define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{tex}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define tex name define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{name}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define value define x as y end define as "
[ "[ texname x end texname ]"
\mathrel{\dot{=}} "[ y ]"
]" end define ]]"

\item "[[ tex define message define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{msg}{=} "[ y ]"
]" end define ]]"

\item "[[ tex define Macro define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{\circ}{=} "[ y ]"
]" end define ]]"

\item "[[ tex define macro define x as y end define as "
[ "[ texname x end texname ]"
\mathrel{\ddot{=}} "[ y ]"
]" end define ]]"

\item "[[ tex define priority table x as "
\mathbf{Priority\ table} \linebreak[4] "[ x ]"" end define ]]"

\item "[[ tex name define priority table x as "
\mathbf{Priority\ table} \ "[ x ]"" end define ]]"

\item "[[ tex define verifier x end verifier as "
[ \mathbf{Verifier\colon} "[ x ]"
]" end define ]]"

\item "[[ tex define unpacker x end unpacker as "
[ \mathbf{Unpacker\colon} "[ x ]"
]" end define ]]"

\item "[[ tex define renderer x end renderer as "
[ \mathbf{Renderer\colon} "[ x ]"
]" end define ]]"

\item "[[ tex define expander x end expander as "
[ \mathbf{Expander\colon} "[ x ]"
]" end define ]]"

\item "[[ tex define executer x end executer as "
[ \mathbf{Executer\colon} "[ x ]"
]" end define ]]"

\item "[[ tex define executables x end executables as "
[ \mathbf{Executables\colon} "[ x ]"
]" end define ]]"

\item "[[ tex define ragged right as "
\raggedright" end define ]]"

\item "[[ tex name define ragged right as "
\backslash raggedright " end define ]]"

\item "[[ tex define make macro expanded version ragged right as "" end define ]]"

\item "[[ tex name define make macro expanded version ragged right as "
make\ expansion\ ragged\ right " end define ]]"

\item "[[ tex define <<>> as "
\langle \, \rangle" end define ]]"

\item "[[ tex define << x >> as "
\langle "[ x ]"
\rangle " end define ]]"

\item "[[ tex define eager define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{\bullet}{=} "[ y ]"
]" end define ]]"

\item "[[ tex define eager message define x as y end define as "
[ message\ "[ texname x end texname ]"
: "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define destructure as "
dest" end define ]]"

\item "[[ tex define destructure define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{dest}{=} "[ y ]"
]" end define ]]"

\item "[[ tex define back x quote y end quote as "
\lceil_{\!"[ x ]"
\,} "[ y ]"
\rceil " end define ]]"

\item "[[ tex define text x : y end text as "text"[ x ]y end define ]]"

\item "[[ tex name define text x : y end text as "
text\ "[ x ]"
: "[ y ]"
end\ file" end define ]]"

\item "[[ tex define tex ( x ) as "tex",x end define ]]"

\item "[[ tex name define tex ( x ) as "
tex("[ x ]"
)" end define ]]"

\item "[[ tex define latex ( x ) as "latex",x end define ]]"

\item "[[ tex name define latex ( x ) as "
latex("[ x ]"
)" end define ]]"

\item "[[ tex define bibtex ( x ) as "bibtex",x end define ]]"

\item "[[ tex name define bibtex ( x ) as "
bibtex("[ x ]"
)" end define ]]"

\item "[[ tex define makeindex ( x ) as "makeindex",x end define ]]"

\item "[[ tex name define makeindex ( x ) as "
makeindex("[ x ]"
)" end define ]]"

\item "[[ tex define dvipdfm ( x ) as "dvipdfm",x end define ]]"

\item "[[ tex name define dvipdfm ( x ) as "
dvipdfm("[ x ]"
)" end define ]]"

\item "[[ tex name define page ( x , y ) title t bib b main text m appendix a end page as "
page ( "[ x ]"
, "[ y ]"
, "[ t ]"
, "[ b ]"
, "[ m ]"
, "[ a ]"
) " end define ]]"

\item "[[ tex define page ( x , y ) title t bib b main text m appendix a end page as

tex-file ( "text" , "page.html" , ""+
<body><h2>"[ t ]"</h2>
<p><a href='../index.html'>Up</a></p>
<p>Contents:
<a href='page.pdf'>Main text</a>
<a href='appendix.pdf'>Appendix</a>
<a href='chores.pdf'>Chores</a>
</p>
</body>
" ) ,,

tex-file ( "text" , "page.bib" , b ) ,,

tex-file ( "text" , "page.tex" , ""+
\documentclass[fleqn]{article}
% Include definitions generated by pyk
\input{lgwinclude}
% Make latexsym characters available
\usepackage{latexsym}
% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}
% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
% Enable generation of a bibliography
\bibliographystyle{plain}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle="[ t ]"}
% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}
\begin{document}
"[ m ]"
\end{document}
" ) ,,
tex-command ( "latex" , "page" ) ,,
tex-command ( "bibtex" , "page" ) ,,
tex-command ( "makeindex" , "page" ) ,,
tex-command ( "latex" , "page" ) ,,
tex-command ( "latex" , "page" ) ,,
tex-command ( "dvipdfm" , "page" ) ,,

tex-file ( "text" , "appendix.tex" , ""+
\documentclass[fleqn]{article}
% Include definitions generated by pyk
\input{lgwinclude}
% Make latexsym characters available
\usepackage{latexsym}
% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}
% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
% Enable generation of a bibliography
\bibliographystyle{plain}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle="[ t ]" - appendix}
% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}
\begin{document}
"[ a ]"
\end{document}
" ) ,,
tex-command ( "latex" , "appendix" ) ,,
tex-command ( "latex" , "appendix" ) ,,
tex-command ( "latex" , "appendix" ) ,,
tex-command ( "dvipdfm" , "appendix" ) ,,

tex-file ( "text" , "chores.tex" , ""+
\documentclass[fleqn]{article}
% Include definitions generated by pyk
\input{lgwinclude}
% Make latexsym characters available
\usepackage{latexsym}
% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}
% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
% Enable generation of a bibliography
\bibliographystyle{plain}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle="[ t ]" - chores}
% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}
\begin{document}
\title{"[ t ]"}
\author{The \href{http://logiweb.eu/}{pyk} compiler}
\maketitle
\tableofcontents
\section{Pyk definitions}
\begin{flushleft}
$"[ x ]"$
\end{flushleft}
\section{Priority table}
\begin {flushleft}
$"[ y ]"$
\end {flushleft}
\end{document}
" ) ,,
tex-command ( "latex" , "chores" ) ,,
tex-command ( "latex" , "chores" ) ,,
tex-command ( "latex" , "chores" ) ,,
tex-command ( "dvipdfm" , "chores" )

end define ]]"

\item "[[ tex define -x as "
{}^{-}\! ",x end define ]]"

\item "[[ tex define + x as "
{+} "[ x ]"" end define ]]"

"[[ tex define x factorial as ""[ x ]"
!" end define ]]"

"[[ tex define x _ { y } as ""[ x ]"
_{"[ y ]"
}" end define ]]"

"[[ tex define x prime as ""[ x ]"
{}' " end define ]]"

"[[ tex name define x _ { y } as ""[ x ]"
\_\{"[ y ]"
\}" end define ]]"

"[[ tex define x %0 as ""[ x ]"0" end define ]]"

"[[ tex define x %1 as ""[ x ]"1" end define ]]"

"[[ tex define x %2 as ""[ x ]"2" end define ]]"

"[[ tex define x %3 as ""[ x ]"3" end define ]]"

"[[ tex define x %4 as ""[ x ]"4" end define ]]"

"[[ tex define x %5 as ""[ x ]"5" end define ]]"

"[[ tex define x %6 as ""[ x ]"6" end define ]]"

"[[ tex define x %7 as ""[ x ]"7" end define ]]"

"[[ tex define x %8 as ""[ x ]"8" end define ]]"

"[[ tex define x %9 as ""[ x ]"9" end define ]]"

"[[ tex define x head as ""[ x ]"
{}^h" end define ]]"

"[[ tex define x tail as ""[ x ]"
{}^t" end define ]]"

"[[ tex define x raise as ""[ x ]"
{}^{\bullet}" end define ]]"

"[[ tex define x catch as ""[ x ]"
{}^{\circ}" end define ]]"

"[[ tex define x catching maptag as ""[ x ]"
{}^{M^{\circ}}" end define ]]"

"[[ tex define x maptag as ""[ x ]"
{}^M" end define ]]"

"[[ tex define x untag as ""[ x ]"
{}^U" end define ]]"

"[[ tex define x root as ""[ x ]"
{}^R" end define ]]"

"[[ tex define x norm as ""[ x ]"
{}^N" end define ]]"

"[[ tex define x boolp as ""[ x ]"
\in \mathbf{B}" end define ]]"

"[[ tex define x truep as ""[ x ]"
\in \mathbf{T}" end define ]]"

"[[ tex define x falsep as ""[ x ]"
\in \mathbf{F}" end define ]]"

"[[ tex define x intp as ""[ x ]"
\in \mathbf{Z}" end define ]]"

"[[ tex define x pairp as ""[ x ]"
\in \mathbf{P}" end define ]]"

"[[ tex define x atom as ""[ x ]"
\in \mathbf{A}" end define ]]"

"[[ tex define x mapp as ""[ x ]"
\in \mathbf{M}" end define ]]"

"[[ tex define x objectp as ""[ x ]"
\in \mathbf{O}" end define ]]"

"[[ tex define x zeroth as ""[ x ]"
{}^0" end define ]]"

"[[ tex define x first as ""[ x ]"
{}^1" end define ]]"

"[[ tex define x second as ""[ x ]"
{}^2" end define ]]"

"[[ tex define x third as ""[ x ]"
{}^3" end define ]]"

"[[ tex define x fourth as ""[ x ]"
{}^4" end define ]]"

"[[ tex define x fifth as ""[ x ]"
{}^5" end define ]]"

"[[ tex define x sixth as ""[ x ]"
{}^6" end define ]]"

"[[ tex define x seventh as ""[ x ]"
{}^7" end define ]]"

"[[ tex define x eighth as ""[ x ]"
{}^8" end define ]]"

"[[ tex define x ninth as ""[ x ]"
{}^9" end define ]]"

"[[ tex define x ref as ""[ x ]"
{}^r" end define ]]"

"[[ tex define x idx as ""[ x ]"
{}^i" end define ]]"

"[[ tex define x debug as ""[ x ]"
{}^d" end define ]]"

"[[ tex define a [[ i ]] as ""[ a ]"
\linebreak[0][ "[ i ]"
]" end define ]]"

"[[ tex define a [[ i -> v ]] as ""[ a ]"
\linebreak[0][ "[ i ]"
{\rightarrow} "[ v ]"
]" end define ]]"

"[[ tex define a [[ i => v ]] as ""[ a ]"
\linebreak[0][ "[ i ]"
{\Rightarrow} "[ v ]"
]" end define ]]"

\item "[[ tex define x unquote as "
\underline{ "[ x ]"
} " end define ]]"

\item "[[ tex name define x unquote as ""[ x ]"
unquote" end define ]]"

\item "[[ tex define newline x as "
\newline "[ x ]"" end define ]]"

\item "[[ tex name define newline x as "
newline\ "[ x ]"" end define ]]"

\item "[[ tex define x ' y as ""[ x ]"
\mathbin {\mbox {'}}"[ y ]"" end define ]]"

\item "[[ tex define x apply y as ""[ x ]"
\mathbin {\mbox {''}}"[ y ]"" end define ]]"

\item "[[ tex define texname x end texname as "
\underline{ "[ x ]"
}" end define ]]"

\item "[[ tex define - x as "
{-} "[ x ]"" end define ]]"

\item "[[ tex define +x as "
{}^{+}\! ",x end define ]]"

\item "[[ tex define x * y as ""[ x ]"
\cdot "[ y ]"" end define ]]"

\item "[[ tex define x + y as ""[ x ]"
+ "[ y ]"" end define ]]"

\item "[[ tex define x - y as ""[ x ]"
- "[ y ]"" end define ]]"

\item "[[ tex define x :: y as ""[ x ]"
\mathop{:\,:} "[ y ]"" end define ]]"

\item "[[ tex define x ,, y as ""[ x ]"
, "[ y ]"" end define ]]"

\item "[[ tex define x = y as ""[ x ]"
= "[ y ]"" end define ]]"

\item "[[ tex define x != y as ""[ x ]"
\neq "[ y ]"" end define ]]"

\item "[[ tex define x < y as ""[ x ]"
< "[ y ]"" end define ]]"

\item "[[ tex define x > y as ""[ x ]"
> "[ y ]"" end define ]]"

\item "[[ tex define x <= y as ""[ x ]"
\le "[ y ]"" end define ]]"

\item "[[ tex define x >= y as ""[ x ]"
\ge "[ y ]"" end define ]]"

\item "[[ tex define x r= y as ""[ x ]"
\stackrel{r}{=} "[ y ]"" end define ]]"

\item "[[ tex define x t= y as ""[ x ]"
\stackrel{t}{=} "[ y ]"" end define ]]"

\item "[[ tex define x t=* y as ""[ x ]"
\stackrel{t^*}{=} "[ y ]"" end define ]]"

\item "[[ tex define .not. x as "
{\bf not} \ \linebreak [0]"[ x ]"" end define ]]"

\item "[[ tex define x .and. y as ""[ x ]"
\ {\bf and} \ \linebreak [0]"[ y ]"" end define ]]"

\item "[[ tex define x &c y as ""[ x ]"
\wedge_c "[ y ]"" end define ]]"

\item "[[ tex define x .or. y as ""[ x ]"
\ {\bf or} \ \linebreak [0]"[ y ]"" end define ]]"

\item "[[ tex define x is val : y as ""[ x ]"
{\in} \mathbf{V} \colon "[ y ]"" end define ]]"

\item "[[ tex define x is bool : y as ""[ x ]"
{\in} \mathbf{B} \colon "[ y ]"" end define ]]"

\item "[[ tex define x is int : y as ""[ x ]"
{\in} \mathbf{Z} \colon "[ y ]"" end define ]]"

\item "[[ tex define x is pair : y as ""[ x ]"
{\in} \mathbf{P} \colon "[ y ]"" end define ]]"

\item "[[ tex define x is map : y as ""[ x ]"
{\in} \mathbf{M} \colon "[ y ]"" end define ]]"

\item "[[ tex define x is object : y as ""[ x ]"
{\in} \mathbf{O} \colon "[ y ]"" end define ]]"

\item "[[ tex define x Select y else z end select as
""[ x ]"
\left\langle\protect \begin {array}{l}"[ y ]"
\\"[ z ]"
\protect \end {array}\right." end define ]]"

\item "[[ tex define x IN y as ""[ x ]"
\ \mathbf{in}\ \linebreak [0] "[ y ]"" end define ]]"

\item "[[ tex define \ x . y as "
\lambda "[ x ]"
."[ y ]"" end define ]]"

\item "[[ tex define If x then y else z as "
{\bf If} \ \linebreak [0]"[ x ]"
\ {\bf then} \ \linebreak [0]"[ y ]"
\ {\bf else} \ \linebreak [0]"[ z ]"" end define ]]"

\item "[[ tex define if x then y else z as "
{\bf if} \ \linebreak [0]"[ x ]"
\ {\bf then} \ \linebreak [0]"[ y ]"
\ {\bf else} \ \linebreak [0]"[ z ]"" end define ]]"

\item "[[ tex define LET x BE y as "
{\bf let} \ \linebreak [0]"[ x ]"
\ {\bf be} \ \linebreak [0]"[ y ]"" end define ]]"

\item "[[ tex define let x := y in z as "
{\bf let} \ \linebreak [0]"[ x ]"
\mathrel{\ddot{=}} "[ y ]"
\ {\bf in} \ \linebreak [0]"[ z ]"" end define ]]"

\item "[[ tex define let x = y in z as "
{\bf let} \ \linebreak [0]"[ x ]"
= "[ y ]"
\ {\bf in} \ \linebreak [0]"[ z ]"" end define ]]"

\item "[[ tex define ttst x end test as "
[ "[ x ]"
]^{\cdot}" end define ]]"

\item "[[ tex define ftst x end test as "
[ "[ x ]"
]^{-}" end define ]]"

\item "[[ tex define etst x ; y end test as "
[ "[ x ]"
= "[ y ]"
]^{=}" end define ]]"

\item "[[ tex define x reduce to y as ""[ x ]"
\stackrel {+}{\rightarrow }"[ y ]"" end define ]]"

\item "[[ tex define x == y as ""[ x ]"
\equiv "[ y ]"" end define ]]"

\item "[[ tex define x,y as ""[ x ]""[ y ]"" end define ]]"

\item "[[ tex name define x,y as ""[ x ]"
\mathrel{,}"[ y ]"" end define ]]"

\item "[[ tex define x[ y ]z as ""[ x ]""[ y ]""[ z ]"" end define ]]"

\item "[[ tex name define x[ y ]z as ""[ x ]"
{[}"[ y ]"
{]}"[ z ]"" end define ]]"

\item "[[ tex define x[[ y ]]z as ""[ x ]"$"[ y ]"$"[ z ]"" end define ]]"

\item "[[ tex name define x[[ y ]]z as ""[ x ]"
{\$}"[ y ]" {\$}"[ z ]"" end define ]]"

\item "[[ tex define x[[[ y ]]]z as ""[ x ]"$"[ y ]"$"[ z ]"" end define ]]"

\item "[[ tex name define x[[[ y ]]]z as ""[ x ]"
{\backslash[}"[ y ]"
{\backslash]}"[ z ]"" end define ]]"

\item "[[ tex define x linebreak y as ""[ x ]"
\linebreak[4] "[ y ]"" end define ]]"

\item "[[ tex name define x linebreak y as ""[ x ]"
\mathrel{linebreak} "[ y ]"" end define ]]"

\item "[[ tex define x & y as ""[ x ]"
& "[ y ]"" end define ]]"

\item "[[ tex name define x & y as ""[ x ]"
\& "[ y ]"" end define ]]"

\item "[[ tex define x \\ y as ""[ x ]"
\\{}"[ y ]"" end define ]]"

\item "[[ tex name define x \\ y as ""[ x ]"
\backslash\!\backslash "[ y ]"" end define ]]"

\end{statements}

\section{Pyk definitions}

\begin{flushleft}
"[[ protect Pyk end protect ]]"
\end{flushleft}

\section{Priority table}

This would normaly be done using "[[ name priority table ... end name ]]" but we do it this way to avoid problems with "[[ protect let asterisk := asterisk in asterisk end protect ]]".

\begin {flushleft}
"[[ protect define priority of base as Priority end define end protect ]]"
\end {flushleft}

\end{document}
" end text ,,

latex ( "chores" ) ,,
latex ( "chores" ) ,,
dvipdfm ( "chores" )

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:10:57.067491 = MJD-54293.TAI:20:11:30.067491 = LGT-4690987890067491e-6