text "page.html" : "<head>

<title>

A Logiweb base page

</title>

</head>

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

<p><address>Klaus Grue</address></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}

% Enable hyperlinks

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

\hypersetup{colorlinks=true}

% 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

"[ 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 "[[ optimized define value of ( x ) as x end define ]]". 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 "[[ x ]]" 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 "[[ optimized define value of newline x as x end define ]]". 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 + 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 If y then true else false else 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 If x BoolP then x TheBool else If x IntP then int ( x Tail ) else If x PairP then x Tail Head :: x Tail Tail else If x ExP then x Tail raise else If x MapP then map ( x Tail ) else 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 if x boolp then x Equal y else if x intp then x Equal y else if x pairp then y pairp .and. x head = y head .and. x tail = y tail else if x mapp then y mapp else 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}

\subsection{Integer addition}\label{sec:IntegerAddition}

\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 t Select PlusTag x Plus y else x LT y Select MinusTag y Minus x else PlusTag x Minus y end select end select else t Select x LT y Select PlusTag y Minus x else MinusTag x Minus y end select else 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 t Select x LT y else false end select else t Select true else 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 : if x = -1 then -1 else if y = -1 then -1 else 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 : if x = -1 then lognot ( y ) else if y = -1 then lognot ( x ) else 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 : if x = -1 then y else if y = -1 then x else 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 "[[ %% %6 %5 :: %% %6 %6 :: <<>> ]]" is represented by the number "[[ %% %6 %5 + %% %2 %5 %6 * %% %6 %6 + %% %2 %5 %6 * %% %2 %5 %6 * 1 ]]".

Strings like "[[ name "AB" end name ]]" are treated as vectors. The value of "[[ name "AB" end name ]]" is "[[ %% %6 %5 + %% %2 %5 %6 * %% %6 %6 + %% %2 %5 %6 * %% %2 %5 %6 * 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 "[[ %% %6 %5 + %% %2 %5 %6 * %% %6 %6 + %% %2 %5 %6 * %% %2 %5 %6 * 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 ) = %% %6 %6 ]]".

\item "[[ define value of vector-head ( x ) as norm x is val : vector-index ( x , 0 ) end define ]]".

\item "[[ define value of vector-tail ( x ) as norm x is val : 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 ) ]" & = & "[ %% %6 %5 :: %% %6 %6 :: %% %6 %7 :: <<>> ]" \\

"[ bt2byte* ( %% %6 %5 :: %% %6 %6 :: - 1 :: %% %2 %5 %6 :: true :: %% %6 %7 :: false :: %% %6 %8 ) ]" & = & "[ %% %6 %5 :: %% %6 %6 :: %% %6 %7 :: %% %6 %8 :: <<>> ]" \\

"[ bt2vector ( %% %6 %5 :: %% %6 %6 :: - 1 :: %% %2 %5 %6 :: true :: %% %6 %7 :: false :: %% %6 %8 ) ]" & = & "[ name "ABCD" end name ]" \\

"[ vt2byte* ( name "A" end name :: name "BC" end name :: - 1 :: name "" end name :: false :: name "D" end name ) ]" & = & "[ %% %6 %5 :: %% %6 %6 :: %% %6 %7 :: %% %6 %8 :: <<>> ]" \\

"[ 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 : if vector-empty ( x ) then reverse ( r ) else 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 : if x pairp then bt2byte*1 ( x tail , bt2byte*1 ( x head , r ) ) else 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 : if x atom then r else 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 : if vector-empty ( x ) then y else 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 : if x pairp then vt2byte*1 ( x tail , vt2byte*1 ( x head , r ) ) else 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 if x < y then 0 :: x else LET floor1 ( x , 2 * y ) BE z IN 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 LET floor1 ( x , y ) BE z IN 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 LET floor1 ( x , y ) BE z IN if z tail * 2 < y then z else if z tail * 2 > y then z head + 1 :: z tail - y else if evenp ( z head ) then z else 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 if y <= 0 then exception else if 0 <= x then floor1 ( x , y ) else 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 if y <= 0 then exception else if 0 <= x then floor1 ( x , y ) else 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 if y <= 0 then exception else if 0 < x then ceiling1 ( x , y ) else 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 if y <= 0 then exception else if 0 < x then round1 ( x , y ) else 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 : 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 : if n <= 0 then x head else nth ( n - 1 , x tail ) end define ]]"

\item "[[ define value of length ( x ) as norm x is val : length1 ( x , 0 ) end define ]]".

Compute length of list.

