Logiweb defines an open format for storing the syntax and semantics of mathematical documents in such a way that one document can refer to other documents across the internet and in such a way that mathematical proof checkers can verify the documents. Such documents are referred to as 'Logiweb pages'.
As an example, a user X may publish a Logiweb page that defines an axiomatic theory T, a user Y may then publish a Logiweb page that defines a lemma L in theory T, and a user Z may then publish a Logiweb page that states a proof P of lemma L in theory T. After that, one may use the Logiweb system to verify the proof despite that the three Logiweb pages may reside different places in the world.
At the time of writing, the Logiweb system comprises the following applications: compiler, browser, server, relay, and lgwping.
The Logiweb compiler allows to generate Logiweb pages. The compiler takes 'pyk' source files as input and produces Logiweb pages as output. Pyk source files look like 'spoken mathematics'.
The Logiweb browser allows to view Logiweb pages and to check their correctness. At the time of writing, the only browser available is a 'crossbrowser'.
The crossbrowser is a collection of ordinary html pages that make an ordinary web browser act as if it were a Logiweb browser. In reality, the crossbrowser is a part of the compiler above: when translating a pyk source file, the compiler precomputes all windows, menus, and submenus a Logiweb browser may display, and stores them all in html format with proper links between them.
Click here to open a sample page with the crossbrowser. Click 'Body' and then 'Pdf' to view the page.
The network of Logiweb servers works behind the scenes, maintaining a catalog all Logiweb pages.
Logiweb pages are referenced by 'Logiweb references'. Every Logiweb page has a Logiweb reference which is worldwide unique. The reference does not indicate the physical location of the page. Rather, a Logiweb page may be moved and copied around the world without changing the reference.
The task of Logiweb servers is to translate Logiweb references to Uniform Resource Locators (URLs) with which one can then fetch the associated Logiweb pages. The actual delivery of Logiweb pages is done by other systems like web or ftp servers. When a web server delivers a Logiweb page, the Mime type is x-Logiweb since Logiweb is experimental at present.
Logiweb servers communicate their clients and each other using the Logiweb protocol. The Logiweb protocol can be caried by any byte-oriented host protocol, but the current Logiweb server uses UDP/IP and typically listens at port 65535 (since the current Logiweb system is experimental).
The Logiweb relay allows to get hands-on experience with the Logiweb protocol. The Logiweb protocol itself is a byte oriented protocol which is not particularly human tolerant. The Logiweb relay allows a user to send reasonable Logiweb requests to a Logiweb server and to get a reasonable explanation of what the associated Logiweb response means.
Most of the relay application actually resides inside the Logiweb server but also consists of a microscopic CGI-program which relays back and fourth between an ordinary web browser and the Logiweb server.
Click here to try the Logiweb relay interface.
Finaly, the Logiweb suite contains a program named lgwping which allows to send raw Logiweb requests to Logiweb servers.
When a Logiweb page is published, the Logiweb system computes a 'reference' for the page. The reference is worldwide unique and allows to refer to the page across the internet. When the Logiweb system looks up a page, it always does so using the reference.
A Logiweb reference of a Logiweb page contains a RIPEMD-160 signature. That signature is computed on basis of the contents of the page. Any change to the contents of the page also changes the signature. Hence, looking up a Logiweb page several times using the same reference is guaranteed to yeild the same page each time.
We shall say that Logiweb pages are 'immutable' because no-one, not even the author, is able to change the Logiweb page associated to a given reference once the page is published.
A Logiweb reference expressed in mixed endian kana may look like this:
nani
tita nise kise katu tesa tusa keni nenu tute nuta
siku kutu suku nenu keka kate tuna senu tasi nasa
kita kanu kesu kisi seke seki sita nasa natu
Each of the nonsense words above represents one byte. The reference above consists of 30 bytes in total. The first line contains a version number. The next two lines contain 20 bytes (160 bits) which make up a RIPEMD-160 hash key. The last line indicates the time of publication expressed as the number of seconds that have elapsed since International Atomic Time (TAI) 00:00:00 on Modified Julian Day (MJD) 0. The number of seconds is expressed on the form m*10^(-e) where m and e are cardinals (non-negative integers).
One of the major components of the Logiweb system is the 'Logiweb server'. The main task of Logiweb servers is to translate Logiweb references to uniform resource locators (urls). As an example, given a reference like the one above, a Logiweb server is able to provide a list of urls where the contents of the page can be found. The actual delivery of the page is outside the scope of the Logiweb server. One must use ordinary web servers for the actual delivery of Logiweb pages.
If a Logiweb server is requested to translate a reference to an url but is unable to do so, then the server may do one of two things: If the server thinks that no page with the given reference exists, then the server says so. But if the server just does not index that particular page but knows another Logiweb that is more informed, then the server refers to that other server.
Hence, when translating a reference to an url, the requester may have to go from server to server until some server eventually either provides an url or says that the page does not seem to exist. In the worst case, one may have to consult as many servers as there are bits in the reference before getting a definitive answer.
The main task of the Logiweb browser is to display Logiweb pages to the user and to allow the user to browse on Logiweb. At the time of writing, no stand-alone Logiweb browser has been implemented yet, but it is possible to use the crossbrowser to view pages.
The main task of the pyk compiler is to translate a source text expressed in 'pyk' to a Logiweb page.
The name "pyk" is constructed from the name "Volapyk" in the same way that Rene Thom construct the word "versal" from "universal": "pyk" is constructed by removing "Vola" from "Volapyk". Volapyk 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 construct from "Vola" which is a simplification of "World" and "pyk" which is a simplification of "speak".
The pyk language may be used for "spoken mathematics" and may, among other, be entered through a microphone when editing mathematical text.
As an example, the following pyk source defines a functions f(x) to denote x+2:
define the value of function f of var x end as var x plus two end define
The pyk language is basicly user definable, and the pyk source above only makes sense if one has defined the following constructs beforehand:
define * of * as * end define
the value
function f of * end
var x
* plus *
two
When the pyk compiler translates a pyk source into a Logiweb page, it generates, as a bonus, a number of html pages that allows a user to view the page without having a Logiweb browser. This collection of interlinked pages was called the 'crossbrowser' above.
When the pyk compiler generates a Logiweb page, it places the bonus pages at fixed, relative locations, relative to the Logiweb page itself.
The Logiweb servers communicate with each other and with Logiweb clients using 'Logiweb messages'. A Logiweb message is a sequence of bytes that conforms to a certain syntax.
Logiweb messages are supposed to be sent around using some carrier protocol. The present Logiweb server uses UDP/IP as carrier protocol and each UDP packet contains exactly one Logiweb message.
Logiweb messages are suited for both datagram protocols like UDP and connection oriented protocols like TCP. When sending Logiweb messages over a connection oriented protocol one may simply send the messages back-to-back since message boundaries can be reestablished by parsing the stream of messages.
Logiweb messages are compact; they are not at all intended for human consumption.
The Logiweb relay is a component of the Logiweb system that allows humans to interact with a Logiweb server through a human tolerant interface. The relay is intended for implementers of Logiweb servers or Logiweb clients who want to play with the system to see how it is supposed to react. As an example, one may find a Logiweb relay here.
Klaus Grue, GRD-2004-08-03