Theory

Definitions

 		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.

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:

A more complex model separates out a part of the document in this form:

A simple piece of documentation has no definitions or axioms (and so no theorems):

A basic piece of documentation has no theorems or definitions:

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, ???) Carnap 37, Rudolf Carnap, Testability and Meaning, Philosophy of Science, Vol 4.

Validity of Documentation

Consistency is established by the author showing something that satisfies the documentation.

Valid documentation is consistent, its variables are declared or defined, and all theorems are provable by assuming the axioms:

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 ]

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

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].

Example declarations and definitions

Note: these are not examples of good style. The identifiers are deliberately abstract. The declarations are in short hand.
1. 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>>

Example Nets

Note: these are not examples of good style. The identifiers are deliberately abstract. Realistic documentatin gives more clues to the system being described. They also omit some type definitions for sets like A, B, and C.

Simple Net

1. ABC::=Net{ a:A, b:B, c:C}.
   
2. (ABC)|-ABC=following,
   Net
   1. a::A.
   2. b::B.
   3. c::C.

   
   (End of Net)
   
   

   From the above definition the following notations are defined:
   

3. (ABC)|-$(ABC) = (a=>a, b=>b, c=>c), the standard tuple for ABC.

   
   

4. (ABC)|-for ABC, ... =for a:A, b:B, c:C ..., a special quantifier making it easy to say things about ABC's

   
   

5. (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.

Example Non_simple Net

1. ABC2::=following,
   Net
   1. a::A, b::B(a), c::=C(a,b), P(a,b,c).

   
   (End of Net)
   
   
   
2. (ABC2)|-declarations(ABC2)={(a,A), (b,B(a))},
   
3. (ABC2)|-variables(ABC2)={a,b},
   
4. (ABC2)|-definitions(ABC2)={(c,,C(a,b)},
   
5. (ABC2)|-assertions(ABC2)={P(a,b,c)},
   
6. (ABC2)|-constraint(ABC2)=P(a,b,C(a,b)).
   
7. (ABC2)|-ABC2=Net{ a:B, b:B(a), c:=C(a,b), P(a,b,c).}.

   Example Basic Net

   1. ABC3::=Net{ a,b,c:A, a=b+c.}.
      
   2. (ABC3)|-declarations(ABC2)={(a,A), (b,A), (c,A)},
      
   3. (ABC3)|-variables(ABC2)={a,b,c},
      
   4. (ABC3)|-definitions(ABC2)={},
      
   5. (ABC3)|-assertions(ABC2)={a=b+c},
      
   6. (ABC3)|-constraint(ABC2)=a=b+c.
      
   7. (ABC3)|-ABC2=following,
      Net
      a,b,c::A.
      
      1. |- (L): a=b+c.

      
      (End of Net)
      
      
      
   8. (ABC3)|-for all b, all c, 1 a(ABC3) = for all b:A, all c:A, 1 a:A(a=b+c).

      
      

   9. (ABC3)|-@{ABC3||for all b, some a, 2 c} =
   10. {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)}.

       
       

   11. (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 of a Piece of Documentation