One purpose of caches is to avoid loading the same reference more than once. Another is that the cache of a page constitutes the well-defined subset of the entire Logiweb that is needed for codifying, verifying, executing, and rendering the page.

To unpack a page one has, among other, to load all proper entries in the bibliography of the page. Loading those entries involves unpacking which may require further pages to by loaded and so on. Hence, unpacking a page includes loading all pages reachable from the page through bibliographic references. The process stops when reaching 'base' pages which are pages with no proper bibliographic entries.

To explain the notions of Logiweb 'bodies' and Logiweb 'dictionaries', we first need to introduce Logiweb 'reference cardinals' and Logiweb 'symbols'.

A Logiweb general symbol is a pair (r,i) of cardinals.

Logiweb general symbols is to Logiweb what identifiers are to programming languages. In particular, Logiweb general symbols are inspired by Lisp symbols.

If r is the reference cardinal of some page then we shall refer to a general symbol (r,i) as the i'th general symbol of that page.

A 'string' symbol is a symbol of form (0,I) where I is a cardinal which represents a string S. The cardinal I represents the the string S as follows: Write S as a sequence of bytes using UTF8 encoding:

(b_0,b_1,...,b_n)

Then compute I thus:

I = b_0 * 256^0 + b_1 * 256^1 + ... + b_n * 256^n

As an example, letter "i" and "f" are represented by Unicode 105 and 102, respectively, and UTF8 encode them as one byte each. Hence, the cardinal associated to "if" is 105+256*102=26217, and (0,26217) is the string symbol representing "if".

All string symbols are improper since 0 cannot be a reference cardinal.

String symbols are understood to have arity zero.

We shall refer collectively to proper and string symbols as 'Logiweb symbols' or just 'symbols'.

A Logiweb 'tree' is a list that consists of a symbol s followed by zero, one or more trees. The number of trees that follow the symbol must be equal to the arity of the symbol.

As an example, suppose r is a reference cardinal. Let plus = (r,1), let varx = (r,2), and let two = (r,3). Suppose plus has arity two and that varx and two have arity zero. In this case,

(plus (two) (plus (varx) (two)))

is a tree.

The third activity when loading a page is to 'codify' it. 'Codifying' a Logiweb page is a process which takes a Logiweb body and Logiweb cache as input and produces a Logiweb 'expansion' and Logiweb 'codex' as output.

Codifying a tree consists of two processes: 'macro expansion' and 'harvesting'.

Codification is iterative and, if it terminates, finds a fixed point in which the expansion is the result of macro expanding the body and the codex is the result of harvesting the expansion. This is circular since macro expansion depends on the codex.

A codex is a 5-dimensional array of Logiweb trees.

If C is a codex, if p is a reference cardinal, if (r,i) is a proper symbol, if (R,I) is a symbol, and if A = C[p][r][i][R][I] is defined, then we shall refer to A as the (R,I) aspect of the (r,i) symbol as defined on page p. An aspect is 'domestic' when p=r, and we shall refer to C[r][r][i][R][I] as the 'domestic' (R,I) aspect of the (r,i) symbol. We shall refer to C[r][r][i] as the domestic 'property list' of the (r,i) symbol.

The 'value' aspect of a symbol is particularly important. When a mathematician defines e.g. g(x)=2*x+4 then we shall say that the mathematician defines the 'value' aspect of the 'g' symbol where the 'g' symbol is supposed to have arity one. When a programmer defines e.g. void main(){printf("Hello world");} then we shall say that the programmer defines the 'value' aspect of the 'main' symbol.

The 'pyk' aspect of a symbol is also important. The 'pyk' aspect of a symbol defines what the symbol looks like. To Logiweb, a symbol is a pair of cardinals. That is machine friendly but not particularly user tolerant. The 'pyk' aspect of a symbol defines what the symbol looks like expressed in the 'pyk' language and, possibly, what the symbol looks like when expressed in TeX source text. The 'pyk' language is designed for authoring Logiweb pages.

Loading a page results in a codex and, as by-products, a vector, a bibliography, a dictionary, a body, a cache, an expansion, some code and, possibly, a diagnose. All these entities are collected into the rack of the page.

The rack of a page is eventually added to the cache of the page, so the end result of loading is a 'cache' which contains a 'rack' for the page plus one for each transitively referenced page where each 'rack' in turn contains the 'codex' of each page plus additional information. For more details see the 'base page' that comes with Logiweb.

Logiweb has several predefined concepts. A 'proclamation' is a construct that attaches predefined concepts to symbols. In contrast, 'definitions' described later attaches user defined concepts to symbols.

As an example, the if-then-else construct is a predefined concept of Logiweb and one may 'proclaim' that some symbol (r,i) denotes if-then-else.

Proclamations are best described by an example. Suppose a base page with reference r defines the following symbols:

proclaim	=	(r,1)	has arity 2
if	=	(r,2)	has arity 3
x	=	(r,3)	has arity 0

Furthermore suppose (r,1) is a 'proclamation symbol'. How a symbol becomes a proclamation symbol is described later. Finally let "if" denote the string symbol (0,26217) which represents the "if" string.

