Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/5861
 Title: Abstract Identifiers and Textual Reference Authors: Allen, Stuart Keywords: computer sciencetechnical report Issue Date: 15-Nov-2002 Publisher: Cornell University Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1885 Abstract: Here are three proposals concerning the structure and maintenance of formal, inter-referential, digitally stored texts: (1) include abstract atomic identifiers in texts, (2) identify these identifiers with references to text objects, and (3) keep among the texts records of computationally substantiated claims about those texts. We use formal'' in a narrow sense approximating computer-checkable. We are informed by informal symbolic practices used in mathematical text and program source text, which we hope to enhance and exploit explicitly; the basic management problem is how to alter texts {\em rather} {\em freely} without ruining the bases for claims depending upon them, which becomes an issue of accounting for various dependencies between texts. We are {\em not} here proposing the use of abstract structured text; nonetheless, experience using it in Nuprl4 has led us to appreciate the benefits of distinguishing abstract form from concrete presentation, and also has shown us the cognitive and practical {\em un}importance of just which identifiers occur in abstract structured texts when texts are mediated by a system that realizes concrete presentation. Abstract treatment of identifiers involves concrete realization during communications between text servers'' and their clients. The benefit of treating identifiers abstractly is a radical avoidance of name collision, even at runtime, and is important for claims about texts that are based upon program execution. The notion of text collections and equivalence of text collections modulo change of identifiers is made precise by the second proposal. The complete identification of abstract identifiers with reference values is discussed, addressing the issues of dangling pointers, the association of ordinary symbolic identifiers with meaningful defining texts, the flatness'' of the pointer space, and the perhaps counterintuitive collapse of two abstract name spaces into one. The notion of certification system'' is introduced as a formalization of generic computationally defined claims about texts, emphasizing the diversity of clients who may not agree on a common logic''. The notion of a certificate whose computational meaning, in the context of the texts it refers to, is completely specified (although perhaps non-deterministic), and the notion of a certificate further being deterministic, are introduced and elaborated with regard to their epistemic value. What it means to give certificate texts the force of factual records, and mechanisms to accomplish this, are discussed. Scenarios for practically exploiting identifier abstractness and fully deterministic certificates are considered, involving the combination of partially independently developed texts and the experimental modification of texts in a collection. The importance of implementing multiple certification systems is articulated. URI: http://hdl.handle.net/1813/5861 Appears in Collections: Computer Science Technical Reports

Files in This Item:

File SizeFormat
2002-1885.ps257.65 kBPostscriptView/Open