Abstract Identifiers and Textual Reference

Other Titles


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.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record