.Open Semantics of Documentation
. Introduction
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::=http://www/dick/maths/notn_13_Docn_Syntax.html,
for the syntax of documentation.

. Theory
There is a more than adequate theory of MATHS in the Algebraic Specifications
of 
.See [Wirsing90].

. Definitions
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:
.As_is 		piece.section["title"].sentence[3].item[2].lexeme[10]

There are also some convenient
.See http://www/dick/maths/notn_12_Expressions.html#Large 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,  \Sigma.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).
. Formal Semantics
The above section can be formalized in the following piece of formal documentation -
.See http://www/dick/maths/logic_7_Semantics.html
	|- symbol in @( Strings, Types, Values),
.See http://www/dick/maths/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.
.Close.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.

. Validity of Documentation
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
.See http://www/dick/maths/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.

. Types and Nets
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)`.

.See http://www/dick/maths/types.html

In theoretical terms the set of objects associated with a piece of
documents is an `initial model`
.See [Wirsing90].
.Open Example declarations and definitions
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`)}.
.Close Example declarations and definitions
.Open Example Nets
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.
.Open Simple Net
ABC::=Net{ a:A, b:B, c:C}.
(ABC)|-ABC=following,
.Net
	a::A.
	b::B.
	c::C.
.Close.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...

.Close Simple Net

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.
. Example Non_simple Net
ABC2::=following,
.Net
a::A, b::B(a), c::=C(a,b), P(a,b,c).
.Close.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)}.

.Open Example Basic Net
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.
.Close.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.`.

.Close Example Basic Net
.Close Example Nets

. Other Attributes of a Piece of Documentation
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
		Origination_date::Times.
		Release_date::Times.
		Until_date::Times.
		|-Origination_date <= Release_date < Until_date.
		Revision_cycle::Period_of_time. ... 
.Close.Net
	|-Plan.Release_date=Copyright.Dates,

Documents can be cited...
	References::Times<>->@$ Net{who: people, why: char, where:names_of_documents},
	Citation_count::Times<>->Natural::=Card o References.

Documents can be reviewed
	Review_dates::Times<>->$ following
.Net
		who:: @people, 
		what::@defects,
		action::{accept, reject, ...}, 
		comments::#char
.Close.Net Review_dates.

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)
.Close.Net
	Life::=sequence following,
.List
		originate
		release 
		#(review | change | cited | citing_document_deleted ) 
		mark_for_deletion
		#citations_exist
		no_citations
		purge
.Close.List

.Close.Let
.Or
.Let
 A document is fixed but other documents are derived from it.  
.Source Ted Nelson
	Parent::Documents.
	Life::=following,
.Box
		originate
		release 
		#(review | cited | citing_document_deleted | cited_documented_has_new_version) 
		originate_new_version
		#citations_exist
		no_citations
		purge
.Close.Box
	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

.See http://www/dick/maths/notn_5_Form.html

.Close.Net OTHER_ATTRIBUTES

.Road_works_ahead

.  Translation into a Z Schema
 For In:Net, Net_to_Z(In) ::=with{signature, axioms:Sets} following
.List
(
	(signature, axioms) := ({},{});
	do
.List
	(with{piece:piece_of_documentations}
.List
	 (
		piece:?In;
.Set
		( 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)
		)			
.Close.Set
	)
.Close.List
	); 
.Close.List
	end(In);
	output_Z_schema(signature, axioms);
).
.Close.List

.Close Semantics of Documentation