'Loading' a Logiweb page is a process which takes a Logiweb 'reference' as input and produces a Logiweb 'codex' as output.

Loading a page consists of fetching, unpacking, codifying, and verifying the page which is described in the following.

Table of contents

'Getting' a page is done by sending the url to an ordinary web server. Hence, Logiweb servers merely locate the page, the actual delivery is done by an ordinary web server.

The translation from reference to vector is 'univocal' in the sense that doing the translation twice yields the same result. The translation from reference to url, however, is not univocal: Identical copies of a Logiweb page may reside many different places, and the Logiweb servers just point out a random one of them.

If you depend very much on a particular Logiweb page, you should copy it to your local machine and make it available through your local Logiweb server. That way the page will continue to exist on Logiweb, even if all other copies are deleted.

The second activity when loading a page is to 'unpack' it. 'Unpacking' a Logiweb page is a process which takes a Logiweb vector as input and produces a Logiweb 'bibliography', 'cache', 'dictionary', and 'body' as output.

As mentioned, when 'loading' a Logiweb reference one obtains a Logiweb 'codex'. Loading a reference is univocal, so loading a reference twice gives the same codex both times.

Loading a reference may require quite some computational resources, so it is reasonable to avoid loading the same reference twice.

A Logiweb cache is an associative structure that maps Logiweb references to their codices. 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.

The 'cache' of a page associates all references loaded during unpacking to their codices.

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.

In the next section, we divide general symbols into 'proper symbols' and 'improper symbols'. We reserve the term 'symbol' to denote 'proper symbol'.

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.

To explain the notion of a 'codex' we first need to introduce the notion of a Logiweb 'array'.

A Logiweb array is an associative structure (a Lisp association list, actually) that maps cardinals to values. Technically, a Logiweb array is a list

((key_1 . value_1) (key_2 . value_2) ... (key_n . value_n))

for which all the keys are cardinals and for which the sequence key_1,key_2,...,key_n is strictly decreasing.

The keys are required to be strictly decreasing to ensure that two arrays define the same mapping if and only if the two arrays are equal. Such a property allows to implement Logiweb arrays such that they appear to be lists of pairs but really are traditional arrays or traditional hash tables behind the scenes.

That the keys are required to be decreasing rather than increasing is a matter of taste. I have considered pro et contra, taking into account that pairing is right associative, that Logiweb is lazy, and many other issues, and have settled on decreasing keys.

As a special case, the values of an array may themselves be arrays. We shall refer to an arbitrary value as a 0-dimensional array and to an array of n-dimensional arrays as an (n+1)-dimensional array.

Until further, we have introduced the notions of 'general', 'proper', and 'improper' symbols. We now introduce the notion of a 'predefined' symbol.

A 'predefined' symbol is a symbol of form (0,I) where I is one of the cardinals below.

Cardinal	Name
521510350945	apply
107083775959404	lambda
1702195828	true
26217	if
7883939740841374320	proclaim
111524889126244	define
7312272863631011951	optimize
7043440	pyk
435761734006	value
28542640894207341	message
118074580692597	unpack
133480761814883	codify
469919427683	claim
8751735916104086128	priority
478660485485	macro
1889378671569615937901	macroself
2074066507213475897709	macrostop
36020423902285563354362896749	macroprotect
2055186851327050473837	macroprio
121413839713092787058729325	macroexpand
8241999014097281389	macrovar
6648432	pre
1953722224	post
2147777197149639505011	statement
126935164677737	infers
495890755437	modus
32195308414068077	metavar
7305804385369681513	instance
7173491	sum
465557414252	label
8315179222341807717	endorses
126879615906416	proves
435459876200	hence

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

We shall refer to proper and predefined symbols collectively as Logiweb 'aspects'.

Predefined symbols have 'names', where a 'name' is a list of small letters from the English alphabet.

A name is converted to the associated cardinal thus: Convert each character in the name to its ASCII value. Then interpret the sequence of cardinals as a number in little-endian base 256. As an example, letter "i" and "f" are letter number 9 and 6 in the English alphabet, respectively. Hence, their ASCII values are 96+9=105 and 96+6=102, respectively. Hence, the cardinal associated to "if" is 105+256*102=26217.

(Implementation note: The set of predefined symbols is intended to be fixed. But if it is ever changed and if names are allowed to be composed of characters with codes beyond 127, then one should convert each character to a sequence of bytes using little-endian base 128 and add 128 to all bytes except the last byte of each character before converting to a cardinal using little endian base 256. In other words, each character should be encoded in the septet-scheme used elsewhere in Logiweb.)

A codex is a 4-dimensional array. With a few exceptions, a codex is a 4-dimensional array of Logiweb trees. In this context, a tree may be either a tree of proper symbols or a one-node tree whose sole node is a predefined symbol.

