[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / notn_14_Docn_Semantics
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Wed Nov 9 10:40:34 PST 2011


    Semantics of Documentation


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


    1. 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:


      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.

    2. For s: documentation | name_of_documentation,
    3. type(s)::=type of object in s
    4. terms(s)::=terms defined in s,
    5. expressions(s)::=expressions defining terms in s, definitions(s):@(terms(s), types(s), expressions(s)) ::= definitions in s,
    6. declarations(s)::@(variables(s), types(s))= declared symbols and defined terms in s,
    7. types(s)::=types used in s,
    8. variables(s)::=symbols bound in declarations in s,
    9. assumed(s)::=axioms assumed to be true,
    10. defined(s)::=equalities resulting from definitions,
    11. axioms(s)::=assumed(s) | defined(s),
    12. theorems(s)::=formula that are true given the axioms of s,
    13. 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:

    14. complete(s)::=[ signature(s) ] ( constraint(s) ). The signature(s) is defined formally below and
    15. constraint(s)::=for some declare_defined(s) ( and (assertions(s)) ) where
    16. 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:

    17. 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:
    18. |- (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):

    19. 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:

    20. 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,
    21. |-basic(s) iff given(s)=complete(s).

      Formal Semantics

      The above section can be formalized in the following piece of formal documentation - [ logic_7_Semantics.html ]
    22. |-symbol in @( Strings, Types, Values), [ types.html ]
    23. |-Types in @Net{ description, other_descriptions, objects, expressions, variables,...}.
    24. DOC::=following.
        Types, Terms, Expressions, Variables :: Types.
      1. LPC(Propositions).
      2. Propositions=>>Expressions.
      3. type::Types=type of object satisfying the document
      4. terms::Term=terms defined,
      5. expressions::Expression=expressions defining terms in s,
      6. definitions::@(terms, types, expressions)=term(1st) of type (2nd) equals (3rd),
      7. declarations::@(variables, types)=variable (1st) has type(2nd),
      8. types::@Types=types used,
      9. variables::@Variables=symbols bound in declaration,
      10. assumed(s)::=axioms assumed to be true,
      11. defined(s)::= {equal(t.T, e) || (t,T,e):definitions },
      12. equal::Expression><Expression->Propositions=(1st) = (2nd).

      13. axioms::@Propositions=assumed(s) | defined(s),
      14. theorems::@Propositions=proved from zero or more axioms.
      15. assertions::@Propositions=remove_local_terms(axioms | theorems).

      16. declare_defined:= List{ t:T || (t,T,e): definitions}.
      17. constraint::=for some declare_defined ( and(assertions) )
      18. signature::= List{ t:T || (t,T,e) in definitions or (t,T) in declarations}.
      19. given_signature::=List{ t:T || (t,T) in declarations}.
      20. goal_signature::=List{ t:T || (t,T,e) in definitions}

      21. complete::=[signature](constraint).
      22. given::=[given_signature]( and(remove_local_terms(assumed)) ).
      23. GIGO::= For all given, some complete

      24. simple::@=no axioms.



      (End of Net)

      Note. this does not cover conditional definitions of form

    25. For x:T, if C(x) then f(x) = e. or even
    26. 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:
    27. 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:
    28. 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:
    29. names: name_of_a_piece_of_documentation >-- piece_of_documentation. Thus documentation names should not be overloaded and all documentation has to be named.

    30. For s:=names(n),
    31. type(n)::=type(s),
    32. declarations(n)::=declarations(s),
    33. definitions(n)::=definitions(s),
    34. axioms(n)::=axioms(s),
    35. theorems(n)::=theorems(s).
    36. |-For s:=names(n),
    37. types(n)=types(s) and variables(n)=variables(s)
    38. and terms(n)=terms(s) and expressions(n)=expressions(s)
    39. and freevars(n)=freevars(s).

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

    40. For s: piece_of_documentation,
    41. 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:

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

    43. 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).

      [ 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,
      2. types(s)= {T},
      3. variables(s)= {x,y},
      4. declarations(s)= {(x,T), (y,T).

        For s:=t::T=e,

      5. types(s)= {T},
      6. terms(s)= {t},
      7. expressions(s)= {e},
      8. 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 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.

        Simple Net

        1. ABC::=Net{ a:A, b:B, c:C}.
        2. (ABC)|-ABC=following,
          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.

        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

      1. ABC2::=following,
        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).}.
      8. (ABC2)|-type(ABC2)=$ Net{ a:B, b:B(a)}.

        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)|-type(ABC2)=$ Net{ a,b,c:A }.
        8. (ABC3)|-ABC2=following,
          1. |- (L): a=b+c.

          (End of Net)

        9. (ABC3)|-for all b, all c, 1 a(ABC3) = for all b:A, all c:A, 1 a:A(a=b+c).

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

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

    44. OTHER_ATTRIBUTES::=following
        Other attributes of a piece of documentation include:
      1. Copyright::Times,
      2. Authors::@people,
      3. Owners::Times->@people::=Those who can change it at this time.
      4. Plan::$ following
        1. Origination_date::Times.
        2. Release_date::Times.
        3. Until_date::Times.
        4. |-Origination_date <= Release_date < Until_date.
        5. Revision_cycle::Period_of_time. ...

        (End of Net)

      5. |-Plan.Release_date=Copyright.Dates,

        Documents can be cited...

      6. References::Times<>->@$ Net{who: people, why: char, where:names_of_documents},
      7. Citation_count::Times<>->Nat::=Card o References.

        Documents can be reviewed

      8. Review_dates::Times<>->$ following
        1. who::@people,
        2. what::@defects,
        3. action::{accept, reject, ...},
        4. comments::#char

        (End of Net Review_dates.)

        Someone is responsible for each document at any given time:

      9. Ownership::$ Net{time:Times, owner:people}.


        1. A document evolves over time.
        2. Changes::Times<>->Change.
        3. change::=$ following,
            who: @people, what:: @defects, why:text,
          1. request_from::@person,
          2. delta::@(documentation, documentation)

          (End of Net)

        4. Life::=sequence following,
          1. originate
          2. release
          3. #(review | change | cited | citing_document_deleted )
          4. mark_for_deletion
          5. #citations_exist
          6. no_citations
          7. purge

        (Close Let )
        1. A document is fixed but other documents are derived from it.

          Source: Ted Nelson

        2. Parent::Documents.
        3. Life::=following,
          1. originate
          2. release
          3. #(review | cited | citing_document_deleted | cited_documented_has_new_version)
          4. originate_new_version
          5. #citations_exist
          6. no_citations
          7. purge

        4. During the citations_exist phase new citations and reviews are linked to the child version.
        5. Child::O(Documents).

        6. Link::@(Documents,Documents).
        7. Link.life::=(citation_made citation_purged).

        (Close Let )

        [ notn_5_Form.html ]

      (End of Net OTHER_ATTRIBUTES)


      Translation into a Z Schema

    45. For In:Net, Net_to_Z(In)::=with{signature, axioms:Sets} following
      1. (signature, axioms) := ({},{});
      2. do
        1. (with{piece:piece_of_documentations}
          1. (
          2. 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)
            • )
          3. )

        2. );

      3. end(In);
      4. output_Z_schema(signature, axioms); ).

    . . . . . . . . . ( end of section Semantics of Documentation) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.