The Nuprl Library Manager is the common foundation for sharing mathematics; it provides clients with utilities for building, storing, and sharing, collections of ``session objects''. Session objects are things such as expressions, rules, definitions, programs, proofs, and informal items such as documentation or explanations.
The Nuprl system includes a ``native'' inference method, which comprises execution of proof tactics written in ML, and with a specificly defined method of interpreting inference rules and definitions, but the Nuprl Library Manager is not dependent on those details. Indeed, one may define alternative inference methods, implemented as processes called ``refiners.'' An example is Nuprl-Light. It has its own concepts of how rules and definitions are to be specified. It is possible for a proof in a Nuprl library to call different kinds of refiners for different inference steps within it, because each inference step may be expressed as an object content, thus one way to interface to a new or foreign system is to call it as a new kind of refiner.
Now, let us consider how Nuprl relates session objects to each other. Objects used in a client session are named, and there is a method for including object names inside expressions that are the content of objects, thus implementing pointers between objects.
A key service provided by the Library Manager is to enforce a discipline for building named collections so that collision can be easily avoided in selecting new identifiers and object addresses, without explicit interaction between users. This is effected by making such identifiers and object addresses abstract, and we have assimilated abstract identifiers to abstract object addresses to avoid duplicating name management; so allocating a new abstract identifier is allocating a new object in the session collection. There are infinitely many abstract identifiers, so one can always find new ones, and one can always determine identity between identifiers; no further structure is supported.
The Library Manager includes a repository of such object collections, and one may store a client session's collection, or a subcollection, under an externally significant name, such as a string, into the library. When one retrieves a stored collection, however, one is not guaranteed to get a collection back with the same addresses - one is only assured of getting a ``similar'' collection, which is like the original except for uniform renaming of the objects throughout the collection, including adjustments of the object addresses mentioned within object contents.
For various purposes, one may define notions of ``Coherency'' for collections of session objects, and the Library Manager helps maintain and combine coherent maps. The basic coherency condition is that if some object contains an object address, then the addressed object is also in the collection. Another typical coherency condition would be that there are no two objects that define the same operator, and that definition chains are well-founded. Obviously one would expand the coherency conditions to assist in maintaining variously ``meaningful'' collections of interdependent objects.
The structure of session collections described here is essentially ``flat.'' When one wishes to impose more structure on a collection of objects, such structure may be expressed as contents of other objects created for that purpose, such as the Module System described elsewhere in this proposal. Yet one may alway ask after the ``internal'' relations between objects determined by their contents, and may choose to impose different external structures on the collection by description.
Here are some examples of operations we wish to implement on session collections:
=0in=0in