If C is a codex, if (r,i) is a symbol, if (R,I) is an aspect, and if A = C[r][i][R][I] is defined, then we shall refer to A as the (R,I) aspect of the (r,i) symbol. We shall refer to C[r][i] as the 'property list' of the (r,i) symbol.

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
etx	=	(r,4)	has arity 0
f	=	(r,101)	has arity 1
i	=	(r,105)	has arity 1

Furthermore suppose (r,1) is a 'proclamation symbol'. How a symbol becomes a proclamation symbol is described later.

A tree of form

(proclaim (if (x) (x) (x)) (i (f (etx))))

is a proclamation that proclaims (r,2) to denote the predefined if-then-else construct of Logiweb. Note that 105 and 102 are the ascii codes for a small letter i and f, respectively.

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 tree'.

A 'string tree' is a tree which denotes a string of characters in a particularly simple way. To translate a string tree to a string, do as follows: Scan the tree from root to leaf, left to right, depth first, and note the identifier i of each symbol (r,i). Ignore all identifiers in the range 0..9 and 11..31. The remaining identifiers make up the string. In the example above, (i(f(etx))) gives rise to the sequence (105 102 4) except that 4 (ascii end of text) is ignored. Hence, (i(f(etx))) denotes the sequence (105 102) where 105 and 102 are the ascii codes for a small letter i and f, respectively. Hence, (i(f(etx))) denotes the two character string "if". The string "if" happens to identify the predefined if-then-else concept of Logiweb.

In Logiweb, the newline character has code 10 and may occur in string trees.

'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, its string tree is translated to a string, and 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)) (i (f (etx))))

The string tree of the proclamation translates to "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 a one-node tree ((0 . 26217)) where (0 . 26217) is the predefined 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 'optimize'. They have identical semantics, but 'optimize' invites the Logiweb browser to do something special behind the scenes. Stupid use of 'optimize' typically has no effect but may ruin efficiency. Clever use of 'optimize' 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 not yet documented.

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 then 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 predefined 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 and last 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.

If verification finds that the page is correct (contains no formal errors), then it returns the codex unchanged.

If verification finds errors in the page, then it sets the diagnose aspect of the page symbol to some tree which identifies the error.

Errors found during the first three activities (fetching, unpacking, and codifying) are considered 'fatal' and are reported by returning an empty codex from the loading process.

Unpacking a page may involve loading lots of referenced pages. If any one of those referenced pages contain errors (result in an empty codex or in a codex where the error aspect of the page symbol is set), then the page itself is considered to contain a fatal error and results in an empty codex.

Logiweb has a facility for proof checking which is invoked during verification.

The proof checing facility has been included in Logiweb in order to get started, but is going to be removed as Logiweb matures. The 'exit strategy' is as follows:

During alpha test, the proof checing facility will be in flux.

During beta test, the proof checing facility will be fixed, except that bugs will be corrected.

Later, when Logiweb has matured, the proof checking facility will be programmed within the Logiweb programming language and placed on a Logiweb page P. Then, a new, predefined aspect named "claim" will be introduced. After that, a page will be considered correct if the claim aspect of the page symbol of the page evaluates to T when applied to the codex of the page. If no claim aspect is defined for a page symbol, the claim will default to the proof checker defined on page P above. This way, the Logiweb standard will be simplified in a backward compatible manner some time in the future.

A 'statement' is a Logiweb tree which is used for representing rules, theories, lemmas, proofs, and similar.

In the following, we shall use x |- y to denote a tree whose root is proclaimed to denote "infers" and whose first and second subtree is x and y, respectively. The |- symbol is an ASCII approximation of Unicode 0x22A2 (RIGHT TACK, turnstile, proves, implies, yields, reducible). The following table lists similar operators:

Operator	Logiweb name	Unicode	Unicode name
x |- y	infers	0x22A2	Right tack
x ||- y	endorses	0x22A9	Forces
< x > y	all	0x2329/0x232A	Angle bracket
x + y	sum	0x2295	Circled plus

x |- y reads "x infers y" and denotes that if x has a proof then y has a proof. In x |- y we shall refer to x and y as 'premise' and 'conclusion', respectively.

x ||- y reads "x endorses y" and denotes that if x evaluates to T (truth) then y has a proof. Note that Logiweb uses ||- to denote 'endorsement' rather than 'enforcement', where the latter is the normal use in the literature. In x ||- y we shall refer to x and y as 'side condition' and 'conclusion', respectively.

< x > y reads "all x indeed y" and denotes that y has a proof regardless of which Logiweb tree is substituted for the Logiweb tree x. The root of the Logiweb tree x must be proclaimed as a "metavariable".

x + y reads "x sum y" and denotes that x as well as y has a proof.

We overload angle brackets heavily in the following since we shall use <x>y to denote meta-quantification, <x,y,z> to denote a tuple, and <x|y:=z> to denote x in which all free occurrences of y are replaced by z.

A 'Logiweb conjunction' is a sorted list of statements without duplicates. Conjunctions are sorted according to a rather arbitrary ordering relation which is described soon.

