1.10 References and indexes

Page 12 of 333

As you have already seen, each Logiweb page has a reference which is about 30 bytes long. The reference of a Logiweb page is world wide unique.

In addition, each construct defined by a page has an index. The page construct always has index 0. All other constructs are numbered consecutively, starting with 1.

Hence, each construct is uniquely identified by its index together with the reference of the 'home page' of the construct, where the 'home page' is the page on which the construct is defined.

On the combinations page, the combinations construct has index 0 and the (( " , " )) construct has index 1. You can see this and a lot of other information in the extract generated by the lgc compiler.

Each construct has an 'arity' which is the number of double quotes in the construct. As an example, the (( " , " )) construct has arity 2.

The vector of a page contains:

• A bibliography which lists the Logiweb reference of the page itself followed by the Logiweb references of all referenced pages.
• A dictionary which lists the arities of all constructs defined by the page.
• A body which is just the parse tree of the body of the source expressed in Polish prefix.

To Logiweb, a construct is just a pair of a reference and an index. A construct exists if there exists a vector with the given reference whose dictionary assigns an arity to the given index. This machinery ensures:

• Logiweb offers notational freedom. You can assign a name to a construct by a name definition and a rendering by a show definition.
• Your notational freedom does not interfere with the notational freedom of others: Different authors can assign the same name or rendering to distinct constructs. Thus, even though I use x + y to denote integer addition, you are free to use x + y for anything you like.
• The uniqueness of Logiweb references ensures that each and every version of a page you publish gets its own reference. If you reference a page somebody else has published, it is the Logiweb reference of that page which is included in the bibliography of your page. Thus, even if the author or the other page publishes a new version, your page still references the old version. This ensures that if you have a working Logiweb program which relies on code published by others, your program will continue working regardless of what other people do. And if you have a correct proof which relies on axioms or lemmas published by others, your proof will remain correct regardless of what changes others make to their lemmas or axioms.

If two distinct authors use e.g. x + y for two, distinct things, you may run into trouble if you reference both authors pages from your page. In that case you need the lgc name qualification features described later.

Page 12 of 333