A tree of form

(proclaim (if (x) (x) (x)) ("if"))

is a proclamation that proclaims (r,2) to denote the predefined if-then-else construct of Logiweb.

In general, a proclamation is a tree for which the root is a proclamation symbol, the root of the first subtree is the symbol to receive a predefined meaning, and the second subtree is a string.

'Harvesting' is the process that collects proclamations and definitions from an expansion. In this section we consider harvesting of proclamations.

Given a tree, harvesting scans the tree for proclamations and definitions. Whenever a proclamation is found, if the string is recognised and matches the arity of the proclaimed symbol, harvesting adds an entry to the codex.

As an example, suppose the expansion of the base page with reference cardinal r from the previous section contains the following proclamation:

(proclaim (if (x) (x) (x)) ("if"))

The string of the proclamation is "if" which is recognised as denoting the if-then-else concept. The if-symbol (r,2) happens to have correct arity (three) and, hence, harvesting sets the value aspect of the if-symbol to the one-node tree ((0 . 26217)) where (0 . 26217) was the string symbol that represents "if". This allows to look up the defintion of the value aspect of the if-symbol in the codex.

Continuing the example of the previous two sections, suppose

define	=	(r,5)	has arity 3
f	=	(r,6)	has arity 2
u	=	(r,7)	has arity 0
v	=	(r,8)	has arity 0

Furthermore suppose that the 'define' and 'value' symbols are proclaimed to denote the predefined 'define' and 'value' concepts of Logiweb, respectively. With these assumptions,

(define (value) (f (u) (v)) (if (u) (v) (u)))

is a definition that defines the value aspect of (f u v) to be (if u v u).

For completeness, we mention that Logiweb has two definition concepts, one named 'define' and one named 'introduce'. They have identical semantics, but 'introduce' invites the Logiweb browser to do something special behind the scenes. Stupid use of 'introduce' typically has no effect but occasionally may ruin efficiency. Clever use of 'introduce' a few places may increase efficiency by many orders of magnitude. The implementers of Logiweb browsers can tell stupid from clever use, so read their documentation.

The expansion of a page is a Logiweb tree. The expansion of a page is the result of macro expanding the body.

Macro expansion is a user defined process which may be quite complex. See the 'base page' that comes with Logiweb for details.

Codification of a page with reference cardinal R takes the cache C and the body P of the page as input. C and P remain fixed during codification.

A page whose bibliography contains no proper entries is a 'base page'. To start the iteration, an initial codex X_0 is constructed. If the page being codified is no base page then the initial codex is empty. If the page being codified is a base page and symbol number one of the page has arity two, then that symbol is made a proclamation symbol in X_0. That is done by setting the 'definition' aspect of symbol number one to ((0 . 7883939740841374320)) where (0 . 7883939740841374320) is the string symbol whose name is "proclaim".

Given the cache C, the codex X_i, and the body P, each iteration consists of three steps.

Step 1. A new cache C' is constructed. C' is identical to C except that reference cardinal R is mapped to X_i. In other words, the codex X_i is non-destructively added to the cache C.

Step 2. The body P is macro expanded into an expansion S using the cache C'. The constructs in P are macro expanded according the the macro aspects of the constructs as defined by C'.

Step 3. The expansion S is harvested, yielding a new codex X_{i+1}.

The iteration ends when X_i equals X_{i+1}. If that never happens, then codification does not terminate.

When writing base pages, one should ensure that symbol number one proclaims itself to be a proclamation symbol. This ensures that symbol number one will be a proclamation symbol not only in X_0, but also in X_i for i>0. (Exercise: write a base page in which symbol number two ends up being a proclamation symbol whereas symbol number one ends up not being a proclamation symbol).

The fourth activity when loading a page is to 'verify' it. 'Verifying' a Logiweb page is a process which takes a Logiweb codex as input and produces a Logiweb codex as output. Verification is a user defined process. See the 'check page' that comes with Logiweb for an example of a user defined proof checker.

If verification finds that the page is correct (contains no formal errors), then it returns the rack of the page unchanged. If verification finds errors in the page, then it hangs an error message on the diagnose hook of the rack.

Unpacking a page may involve loading lots of referenced pages. Referenced pages may contain errors (i.e. have non-empty diagnose aspects). Proof checkers will typically require pages that contain referenced lemmas to be error-free. Logiweb itself does not care whether or not published pages are correct.

When a page is loaded, one may 'render' it. 'Rendering' a Logiweb page is a process which converts the body of the page into a collection of files. The rendering process is under user control in that it is controlled by definitions present in the codex.

Rendering of a page may result in an arbitrary number of files in an arbitrary number of formats. Rendering typically results in html and pdf files, but may also result in e.g. C source code and make files. Rendering may result in text as well as binary files.

When a page is loaded, one may 'execute' it. 'Executing' a Logiweb page executes one, particular Logiweb machine defined on the page.

Logiweb has two mechanisms for defining Logiweb machines: One mechanism for producing one, nameless machine and one mechanism for producing an arbitrary number of named machines. When 'executing' a page, it is the nameless machine (if any) which is executed.