An ordered list without duplicates is a convenient representation for a set. Hence, effectively, a conjunction is a set of statements.

The representation of conjunctions has the benefit that, given a conjunction, it is well-defined what that first element of the conjunction is (because of the chosen ordering). This allows implementors of Logiweb to implement conjunctions efficiently backstage and still pretend that the conjunctions are just lists. The user may notice that testing for membership of a conjuction is remarkably fast and that taking the head or tail of a conjunction is suspiciously slow, but the implementor must ensure that conjunctions always behave as if they were lists.

Now let t be a Logiweb tree. If one scans t root to leaf, left to right, depth first and notes the reference and id of all symbols, then one will get a list s = r_0,i_0,r_1,i_0,...,r_n,i_n of cardinals where (r_0,i_0) is the root of the tree, (r_1,i_1) is the root of the leftmost subtree, and (r_n,i_n) is the rightmost leaf. We shall refer to s as the 'flattening' of t.

The ordering on trees used for sorting conjunctions is lexicographic ordering on the flattenings of the trees.

Two trees are considered 'equivalent' if they have the same flatting, i.e. if they are equal except for attached debugging information. A conjunction must be 'without duplicates' in the sense that distinct elements of a conjunction must have distinct flattenings. A statement b is a member of a conjunction B if B contains an element that is equivalent to b.

We introduce the following operations for constructing conjunctions: 0 denotes the empty conjunction, {a} denotes the unit conjunction that merely contains a, A u B denotes the union of A and B, and A \ B denotes the conjunction of elements of A that are not elements of B.

The union A u B equals A u ( B \ A ), i.e. if A and B contain a and b, respectively, and a and b are equivalent, then A u B will contain a.

A 'Logiweb sequent' is a quadruple <L,P,S,C> where L, P, and S are conjunctions and C is a statement. A sequent <P,S,C> denotes that if all elements of L and P have a proof and all elements of S evaluate to T (truth), then C has a proof. In a sequent <L,P,S,C> we shall refer to L, P, S, and C as the 'lemmas', 'premises', 'side conditions' and 'conclusion' of the sequent, respectively.

As a special case, a Logiweb sequent may also be the value T which denotes triviality, but which we shall refer to as an 'exception' following.

'Logiweb sequent calculus' is a collection of twelve sequent operations. The following nine sequent operations all take one sequent and, possibly, one statement as input and yield one sequent as output:

infer-( < L , P , S , a |- b > )	=	< L , P u {a} , S , b >
infer+( a , < L , P , S , b > )	=	< L , P \ {a} , S , a |- b >
endorse-( < L , P , S , a ||- b > )	=	< L , P , S u {a} , b >
endorse+( a , < L , P , S , b >)	=	< L , P , S \ {a} , a ||- b >
eval( < L , P , S , a ||- b > )	=	< L , P , S , b >	if a is true
all-( c , < L , P , S , <a>b > )	=	< L , P , S , <b|a:=c> >	if c is free for a in b
all+( a , < L , P , S , b > )	=	< L , P , S , <a>b >	if a is not free in P and S
Curry-( < L , P , S , a |- b |- c > )	=	< L , P , S , a + b |- c >
Curry+( < L , P , S , a + b |- c > )	=	< L , P , S , a |- b |- c >

The following two sequent operations takes one statement as input and yields one sequent as output:

premise( A )	=	< 0 , {A} , 0 , A >
lemma( A )	=	< {A} , 0 , 0 , A >

The following sequent operation takes two sequents as input and yields one sequent as output:

cut( < L_1 , P_1 , S_1 , C_1 > , < L_2 , P_2 , S_2 , C_2 > ) = < L_1 u L_2 , P_1 u ( P_2 \ { C_1 } ) , S_1 u S_2 , C_2 >

Sequent operations return the exception in all cases not covered by the definitions above. As an example, infer-( < L , P , S , a ||- b > ) = T because the conclusion does not have the required form a |- b. As another example, eval( < 0 , 0 , 0 , F ||- b > ) = T because F (falsehood) does not evaluate to T (truth).

In the definitions of all- and all+ above it is understood that a must be a metavariable, i.e. that the root of a must be proclaimed as a metavariable.

We shall refer to an expression made up from Logiweb sequent operations as a 'raw Logiweb proof'. We shall refer to the result of evaluating all the sequent operations of a raw proof as the 'proof value' of the proof.

We shall say that B is a proof of C if the proof value of B is a sequent of form < 0 , 0 , 0 , C >. We shall say that a statement C is a 'Logiweb theorem' if it has a raw Logiweb proof.

The proof checking facility of Logiweb accepts a somewhat wider class of 'general Logiweb proofs'. General proofs are statements that the proof checker expands into raw proofs on the fly. Furthermore, the proof checker accepts B as a proof of C if the proof value of B has form < L , 0 , 0 , C > where all elements of L are previously proved lemmas.

Not yet written