[Skip Navigation] [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >> notn_2_Structure
[Contents] || [Source] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Apr 12 08:13:47 PDT 2005

Contents


    Structure of Documentation

      Introduction

      At the lowest level MATHS associates a mathematical object with just about any ASCII (.txt) file. This can be refered to and used in formaulae in other documents.

      But the main use of MATHS is to assemble notaions, definitions, and assumptions into a narative about some domain of interest. Here the MATHS syntax distinguishes (and labels) well-formed formulae, declarations, definitions and comments. These are grouped into paragraphs separated by blank lines and directives. A sequence of paragraphs can be grouped into a section and named by a section header directive. So the document is split into sections that are made up of paragraphs. Sections can be further grouped into "supersections". These supersections can themselves be grouped and named. Ultimately the top-most sections (or paragraphs) are given a title and so can name the whole document. However this can also be supplied by an operating system.

      Within a section, paragraphs are numbered. Sections are identified (in a document) by the header. So paragraph 7 in section A can be named by

       document["A"].paragraph(1)
      for example.

      On the web section names are marked up as anchors so that other web pages can refer to them using standard URLs:

       		http://www.csci.csusb.edu/dick/maths/notn_2_Structure.html#Intorduction
      However, separate paragraphs are not normally given anchors. Indeed these tend t be highly unstable.

      On the other hand all gloabblay defined terms and declared variables are given an anchor and others are invite to linke to them.

      There are a number of specialized formats for sets, lists, tables, proofs(Let), boxes, and nets(of variables and assertions). These also have a formal meaning as sets, maps, and relations.

      A subsection is bracketted by Open and Close directives. There exist more powerful versions of Open: Box and Net open up a piece of documentation with local declarations, definitions, and formula. The local statements are not part of the outer document. Instead they are named and used indireclty via that name. The Let directive is used specifically to open up an exploration of the consequences ofone or more assumptions. It is used as a way to prove formula. However the valid consequences of such an assumption never include the assumptions.

      A directive can give a name to a piece of documentation and this is a way to refer to the next part. If a name is missing then the serial number can be used instead. The next part is the sequence of following paragraphs or subsections.

      The open/close directives indicate the start and end of a new section of the document. It includes all nested "blocks". All parts are refered by name or number of the directive above it.

      Example 1

       		. A
       		. B
       		.Open C
       		. D
       		.Close C
       		. E

      Above we have sections A, B, C and E. C has a part called C.D.

      Outlines

      Without content and format we have an outline.

      Philosophy

      Different formats can be associated with each level by an organization to give a particular look and feel by a browser or print program. It is part of the MATHS philosophy that the aesthetics of a document should be determined by the viewer, but the meaning by the author. This is not disimilar to the SGML and HTML languages. It is utterly oposed to the \TeX attitude that the author determines the detailed form of the document and the viewer uses the appearance to determine the meaning:

      Semantics

        Properties of a Piece of a Document

        A piece of documentation (wff, definition, paragraph, section,..., document) has the following properties or attributes that are important enough to be encoded:
      1. PIECE::=
        Net{
        1. name::#non(eoln). start_date, release_date, until_date::O(Times).
        2. marked_for_deletion::@. start,end::Positions_in_file.
        3. file::File_name.
        4. node::Node_identifier.
        5. is_part_of::O(PIECE),
        6. has_parts::@PIECE.
        7. is_local_environment::@.
        8. input_form::Input_forms.
        9. purpose::Purposes.
        10. output_form::Output_Forms.
        11. road_sign::@Road_sign.
        12. ...
        13. content::#char.

        }=::PIECE.

        Validity of a Set of Pieces of a Document

      2. VALID_SET_OF_PIECES::=
        Net{
        1. pieces::Finite_set(PIECE).
        2. |-For all p,q:pieces (q in has_parts(p) iff p = is_part_of(q) ).
        3. |-(node,file,start,end) is_id pieces.
        4. ...

        }=::VALID_SET_OF_PIECES.

        Tags and Anchors

        Tags, anchor, or links are used to indicate a particular place in a file that can be reffered to by another file. Notice that this connects one place in a file to other documents without necessarily changing the meaning or content of either document. A piece refers to a section of a larger document.
      3. TAG::=
        Net{
        1. name::#non(eoln).
        2. marked_for_deletion::@.
        3. position::Positions_in_file.
        4. file::File_name.
        5. node::Node_identifier.
        6. is_in::PIECE,

        }=::TAG.

      4. VALID_SET_OF_TAGS::=
        Net{
        1. tags::Finite_set(TAG).
        2. |-(node,file,position) is_id tags.
        3. |-(name) is_id tags.
        4. ...

        }=::VALID_SET_OF_TAGS.

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

      HTML implementation

        URL

        In HTML TAGs become named anchors. The HTML implementation maps each tag into a URL:
      1. file://node/file#Positions_in_file
      2. http://node/file.html#Positions_in_file The position in the file is always the start of the section or paragraph.

        Tools

        Current tools use HTML as a display prototype and the World Wide web as a laboratory for experiemtns with MATHS. The key tool is a C program and a shell script that map a subset of MATHS into HTML. All the current documentation and samples has been used to help co-evolve this tool and the MATHS language.

      Syntax

        MATHS allows, but does not define, directives using the same 'dot' form as the roff and WordStar families of text preparation systems.

      1. documentation::syntax=#(piece | blank_line ).
      2. piece::= #directive_line (paragraph | section | tag_line ) .
      3. directive_line::= "." directives eoln,

        .Note By default there should be an outline or list of contents at the start of each file of MATHS documentation and an index of definitions at the end. The contents list should list the headers - ideally indicating the structure with indentation. This has been shown to be feasible in the current 'mth2html' tool.

      4. section::=simple_section | open_close_section | local_section.
      5. simple_section::= header_line #(paragraph | blank_line | insertion).

      6. header_line::="." white_space name #whitespace eoln,
      7. header::syntax->syntax="." whitespace (_) eoln.
      8. |-header_line= |[H:name](header(H)).

      9. open_close_section::= |[H:name](open(H) #piece close(H))
      10. open::syntax->syntax=".Open" SP (_) eoln,
      11. close::syntax=".Close" O(SP (_)) eoln.

      12. local_section::= |[T:{".Let", ".Net", ".Box", ".List", ".Set", ...}]( T eoln #piece ".Close" T eoln).

        Blank-lines separate paragraphs in a text.

      13. paragraph::syntax=#(line~blank_line) & #(comment | line_break_line | declaration | definition | wff | ... ).

        A line break must be preserved in any marked up versions. It is also used to indicate some formal statements.

      14. line_break_line::=line & ( whitespace #char).

      15. directives::=directive more_formats,
      16. more_formats::=#("." format),
      17. blank_line::=#whitespace eoln,
      18. directive::=identifier,
      19. name::=#non(eoln),
      20. tag_name::@name, -- probably only #non(white_space).

      21. directive_information::=(relative_level_number | ) ( name | sequence_number ) position_in_text #attribute.

        Formats are defined elsewhere. However they are always logical formats describing the desired effects with out specifying how they might be obtained. [ notn_5_Form.html ]

        .Road_Works_ahead The folowing are some Partly-Baked-Ideas....

        Lists

          Introduction to lists

          Use tables... Lists are used both formally and informally.

          Example of a formal list

        1. octal::=following,
          StringDigit
          "0"0
          "1"1
          "2"2
          "3"3
          "4"4
          "5"5
          "6"6
          "7"7

        2. |-octal = "0"+>0 | "1"+>1 | ... | "7"+>7.

        . . . . . . . . . ( end of section Lists) <<Contents | End>>

      . . . . . . . . . ( end of section Syntax) <<Contents | End>>

    . . . . . . . . . ( end of section Structure 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%20Structure in logic_2_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints, and give them a name. 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.

End