A piece of documentation does not come with a guarantee that
it refers to anything in the real world, or inside a computer!
The warrantee has to come from some corporate entity or person.
For this reason I like Francis Bacon's description:
"so many stage plays, representing worlds of their own creation after an unreal & scenic fashion. "
See
- SYNTAX::= See http://cse.csusb.edu/dick/maths/notn_13_Docn_Syntax.html,
for the syntax of documentation.
There is a more than adequate theory of MATHS in the Algebraic Specifications
of
[Wirsing90].
First, we can ignore sections in the SYNTAX
which merely provide an organization
for human readers. They can be referred to in other documents
but then they become another piece of documentation. Similarly for the comments
that make a piece of documentation user friendly.
.Road_works_ahead
A typical comment
defines a structured object and its components can be refered to in
a syntax (inspired by HyperTalk) like this with subscripts:
piece.section["title"].sentence[3].item[2].lexeme[10]
There are also some convenient
[ Large Expressions in notn_12_Expressions ]
that define sets, lists, and tables of data. These are formulae
that encode objects and so appear as expressions below.
I assume that all comments are removed and some abbreviations are expanded
so that we only have to define the meaning of a collection of simple
declarations ( variable::type ), simple definitions ( `variable::type=
expressions` ), and well-formed formulae ( axioms and theorems). Further
multiple declarations have also been resolved so that for each symbol and
type there is no more than a single declaration and/or definition - hence
we can model the documentation as a collection of sets of declarations.
definitions, and formula.
- For s: documentation | name_of_documentation,
- type(s)::=type of object in s
- terms(s)::=terms defined in s,
- expressions(s)::=expressions defining terms in s,
definitions(s):@(terms(s), types(s), expressions(s)) ::= definitions in s,
- declarations(s)::@(variables(s), types(s))= declared symbols and defined terms in s,
- types(s)::=types used in s,
- variables(s)::=symbols bound in declarations in s,
- assumed(s)::=axioms assumed to be true,
- defined(s)::=equalities resulting from definitions,
- axioms(s)::=assumed(s) | defined(s),
- theorems(s)::=formula that are true given the axioms of s,
- assertions(s)::=(axioms(s) | theorems(s)).
Documentation defines the classes of objects that fit. Documentation
defines the structure or type of the objects - the components must be the
variables of the documentation (the signature of Z, Σ.Algebras,
S-Algebras). Each object must also fit the wffs asserted in the
documentation - this defines the class of the documentation. The added
constraint is the conjunction of (1) the axioms and (2) defined terms:
So, the simplest theory of a piece of documentation is that documentation s is reducible to a schema form like this:
- complete(s)::=[ signature(s) ] ( constraint(s) ).
The signature(s) is defined formally below and
- constraint(s)::=for some declare_defined(s) ( and (assertions(s)) ) where
- declare_defined(s):= List{ t:T || (t,T,e):definitions(s) }.
A more complex model separates out a part of the document in this form:
- given(s)::= [ variables(s) ] (and( assumed(s)) ).
Then the given(s) describes the circumstances in which the document can used, and complete(s) describes what must follow. In logical terms suppose we have the given: [x](G(x)) and the complete: [x, y](C(x,y)) then we have this meta-theorem and derivation rule:
- |- (gigo): for all x, if G(x) then for some y (C(x, y)).
A simple piece of documentation has no definitions or axioms (and so no theorems):
- simple(s)::@=no axioms(s).
Notice that any piece of documentation has a basic document embedded in it.
A basic piece of documentation has no theorems or definitions:
- basic(s)::@=no theorems(s) and no definitions(s).
A basic piece of documentation has the property that an axiom can be removed from it with out invalidating it. In some pieces of documentation we can replace their definitions by axioms and remove their theorems and so get an equivalent but basic piece of documentation. Clearly,
- |-basic(s) iff given(s)=complete(s).
The above section can be formalized in the following piece of formal documentation -
[ logic_7_Semantics.html ]
- |-symbol in @( Strings, Types, Values),
[ types.html ]
- |-Types in @Net{ description, other_descriptions, objects, expressions, variables,...}.
- DOC::=following.
Net
Types, Terms, Expressions, Variables :: Types.
- LPC(Propositions).
- Propositions=>>Expressions.
- type::Types=type of object satisfying the document
- terms::Term=terms defined,
- expressions::Expression=expressions defining terms in s,
- definitions::@(terms, types, expressions)=term(1st) of type (2nd) equals (3rd),
- declarations::@(variables, types)=variable (1st) has type(2nd),
- types::@Types=types used,
- variables::@Variables=symbols bound in declaration,
- assumed(s)::=axioms assumed to be true,
- defined(s)::= {equal(t.T, e) || (t,T,e):definitions },
- equal::Expression><Expression->Propositions=(1st) = (2nd).
- axioms::@Propositions=assumed(s) | defined(s),
- theorems::@Propositions=proved from zero or more axioms.
- assertions::@Propositions=remove_local_terms(axioms | theorems).
- declare_defined:= List{ t:T || (t,T,e): definitions}.
- constraint::=for some declare_defined ( and(assertions) )
- signature::= List{ t:T || (t,T,e) in definitions or (t,T) in declarations}.
- given_signature::=List{ t:T || (t,T) in declarations}.
- goal_signature::=List{ t:T || (t,T,e) in definitions}
- complete::=[signature](constraint).
- given::=[given_signature]( and(remove_local_terms(assumed)) ).
- GIGO::= For all given, some complete
- simple::@=no axioms.
See
- |-OTHER_ATTRIBUTES.
(End of Net)
Note. this does not cover conditional definitions of form
- For x:T, if C(x) then f(x) = e.
or even
- For x:T, if C1(x) then f(x) = e1,if C2(x) then f(x) = e2,....
Clearly such definitions introduce a declaration:
f:: T<>->Type(e)
The correct axiom is:
- For all x:T, if C(x) then f(x)=e
which is (of course) the source for the syntax of conditional documentation.
Carnap shows that it would be incorrect to add an axiom like this:
- For all x:T, f(x) = if(C(x), e, ???)
Source: Carnap 37, Rudolf Carnap, Testability and Meaning, Philosophy of Science, Vol 4.
To be valid there must be an unambiguous relationship between names and
documentation:
- names: name_of_a_piece_of_documentation >-- piece_of_documentation.
Thus documentation names should not be overloaded and all documentation has
to be named.
- For s:=names(n),
- type(n)::=type(s),
- declarations(n)::=declarations(s),
- definitions(n)::=definitions(s),
- axioms(n)::=axioms(s),
- theorems(n)::=theorems(s).
- |-For s:=names(n),
- types(n)=types(s) and variables(n)=variables(s)
- and terms(n)=terms(s) and expressions(n)=expressions(s)
- and freevars(n)=freevars(s).
Consistency is established by the author showing something that satisfies
the documentation.
- For s: piece_of_documentation,
- consistent(s)::=for some X:Universe (X satisfies constraints(s)),
Valid documentation is consistent, its variables are declared or defined,
and all theorems are provable by assuming the axioms:
- valid(s)::=(consistent(s) and (freevars(s) ==> terms(s) | variables(s)) and for all t:theorems(s)(if &(axioms(s)) then t ) ).
Church's Theorem means that proofs can not be automatically constructed.
However if a putative proof has been written then
it can be verified automatically by comparing with
the rules of logic
[ logic_2_Proofs.html ]
- For s:valid, v:variables(s), type(v,s)::= the[ t:Types]( (v,T) in declarations(s)).
Notice that adding a definition or declaration to a consistent valid pece
of documentation generates another valid piece of documentation - when ever
the definition uses terms that are already defined and the defined term or
declared variable is not used in the original documentation.
When a piece of documentation is enclosed it becomes a "net" - a network of
constrained variables. Associated with such a net are sets of object that
satisfy them:
For declarations and definitions D,
$ Net{D}::=Class of objects described by D,
$ Net{D. W(v)}::= set v:$ Net{D} satisfying W(v),
$ Net{D. W(v',v)}::=relation v,v':$ Net{D} satisfying W(v',v).
[ types.html ]
In theoretical terms the set of objects associated with a piece of
documents is an initial model
[Wirsing90].
Note: these are not examples of good style. The identifiers
are deliberately abstract. The declarations are in short hand.
- For s:=x, y::T,
- types(s)= {T},
- variables(s)= {x,y},
- declarations(s)= {(x,T), (y,T).
For s:=t::T=e,
- types(s)= {T},
- terms(s)= {t},
- expressions(s)= {e},
- definitions(s)= {(t,T,e)}.
. . . . . . . . . ( end of section Example declarations and definitions) <<Contents | End>>
Note: these are not examples of good style. The identifiers
are deliberately abstract. Realistic documentation gives more clues to the
system being described. They also omit some type definitions for sets like
A, B, and C. Finally, they don't provide any example objects that can be proven
to fit the nets.
- ABC::=Net{ a:A, b:B, c:C}.
- (ABC)|-ABC=following,
Net
- a::A.
- b::B.
- c::C.
(End of Net)
From the above definition the following notations are defined:
- (ABC)|-$(ABC) = (a=>a, b=>b, c=>c), the standard tuple for ABC.
- (ABC)|-for ABC, ... =for a:A, b:B, c:C ..., a special quantifier
making it easy to say things about ABC's
- (ABC)|-for x:ABC,... = for x.a:A, x.b:B, x.c:C,..., a way
to introduce a non-standard tuple...
. . . . . . . . . ( end of section Simple Net) <<Contents | End>>
Simple nets just define an unconstrained list of variables... very
like a Cartesian product or C struct. Non-simple nets introduce
variables and state assumptions that constrain them.
The type of a net is the universal set of object that fit the net.
It is the set of object fitting the simple net with the same signature.
- ABC2::=following,
Net
- a::A, b::B(a), c::=C(a,b), P(a,b,c).
(End of Net)
- (ABC2)|-declarations(ABC2)={(a,A), (b,B(a))},
- (ABC2)|-variables(ABC2)={a,b},
- (ABC2)|-definitions(ABC2)={(c,,C(a,b)},
- (ABC2)|-assertions(ABC2)={P(a,b,c)},
- (ABC2)|-constraint(ABC2)=P(a,b,C(a,b)).
- (ABC2)|-ABC2=Net{ a:B, b:B(a), c:=C(a,b), P(a,b,c).}.
- (ABC2)|-type(ABC2)=$ Net{ a:B, b:B(a)}.
- ABC3::=Net{ a,b,c:A, a=b+c.}.
- (ABC3)|-declarations(ABC2)={(a,A), (b,A), (c,A)},
- (ABC3)|-variables(ABC2)={a,b,c},
- (ABC3)|-definitions(ABC2)={},
- (ABC3)|-assertions(ABC2)={a=b+c},
- (ABC3)|-constraint(ABC2)=a=b+c.
- (ABC3)|-type(ABC2)=$ Net{ a,b,c:A }.
- (ABC3)|-ABC2=following,
Net
a,b,c::A.
- |- (L): a=b+c.
(End of Net)
- (ABC3)|-for all b, all c, 1 a(ABC3) = for all b:A, all c:A, 1 a:A(a=b+c).
- (ABC3)|-@{ABC3||for all b, some a, 2 c} =
- {X:@ABC3||for all b:A, some a:A, 2 c:A( (a=>a,b=>b,c=>c) in X and
a.a=b.b+c.c)}.
- (ABC3)|-ABC3 without L equivalent to standard with a,b,c:A..
. . . . . . . . . ( end of section Example Basic Net) <<Contents | End>>
. . . . . . . . . ( end of section Example Nets) <<Contents | End>>
- OTHER_ATTRIBUTES::=following
Net
Other attributes of a piece of documentation include:
- Copyright::Times,
- Authors::@people,
- Owners::Times->@people::=Those who can change it at this time.
- Plan::$ following
Net
- |-Plan.Release_date=Copyright.Dates,
Documents can be cited...
- References::Times<>->@$ Net{who: people, why: char, where:names_of_documents},
- Citation_count::Times<>->Nat::=Card o References.
Documents can be reviewed
- Review_dates::Times<>->$ following
Net
Someone is responsible for each document at any given time:
- Ownership::$ Net{time:Times, owner:people}.
.Fork_in_Road.Road_work_ahead
Let
- A document evolves over time.
- Changes::Times<>->Change.
- change::=$ following,
Net
who: @people, what:: @defects, why:text,
- request_from::@person,
- delta::@(documentation, documentation)
(End of Net)
- Life::=sequence following,
- originate
- release
- #(review | change | cited | citing_document_deleted )
- mark_for_deletion
- #citations_exist
- no_citations
- purge
(Close Let )
.Or
Let
- A document is fixed but other documents are derived from it.
Source: Ted Nelson
- Parent::Documents.
- Life::=following,
- originate
- release
- #(review | cited | citing_document_deleted | cited_documented_has_new_version)
- originate_new_version
- #citations_exist
- no_citations
- purge
- During the citations_exist phase new citations and reviews are linked to the child version.
- Child::O(Documents).
- Link::@(Documents,Documents).
- Link.life::=(citation_made citation_purged).
(Close Let )
[ notn_5_Form.html ]
(End of Net
OTHER_ATTRIBUTES)
.Road_works_ahead
- For In:Net, Net_to_Z(In)::=with{signature, axioms:Sets} following
(
- (signature, axioms) := ({},{});
- do
- (with{piece:piece_of_documentations}
- (
- piece:?In;
- ( piece in declaration; signature:|declaration_to_Z(piece)
- | piece in wff; axioms:|wff_to_Z(piece)
- | piece in definition; signature:|definition_to_Z_declaration(piece); axioms:|definition_to_Z_equality(piece)
- | piece in (theorem | comment)
- )
- )
- );
- end(In);
- output_Z_schema(signature, axioms);
).