\item "[[ define value of length1 ( x , r ) as norm x is val : r is val : 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 "[[ define value of list-prefix ( l , n ) as norm l is val : n is val : 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 "[[ define value of list-suffix ( l , n ) as norm l is val : n is val : 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 : if x atom .or. y atom then true else 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 : if a atom then true else if a head intp then if i = a head then a tail else true else 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 : if a atom then array3 ( i , v ) else if a head intp then if i = a head then array3 ( i , v ) else array5 ( a head , a tail , i , v , x ) else if logbitp ( x , i ) then array4 ( a head , array2 ( a tail , i , v , x + 1 ) ) else 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 atom then if b atom then true else if b head intp then b else a :: b else 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 : if logbitp ( x , i ) then if logbitp ( x , j ) then true :: array5 ( i , v , j , w , x + 1 ) else j :: w :: i :: v else if logbitp ( x , j ) then i :: v :: j :: w else 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 : LET t ref BE r IN LET t idx BE i IN if r = 0 then i maptag else if i = 0 then if r = c [[ 0 ]] then c maptag else c [[ c [[ 0 ]] ]] [[ "cache" ]] [[ r ]] maptag else LET c [[ r ]] [[ "code" ]] [[ i ]] BE f IN if f mapp then eval1 ( f , t tail , s , c ) else if f = true then lookup ( t , s , map ( true ) ) else if f = 1 then t first maptag else 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 : if t atom then f else 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 : LET test3 ( c [[ c [[ 0 ]] ]] [[ "expansion" ]] , c ) catch BE p IN if p tail != true then p tail else 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 : LET t ref BE r IN LET t idx BE i IN if r = 0 .or. i = 0 then true else LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "claim" ]] BE d IN if d pairp then eval ( d third , true , c ) apply t :: c :: true maptag untag else 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 "[[ define value of testfunc1 ( x ) as x + 3 end define ]]" This is an ordinary definition: "[[ etst testfunc1 ( 2 ) ; 5 end test ]]".

\item "[[ define value of 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 base [[ 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 define value of testfunc2 ( x , x ) as x end define end quote end hide end test ]]".

\item "[[ define value of testfunc3 as 2 end define ]]" and "[[ define value of 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 "[[ define value of testfunc4 as quote define value of 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 define value of 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 "[[ define value of 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 base [[ quote y end quote ref ]] [[ "code" ]] [[ quote y end quote idx ]] ; true end test ]]"

\item "[[ define value of 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 "[[ define value of 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 "[[ define value of 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 : 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 : LET t ref BE r IN LET t idx BE i IN if r = 0 then t else if i = 0 then t else LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "macro" ]] BE d IN if d = true then t head :: macro3* ( t tail , s , c ) else 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 : 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 : if t atom then true else 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 : LET lookup ( t , s , true ) BE d IN 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 : if t atom then true else 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 : LET x zeroth BE t IN LET zip ( d first tail , t tail ) BE s IN 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 define macro of x as \ x . expand ( quote macro define x as y end define end quote , x ) 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 "[[ define macro of protect u end protect as \ x . x zeroth first end define ]]"

The "[[ x ]]" 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 "[[ define macro of Macro define u as v end define as \ x . Macrodefine ( x ) end define ]]"

The "[[ hide define macro of u as v end define end hide ]]" construct macro expands into "[[ hide define macro of u as v end define 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 : if x = true then quote true end quote else LET x zeroth BE t IN LET t first BE u IN LET t second BE v IN LET quote u end quote :: u :: quote v end quote :: v :: true BE s IN substitute ( t , quote define macro of u as v end define end quote , s ) end define ]]"

This function performs the actual work of the "[[ hide define macro of 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 define macro of 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 define macro of u as v end define 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 "[[ define macro of 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 : LET x zeroth BE t IN LET t first BE u IN LET quote t end quote :: t :: quote u end quote :: u :: true BE s IN 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 "[[ define macro of self as \ x . makeself ( x ) end define ]]" The "[[ base ]]" construct expands into the page symbol of the page on which the "[[ base ]]" construct occurs.

\item "[[ define value of makeself ( x ) as norm x is val : LET x zeroth BE t IN LET x second BE c IN LET t debug BE d IN LET c [[ 0 ]] BE r IN r :: 0 :: d :: true end define ]]"

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

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

The "[[ u ]]" 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 : LET x zeroth BE t IN LET t first BE u IN LET u ref BE r IN LET u idx BE i IN LET t debug BE d IN r :: i :: d :: stateexpand* ( u tail , x first , x second ) end define ]]"

\end{statements}

\subsection{Definition macros}

\begin{statements}

\item "[[ define macro of render define x as y end define as \ x . expand ( quote macro define render define x as y end define as Define render of root protect x end protect as y end define end define end quote , x ) end define ]]"

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

\item "[[ define macro of tex define x as y end define as \ x . expand ( quote macro define tex define x as y end define as Define tex of root protect x end protect as y end define end define end quote , x ) end define ]]"

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

\item "[[ define macro of tex name define x as y end define as \ x . expand ( quote 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 end quote , x ) end define ]]"

\item "[[ define macro of value define x as y end define as \ x . expand ( quote macro define value define x as y end define as define value of root protect x end protect as y end define end define end quote , x ) end define ]]"

\item "[[ define macro of message define x as y end define as \ x . expand ( quote macro define message define x as y end define as define message of root protect x end protect as y end define end define end quote , x ) end define ]]"

\item "[[ define macro of priority table x as \ x . expand ( quote macro define priority table x as define priority of self as protect x end protect end define end define end quote , x ) end define ]]"

Define the priority table of the page.

\item "[[ define macro of verifier x end verifier as \ x . expand ( quote macro define verifier x end verifier as define claim of self as x end define end define end quote , x ) end define ]]"

Define the claim of the page.

\item "[[ define macro of unpacker x end unpacker as \ x . expand ( quote macro define unpacker x end unpacker as define unpack of self as x end define end define end quote , x ) end define ]]"

Define the unpacker of the page.

\item "[[ define macro of renderer x end renderer as \ x . expand ( quote macro define renderer x end renderer as define render of self as x end define end define end quote , x ) end define ]]"

Define the renderer of the page.

\item "[[ define macro of expander x end expander as \ x . expand ( quote macro define expander x end expander as define macro of self as x end define end define end quote , x ) end define ]]"

Define the macro expansion engine of the page.

\item "[[ define macro of executer x end executer as \ x . expand ( quote macro define executer x end executer as define execute of self as x end define end define end quote , x ) end define ]]"

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

\item "[[ define macro of executables x end executables as \ x . expand ( quote macro define executables x end executables as define executables of self as x end define end define end quote , x ) end define ]]"

Define an association list from names to programs.

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

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 "[[ proclaim tex name define x as y end define as "hide" end proclaim ]]"

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

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

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

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

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 "[[ define macro of ( x ) as \ x . expand ( quote macro define ( x ) as x end define end quote , x ) end define ]]"

\item "[[ define macro of newline x as \ x . expand ( quote macro define newline x as x end define end quote , 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 "[[ %% %1 %2 %3 ]]" 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 "[[ define macro of 0x as \ x . numeral ( x ) end define ]]"

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

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

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

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

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

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

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

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

\item "[[ define macro of 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 "[[ 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 ]]"

\item "[[ define value of num2 ( r , t , u ) as norm r is val : t is val : u is val : LET quote x end quote :: u :: true BE s IN if t r= quote 0 end quote then substitute ( r , quote x %0 end quote , s ) else if t r= quote 1 end quote then substitute ( r , quote x %1 end quote , s ) else if t r= quote 2 end quote then substitute ( r , quote x %2 end quote , s ) else if t r= quote 3 end quote then substitute ( r , quote x %3 end quote , s ) else if t r= quote 4 end quote then substitute ( r , quote x %4 end quote , s ) else if t r= quote 5 end quote then substitute ( r , quote x %5 end quote , s ) else if t r= quote 6 end quote then substitute ( r , quote x %6 end quote , s ) else if t r= quote 7 end quote then substitute ( r , quote x %7 end quote , s ) else if t r= quote 8 end quote then substitute ( r , quote x %8 end quote , s ) else if t r= quote 9 end quote then substitute ( r , quote x %9 end quote , s ) else substitute ( r , quote exception end quote , true ) end define ]]"

\end{statements}

\subsection{Formating of the expansion}

\begin{statements}

\item "[[ define macro of make macro expanded version ragged right as \ x . expand ( quote macro define make macro expanded version ragged right as ragged right end define end quote , x ) 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 x 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 "[[ define macro of macro name x end name as \ x . expand ( quote macro define macro name x end name as x end define end quote , 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 "[[ define macro of hiding name x end name as \ x . expand ( quote macro define hiding name x end name as protect hiding name x end name end protect end define end quote , x ) end define ]]"

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

\end{statements}

\subsection{Tuples}

\begin{statements}

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

\item "[[ define macro of << 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 : if .not. u r= quote x ,, y end quote then substitute ( t , quote u :: <<>> end quote , quote u end quote :: u :: true ) else 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 "[[ define macro of eager define u as v end define as \ x . eager1 ( x ) end define ]]"

\item "[[ define value of eager1 ( x ) as norm x is val : LET x zeroth BE t IN LET t first BE u IN LET t second BE v IN LET quote u end quote :: u :: quote w end quote :: eager2 ( t , u tail , v ) :: true BE s IN 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 : if p atom then v else LET quote x end quote :: p head :: quote v end quote :: eager2 ( t , p tail , v ) :: true BE s IN substitute ( t , quote x is val : v end quote , s ) end define ]]"

\item "[[ define macro of eager message define x as y end define as \ x . expand ( quote 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 quote , x ) end define ]]"

\end{statements}

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

\begin{statements}

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

\item "[[ define value of macrolet1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN LET t first BE u IN LET t third BE w IN LET u ref BE r IN LET u idx BE i IN LET c [[ r :: "codex" :: r :: i :: 0 :: "macro" :: true => macrodefine ( x ) ]] BE c IN stateexpand ( w , s , c ) end define ]]"

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

\item "[[ define macro of destructure define x as y end define as \ x . expand ( quote macro define destructure define x as y end define as define destructure of root protect x end protect as y end define end define end quote , x ) end define ]]"

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

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

\item "[[ define value of let1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN LET t first BE u IN LET t second BE v IN LET t third BE w IN LET stateexpand ( u , s , c ) BE u IN LET stateexpand ( v , s , c ) BE v IN LET stateexpand ( w , s , c ) BE w IN LET make-prime ( make-var ( t ) ) BE x IN LET let2 ( x , u , w , c ) BE w IN 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 : LET p ref BE r IN LET p idx BE i IN LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] BE c prime IN LET c prime [[ "destructure" ]] BE d IN if d = true then if c prime [[ "value" ]] != true then w else make-let ( p , quote asterisk end quote , w ) else LET let3 ( x , p tail , w , c ) BE w IN 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 : if p prime = true then w else LET p prime head BE p IN LET p prime tail BE p prime IN LET let3 ( x , p prime , w , c ) BE w IN LET let2 ( make-prime ( x ) , p , w , c ) BE w IN LET make-let ( x , make-tail ( x ) , w ) BE w IN make-let ( quote asterisk end quote , make-head ( x ) , w ) end define ]]"

\item "[[ define value of make-var ( t ) as norm t is val : 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 : LET quote u end quote :: u :: quote v end quote :: v :: quote w end quote :: w :: true BE s IN 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 : LET quote x end quote :: x :: true BE s IN substitute ( x , quote x prime end quote , s ) end define ]]"

\item "[[ define value of make-head ( x ) as norm x is val : LET quote x end quote :: x :: true BE s IN substitute ( x , quote x head end quote , s ) end define ]]"

\item "[[ define value of make-tail ( x ) as norm x is val : LET quote x end quote :: x :: true BE s IN substitute ( x , quote x tail end quote , s ) end define ]]"

\end{statements}

\subsection{Backquoting}

\begin{statements}

\item "[[ define macro of 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 : if v r= quote true unquote end quote then v first else 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 : if v atom then make-true ( t ) else 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 , define priority of base as y end define ) 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 "[[ define macro of 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 : LET z zeroth BE t IN LET z first BE s IN LET z second BE c IN LET name quote priority table x end quote end name BE p IN LET p ref :: p idx :: t debug :: t second :: true BE y IN LET stateexpand ( y , s , c ) BE y IN LET stateexpand ( t fifth , s , c ) BE m IN LET stateexpand ( t sixth , s , c ) BE a IN LET name quote page ( x , y ) title t bib b main text m appendix a end page end quote end name BE p IN 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 ) define value of quit ( x ) as 0 :: "quit" :: <<>> :: x :: <<>> end define \\ define value of write ( s ) as 0 :: "write" :: <<>> :: s :: <<>> end define \\ define value of exec ( p , h ) as 0 :: "exec" :: <<>> :: p :: h :: <<>> end define \\ define value of extend ( s ) as 0 :: "extend" :: <<>> :: s :: <<>> end define end array ]"\]

\noindent And the following input events:

\["[ array ( left ) define value of boot ( a , e , c ) as 0 :: "boot" :: <<>> :: a :: e :: c :: <<>> end define \\ define value of read ( c ) as 0 :: "read" :: <<>> :: c :: <<>> end define \\ define value of int ( i , p ) as 0 :: "int" :: <<>> :: i :: p :: <<>> end define \\ define value of 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 "[[ %% %1 %0 + %% %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 "[[ define value of 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 "[[ define value of Echo as map ( \ x . Echo1 ( x ) ) end define ]]"

\noindent "[[ define value of Echo1 ( x ) as if x atom then exec ( true , Echo ) :: <<>> else LET x head BE e IN LET Echo1 ( x tail ) BE r IN if .not. e head = 0 :: "read" :: <<>> then r else 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 "[[ define value of Eecho as map ( \ x . Eecho1 ( x ) ) end define ]]"

\noindent "[[ define value of Eecho1 ( x ) as if x atom then exec ( true , Eecho ) :: <<>> else LET x head BE e IN LET Eecho1 ( x tail ) BE r IN if .not. e head = 0 :: "read" :: <<>> then r else 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, "[[ define execute of base as Eecho end define ]]" 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.

"[[ define executables of base as "hello" :: Hello World :: "echo" :: Echo :: <<>> end define ]]" 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}

% Enable hyperlinks

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

\hypersetup{colorlinks=true}

% 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 "[[ Define tex of proclaim x as y end proclaim as "

[ "[ texname x end texname ]"

\bowtie "[ texname y end texname ]"

]" end define ]]"

\item "[[ Define tex of empty as "" end define ]]"

\item "[[ Define tex name of empty as "empty" end define ]]"

\item "[[ Define tex of preassociative x greater than y as "

\newline \mathbf {Preassociative} \newline "[ x ]"

; "[ y ]"" end define ]]"

\item "[[ Define tex name of preassociative x greater than y as "

\mathbf{Preassociative}\,"[ x ]"

; "[ y ]"" end define ]]"

\item "[[ Define tex of postassociative x greater than y as "

\newline\mathbf{Postassociative} \newline "[ x ]"

; "[ y ]"" end define ]]"

\item "[[ Define tex name of postassociative x greater than y as "

\mathbf{Postassociative}\,"[ x ]"

; "[ y ]"" end define ]]"

\item "[[ Define tex of priority x equal y as "

["[ texname x end texname ]"

] , \linebreak [0] "[ y ]"" end define ]]"

\item "[[ Define tex name of priority x equal y as "

["[ x ]"

] , \linebreak [0] "[ y ]"" end define ]]"

\item "[[ Define tex of priority x end priority as "

["[ texname x end texname ]"

]" end define ]]"

\item "[[ Define tex name of priority x end priority as "

priority \ "[ x ]"

\ end" end define ]]"

\item "[[ Define tex of asterisk as "

\ast " end define ]]"

\item "[[ Define tex of pyk as "

pyk" end define ]]"

\item "[[ Define tex of define x of y as z end define as "

[ "[ texname y end texname ]"

\stackrel{"[ x ]"

}{\rightarrow}"[ z ]"

]" end define ]]"

\item "[[ Define tex of math x end math as "$"[ x ]"$" end define ]]"

\item "[[ Define tex name of math x end math as "

\ \$"[ x ]"\$\linebreak[0]\ " end define ]]"

\item "[[ Define tex of display math x end math as "$$"[ x ]"$$" end define ]]"

\item "[[ Define tex name of display math x end math as "

\ \$\$"[ x ]"\$\$\linebreak[0]\ " end define ]]"

\item "[[ Define tex of a as "

\mathit{a}" end define ]]"

\item "[[ Define tex of b as "

\mathit{b}" end define ]]"

\item "[[ Define tex of c as "

\mathit{c}" end define ]]"

\item "[[ Define tex of d as "

\mathit{d}" end define ]]"

\item "[[ Define tex of e as "

\mathit{e}" end define ]]"

\item "[[ Define tex of f as "

\mathit{f}" end define ]]"

\item "[[ Define tex of g as "

\mathit{g}" end define ]]"

\item "[[ Define tex of h as "

\mathit{h}" end define ]]"

\item "[[ Define tex of i as "

\mathit{i}" end define ]]"

\item "[[ Define tex of j as "

\mathit{j}" end define ]]"

\item "[[ Define tex of k as "

\mathit{k}" end define ]]"

\item "[[ Define tex of l as "

\mathit{l}" end define ]]"

\item "[[ Define tex of m as "

\mathit{m}" end define ]]"

\item "[[ Define tex of n as "

\mathit{n}" end define ]]"

\item "[[ Define tex of o as "

\mathit{o}" end define ]]"

\item "[[ Define tex of p as "

\mathit{p}" end define ]]"

\item "[[ Define tex of q as "

\mathit{q}" end define ]]"

\item "[[ Define tex of r as "

\mathit{r}" end define ]]"

\item "[[ Define tex of s as "

\mathit{s}" end define ]]"

\item "[[ Define tex of t as "

\mathit{t}" end define ]]"

\item "[[ Define tex of u as "

\mathit{u}" end define ]]"

\item "[[ Define tex of v as "

\mathit{v}" end define ]]"

\item "[[ Define tex of w as "

\mathit{w}" end define ]]"

\item "[[ Define tex of x as "

\mathit{x}" end define ]]"

\item "[[ Define tex of y as "

\mathit{y}" end define ]]"

\item "[[ Define tex of z as "

\mathit{z}" end define ]]"

\item "[[ Define tex of A as "

\mathit{A}" end define ]]"

\item "[[ Define tex of B as "

\mathit{B}" end define ]]"

\item "[[ Define tex of C as "

\mathit{C}" end define ]]"

\item "[[ Define tex of D as "

\mathit{D}" end define ]]"

\item "[[ Define tex of E as "

\mathit{E}" end define ]]"

\item "[[ Define tex of F as "

\mathit{F}" end define ]]"

\item "[[ Define tex of G as "

\mathit{G}" end define ]]"

\item "[[ Define tex of H as "

\mathit{H}" end define ]]"

\item "[[ Define tex of I as "

\mathit{I}" end define ]]"

\item "[[ Define tex of J as "

\mathit{J}" end define ]]"

\item "[[ Define tex of K as "

\mathit{K}" end define ]]"

\item "[[ Define tex of L as "

\mathit{L}" end define ]]"

\item "[[ Define tex of M as "

\mathit{M}" end define ]]"

\item "[[ Define tex of N as "

\mathit{N}" end define ]]"

\item "[[ Define tex of O as "

\mathit{O}" end define ]]"

\item "[[ Define tex of P as "

\mathit{P}" end define ]]"

\item "[[ Define tex of Q as "

\mathit{Q}" end define ]]"

\item "[[ Define tex of R as "

\mathit{R}" end define ]]"

\item "[[ Define tex of S as "

\mathit{S}" end define ]]"

\item "[[ Define tex of T as "

\mathit{T}" end define ]]"

\item "[[ Define tex of U as "

\mathit{U}" end define ]]"

\item "[[ Define tex of V as "

\mathit{V}" end define ]]"

\item "[[ Define tex of W as "

\mathit{W}" end define ]]"

\item "[[ Define tex of X as "

\mathit{X}" end define ]]"

\item "[[ Define tex of Y as "

\mathit{Y}" end define ]]"

\item "[[ Define tex of Z as "

\mathit{Z}" end define ]]"

\item "[[ Define tex of true as "

\mathsf{T}" end define ]]"

\item "[[ Define tex of quote x end quote as "

\lceil "[ x ]"

\rceil " end define ]]"

\item "[[ Define tex of optimized define x of y as z end define as "

["[ texname y end texname ]"

\stackrel {"[ x ]"

}{\rightarrow\rightarrow }"[ z ]"

]" end define ]]"

\item "[[ Define tex of tex as "

tex" end define ]]"

\item "[[ Define tex of tex name as "

name" end define ]]"

\item "[[ Define tex of priority as "

prio" end define ]]"

\item "[[ Define tex of value as "

val" end define ]]"

\item "[[ Define tex of macro as "

macro" end define ]]"

\item "[[ Define tex of claim as "

claim" end define ]]"

\item "[[ Define tex of message as "

msg" end define ]]"

\item "[[ Define tex of name x end name as ""[ texname x end texname ]"" end define ]]"

\item "[[ Define tex name of name x end name as "

name("[ x ]"

)" end define ]]"

\item "[[ Define tex of macro name x end name as ""[ texname x end texname ]"" end define ]]"

\item "[[ Define tex name of macro name x end name as "

macroname("[ x ]"

)" end define ]]"

\item "[[ Define tex of hiding name x end name as ""[ texname x end texname ]"" end define ]]"

\item "[[ Define tex name of hiding name x end name as "

hidename("[ x ]"

)" end define ]]"

\item "[[ Define tex of hide x end hide as x end define ]]"

\item "[[ Define tex name of hide x end hide as "

hide("[ x ]"

)" end define ]]"

\item "[[ Define tex of array ( x ) y end array as "

\begin{array}{"[ x ]"}

"[ y ]"

\end{array}" end define ]]"

\item "[[ Define tex name of array ( x ) y end array as "

array("[ x ]"

)\{"[ y ]"

\}" end define ]]"

\item "[[ Define tex of left as "l" end define ]]"

\item "[[ Define tex of center as "c" end define ]]"

\item "[[ Define tex of right as "r" end define ]]"

\item "[[ Define tex of %% as "" end define ]]"

\item "[[ Define tex name of %% as "\{\}" end define ]]"

\item "[[ Define tex of ( x ) as "

("[ x ]"

)" end define ]]"

\item "[[ Define tex of < x | y := z > as "

\langle "[ x ]"

\,{|}"[ y ]"

{:=}\,"[ z ]"

\rangle " end define ]]"

\item "[[ Define tex of bottom as "

\bot " end define ]]"

\item "[[ Define tex of false as "

\mathsf{F}" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex of ... as "

\ldots " end define ]]"

\item "[[ Define tex of --- as "

\cdots " end define ]]"

\item "[[ Define tex of exception as "

\bullet " end define ]]"

\item "[[ Define tex of 0 as "

0" end define ]]"

\item "[[ Define tex of 1 as "

1" end define ]]"

\item "[[ Define tex of 2 as "

2" end define ]]"

\item "[[ Define tex of 3 as "

3" end define ]]"

\item "[[ Define tex of 4 as "

4" end define ]]"

\item "[[ Define tex of 5 as "

5" end define ]]"

\item "[[ Define tex of 6 as "

6" end define ]]"

\item "[[ Define tex of 7 as "

7" end define ]]"

\item "[[ Define tex of 8 as "

8" end define ]]"

\item "[[ Define tex of 9 as "

9" end define ]]"

\item "[[ Define tex of protect x end protect as "

protect("[ x ]"

)" end define ]]"

\item "[[ Define tex of root protect x end protect as "

root\ protect( "[ x ]"

)" end define ]]"

\item "[[ Define tex of render define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{render}{=} "[ texname y end texname ]"

]" end define ]]"

\item "[[ Define tex of tex define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{tex}{=} "[ texname y end texname ]"

]" end define ]]"

\item "[[ Define tex of tex name define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{name}{=} "[ texname y end texname ]"

]" end define ]]"

\item "[[ Define tex of value define x as y end define as "

[ "[ texname x end texname ]"

\mathrel{\dot{=}} "[ y ]"

]" end define ]]"

\item "[[ Define tex of message define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{msg}{=} "[ y ]"

]" end define ]]"

\item "[[ Define tex of Macro define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{\circ}{=} "[ y ]"

]" end define ]]"

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

[ "[ texname x end texname ]"

\mathrel{\ddot{=}} "[ y ]"

]" end define ]]"

\item "[[ Define tex of priority table x as "

\mathbf{Priority\ table} \linebreak[4] "[ x ]"" end define ]]"

\item "[[ Define tex name of priority table x as "

\mathbf{Priority\ table} \ "[ x ]"" end define ]]"

\item "[[ Define tex of verifier x end verifier as "

[ \mathbf{Verifier\colon} "[ x ]"

]" end define ]]"

\item "[[ Define tex of unpacker x end unpacker as "

[ \mathbf{Unpacker\colon} "[ x ]"

]" end define ]]"

\item "[[ Define tex of renderer x end renderer as "

[ \mathbf{Renderer\colon} "[ x ]"

]" end define ]]"

\item "[[ Define tex of expander x end expander as "

[ \mathbf{Expander\colon} "[ x ]"

]" end define ]]"

\item "[[ Define tex of executer x end executer as "

[ \mathbf{Executer\colon} "[ x ]"

]" end define ]]"

\item "[[ Define tex of executables x end executables as "

[ \mathbf{Executables\colon} "[ x ]"

]" end define ]]"

\item "[[ Define tex of ragged right as "

\raggedright" end define ]]"

\item "[[ Define tex name of ragged right as "

\backslash raggedright " end define ]]"

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

\item "[[ Define tex name of make macro expanded version ragged right as "

make\ expansion\ ragged\ right " end define ]]"

\item "[[ Define tex of <<>> as "

\langle \, \rangle" end define ]]"

\item "[[ Define tex of << x >> as "

\langle "[ x ]"

\rangle " end define ]]"

\item "[[ Define tex of eager define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{\bullet}{=} "[ y ]"

]" end define ]]"

\item "[[ Define tex of eager message define x as y end define as "

[ message\ "[ texname x end texname ]"

: "[ texname y end texname ]"

]" end define ]]"

\item "[[ Define tex of destructure as "

dest" end define ]]"

\item "[[ Define tex of destructure define x as y end define as "

[ "[ texname x end texname ]"

\stackrel{dest}{=} "[ y ]"

]" end define ]]"

\item "[[ Define tex of back x quote y end quote as "

\lceil_{\!"[ x ]"

\,} "[ y ]"

\rceil " end define ]]"

\item "[[ Define tex of text x : y end text as "text"[ x ]y end define ]]"

\item "[[ Define tex name of text x : y end text as "

text\ "[ x ]"

: "[ y ]"

end\ file" end define ]]"

\item "[[ Define tex of tex ( x ) as "tex",x end define ]]"

\item "[[ Define tex name of tex ( x ) as "

tex("[ x ]"

)" end define ]]"

\item "[[ Define tex of latex ( x ) as "latex",x end define ]]"

\item "[[ Define tex name of latex ( x ) as "

latex("[ x ]"

)" end define ]]"

\item "[[ Define tex of bibtex ( x ) as "bibtex",x end define ]]"

\item "[[ Define tex name of bibtex ( x ) as "

bibtex("[ x ]"

)" end define ]]"

\item "[[ Define tex of makeindex ( x ) as "makeindex",x end define ]]"

\item "[[ Define tex name of makeindex ( x ) as "

makeindex("[ x ]"

)" end define ]]"

\item "[[ Define tex of dvipdfm ( x ) as "dvipdfm",x end define ]]"

\item "[[ Define tex name of dvipdfm ( x ) as "

dvipdfm("[ x ]"

)" end define ]]"

\item "[[ Define tex name of 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 "[[ Define tex of page ( x , y ) title t bib b main text m appendix a end page as tex-file ( "text" , "page.html" , "<head><title>"[ t ]"</title></head>

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

<p><address>The <a href="!http://logiweb.eu/"!>pyk</a> compiler</address></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}

% Enable hyperlinks

\usepackage[dvipdfm=true]{hyperref}

\hypersetup{pdfpagemode=none}

\hypersetup{pdfstartpage=1}

\hypersetup{pdfstartview=FitBH}

\hypersetup{pdfpagescrop={120 80 490 730}}

\hypersetup{pdftitle="[ t ]"}

\hypersetup{colorlinks=true}

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

% Enable hyperlinks

\usepackage[dvipdfm=true]{hyperref}

\hypersetup{pdfpagemode=none}

\hypersetup{pdfstartpage=1}

\hypersetup{pdfstartview=FitBH}

\hypersetup{pdfpagescrop={120 80 490 730}}

\hypersetup{pdftitle="[ t ]" - appendix}

\hypersetup{colorlinks=true}

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

% Enable hyperlinks

\usepackage[dvipdfm=true]{hyperref}

\hypersetup{pdfpagemode=none}

\hypersetup{pdfstartpage=1}

\hypersetup{pdfstartview=FitBH}

\hypersetup{pdfpagescrop={120 80 490 730}}

\hypersetup{pdftitle="[ t ]" - chores}

\hypersetup{colorlinks=true}

% 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 "[[ Define tex of -x as "

{}^{-}\! ",x end define ]]"

\item "[[ Define tex of + x as "

{+} "[ x ]"" end define ]]"

"[[ Define tex of x factorial as ""[ x ]"

!" end define ]]"

"[[ Define tex of x _ { y } as ""[ x ]"

_{"[ y ]"

}" end define ]]"

"[[ Define tex of x prime as ""[ x ]"

{}' " end define ]]"

"[[ Define tex name of x _ { y } as ""[ x ]"

\_\{"[ y ]"

\}" end define ]]"

"[[ Define tex of x %0 as ""[ x ]"0" end define ]]"

"[[ Define tex of x %1 as ""[ x ]"1" end define ]]"

"[[ Define tex of x %2 as ""[ x ]"2" end define ]]"

"[[ Define tex of x %3 as ""[ x ]"3" end define ]]"

"[[ Define tex of x %4 as ""[ x ]"4" end define ]]"

"[[ Define tex of x %5 as ""[ x ]"5" end define ]]"

"[[ Define tex of x %6 as ""[ x ]"6" end define ]]"

"[[ Define tex of x %7 as ""[ x ]"7" end define ]]"

"[[ Define tex of x %8 as ""[ x ]"8" end define ]]"

"[[ Define tex of x %9 as ""[ x ]"9" end define ]]"

"[[ Define tex of x head as ""[ x ]"

{}^h" end define ]]"

"[[ Define tex of x tail as ""[ x ]"

{}^t" end define ]]"

"[[ Define tex of x raise as ""[ x ]"

{}^{\bullet}" end define ]]"

"[[ Define tex of x catch as ""[ x ]"

{}^{\circ}" end define ]]"

"[[ Define tex of x catching maptag as ""[ x ]"

{}^{M^{\circ}}" end define ]]"

"[[ Define tex of x maptag as ""[ x ]"

{}^M" end define ]]"

"[[ Define tex of x untag as ""[ x ]"

{}^U" end define ]]"

"[[ Define tex of x root as ""[ x ]"

{}^R" end define ]]"

"[[ Define tex of x norm as ""[ x ]"

{}^N" end define ]]"

"[[ Define tex of x boolp as ""[ x ]"

\in \mathbf{B}" end define ]]"

"[[ Define tex of x truep as ""[ x ]"

\in \mathbf{T}" end define ]]"

"[[ Define tex of x falsep as ""[ x ]"

\in \mathbf{F}" end define ]]"

"[[ Define tex of x intp as ""[ x ]"

\in \mathbf{Z}" end define ]]"

"[[ Define tex of x pairp as ""[ x ]"

\in \mathbf{P}" end define ]]"

"[[ Define tex of x atom as ""[ x ]"

\in \mathbf{A}" end define ]]"

"[[ Define tex of x mapp as ""[ x ]"

\in \mathbf{M}" end define ]]"

"[[ Define tex of x objectp as ""[ x ]"

\in \mathbf{O}" end define ]]"

"[[ Define tex of x zeroth as ""[ x ]"

{}^0" end define ]]"

"[[ Define tex of x first as ""[ x ]"

{}^1" end define ]]"

"[[ Define tex of x second as ""[ x ]"

{}^2" end define ]]"

"[[ Define tex of x third as ""[ x ]"

{}^3" end define ]]"

"[[ Define tex of x fourth as ""[ x ]"

{}^4" end define ]]"

"[[ Define tex of x fifth as ""[ x ]"

{}^5" end define ]]"

"[[ Define tex of x sixth as ""[ x ]"

{}^6" end define ]]"

"[[ Define tex of x seventh as ""[ x ]"

{}^7" end define ]]"

"[[ Define tex of x eighth as ""[ x ]"

{}^8" end define ]]"

"[[ Define tex of x ninth as ""[ x ]"

{}^9" end define ]]"

"[[ Define tex of x ref as ""[ x ]"

{}^r" end define ]]"

"[[ Define tex of x idx as ""[ x ]"

{}^i" end define ]]"

"[[ Define tex of x debug as ""[ x ]"

{}^d" end define ]]"

"[[ Define tex of a [[ i ]] as ""[ a ]"

\linebreak[0][ "[ i ]"

]" end define ]]"

"[[ Define tex of a [[ i -> v ]] as ""[ a ]"

\linebreak[0][ "[ i ]"

{\rightarrow} "[ v ]"

]" end define ]]"

"[[ Define tex of a [[ i => v ]] as ""[ a ]"

\linebreak[0][ "[ i ]"

{\Rightarrow} "[ v ]"

]" end define ]]"

\item "[[ Define tex of x unquote as "

\underline{ "[ x ]"

} " end define ]]"

\item "[[ Define tex name of x unquote as ""[ x ]"

unquote" end define ]]"

\item "[[ Define tex of newline x as "

\newline "[ x ]"" end define ]]"

\item "[[ Define tex name of newline x as "

newline\ "[ x ]"" end define ]]"

\item "[[ Define tex of x ' y as ""[ x ]"

\mathbin {\mbox {'}}"[ y ]"" end define ]]"

\item "[[ Define tex of x apply y as ""[ x ]"

\mathbin {\mbox {''}}"[ y ]"" end define ]]"

\item "[[ Define tex of texname x end texname as "

\underline{ "[ x ]"

}" end define ]]"

\item "[[ Define tex of - x as "

{-} "[ x ]"" end define ]]"

\item "[[ Define tex of +x as "

{}^{+}\! ",x end define ]]"

\item "[[ Define tex of x * y as ""[ x ]"

\cdot "[ y ]"" end define ]]"

\item "[[ Define tex of x + y as ""[ x ]"

+ "[ y ]"" end define ]]"

\item "[[ Define tex of x - y as ""[ x ]"

- "[ y ]"" end define ]]"

\item "[[ Define tex of x :: y as ""[ x ]"

\mathop{:\,:} "[ y ]"" end define ]]"

\item "[[ Define tex of x ,, y as ""[ x ]"

, "[ y ]"" end define ]]"

\item "[[ Define tex of x = y as ""[ x ]"

= "[ y ]"" end define ]]"

\item "[[ Define tex of x != y as ""[ x ]"

\neq "[ y ]"" end define ]]"

\item "[[ Define tex of x < y as ""[ x ]"

< "[ y ]"" end define ]]"

\item "[[ Define tex of x > y as ""[ x ]"

> "[ y ]"" end define ]]"

\item "[[ Define tex of x <= y as ""[ x ]"

\le "[ y ]"" end define ]]"

\item "[[ Define tex of x >= y as ""[ x ]"

\ge "[ y ]"" end define ]]"

\item "[[ Define tex of x r= y as ""[ x ]"

\stackrel{r}{=} "[ y ]"" end define ]]"

\item "[[ Define tex of x t= y as ""[ x ]"

\stackrel{t}{=} "[ y ]"" end define ]]"

\item "[[ Define tex of x t=* y as ""[ x ]"

\stackrel{t^*}{=} "[ y ]"" end define ]]"

\item "[[ Define tex of .not. x as "

{\bf not} \ \linebreak [0]"[ x ]"" end define ]]"

\item "[[ Define tex of x .and. y as ""[ x ]"

\ {\bf and} \ \linebreak [0]"[ y ]"" end define ]]"

\item "[[ Define tex of x &c y as ""[ x ]"

\wedge_c "[ y ]"" end define ]]"

\item "[[ Define tex of x .or. y as ""[ x ]"

\ {\bf or} \ \linebreak [0]"[ y ]"" end define ]]"

\item "[[ Define tex of x is val : y as ""[ x ]"

{\in} \mathbf{V} \colon "[ y ]"" end define ]]"

\item "[[ Define tex of x is bool : y as ""[ x ]"

{\in} \mathbf{B} \colon "[ y ]"" end define ]]"

\item "[[ Define tex of x is int : y as ""[ x ]"

{\in} \mathbf{Z} \colon "[ y ]"" end define ]]"

\item "[[ Define tex of x is pair : y as ""[ x ]"

{\in} \mathbf{P} \colon "[ y ]"" end define ]]"

\item "[[ Define tex of x is map : y as ""[ x ]"

{\in} \mathbf{M} \colon "[ y ]"" end define ]]"

\item "[[ Define tex of x is object : y as ""[ x ]"

{\in} \mathbf{O} \colon "[ y ]"" end define ]]"

\item "[[ Define tex of x Select y else z end select as ""[ x ]"

\left\langle\protect \begin {array}{l}"[ y ]"

\\"[ z ]"

\protect \end {array}\right." end define ]]"

\item "[[ Define tex of x IN y as ""[ x ]"

\ \mathbf{in}\ \linebreak [0] "[ y ]"" end define ]]"

\item "[[ Define tex of \ x . y as "

\lambda "[ x ]"

."[ y ]"" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex of 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 "[[ Define tex of LET x BE y as "

{\bf let} \ \linebreak [0]"[ x ]"

\ {\bf be} \ \linebreak [0]"[ y ]"" end define ]]"

\item "[[ Define tex of let x := y in z as "

{\bf let} \ \linebreak [0]"[ x ]"

\mathrel{\ddot{=}} "[ y ]"

\ {\bf in} \ \linebreak [0]"[ z ]"" end define ]]"

\item "[[ Define tex of let x = y in z as "

{\bf let} \ \linebreak [0]"[ x ]"

= "[ y ]"

\ {\bf in} \ \linebreak [0]"[ z ]"" end define ]]"

\item "[[ Define tex of ttst x end test as "

[ "[ x ]"

]^{\cdot}" end define ]]"

\item "[[ Define tex of ftst x end test as "

[ "[ x ]"

]^{-}" end define ]]"

\item "[[ Define tex of etst x ; y end test as "

[ "[ x ]"

= "[ y ]"

]^{=}" end define ]]"

\item "[[ Define tex of x reduce to y as ""[ x ]"

\stackrel {+}{\rightarrow }"[ y ]"" end define ]]"

\item "[[ Define tex of x == y as ""[ x ]"

\equiv "[ y ]"" end define ]]"

\item "[[ Define tex of x,y as ""[ x ]""[ y ]"" end define ]]"

\item "[[ Define tex name of x,y as ""[ x ]"

\mathrel{,}"[ y ]"" end define ]]"

\item "[[ Define tex of x[ y ]z as ""[ x ]""[ y ]""[ z ]"" end define ]]"

\item "[[ Define tex name of x[ y ]z as ""[ x ]"

{[}"[ y ]"

{]}"[ z ]"" end define ]]"

\item "[[ Define tex of x[[ y ]]z as ""[ x ]"$"[ y ]"$"[ z ]"" end define ]]"

\item "[[ Define tex name of x[[ y ]]z as ""[ x ]"

{\$}"[ y ]"

{\$}"[ z ]"" end define ]]"

\item "[[ Define tex of x[[[ y ]]]z as ""[ x ]"\["[ y ]"\]"[ z ]"" end define ]]"

\item "[[ Define tex name of x[[[ y ]]]z as ""[ x ]"

{\backslash[}"[ y ]"

{\backslash]}"[ z ]"" end define ]]"

\item "[[ Define tex of x linebreak y as ""[ x ]"

\linebreak[4] "[ y ]"" end define ]]"

\item "[[ Define tex name of x linebreak y as ""[ x ]"

\mathrel{linebreak} "[ y ]"" end define ]]"

\item "[[ Define tex of x & y as ""[ x ]"

& "[ y ]"" end define ]]"

\item "[[ Define tex name of x & y as ""[ x ]"

\& "[ y ]"" end define ]]"

\item "[[ Define tex of x \\ y as ""[ x ]"

\\{}"[ y ]"" end define ]]"

\item "[[ Define tex name of x \\ y as ""[ x ]"

\backslash\!\backslash "[ y ]"" end define ]]"

\end{statements}

\section{Pyk definitions}

\begin{flushleft}

"[[ Define pyk of proclaim asterisk as asterisk end proclaim as "proclaim "! as "! end proclaim" end define linebreak Define pyk of empty as "empty" end define linebreak Define pyk of preassociative asterisk greater than asterisk as "preassociative "! greater than "!" end define linebreak Define pyk of postassociative asterisk greater than asterisk as "postassociative "! greater than "!" end define linebreak Define pyk of priority asterisk equal asterisk as "priority "! equal "!" end define linebreak Define pyk of priority asterisk end priority as "priority "! end priority" end define linebreak Define pyk of asterisk as "asterisk" end define linebreak Define pyk of pyk as "pyk" end define linebreak Define pyk of Define asterisk of asterisk as asterisk end define as "Define "! of "! as "! end define" end define linebreak Define pyk of math asterisk end math as "math "! end math" end define linebreak Define pyk of display math asterisk end math as "display math "! end math" end define linebreak Define pyk of make math asterisk end math as "make math "! end math" end define linebreak Define pyk of a as "a" end define linebreak Define pyk of b as "b" end define linebreak Define pyk of c as "c" end define linebreak Define pyk of d as "d" end define linebreak Define pyk of e as "e" end define linebreak Define pyk of f as "f" end define linebreak Define pyk of g as "g" end define linebreak Define pyk of h as "h" end define linebreak Define pyk of i as "i" end define linebreak Define pyk of j as "j" end define linebreak Define pyk of k as "k" end define linebreak Define pyk of l as "l" end define linebreak Define pyk of m as "m" end define linebreak Define pyk of n as "n" end define linebreak Define pyk of o as "o" end define linebreak Define pyk of p as "p" end define linebreak Define pyk of q as "q" end define linebreak Define pyk of r as "r" end define linebreak Define pyk of s as "s" end define linebreak Define pyk of t as "t" end define linebreak Define pyk of u as "u" end define linebreak Define pyk of x as "x" end define linebreak Define pyk of y as "y" end define linebreak Define pyk of z as "z" end define linebreak Define pyk of v as "v" end define linebreak Define pyk of w as "w" end define linebreak Define pyk of A as "A" end define linebreak Define pyk of B as "B" end define linebreak Define pyk of C as "C" end define linebreak Define pyk of D as "D" end define linebreak Define pyk of E as "E" end define linebreak Define pyk of F as "F" end define linebreak Define pyk of G as "G" end define linebreak Define pyk of H as "H" end define linebreak Define pyk of I as "I" end define linebreak Define pyk of J as "J" end define linebreak Define pyk of K as "K" end define linebreak Define pyk of L as "L" end define linebreak Define pyk of M as "M" end define linebreak Define pyk of N as "N" end define linebreak Define pyk of O as "O" end define linebreak Define pyk of P as "P" end define linebreak Define pyk of Q as "Q" end define linebreak Define pyk of R as "R" end define linebreak Define pyk of S as "S" end define linebreak Define pyk of T as "T" end define linebreak Define pyk of U as "U" end define linebreak Define pyk of V as "V" end define linebreak Define pyk of W as "W" end define linebreak Define pyk of X as "X" end define linebreak Define pyk of Y as "Y" end define linebreak Define pyk of Z as "Z" end define linebreak Define pyk of true as "true" end define linebreak Define pyk of quote asterisk end quote as "quote "! end quote" end define linebreak Define pyk of optimized define asterisk of asterisk as asterisk end define as "optimized define "! of "! as "! end define" end define linebreak Define pyk of tex as "tex" end define linebreak Define pyk of tex name as "tex name" end define linebreak Define pyk of priority as "priority" end define linebreak Define pyk of value as "value" end define linebreak Define pyk of macro as "macro" end define linebreak Define pyk of render as "render" end define linebreak Define pyk of claim as "claim" end define linebreak Define pyk of message as "message" end define linebreak Define pyk of unpack as "unpack" end define linebreak Define pyk of execute as "execute" end define linebreak Define pyk of executables as "executables" end define linebreak Define pyk of exampleaspect0 as "exampleaspect0" end define linebreak Define pyk of exampleaspect1 as "exampleaspect1" end define linebreak Define pyk of exampleaspect2 as "exampleaspect2" end define linebreak Define pyk of name asterisk end name as "name "! end name" end define linebreak Define pyk of macro name asterisk end name as "macro name "! end name" end define linebreak Define pyk of hiding name asterisk end name as "hiding name "! end name" end define linebreak Define pyk of hide asterisk end hide as "hide "! end hide" end define linebreak Define pyk of array ( asterisk ) asterisk end array as "array ( "! ) "! end array" end define linebreak Define pyk of left as "left" end define linebreak Define pyk of center as "center" end define linebreak Define pyk of right as "right" end define linebreak Define pyk of %% as "%%" end define linebreak Define pyk of ( asterisk ) as "( "! )" end define linebreak Define pyk of < asterisk | asterisk := asterisk > as "< "! | "! := "! >" end define linebreak Define pyk of bottom as "bottom" end define linebreak Define pyk of false as "false" end define linebreak Define pyk of define asterisk of asterisk as asterisk end define as "define "! of "! as "! end define" end define linebreak Define pyk of ... as "..." end define linebreak Define pyk of --- as "---" end define linebreak Define pyk of Zero as "Zero" end define linebreak Define pyk of One as "One" end define linebreak Define pyk of Two as "Two" end define linebreak Define pyk of Three as "Three" end define linebreak Define pyk of Four as "Four" end define linebreak Define pyk of Five as "Five" end define linebreak Define pyk of Six as "Six" end define linebreak Define pyk of Seven as "Seven" end define linebreak Define pyk of Eight as "Eight" end define linebreak Define pyk of Nine as "Nine" end define linebreak Define pyk of Ten as "Ten" end define linebreak Define pyk of Base as "Base" end define linebreak Define pyk of Xor ( asterisk , asterisk , asterisk ) as "Xor ( "! , "! , "! )" end define linebreak Define pyk of Carry ( asterisk , asterisk , asterisk ) as "Carry ( "! , "! , "! )" end define linebreak Define pyk of Plus ( asterisk , asterisk , asterisk ) as "Plus ( "! , "! , "! )" end define linebreak Define pyk of Borrow ( asterisk , asterisk , asterisk ) as "Borrow ( "! , "! , "! )" end define linebreak Define pyk of Compare ( asterisk , asterisk , asterisk ) as "Compare ( "! , "! , "! )" end define linebreak Define pyk of Minus ( asterisk , asterisk , asterisk ) as "Minus ( "! , "! , "! )" end define linebreak Define pyk of BoolTag as "BoolTag" end define linebreak Define pyk of IntTag as "IntTag" end define linebreak Define pyk of PairTag as "PairTag" end define linebreak Define pyk of ExTag as "ExTag" end define linebreak Define pyk of MapTag as "MapTag" end define linebreak Define pyk of equal1 ( asterisk , asterisk ) as "equal1 ( "! , "! )" end define linebreak Define pyk of TheInt ( asterisk , asterisk ) as "TheInt ( "! , "! )" end define linebreak Define pyk of int ( asterisk ) as "int ( "! )" end define linebreak Define pyk of plus1 ( asterisk , asterisk ) as "plus1 ( "! , "! )" end define linebreak Define pyk of plus2 ( asterisk , asterisk , asterisk , asterisk ) as "plus2 ( "! , "! , "! , "! )" end define linebreak Define pyk of minus1 ( asterisk ) as "minus1 ( "! )" end define linebreak Define pyk of minus2 ( asterisk , asterisk ) as "minus2 ( "! , "! )" end define linebreak Define pyk of times1 ( asterisk , asterisk ) as "times1 ( "! , "! )" end define linebreak Define pyk of times2 ( asterisk , asterisk , asterisk , asterisk ) as "times2 ( "! , "! , "! , "! )" end define linebreak Define pyk of lt1 ( asterisk , asterisk ) as "lt1 ( "! , "! )" end define linebreak Define pyk of lt2 ( asterisk , asterisk , asterisk , asterisk ) as "lt2 ( "! , "! , "! , "! )" end define linebreak Define pyk of reverse ( asterisk ) as "reverse ( "! )" end define linebreak Define pyk of revappend ( asterisk , asterisk ) as "revappend ( "! , "! )" end define linebreak Define pyk of nth ( asterisk , asterisk ) as "nth ( "! , "! )" end define linebreak Define pyk of exception as "exception" end define linebreak Define pyk of map ( asterisk ) as "map ( "! )" end define linebreak Define pyk of Catch ( asterisk ) as "Catch ( "! )" end define linebreak Define pyk of catch ( asterisk ) as "catch ( "! )" end define linebreak Define pyk of object ( asterisk ) as "object ( "! )" end define linebreak Define pyk of Object ( asterisk , asterisk , asterisk ) as "Object ( "! , "! , "! )" end define linebreak Define pyk of destruct ( asterisk ) as "destruct ( "! )" end define linebreak Define pyk of 0 as "0" end define linebreak Define pyk of 1 as "1" end define linebreak Define pyk of 2 as "2" end define linebreak Define pyk of 3 as "3" end define linebreak Define pyk of 4 as "4" end define linebreak Define pyk of 5 as "5" end define linebreak Define pyk of 6 as "6" end define linebreak Define pyk of 7 as "7" end define linebreak Define pyk of 8 as "8" end define linebreak Define pyk of 9 as "9" end define linebreak Define pyk of numeral ( asterisk ) as "numeral ( "! )" end define linebreak Define pyk of num1 ( asterisk , asterisk , asterisk ) as "num1 ( "! , "! , "! )" end define linebreak Define pyk of num2 ( asterisk , asterisk , asterisk ) as "num2 ( "! , "! , "! )" end define linebreak Define pyk of evenp ( asterisk ) as "evenp ( "! )" end define linebreak Define pyk of oddp ( asterisk ) as "oddp ( "! )" end define linebreak Define pyk of half ( asterisk ) as "half ( "! )" end define linebreak Define pyk of small ( asterisk ) as "small ( "! )" end define linebreak Define pyk of double ( asterisk , asterisk ) as "double ( "! , "! )" end define linebreak Define pyk of lognot ( asterisk ) as "lognot ( "! )" end define linebreak Define pyk of logior ( asterisk , asterisk ) as "logior ( "! , "! )" end define linebreak Define pyk of logxor ( asterisk , asterisk ) as "logxor ( "! , "! )" end define linebreak Define pyk of logand ( asterisk , asterisk ) as "logand ( "! , "! )" end define linebreak Define pyk of logeqv ( asterisk , asterisk ) as "logeqv ( "! , "! )" end define linebreak Define pyk of lognand ( asterisk , asterisk ) as "lognand ( "! , "! )" end define linebreak Define pyk of lognor ( asterisk , asterisk ) as "lognor ( "! , "! )" end define linebreak Define pyk of logandc1 ( asterisk , asterisk ) as "logandc1 ( "! , "! )" end define linebreak Define pyk of logandc2 ( asterisk , asterisk ) as "logandc2 ( "! , "! )" end define linebreak Define pyk of logorc1 ( asterisk , asterisk ) as "logorc1 ( "! , "! )" end define linebreak Define pyk of logorc2 ( asterisk , asterisk ) as "logorc2 ( "! , "! )" end define linebreak Define pyk of logtest ( asterisk , asterisk ) as "logtest ( "! , "! )" end define linebreak Define pyk of ash ( asterisk , asterisk ) as "ash ( "! , "! )" end define linebreak Define pyk of ash+ ( asterisk , asterisk ) as "ash+ ( "! , "! )" end define linebreak Define pyk of ash- ( asterisk , asterisk ) as "ash- ( "! , "! )" end define linebreak Define pyk of logbitp ( asterisk , asterisk ) as "logbitp ( "! , "! )" end define linebreak Define pyk of logcount ( asterisk ) as "logcount ( "! )" end define linebreak Define pyk of logcount1 ( asterisk ) as "logcount1 ( "! )" end define linebreak Define pyk of integer-length ( asterisk ) as "integer-length ( "! )" end define linebreak Define pyk of vector-mask as "vector-mask" end define linebreak Define pyk of vector-empty ( asterisk ) as "vector-empty ( "! )" end define linebreak Define pyk of vector-head1 ( asterisk ) as "vector-head1 ( "! )" end define linebreak Define pyk of vector-tail1 ( asterisk ) as "vector-tail1 ( "! )" end define linebreak Define pyk of vector-cons ( asterisk , asterisk ) as "vector-cons ( "! , "! )" end define linebreak Define pyk of vector ( asterisk ) as "vector ( "! )" end define linebreak Define pyk of vector-suffix ( asterisk , asterisk ) as "vector-suffix ( "! , "! )" end define linebreak Define pyk of vector-prefix ( asterisk , asterisk ) as "vector-prefix ( "! , "! )" end define linebreak Define pyk of vector-subseq ( asterisk , asterisk , asterisk ) as "vector-subseq ( "! , "! , "! )" end define linebreak Define pyk of vector-length ( asterisk ) as "vector-length ( "! )" end define linebreak Define pyk of vector-index ( asterisk , asterisk ) as "vector-index ( "! , "! )" end define linebreak Define pyk of vector-head ( asterisk ) as "vector-head ( "! )" end define linebreak Define pyk of vector-tail ( asterisk ) as "vector-tail ( "! )" end define linebreak Define pyk of vector2byte* ( asterisk ) as "vector2byte* ( "! )" end define linebreak Define pyk of vector2byte*1 ( asterisk , asterisk ) as "vector2byte*1 ( "! , "! )" end define linebreak Define pyk of bt2byte* ( asterisk ) as "bt2byte* ( "! )" end define linebreak Define pyk of bt2byte*1 ( asterisk , asterisk ) as "bt2byte*1 ( "! , "! )" end define linebreak Define pyk of bt2vector ( asterisk ) as "bt2vector ( "! )" end define linebreak Define pyk of revbyte*2vector ( asterisk , asterisk ) as "revbyte*2vector ( "! , "! )" end define linebreak Define pyk of vector-revappend ( asterisk , asterisk ) as "vector-revappend ( "! , "! )" end define linebreak Define pyk of vt2byte* ( asterisk ) as "vt2byte* ( "! )" end define linebreak Define pyk of vt2byte*1 ( asterisk , asterisk ) as "vt2byte*1 ( "! , "! )" end define linebreak Define pyk of vt2vector ( asterisk ) as "vt2vector ( "! )" end define linebreak Define pyk of floor1 ( asterisk , asterisk ) as "floor1 ( "! , "! )" end define linebreak Define pyk of ceiling1 ( asterisk , asterisk ) as "ceiling1 ( "! , "! )" end define linebreak Define pyk of round1 ( asterisk , asterisk ) as "round1 ( "! , "! )" end define linebreak Define pyk of floor ( asterisk , asterisk ) as "floor ( "! , "! )" end define linebreak Define pyk of ceiling ( asterisk , asterisk ) as "ceiling ( "! , "! )" end define linebreak Define pyk of truncate ( asterisk , asterisk ) as "truncate ( "! , "! )" end define linebreak Define pyk of round ( asterisk , asterisk ) as "round ( "! , "! )" end define linebreak Define pyk of reverse quotient ( asterisk ) as "reverse quotient ( "! )" end define linebreak Define pyk of length ( asterisk ) as "length ( "! )" end define linebreak Define pyk of length1 ( asterisk , asterisk ) as "length1 ( "! , "! )" end define linebreak Define pyk of list-prefix ( asterisk , asterisk ) as "list-prefix ( "! , "! )" end define linebreak Define pyk of list-suffix ( asterisk , asterisk ) as "list-suffix ( "! , "! )" end define linebreak Define pyk of lookup ( asterisk , asterisk , asterisk ) as "lookup ( "! , "! , "! )" end define linebreak Define pyk of zip ( asterisk , asterisk ) as "zip ( "! , "! )" end define linebreak Define pyk of array1 ( asterisk , asterisk , asterisk ) as "array1 ( "! , "! , "! )" end define linebreak Define pyk of array2 ( asterisk , asterisk , asterisk , asterisk ) as "array2 ( "! , "! , "! , "! )" end define linebreak Define pyk of array3 ( asterisk , asterisk ) as "array3 ( "! , "! )" end define linebreak Define pyk of array4 ( asterisk , asterisk ) as "array4 ( "! , "! )" end define linebreak Define pyk of array5 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "array5 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of eval ( asterisk , asterisk , asterisk ) as "eval ( "! , "! , "! )" end define linebreak Define pyk of eval1 ( asterisk , asterisk , asterisk , asterisk ) as "eval1 ( "! , "! , "! , "! )" end define linebreak Define pyk of spy ( asterisk ) as "spy ( "! )" end define linebreak Define pyk of trace ( asterisk ) as "trace ( "! )" end define linebreak Define pyk of print ( asterisk ) as "print ( "! )" end define linebreak Define pyk of timer ( asterisk ) as "timer ( "! )" end define linebreak Define pyk of test1 as "test1" end define linebreak Define pyk of test2 ( asterisk ) as "test2 ( "! )" end define linebreak Define pyk of test3 ( asterisk , asterisk ) as "test3 ( "! , "! )" end define linebreak Define pyk of test3* ( asterisk , asterisk ) as "test3* ( "! , "! )" end define linebreak Define pyk of ttst1 ( asterisk ) as "ttst1 ( "! )" end define linebreak Define pyk of ftst1 ( asterisk ) as "ftst1 ( "! )" end define linebreak Define pyk of etst1 ( asterisk ) as "etst1 ( "! )" end define linebreak Define pyk of ttst asterisk end test as "ttst "! end test" end define linebreak Define pyk of ftst asterisk end test as "ftst "! end test" end define linebreak Define pyk of etst asterisk ; asterisk end test as "etst "! ; "! end test" end define linebreak Define pyk of texname asterisk end texname as "texname "! end texname" end define linebreak Define pyk of testfunc1 ( asterisk ) as "testfunc1 ( "! )" end define linebreak Define pyk of testfunc2 ( asterisk , asterisk ) as "testfunc2 ( "! , "! )" end define linebreak Define pyk of testfunc3 as "testfunc3" end define linebreak Define pyk of testfunc4 as "testfunc4" end define linebreak Define pyk of testfunc5 ( asterisk ) as "testfunc5 ( "! )" end define linebreak Define pyk of testfunc6 ( asterisk ) as "testfunc6 ( "! )" end define linebreak Define pyk of testfunc7 ( asterisk ) as "testfunc7 ( "! )" end define linebreak Define pyk of testfunc8 ( asterisk , asterisk ) as "testfunc8 ( "! , "! )" end define linebreak Define pyk of macro1 as "macro1" end define linebreak Define pyk of macro2 ( asterisk ) as "macro2 ( "! )" end define linebreak Define pyk of macro3 ( asterisk , asterisk , asterisk ) as "macro3 ( "! , "! , "! )" end define linebreak Define pyk of macro3* ( asterisk , asterisk , asterisk ) as "macro3* ( "! , "! , "! )" end define linebreak Define pyk of macro4 ( asterisk ) as "macro4 ( "! )" end define linebreak Define pyk of macrostate0 as "macrostate0" end define linebreak Define pyk of stateexpand ( asterisk , asterisk , asterisk ) as "stateexpand ( "! , "! , "! )" end define linebreak Define pyk of stateexpand* ( asterisk , asterisk , asterisk ) as "stateexpand* ( "! , "! , "! )" end define linebreak Define pyk of substitute ( asterisk , asterisk , asterisk ) as "substitute ( "! , "! , "! )" end define linebreak Define pyk of substitute* ( asterisk , asterisk , asterisk ) as "substitute* ( "! , "! , "! )" end define linebreak Define pyk of expand ( asterisk , asterisk ) as "expand ( "! , "! )" end define linebreak Define pyk of protect asterisk end protect as "protect "! end protect" end define linebreak Define pyk of Macro define asterisk as asterisk end define as "Macro define "! as "! end define" end define linebreak Define pyk of Macrodefine ( asterisk ) as "Macrodefine ( "! )" end define linebreak Define pyk of macro define asterisk as asterisk end define as "macro define "! as "! end define" end define linebreak Define pyk of macrodefine ( asterisk ) as "macrodefine ( "! )" end define linebreak Define pyk of self as "self" end define linebreak Define pyk of makeself ( asterisk ) as "makeself ( "! )" end define linebreak Define pyk of root protect asterisk end protect as "root protect "! end protect" end define linebreak Define pyk of rootprotect ( asterisk ) as "rootprotect ( "! )" end define linebreak Define pyk of render define asterisk as asterisk end define as "render define "! as "! end define" end define linebreak Define pyk of tex define asterisk as asterisk end define as "tex define "! as "! end define" end define linebreak Define pyk of tex name define asterisk as asterisk end define as "tex name define "! as "! end define" end define linebreak Define pyk of value define asterisk as asterisk end define as "value define "! as "! end define" end define linebreak Define pyk of message define asterisk as asterisk end define as "message define "! as "! end define" end define linebreak Define pyk of priority table asterisk as "priority table "!" end define linebreak Define pyk of verifier asterisk end verifier as "verifier "! end verifier" end define linebreak Define pyk of unpacker asterisk end unpacker as "unpacker "! end unpacker" end define linebreak Define pyk of renderer asterisk end renderer as "renderer "! end renderer" end define linebreak Define pyk of expander asterisk end expander as "expander "! end expander" end define linebreak Define pyk of executer asterisk end executer as "executer "! end executer" end define linebreak Define pyk of executables asterisk end executables as "executables "! end executables" end define linebreak Define pyk of ragged right as "ragged right" end define linebreak Define pyk of make macro expanded version ragged right as "make macro expanded version ragged right" end define linebreak Define pyk of <<>> as "<<>>" end define linebreak Define pyk of << asterisk >> as "<< "! >>" end define linebreak Define pyk of tuple1 ( asterisk ) as "tuple1 ( "! )" end define linebreak Define pyk of tuple2 ( asterisk , asterisk ) as "tuple2 ( "! , "! )" end define linebreak Define pyk of eager define asterisk as asterisk end define as "eager define "! as "! end define" end define linebreak Define pyk of eager1 ( asterisk ) as "eager1 ( "! )" end define linebreak Define pyk of eager2 ( asterisk , asterisk , asterisk ) as "eager2 ( "! , "! , "! )" end define linebreak Define pyk of eager message define asterisk as asterisk end define as "eager message define "! as "! end define" end define linebreak Define pyk of macrolet1 ( asterisk ) as "macrolet1 ( "! )" end define linebreak Define pyk of destructure as "destructure" end define linebreak Define pyk of destructure define asterisk as asterisk end define as "destructure define "! as "! end define" end define linebreak Define pyk of let1 ( asterisk ) as "let1 ( "! )" end define linebreak Define pyk of let2 ( asterisk , asterisk , asterisk , asterisk ) as "let2 ( "! , "! , "! , "! )" end define linebreak Define pyk of let3 ( asterisk , asterisk , asterisk , asterisk ) as "let3 ( "! , "! , "! , "! )" end define linebreak Define pyk of make-var ( asterisk ) as "make-var ( "! )" end define linebreak Define pyk of make-let ( asterisk , asterisk , asterisk ) as "make-let ( "! , "! , "! )" end define linebreak Define pyk of make-prime ( asterisk ) as "make-prime ( "! )" end define linebreak Define pyk of make-head ( asterisk ) as "make-head ( "! )" end define linebreak Define pyk of make-tail ( asterisk ) as "make-tail ( "! )" end define linebreak Define pyk of back asterisk quote asterisk end quote as "back "! quote "! end quote" end define linebreak Define pyk of make-root ( asterisk , asterisk ) as "make-root ( "! , "! )" end define linebreak Define pyk of make-pair ( asterisk , asterisk , asterisk ) as "make-pair ( "! , "! , "! )" end define linebreak Define pyk of make-true ( asterisk ) as "make-true ( "! )" end define linebreak Define pyk of make-quote ( asterisk , asterisk ) as "make-quote ( "! , "! )" end define linebreak Define pyk of make-make-root ( asterisk , asterisk , asterisk ) as "make-make-root ( "! , "! , "! )" end define linebreak Define pyk of backquote0 ( asterisk ) as "backquote0 ( "! )" end define linebreak Define pyk of backquote1 ( asterisk , asterisk , asterisk ) as "backquote1 ( "! , "! , "! )" end define linebreak Define pyk of backquote2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "backquote2 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of backquote2* ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "backquote2* ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of text asterisk : asterisk end text as "text "! : "! end text" end define linebreak Define pyk of tex ( asterisk ) as "tex ( "! )" end define linebreak Define pyk of latex ( asterisk ) as "latex ( "! )" end define linebreak Define pyk of bibtex ( asterisk ) as "bibtex ( "! )" end define linebreak Define pyk of makeindex ( asterisk ) as "makeindex ( "! )" end define linebreak Define pyk of dvipdfm ( asterisk ) as "dvipdfm ( "! )" end define linebreak Define pyk of page ( asterisk , asterisk ) title asterisk bib asterisk main text asterisk appendix asterisk end page as "page ( "! , "! ) title "! bib "! main text "! appendix "! end page" end define linebreak Define pyk of page1 ( asterisk ) as "page1 ( "! )" end define linebreak Define pyk of tex-file ( asterisk , asterisk , asterisk ) as "tex-file ( "! , "! , "! )" end define linebreak Define pyk of tex-command ( asterisk , asterisk ) as "tex-command ( "! , "! )" end define linebreak Define pyk of quit ( asterisk ) as "quit ( "! )" end define linebreak Define pyk of boot ( asterisk , asterisk , asterisk ) as "boot ( "! , "! , "! )" end define linebreak Define pyk of write ( asterisk ) as "write ( "! )" end define linebreak Define pyk of read ( asterisk ) as "read ( "! )" end define linebreak Define pyk of exec ( asterisk , asterisk ) as "exec ( "! , "! )" end define linebreak Define pyk of int ( asterisk , asterisk ) as "int ( "! , "! )" end define linebreak Define pyk of extend ( asterisk ) as "extend ( "! )" end define linebreak Define pyk of extended ( asterisk ) as "extended ( "! )" end define linebreak Define pyk of Hello World as "Hello World" end define linebreak Define pyk of Echo as "Echo" end define linebreak Define pyk of Echo1 ( asterisk ) as "Echo1 ( "! )" end define linebreak Define pyk of Eecho as "Eecho" end define linebreak Define pyk of Eecho1 ( asterisk ) as "Eecho1 ( "! )" end define linebreak Define pyk of +asterisk as "+"!" end define linebreak Define pyk of -asterisk as "-"!" end define linebreak Define pyk of 0asterisk as "0"!" end define linebreak Define pyk of 1asterisk as "1"!" end define linebreak Define pyk of 2asterisk as "2"!" end define linebreak Define pyk of 3asterisk as "3"!" end define linebreak Define pyk of 4asterisk as "4"!" end define linebreak Define pyk of 5asterisk as "5"!" end define linebreak Define pyk of 6asterisk as "6"!" end define linebreak Define pyk of 7asterisk as "7"!" end define linebreak Define pyk of 8asterisk as "8"!" end define linebreak Define pyk of 9asterisk as "9"!" end define linebreak Define pyk of asterisk factorial as ""! factorial" end define linebreak Define pyk of asterisk _ { asterisk } as ""! _ { "! }" end define linebreak Define pyk of asterisk prime as ""! prime" end define linebreak Define pyk of asterisk %0 as ""! %0" end define linebreak Define pyk of asterisk %1 as ""! %1" end define linebreak Define pyk of asterisk %2 as ""! %2" end define linebreak Define pyk of asterisk %3 as ""! %3" end define linebreak Define pyk of asterisk %4 as ""! %4" end define linebreak Define pyk of asterisk %5 as ""! %5" end define linebreak Define pyk of asterisk %6 as ""! %6" end define linebreak Define pyk of asterisk %7 as ""! %7" end define linebreak Define pyk of asterisk %8 as ""! %8" end define linebreak Define pyk of asterisk %9 as ""! %9" end define linebreak Define pyk of asterisk head as ""! head" end define linebreak Define pyk of asterisk tail as ""! tail" end define linebreak Define pyk of asterisk raise as ""! raise" end define linebreak Define pyk of asterisk catch as ""! catch" end define linebreak Define pyk of asterisk catching maptag as ""! catching maptag" end define linebreak Define pyk of asterisk maptag as ""! maptag" end define linebreak Define pyk of asterisk untag as ""! untag" end define linebreak Define pyk of asterisk boolp as ""! boolp" end define linebreak Define pyk of asterisk truep as ""! truep" end define linebreak Define pyk of asterisk falsep as ""! falsep" end define linebreak Define pyk of asterisk intp as ""! intp" end define linebreak Define pyk of asterisk pairp as ""! pairp" end define linebreak Define pyk of asterisk atom as ""! atom" end define linebreak Define pyk of asterisk mapp as ""! mapp" end define linebreak Define pyk of asterisk objectp as ""! objectp" end define linebreak Define pyk of asterisk root as ""! root" end define linebreak Define pyk of asterisk Head as ""! Head" end define linebreak Define pyk of asterisk Tail as ""! Tail" end define linebreak Define pyk of asterisk TheBool as ""! TheBool" end define linebreak Define pyk of asterisk TheNat as ""! TheNat" end define linebreak Define pyk of asterisk norm as ""! norm" end define linebreak Define pyk of asterisk Tag as ""! Tag" end define linebreak Define pyk of asterisk BoolP as ""! BoolP" end define linebreak Define pyk of asterisk IntP as ""! IntP" end define linebreak Define pyk of asterisk PairP as ""! PairP" end define linebreak Define pyk of asterisk ExP as ""! ExP" end define linebreak Define pyk of asterisk MapP as ""! MapP" end define linebreak Define pyk of asterisk ObjectP as ""! ObjectP" end define linebreak Define pyk of asterisk Sign as ""! Sign" end define linebreak Define pyk of asterisk Mag as ""! Mag" end define linebreak Define pyk of asterisk zeroth as ""! zeroth" end define linebreak Define pyk of asterisk first as ""! first" end define linebreak Define pyk of asterisk second as ""! second" end define linebreak Define pyk of asterisk third as ""! third" end define linebreak Define pyk of asterisk fourth as ""! fourth" end define linebreak Define pyk of asterisk fifth as ""! fifth" end define linebreak Define pyk of asterisk sixth as ""! sixth" end define linebreak Define pyk of asterisk seventh as ""! seventh" end define linebreak Define pyk of asterisk eighth as ""! eighth" end define linebreak Define pyk of asterisk ninth as ""! ninth" end define linebreak Define pyk of asterisk ref as ""! ref" end define linebreak Define pyk of asterisk idx as ""! idx" end define linebreak Define pyk of asterisk debug as ""! debug" end define linebreak Define pyk of asterisk [[ asterisk ]] as ""! [[ "! ]]" end define linebreak Define pyk of asterisk [[ asterisk -> asterisk ]] as ""! [[ "! -> "! ]]" end define linebreak Define pyk of asterisk [[ asterisk => asterisk ]] as ""! [[ "! => "! ]]" end define linebreak Define pyk of asterisk unquote as ""! unquote" end define linebreak Define pyk of asterisk ' asterisk as ""! ' "!" end define linebreak Define pyk of asterisk apply asterisk as ""! apply "!" end define linebreak Define pyk of - asterisk as "- "!" end define linebreak Define pyk of + asterisk as "+ "!" end define linebreak Define pyk of asterisk Times asterisk as ""! Times "!" end define linebreak Define pyk of asterisk * asterisk as ""! * "!" end define linebreak Define pyk of asterisk Plus asterisk as ""! Plus "!" end define linebreak Define pyk of asterisk Minus asterisk as ""! Minus "!" end define linebreak Define pyk of asterisk + asterisk as ""! + "!" end define linebreak Define pyk of asterisk - asterisk as ""! - "!" end define linebreak Define pyk of PlusTag asterisk as "PlusTag "!" end define linebreak Define pyk of MinusTag asterisk as "MinusTag "!" end define linebreak Define pyk of asterisk div asterisk as ""! div "!" end define linebreak Define pyk of asterisk mod asterisk as ""! mod "!" end define linebreak Define pyk of asterisk LazyPair asterisk as ""! LazyPair "!" end define linebreak Define pyk of asterisk Pair asterisk as ""! Pair "!" end define linebreak Define pyk of asterisk NatPair asterisk as ""! NatPair "!" end define linebreak Define pyk of asterisk :: asterisk as ""! :: "!" end define linebreak Define pyk of asterisk ,, asterisk as ""! ,, "!" end define linebreak Define pyk of asterisk = asterisk as ""! = "!" end define linebreak Define pyk of asterisk != asterisk as ""! != "!" end define linebreak Define pyk of asterisk Equal asterisk as ""! Equal "!" end define linebreak Define pyk of asterisk LT asterisk as ""! LT "!" end define linebreak Define pyk of asterisk < asterisk as ""! < "!" end define linebreak Define pyk of asterisk <= asterisk as ""! <= "!" end define linebreak Define pyk of asterisk > asterisk as ""! > "!" end define linebreak Define pyk of asterisk >= asterisk as ""! >= "!" end define linebreak Define pyk of asterisk r= asterisk as ""! r= "!" end define linebreak Define pyk of asterisk t= asterisk as ""! t= "!" end define linebreak Define pyk of asterisk t=* asterisk as ""! t=* "!" end define linebreak Define pyk of Not asterisk as "Not "!" end define linebreak Define pyk of .not. asterisk as ".not. "!" end define linebreak Define pyk of notnot asterisk as "notnot "!" end define linebreak Define pyk of asterisk And asterisk as ""! And "!" end define linebreak Define pyk of asterisk .and. asterisk as ""! .and. "!" end define linebreak Define pyk of asterisk .then. asterisk as ""! .then. "!" end define linebreak Define pyk of asterisk &c asterisk as ""! &c "!" end define linebreak Define pyk of asterisk Or asterisk as ""! Or "!" end define linebreak Define pyk of asterisk .or. asterisk as ""! .or. "!" end define linebreak Define pyk of asterisk Iff asterisk as ""! Iff "!" end define linebreak Define pyk of asterisk Select asterisk else asterisk end select as ""! Select "! else "! end select" end define linebreak Define pyk of asterisk IN asterisk as ""! IN "!" end define linebreak Define pyk of \ asterisk . asterisk as "\ "! . "!" end define linebreak Define pyk of If asterisk then asterisk else asterisk as "If "! then "! else "!" end define linebreak Define pyk of if asterisk then asterisk else asterisk as "if "! then "! else "!" end define linebreak Define pyk of newline asterisk as "newline "!" end define linebreak Define pyk of LET asterisk BE asterisk as "LET "! BE "!" end define linebreak Define pyk of let asterisk := asterisk in asterisk as "let "! := "! in "!" end define linebreak Define pyk of let asterisk = asterisk in asterisk as "let "! = "! in "!" end define linebreak Define pyk of norm asterisk as "norm "!" end define linebreak Define pyk of asterisk Guard asterisk as ""! Guard "!" end define linebreak Define pyk of asterisk is val : asterisk as ""! is val : "!" end define linebreak Define pyk of asterisk is bool : asterisk as ""! is bool : "!" end define linebreak Define pyk of asterisk is int : asterisk as ""! is int : "!" end define linebreak Define pyk of asterisk is pair : asterisk as ""! is pair : "!" end define linebreak Define pyk of asterisk is map : asterisk as ""! is map : "!" end define linebreak Define pyk of asterisk is object : asterisk as ""! is object : "!" end define linebreak Define pyk of asterisk reduce to asterisk as ""! reduce to "!" end define linebreak Define pyk of asterisk == asterisk as ""! == "!" end define linebreak Define pyk of asterisk,asterisk as ""!,"!" end define linebreak Define pyk of asterisk[ asterisk ]asterisk as ""![ "! ]"!" end define linebreak Define pyk of asterisk[[ asterisk ]]asterisk as ""![[ "! ]]"!" end define linebreak Define pyk of asterisk[[[ asterisk ]]]asterisk as ""![[[ "! ]]]"!" end define linebreak Define pyk of asterisk linebreak asterisk as ""! linebreak "!" end define linebreak Define pyk of asterisk & asterisk as ""! & "!" end define linebreak Define pyk of asterisk \\ asterisk as ""! \\ "!" end define linebreak Define pyk of base as "base" end define linebreak empty ]]"

\end{flushleft}

\section{Priority table}

This would normaly be done using "[[ name define priority of base as ... end define end name ]]" but we do it this way to avoid problems with "[[ let asterisk := asterisk in asterisk ]]".

\begin {flushleft}

"[[ define priority of base as preassociative priority base equal priority proclaim asterisk as asterisk end proclaim equal priority empty equal priority preassociative asterisk greater than asterisk equal priority postassociative asterisk greater than asterisk equal priority priority asterisk equal asterisk equal priority priority asterisk end priority equal priority asterisk equal priority pyk equal priority Define asterisk of asterisk as asterisk end define equal priority math asterisk end math equal priority display math asterisk end math equal priority make math asterisk end math equal priority a equal priority b equal priority c equal priority d equal priority e equal priority f equal priority g equal priority h equal priority i equal priority j equal priority k equal priority l equal priority m equal priority n equal priority o equal priority p equal priority q equal priority r equal priority s equal priority t equal priority u equal priority x equal priority y equal priority z equal priority v equal priority w equal priority A equal priority B equal priority C equal priority D equal priority E equal priority F equal priority G equal priority H equal priority I equal priority J equal priority K equal priority L equal priority M equal priority N equal priority O equal priority P equal priority Q equal priority R equal priority S equal priority T equal priority U equal priority V equal priority W equal priority X equal priority Y equal priority Z equal priority true equal priority quote asterisk end quote equal priority optimized define asterisk of asterisk as asterisk end define equal priority tex equal priority tex name equal priority priority equal priority value equal priority macro equal priority render equal priority claim equal priority message equal priority unpack equal priority execute equal priority executables equal priority exampleaspect0 equal priority exampleaspect1 equal priority exampleaspect2 equal priority name asterisk end name equal priority macro name asterisk end name equal priority hiding name asterisk end name equal priority hide asterisk end hide equal priority array ( asterisk ) asterisk end array equal priority left equal priority center equal priority right equal priority %% equal priority ( asterisk ) equal priority < asterisk | asterisk := asterisk > equal priority bottom equal priority false equal priority define asterisk of asterisk as asterisk end define equal priority ... equal priority --- equal priority Zero equal priority One equal priority Two equal priority Three equal priority Four equal priority Five equal priority Six equal priority Seven equal priority Eight equal priority Nine equal priority Ten equal priority Base equal priority Xor ( asterisk , asterisk , asterisk ) equal priority Carry ( asterisk , asterisk , asterisk ) equal priority Plus ( asterisk , asterisk , asterisk ) equal priority Borrow ( asterisk , asterisk , asterisk ) equal priority Compare ( asterisk , asterisk , asterisk ) equal priority Minus ( asterisk , asterisk , asterisk ) equal priority BoolTag equal priority IntTag equal priority PairTag equal priority ExTag equal priority MapTag equal priority equal1 ( asterisk , asterisk ) equal priority TheInt ( asterisk , asterisk ) equal priority int ( asterisk ) equal priority plus1 ( asterisk , asterisk ) equal priority plus2 ( asterisk , asterisk , asterisk , asterisk ) equal priority minus1 ( asterisk ) equal priority minus2 ( asterisk , asterisk ) equal priority times1 ( asterisk , asterisk ) equal priority times2 ( asterisk , asterisk , asterisk , asterisk ) equal priority lt1 ( asterisk , asterisk ) equal priority lt2 ( asterisk , asterisk , asterisk , asterisk ) equal priority reverse ( asterisk ) equal priority revappend ( asterisk , asterisk ) equal priority nth ( asterisk , asterisk ) equal priority exception equal priority map ( asterisk ) equal priority Catch ( asterisk ) equal priority catch ( asterisk ) equal priority object ( asterisk ) equal priority Object ( asterisk , asterisk , asterisk ) equal priority destruct ( asterisk ) equal priority 0 equal priority 1 equal priority 2 equal priority 3 equal priority 4 equal priority 5 equal priority 6 equal priority 7 equal priority 8 equal priority 9 equal priority numeral ( asterisk ) equal priority num1 ( asterisk , asterisk , asterisk ) equal priority num2 ( asterisk , asterisk , asterisk ) equal priority evenp ( asterisk ) equal priority oddp ( asterisk ) equal priority half ( asterisk ) equal priority small ( asterisk ) equal priority double ( asterisk , asterisk ) equal priority lognot ( asterisk ) equal priority logior ( asterisk , asterisk ) equal priority logxor ( asterisk , asterisk ) equal priority logand ( asterisk , asterisk ) equal priority logeqv ( asterisk , asterisk ) equal priority lognand ( asterisk , asterisk ) equal priority lognor ( asterisk , asterisk ) equal priority logandc1 ( asterisk , asterisk ) equal priority logandc2 ( asterisk , asterisk ) equal priority logorc1 ( asterisk , asterisk ) equal priority logorc2 ( asterisk , asterisk ) equal priority logtest ( asterisk , asterisk ) equal priority ash ( asterisk , asterisk ) equal priority ash+ ( asterisk , asterisk ) equal priority ash- ( asterisk , asterisk ) equal priority logbitp ( asterisk , asterisk ) equal priority logcount ( asterisk ) equal priority logcount1 ( asterisk ) equal priority integer-length ( asterisk ) equal priority vector-mask equal priority vector-empty ( asterisk ) equal priority vector-head1 ( asterisk ) equal priority vector-tail1 ( asterisk ) equal priority vector-cons ( asterisk , asterisk ) equal priority vector ( asterisk ) equal priority vector-suffix ( asterisk , asterisk ) equal priority vector-prefix ( asterisk , asterisk ) equal priority vector-subseq ( asterisk , asterisk , asterisk ) equal priority vector-length ( asterisk ) equal priority vector-index ( asterisk , asterisk ) equal priority vector-head ( asterisk ) equal priority vector-tail ( asterisk ) equal priority vector2byte* ( asterisk ) equal priority vector2byte*1 ( asterisk , asterisk ) equal priority bt2byte* ( asterisk ) equal priority bt2byte*1 ( asterisk , asterisk ) equal priority bt2vector ( asterisk ) equal priority revbyte*2vector ( asterisk , asterisk ) equal priority vector-revappend ( asterisk , asterisk ) equal priority vt2byte* ( asterisk ) equal priority vt2byte*1 ( asterisk , asterisk ) equal priority vt2vector ( asterisk ) equal priority floor1 ( asterisk , asterisk ) equal priority ceiling1 ( asterisk , asterisk ) equal priority round1 ( asterisk , asterisk ) equal priority floor ( asterisk , asterisk ) equal priority ceiling ( asterisk , asterisk ) equal priority truncate ( asterisk , asterisk ) equal priority round ( asterisk , asterisk ) equal priority reverse quotient ( asterisk ) equal priority length ( asterisk ) equal priority length1 ( asterisk , asterisk ) equal priority list-prefix ( asterisk , asterisk ) equal priority list-suffix ( asterisk , asterisk ) equal priority lookup ( asterisk , asterisk , asterisk ) equal priority zip ( asterisk , asterisk ) equal priority array1 ( asterisk , asterisk , asterisk ) equal priority array2 ( asterisk , asterisk , asterisk , asterisk ) equal priority array3 ( asterisk , asterisk ) equal priority array4 ( asterisk , asterisk ) equal priority array5 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority eval ( asterisk , asterisk , asterisk ) equal priority eval1 ( asterisk , asterisk , asterisk , asterisk ) equal priority spy ( asterisk ) equal priority trace ( asterisk ) equal priority print ( asterisk ) equal priority timer ( asterisk ) equal priority test1 equal priority test2 ( asterisk ) equal priority test3 ( asterisk , asterisk ) equal priority test3* ( asterisk , asterisk ) equal priority ttst1 ( asterisk ) equal priority ftst1 ( asterisk ) equal priority etst1 ( asterisk ) equal priority ttst asterisk end test equal priority ftst asterisk end test equal priority etst asterisk ; asterisk end test equal priority texname asterisk end texname equal priority testfunc1 ( asterisk ) equal priority testfunc2 ( asterisk , asterisk ) equal priority testfunc3 equal priority testfunc4 equal priority testfunc5 ( asterisk ) equal priority testfunc6 ( asterisk ) equal priority testfunc7 ( asterisk ) equal priority testfunc8 ( asterisk , asterisk ) equal priority macro1 equal priority macro2 ( asterisk ) equal priority macro3 ( asterisk , asterisk , asterisk ) equal priority macro3* ( asterisk , asterisk , asterisk ) equal priority macro4 ( asterisk ) equal priority macrostate0 equal priority stateexpand ( asterisk , asterisk , asterisk ) equal priority stateexpand* ( asterisk , asterisk , asterisk ) equal priority substitute ( asterisk , asterisk , asterisk ) equal priority substitute* ( asterisk , asterisk , asterisk ) equal priority expand ( asterisk , asterisk ) equal priority protect asterisk end protect equal priority Macro define asterisk as asterisk end define equal priority Macrodefine ( asterisk ) equal priority macro define asterisk as asterisk end define equal priority macrodefine ( asterisk ) equal priority self equal priority makeself ( asterisk ) equal priority root protect asterisk end protect equal priority rootprotect ( asterisk ) equal priority render define asterisk as asterisk end define equal priority tex define asterisk as asterisk end define equal priority tex name define asterisk as asterisk end define equal priority value define asterisk as asterisk end define equal priority message define asterisk as asterisk end define equal priority priority table asterisk equal priority verifier asterisk end verifier equal priority unpacker asterisk end unpacker equal priority renderer asterisk end renderer equal priority expander asterisk end expander equal priority executer asterisk end executer equal priority executables asterisk end executables equal priority ragged right equal priority make macro expanded version ragged right equal priority <<>> equal priority << asterisk >> equal priority tuple1 ( asterisk ) equal priority tuple2 ( asterisk , asterisk ) equal priority eager define asterisk as asterisk end define equal priority eager1 ( asterisk ) equal priority eager2 ( asterisk , asterisk , asterisk ) equal priority eager message define asterisk as asterisk end define equal priority macrolet1 ( asterisk ) equal priority destructure equal priority destructure define asterisk as asterisk end define equal priority let1 ( asterisk ) equal priority let2 ( asterisk , asterisk , asterisk , asterisk ) equal priority let3 ( asterisk , asterisk , asterisk , asterisk ) equal priority make-var ( asterisk ) equal priority make-let ( asterisk , asterisk , asterisk ) equal priority make-prime ( asterisk ) equal priority make-head ( asterisk ) equal priority make-tail ( asterisk ) equal priority back asterisk quote asterisk end quote equal priority make-root ( asterisk , asterisk ) equal priority make-pair ( asterisk , asterisk , asterisk ) equal priority make-true ( asterisk ) equal priority make-quote ( asterisk , asterisk ) equal priority make-make-root ( asterisk , asterisk , asterisk ) equal priority backquote0 ( asterisk ) equal priority backquote1 ( asterisk , asterisk , asterisk ) equal priority backquote2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority backquote2* ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority text asterisk : asterisk end text equal priority tex ( asterisk ) equal priority latex ( asterisk ) equal priority bibtex ( asterisk ) equal priority makeindex ( asterisk ) equal priority dvipdfm ( asterisk ) equal priority page ( asterisk , asterisk ) title asterisk bib asterisk main text asterisk appendix asterisk end page equal priority page1 ( asterisk ) equal priority tex-file ( asterisk , asterisk , asterisk ) equal priority tex-command ( asterisk , asterisk ) equal priority quit ( asterisk ) equal priority boot ( asterisk , asterisk , asterisk ) equal priority write ( asterisk ) equal priority read ( asterisk ) equal priority exec ( asterisk , asterisk ) equal priority int ( asterisk , asterisk ) equal priority extend ( asterisk ) equal priority extended ( asterisk ) equal priority Hello World equal priority Echo equal priority Echo1 ( asterisk ) equal priority Eecho equal priority Eecho1 ( asterisk ) end priority greater than preassociative priority +asterisk equal priority -asterisk equal priority 0asterisk equal priority 1asterisk equal priority 2asterisk equal priority 3asterisk equal priority 4asterisk equal priority 5asterisk equal priority 6asterisk equal priority 7asterisk equal priority 8asterisk equal priority 9asterisk end priority greater than preassociative priority asterisk factorial equal priority asterisk _ { asterisk } equal priority asterisk prime equal priority asterisk %0 equal priority asterisk %1 equal priority asterisk %2 equal priority asterisk %3 equal priority asterisk %4 equal priority asterisk %5 equal priority asterisk %6 equal priority asterisk %7 equal priority asterisk %8 equal priority asterisk %9 equal priority asterisk head equal priority asterisk tail equal priority asterisk raise equal priority asterisk catch equal priority asterisk catching maptag equal priority asterisk maptag equal priority asterisk untag equal priority asterisk boolp equal priority asterisk truep equal priority asterisk falsep equal priority asterisk intp equal priority asterisk pairp equal priority asterisk atom equal priority asterisk mapp equal priority asterisk objectp equal priority asterisk root equal priority asterisk Head equal priority asterisk Tail equal priority asterisk TheBool equal priority asterisk TheNat equal priority asterisk norm equal priority asterisk Tag equal priority asterisk BoolP equal priority asterisk IntP equal priority asterisk PairP equal priority asterisk ExP equal priority asterisk MapP equal priority asterisk ObjectP equal priority asterisk Sign equal priority asterisk Mag equal priority asterisk zeroth equal priority asterisk first equal priority asterisk second equal priority asterisk third equal priority asterisk fourth equal priority asterisk fifth equal priority asterisk sixth equal priority asterisk seventh equal priority asterisk eighth equal priority asterisk ninth equal priority asterisk ref equal priority asterisk idx equal priority asterisk debug equal priority asterisk [[ asterisk ]] equal priority asterisk [[ asterisk -> asterisk ]] equal priority asterisk [[ asterisk => asterisk ]] equal priority asterisk unquote end priority greater than preassociative priority asterisk ' asterisk equal priority asterisk apply asterisk end priority greater than preassociative priority - asterisk equal priority + asterisk end priority greater than preassociative priority asterisk Times asterisk equal priority asterisk * asterisk end priority greater than preassociative priority asterisk Plus asterisk equal priority asterisk Minus asterisk equal priority asterisk + asterisk equal priority asterisk - asterisk end priority greater than preassociative priority PlusTag asterisk equal priority MinusTag asterisk end priority greater than preassociative priority asterisk div asterisk equal priority asterisk mod asterisk end priority greater than postassociative priority asterisk LazyPair asterisk equal priority asterisk Pair asterisk equal priority asterisk NatPair asterisk equal priority asterisk :: asterisk end priority greater than postassociative priority asterisk ,, asterisk end priority greater than preassociative priority asterisk = asterisk equal priority asterisk != asterisk equal priority asterisk Equal asterisk equal priority asterisk LT asterisk equal priority asterisk < asterisk equal priority asterisk <= asterisk equal priority asterisk > asterisk equal priority asterisk >= asterisk equal priority asterisk r= asterisk equal priority asterisk t= asterisk equal priority asterisk t=* asterisk end priority greater than preassociative priority Not asterisk equal priority .not. asterisk equal priority notnot asterisk end priority greater than preassociative priority asterisk And asterisk equal priority asterisk .and. asterisk equal priority asterisk .then. asterisk equal priority asterisk &c asterisk end priority greater than preassociative priority asterisk Or asterisk equal priority asterisk .or. asterisk end priority greater than postassociative priority asterisk Iff asterisk end priority greater than preassociative priority asterisk Select asterisk else asterisk end select equal priority asterisk IN asterisk end priority greater than preassociative priority \ asterisk . asterisk equal priority If asterisk then asterisk else asterisk equal priority if asterisk then asterisk else asterisk equal priority newline asterisk equal priority LET asterisk BE asterisk equal priority let asterisk := asterisk in asterisk equal priority let asterisk = asterisk in asterisk end priority greater than postassociative priority norm asterisk equal priority asterisk Guard asterisk equal priority asterisk is val : asterisk equal priority asterisk is bool : asterisk equal priority asterisk is int : asterisk equal priority asterisk is pair : asterisk equal priority asterisk is map : asterisk equal priority asterisk is object : asterisk end priority greater than preassociative priority asterisk reduce to asterisk equal priority asterisk == asterisk end priority greater than postassociative priority asterisk,asterisk equal priority asterisk[ asterisk ]asterisk equal priority asterisk[[ asterisk ]]asterisk equal priority asterisk[[[ asterisk ]]]asterisk end priority greater than preassociative priority asterisk linebreak asterisk end priority greater than preassociative priority asterisk & asterisk end priority greater than preassociative priority asterisk \\ asterisk end priority greater than empty end define ]]"

\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