7.10.3 Racks of pages
| Page 220 of 800||
Each page has an associated rack which we shall refer to as the rack of the page. The rack R of a page has the following elements:
- The vector of the page.
- The bibliography of the page as a list of references. Each element of the list is a natural. The first element of the list is 'reference number zero' which is the reference of the page itself.
- The dictionary of the page as an array. The array maps the index of each construct to the arity of the construct. As an example, the plus operation of the base page has index 588 and arity two, so the rack R of the base page satisfies R['dictionary']=2.
- The body of the page as a parse tree.
- The macro expanded version of the body represented as a parse tree.
- A collection of all definitions present on the page represented as a four-dimensional array (i.e. an array of arrays of arrays of arrays). As an example, consider a construct with reference r and index i and consider an aspect with reference r' and index i'. If a page defines the given aspect of the given construct, then the value of R['codex'][r][i][r'][i'] will be the parse tree of the definition.
- An array of compiled versions of value definitions present on the page. As an example, if a page defines a construct with index i and if the pages furthermore value defines the construct, then R['code'][i] will contain a tagged map which computes the construct. Tagged maps are convenient for this because you can apply them to arguments but you cannot look into their structure. Thus, different implementations can represent compiled functions different ways without hurting portability. At the same time, if you (or your proof checker) wants to see how a construct is value defined, the information is available in the codex.
- If the value is then the page is correct. Otherwise, the value has form where D is a parse tree indicating what was wrong. lgc(1) generates a diagnose in PDF by rendering the value D of the diagnose hook. The diagnose hook is maptagged because the diagnose is inserted in the rack before verification. In other words, the diagnose is inserted before it is known. That only works because the diagnose is inserted lazily. If the verifier is dumb enough to access the diagnose of its own page, it effectively tries to access the diagnose it is itself in the middle of computing. If it does, the verifier will loop indefinitely.
- An array of something the eval function needs occasionally.
Note. All 'revelations', i.e. all definitions, introductions, and proclamations of a page end up in the codex. For definitions and introductions, the parse tree of the definition or introduction is included. For proclamations, a quoted version of a string is included. As an example, the base page proclaims to denote lambda abstraction using the proclamation . For that reason, the value of is where r and i are the reference and index of the lambda construct. The debugging information of the quoted string is set to .
Note. The code array contains maptagged compiled functions except for constructs which denote lambda abstraction and quoting. For each construct which denotes lambda abstraction or quoting, the code array contains the integer 0 or the integer 1, respectively. Those integers are not maptagged.
Copyright © 2010
| Page 220 of 800||