FDL notes - DL scenarios4

Glossary FDLnotes

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Continued from Scenarios of FDL Use(part 3)

17a
Two (or more) large FDLs are maintained by parties that learn they can trust each other's FDL maintenance, and decide to accept each other's certificates without always reverifying them locally. This is not a deadly embrace because that a certificate is borrowed from another FDL is part of the certificate.

17b
It is discovered that one institution maintaining an FDL has not been following the protocols that all of a group FDL maintainers agreed to in order to promote federation. Because certifications passed from one FDL to another are recorded as such, they can be located, and all things that depended on them can be identified and scrutinized (and hopefully recertified).

18
A whole FDL's content is replicated into a new FDL because of inadequacies in accessing the original or some threat to its existence.

19
A person decides to introduce a concept, by definition say, but it turns out that someone else has already used the nomenclature they wanted to use. Because such nomenclature is extrensic to the formal material, and the attachment of nomenclature is performed as part of the connection of the user to the FDL, the user simply changes the old name to something she prefers, and adopts it for her newly defined concept. All the formal material using the old name survives the renaming because it was independent of the nomenclature.

20
A person finds a few formal objects of particular interest for a particular purpose, such as an algorithm and a specification and proof of correctness. They decide to collect into a single compact sublibrary just what is necessary to support those few formal objects. This is a basic FDL operation.

21
A person wants to develop some material "offline" at an independent site for a while. The procedure is to build a new temporary FDL (on their laptop, say) extracting the material of interest from a larger FDL. Later, after developing the material locally, that material can be posted back to the large FDL from which it came (or another one). This is possible because name collision is systematically avoided in FDLs by an abstract use of identifiers.

22
(a more speculative scenario, but with some basis in experience) A person wants to formalize a standard text or a chapter thereof not only to get the general benefits of formalization, but because as the original author proceeded, the proofs get progressively sketchier owing to copious allusions to the structure of earlier proofs, and the person wants to work those sketches out and save them. They are relieved to find that much of the basic generic math the text depends on is already in the FDL and can be immediately incorporated, and that using potent tools for manipulating proofs as data makes it easier than expected to realize those "proofs by allusion".

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

Glossary FDLnotes

17a	Two (or more) large FDLs are maintained by parties that learn they can trust each other's FDL maintenance, and decide to accept each other's certificates without always reverifying them locally. This is not a deadly embrace because that a certificate is borrowed from another FDL is part of the certificate.

17b	It is discovered that one institution maintaining an FDL has not been following the protocols that all of a group FDL maintainers agreed to in order to promote federation. Because certifications passed from one FDL to another are recorded as such, they can be located, and all things that depended on them can be identified and scrutinized (and hopefully recertified).

18	A whole FDL's content is replicated into a new FDL because of inadequacies in accessing the original or some threat to its existence.

19	A person decides to introduce a concept, by definition say, but it turns out that someone else has already used the nomenclature they wanted to use. Because such nomenclature is extrensic to the formal material, and the attachment of nomenclature is performed as part of the connection of the user to the FDL, the user simply changes the old name to something she prefers, and adopts it for her newly defined concept. All the formal material using the old name survives the renaming because it was independent of the nomenclature.

20	A person finds a few formal objects of particular interest for a particular purpose, such as an algorithm and a specification and proof of correctness. They decide to collect into a single compact sublibrary just what is necessary to support those few formal objects. This is a basic FDL operation.

21	A person wants to develop some material "offline" at an independent site for a while. The procedure is to build a new temporary FDL (on their laptop, say) extracting the material of interest from a larger FDL. Later, after developing the material locally, that material can be posted back to the large FDL from which it came (or another one). This is possible because name collision is systematically avoided in FDLs by an abstract use of identifiers.

22	(a more speculative scenario, but with some basis in experience) A person wants to formalize a standard text or a chapter thereof not only to get the general benefits of formalization, but because as the original author proceeded, the proofs get progressively sketchier owing to copious allusions to the structure of earlier proofs, and the person wants to work those sketches out and save them. They are relieved to find that much of the basic generic math the text depends on is already in the FDL and can be immediately incorporated, and that using potent tools for manipulating proofs as data makes it easier than expected to realize those "proofs by allusion".