Logiweb(TM)     Logiweb system pages  
        Loading pages  
 

System pages
Site pages

Introduction...
Showroom
Tutorials
Man pages
Help
Download
Wiki...
Wiki submission
Background
Machine room...
Contact

Semantics
Protocol
Protocol as ID...

   

Home. Help index. Crossbrowser. Crossbrowser main menu.

Loading

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

After loading a page it is possible to 'render' and 'execute' it.

At present, loading, rendering, and execution is done by the pyk compiler. Rendering results in a number of interlinked html-, pdf-, and other files. When viewed in an ordinary web browser, the interlinked html-, pdf-, and other files allow to navigate within and among Logiweb pages. A genuine Logiweb browser would allow the same kind of navigation as is possible with an ordinary web browser plus the interlinked html-, pdf-, and other files. Hence, an ordinary web browser plus the interlinked files effectively implement a Logiweb browser. We refer to that browser as the 'Logiweb cross browser' because it is a Logiweb browser that is hosted by an ordinary web browser.

Rendering of a Logiweb page typically results in a number of html- and pdf-files. But the rendering engine of Logiweb is not restricted to any particular format. Rendering of a Logiweb page may also result in .c files, .h files, makefiles, and any other kind of file that can be expressed as a sequence of bytes. It is the author of a Logiweb page who decides which and how many files rendering results in. In particular, rendering of a Logiweb page may result in 'Logiweb machines' which are executable files.

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

Table of contents

References
Fetching
   Locating
   Getting
Unpacking
   Bibliographies
   Arrays
   Caches
   Reference Cardinals
   Symbols
   Dictionaries
   String symbols
   Bodies
Codifying
   Codices
   Proclamations
   Harvesting proclamations
   Definitions
   Harvesting definitions
   Expansions
   Macro expansion
   How the parts play together
Verifying
Rendering
Executing

References

A Logiweb reference is to Logiweb what a http reference is to the worldwide web: It is something that allows to locate a page.

A http reference encodes the physical location of the page (a particular file on a particular server). In contrast, a Logiweb reference is a signature which allows to locate a page with a particular contents regardless of the physical location.

If you load a Logiweb page twice, even with years in between, using the same reference, then you can be sure to receive the same page the two times. In contrast, ordinary web pages are in flux and may change at any time.

A Logiweb reference is a sequence of bytes where a byte is a cardinal (i.e. natural number) in the range 0..255 (i.e. 0 to 255 inclusive). A Logiweb refererence can be arbitrarily long but typically consists of around 30 bytes.

To see the reference of a page, click the 'Reference' entry of the crossbrowser main menu of the page and then click 'Hex bytes'.

Fetching

The first activity when loading a page is to 'fetch' it. 'Fetching' a Logiweb page is a process which takes a Logiweb reference as input and produces a Logiweb vector as output.

A Logiweb vector is a sequence of bytes. The vector of a Logiweb page is the form in which Logiweb pages are stored on disc and transmitted over networks.

A Logiweb vector must either conform to the Logiweb default format or to a user defined format. In the latter case, an advanced Logiweb user must tell Logiweb how to unpack that format. As an example, one may explain Logiweb how to interpret pfb font files. After that, Logiweb can handle such files, but the files have to be prepended with about 70 bytes (two references and a dictionary) which identify the format before submission to Logiweb.

To see the vector of a page, click the 'Vector' entry of the crossbrowser main menu of the page.

The vector of a page starts with the reference of the page. Hence, if you look up both reference and vector you should see that the reference forms a prefix of the vector.

Fetching a page consists of 'locating' and 'getting' the page. 'Locating' a page is a process which takes a Logiweb reference as input and produces a uniform resource locator (url) as output. 'Getting' a page is a process which takes the url as input and produces the vector as output.

Locating

To locate a page, one sends the reference to a Logiweb server using the Logiweb protocol. This is typically done by sending a get request as a udp packet to the server.

The server has four possible responses: (1) The server knows the url of the page and sends this url. (2) The server thinks that the page does not exist anywhere in the world and says so. (3) The server refers to another server by sending the url of the other server. (4) The server sends a short notice saying that it is too busy to reply at the present time.

The last of the four options is a safety valve included in the Logiweb protocol to handle denial of service attacks. That option will be ignored in the following.

When locating a page, option (3) above may occur several times: one may have to consult a chain of servers before ending in situation (1) or (2).

As mentioned, a reference is a sequence of bytes. At any time while locating a page, some of the bits of the reference are 'resolved' and some are 'unresolved'. To begin with, all bits are unresolved and, for each time situation (3) above occurs, the number of resolved bits increases. Hence, locating a page terminates after consulting at most as many servers as there are bits in the reference.

Getting

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

Unpacking

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.

Bibliographies

A Logiweb bibliography is a list of bibliographic entries where an entry is a Logiweb reference. Entry number zero (the first entry) is the reference of the page itself, so every page refers to itself.

Bibliographic entries except entry number zero are termed 'proper' entries. A bibliography may have zero, one or more proper entries. The graph that has Logiweb pages as nodes and proper entries as edges form a directed, acyclic graph.

To see the bibliography of a page, click the 'Bibliography' entry of the crossbrowser main menu of the page.

Arrays

To explain the notion of a 'cache' and many other Logiweb data structures, we first need to introduce the notion of a Logiweb 'array'. A Logiweb array is an associative structure which can map cardinals to arbitrary values. Logiweb arrays are organized such that the access time is logarithmic in the number of entries of the array in the cases of interest to Logiweb.

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.

For an array A and a cardinal n we shall use A[n] to denote the value that A associates to n. For an e.g. 3-dimensional array B, B[u][v][w] denotes ((B[u])[v])[w].

Arrays may be sparse: an array may map e.g. 10 and 20 to values without mapping the numbers in between to anything. The access time of an array A is logarithmic in the number of indices i for which A[i] is defined.

Caches

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

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

The cache of a page is an array which maps cardinals to values. The cache of a page maps the cardinal 0 to the reference cardinal of the page itself. Furthermore, the cache of a page maps the reference cardinals of the page and all its transitively referenced pages to the 'racks' each each page.

The 'rack' of a page is another array which maps cardinals to values. We refer to an array of inhomogeneous data as a 'rack' and to the indices of such an array as 'hooks'. The hooks are strings like 'bibliography' and 'dictionary' converted to cardinals.

The rack of a page maps the bibliography hook to the bibliography of the page, the dictionary hook to the dictionary of the page, and so on. The rack of a page has the following hooks:

bibliography
A list of references
dictionary
An array which maps indices to arities
body
A tree structure: the body as unpacked from the vector.
cache
An array which maps references to the caches of transitively referenced pages. Contrary to the cache of the page, this cache only contains transitively referenced pages, not the page itself. Furthermore, this cache maps references to page caches rather than racks.
vector
A sequence of bytes: the original bytes from which the page was unpacked.
diagnose
Absent if the page is correct. Otherwise, a tree structure which, when rendered, explains what is wrong with the page.
codex
A collection of all definitions present on the page.
code
Compiled versions of all value definitions on the page.
expansion
A tree structure: the macro expanded version of the body.

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.

Reference cardinals

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

As mentioned earlier, a reference is a list of bytes where a byte is a cardinal in the range 0..255. To each reference

r = (b_0,b_1,...,b_n)

we associate the following 'reference cardinal':

R = b_0 * 256^0 + b_1 * 256^1 + ... + b_n * 256^n + 256^(n+1)

As an example, if <2,0> were a valid reference, then the associated reference cardinal would be 2*256^0+0*256^1+256^2 = 2+0+65536 = 65538.

Translation from references to reference cardinals is injective meaning that if one is given a reference cardinal, then one can uniquely determine the associated reference.

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.

Dictionaries

A Logiweb dictionary is an array that maps cardinals to cardinals.

Now consider a page whose reference cardinal is r. If the dictionary of the page maps the cardinal i to the cardinal a, then we say that the general symbol (r,i) is 'proper' and has 'arity' a.

Dictionaries are understood to map zero to zero. Hence, for any page r, the general symbol (r,0) is proper and has arity zero. We shall refer to (r,0) as the 'page symbol' of page r.

We shall say that a general symbol (r,i) is 'improper' in the following two cases. Case 1: no page on Logiweb has reference cardinal r. Case 2: Logiweb contains a page with reference cardinal r, but the dictionary of that page does not map i to anything.

To see the dictionary of a page, click the 'Dictionary' entry of the crossbrowser main menu of the page.

String symbols

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

Bodies

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.

Among other, unpacking a page yields a 'body' which is a tree. To see the body of a page, click the 'Body' entry of the crossbrowser main menu of the page.

The body is unpacked from the flat-tree of the vector of the page.

The body will not display as something like (plus (two) (plus (varx) (two))). Rather, the body will be available in formats like 'pdf' and 'dvi' and will display as something like 2+x+2. We shall refer to various ways of displaying a body as 'faces' of the tree.

Logiweb bodies are inspired by Lisp S-expressions. (When Lisp was introduced around 1960, it was explicitly stated that Lisp S-expressions were just a temporary format intended for bootstrapping the development of the Lisp system. So think of the faces above as the second stage of that bootstrap :-)

Codifying

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.

Codices

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.

Proclamations

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 proclamations

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

Definitions

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.

Harvesting definitions

As mentioned, harvesting scans a tree for proclamations and definitions. Whenever a definition ('define' or 'introduce') is found, harvesting adds the definition to the codex.

As an example, suppose the expansion of the base page with reference cardinal r from the previous three sections contains the following definition:

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

Harvesting first extracts the root of the first subtree. In the example, it extracts the 'value' symbol. Then it looks up the 'message' aspect of that symbol. In the present example, the 'value' symbol denotes the predefined 'value' aspect. Then harvesting extracts the root of the second subtree. In the example, it extracts the 'f' symbol. Finally, harvesting sets the predefined 'value' aspect of the 'f' symbol to the tree (define (value) (f (u) (v)) (if (u) (v) (u))). This allows to look up the defintion of the value aspect of the f-symbol in the codex.

Expansions

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

Macro expansion

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

How the parts play together

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

Verifying

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.

Rendering

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.

In particular, rendering of a Logiweb page may result in zero, one or more Logiweb machines (c.f. Executing below). A Logiweb machine is an executable file whose behaviour is defined in the Logiweb programming language.

Rendering of a page may use a few, external programs: latex, bibtex, makeindex, and dvipdfm.

See the base page for details on the rendering process.

Users can take complete control over the rendering process. There is an example of that in the test suite that comes with logiweb (the pages named 'renderer' and 'rendered' in the test suite).

Executing

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.

The crossbrowser is unable to execute pages. To execute a page, use the pyk compiler. The pyk compiler has command line options which allow to execute the page or to dump the nameless machine to an arbitrary file location. It also has options which allow to dump the named machines to an arbitrary directory.

See the base page for details on Logiweb machines.