Glossary FDLnotes
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Readings

The fundamental relations between Formal objects that are accounted for in the FDL are "internal" ones. For example: the fact that one proof cites another as a lemma; that a certain definition for an operator is employed in a proof or procedure; that a certain inference rule is used by a certain inference engine; that a certain object contains the source code for a given procedure; that a certain object's content is used as data in, or is the result of, a certain computation; that one object refers to another.

But persons and programs normally need much more information about the organization of formal data (see Formal vs Informal), "external" relations between objects, and connections to informal concepts. By a "reading" we mean a collection of objects and procedures that provides a guide to a collection of formal objects. Naturally, a reading is itself stored in the FDL. Readings provide alternatives to simply following internal links among formal objects, and would typically include: pages of text mentioning formal data, hyperlinks to formal objects, to other objects of the reading, and to material beyond the FDL collection; search utilities for focusing on the subject material of the reading; objects specifying how to display expressions to the reader.

Multiple readings may be given for the same material. When content is developed as a formalization of a conventional body of knowledge, one should provide a reading of the material using conventional organization. Other organization is possible as well. For example, presentation and organization for the purposes of programmers looking for graph algorithms may require an emphasis that differs somewhat from presentation for graph theorists. Formalization itself can reveal aspects of material that suggest other organizations as well; persons that formalize material may have something significant to contribute to the explanation and organization of conventional subjects. One might also tailor presentation to the sophistication of the audience.

As an adjunct to readings, one may provide data and utilities for the use of programs employed by those at whom the readings are directed, including as part of the reading an explanation of how they are to be used.

An example of an external organization would be presenting a collection of definitions, proofs and programs as being about abstract algebra, say, based upon a given body of assumptions, and perhaps grouping parts in "modules" sharing common assumptions and methods. This grouping need not be built in to the formal objects themselves since, after all, their correctness need not depend on such grouping. One may well find it efficient or informative to take a few pieces from variously organized collections of material and recombine them into a new reading. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes