[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Monograph] / 03
[Index] || [Contents] || [Source] || [ Search monograph] || [Notation] || [Copyright] Mon Jul 26 12:24:36 PDT 2010

Contents


    Chapter 3 Grammars

      3.1 Introduction

        3.1.1 Outline

        Sections 2 & 3 introduce a theory that accounts for the applicability of data directed program design.

        Sections 4, 5, 6 and 7 discuss new ways to define languages in preparation for defining a complete documentation system in chapter 5.

        3.1.2 Summary

        Well known algorithms and automata can parse languages defined by context free grammars but the context free grammars cannot define even the simplest programming languages. Intersections and complements give more power but still have simple parsers. This allows designs that are clearly based on the user's ideas.

        However some extra techniques are still needed to describe semantics. MATHS can define a term to be any expression. Section 4.5 gives rules to avoid unrecognizable or empty languages.

      . . . . . . . . . ( end of section 3.1 Introduction) <<Contents | End>>

      3.2 On the Power of Data Directed Methods

        3.2.1 Introduction

        The theory of computer languages lags behind the practice. In theory one writes a single grammar to define the language, but in practice a compiler has two or more cooperating parts. Multiple passes and/or concurrency are clearly convenient - but why? The theory does not explain the practice. The gap is closing: the Turing language was defined as the intersection of lexical, syntactic and semantic requirements [Holt & Cordy 88]. Section 2.3 shows that a grammar with intersections in it is handled by a network of parsers.

        Another example is Jackson's program design method (JSP). JSP structure diagrams are context free. Yet JSP designs can recognize {a^n ! b^n ! c^n || n: 0..}[Botting 87b]. This JSP designs is a TDPL translator [ Aho and Ullman 72, chapter 6]. All TDPL parsers have corresponding JSP programs, but some apparent JSP designs are not TDPL parsers. Since any Turing Machine can be simulated by an iterated selection a crafty programmer can simulate any program by a simple structure plus complex flags and logic. But JSP requires that (1) the structure contains the canonical dictionary of the problem, (2) the operations are derived from the problem, (3) each operation has a set of clearly defined places where it should (and should not) be placed in the structure giving the `schematic logic`, and (4) all conditions are derived from the schematic logic[Jackson 75]. If the operations only map pieces of input into pieces of output then a JSP program is a TDPL transducer.

        Many computer professionals are unaware that JSP designs require concurrent communicating processes [Solon 78]. This chapter shows that a network of strict JSP programs can handle more than TDPL languages.

        Similar networks of simpler parsers show their power every time you read a book. Gelernter has argued that massive networks of simple parsers can be created by users to notice patterns in streams of data and summarize them for visual display (the so-called Trellis). He notes that these are very similar to the structures used in living brains for the same task - a fact known to cyberneticians and cognitive psychologists for several decades [ Ross Ashby, Lindsay & Norman, Beer]. The structures analyzed here are an abstract and simplified version of such structures as well as a more powerful language description tool.

        3.2.2 Context Free Grammars

          The definition of a grammar uses an alphabet or vocabulary of elementary symbols. Some are terminal symbols and some non-terminal symbols. A grammar has a set of definitions. Usually one non-terminal symbol is selected to represent the language. A grammar can be seen as a way to generate all possible strings in a language, or as rules for accepting or parsing a given string. Here is an informal introduction, followed by the MATHS formalization.

          3.2.2.1 Introduction

          In a grammar G, each terminal and non-terminal represents a set of symbols in an alphabet or vocabulary V. V is split into the terminals or elements T and the defined terms or non-terminals N. Each term n:N is related to a formula by a definition. We write the formula for non-terminal n as D [n] (m1, m2, ...) where the m1, m2, ... represent the elements of N. Example: if N={"L","P","X"} then definition "L::= a L b P | X " means that
        1. D ["L"] ("L","P","X") = " a L b P | X ". In MATHS strings are generated by starting with an empty string ("") and concatenating symbols with concatenation operator (!) . Union(|), intersection (&), complementation (~), concatenation(), and iteration (#) operate on sets of strings( @#V ) [ Chapters 2 and 5 and Appendices 1 and 3].

          A set of definitions associates a meaning (M(n)) with each defined term (n) by the rule that each M(n) is the smallest set of strings such that all the definitions are true simultaneously when the nonterminals are replaced by their meanings:

        2. For all n:N, M(n) = D [n] (M(m1), M(m2), M(m3), ...), This definition gives a test for whether a string lies in M(L), but does not tell us how to find the Ms. Neither does it prove that they exist. It does not mean that they are unique. Finally the term 'smallest' has not been defined.

          For a wide class of grammars, we can get as complete a listing of the Ms as we like by iterating D:

          This Gauss-Siedel like process repeats for ever and so is not a true algorithm. The successive values normally seem to tend toward a limit. In the theory of languages this means we have to look at longer and longer strings to find one that has not been generated by the iteration. More formally, given a preselected length then if we select to iterate long enough, then the iterates will match the limit up to the preselected length [Bibliography and history in section 7.2, references under TOPOLOGY in chapter 9]. A similar topology applies to any class of constructable objects[See appendix 1 Sample.GENESYS].

          3.2.2.2 MATHS model of a Grammar

        3. CF_GRAMMAR::=
          Net{
          1. V::=alphabet::Finite_Set.
          2. T::=terminals::@V.
          3. N::=non_terminals::@V.

          4. Uses STRINGS. [Appendix 1]

            Syntax.

          5. grammar::@#character.
          6. grammar::= #( definition | comment),
          7. comment::=(#character)~definition,
          8. EBNF_definer::= ":" ":" "=".
          9. definition::=non_terminals EBNF_definer regular_expression,
          10. regular_expression::=sequence ("|" regular_expression | ),
          11. sequence::= #phase,
          12. phase::=("#" |)element,
          13. element::= V | "(" regular_expression ")".

            Semantics A grammar defines a set of productions that together generate a language for each non_terminal. Each production also implies a way of parsing a string. The meaning or denotation maps valid grammars into a set of general productions, and then defining the language generated by the productions. m is this map:

          14. General_Productions::=@(N><@#V).
          15. m::grammar -> General_Productions,
          16. |-grammar= (definition grammar | comment grammar | ),
          17. For d:definition, g:grammar, m(d! g)::={m(d)} | m(g),
          18. For c:comment, g:grammar, m(c! g)::=m(g).
          19. m(())={}.

          20. m::definition -> (N><@#V),
          21. |-definition=N EBNF_definer regular_expression,
          22. For n:N, r:regular_expression, m(n EBNF_definer r)::=(n, m(r)).

          23. m::regular_expression -> @#V
          24. For s:sequence, r:regular_expression, m(s "|" r)::=m(s) | m(r),
          25. For s:sequence, e:element, m(e s)::=m(e) ! m(s),
          26. For e: element, m("#"e)::=#m(e),
          27. m( )=(),
          28. For e:V, m(e)::= e,
          29. For r:regular_expression, m("(" r ")")::=(m(r)).

            We now define the meaning of the set of productions constructed from a particular type of grammar:


          30. |-General_Productions in @(N, @#N).

          31. complete:: @=(pre(m(G))=N).
          32. -- A grammar is complete only if every non-terminal is defined.

          33. normal::@=( m(G) in N -> @#V).

          34. P::General_Productions::=m(G).

            Given P the generation process uses v::N -> @#V. For each non_terminal n in N there is a set of strings v(n) in @#V. Generation consists of replacing each non_terminal n by its current value v(n) in each production.

          35. generate::=Net{v::N -> @#V, For all n:N, v'(n)=(substitute(v, P(n))) }.
          36. |-generate= {(v1, v2):@(N->@#V, N->@#V) || for all n:N (v2(n)=substitute(v1, P(n)) }
          37. substitute::( (N -> @#V)><(@#V|#V) ) -> @#V,
          38. For v:N -> @#V, S:@#V, substitute(v, S)= |{substitute(v, s) || s:S},
          39. For v:N -> @#V, s:#V, substitute(v, s)= ! [i : pre(s)] (if s(i) in T then {s(i)} else v(s(i)) ).

            The generated language is smallest invariant language or fixed language under repeated substitution:

          40. generated::=the first fix(generate) where first=generate.min.

          41. Kleene_sequence::=map [i:0..] ( (map [n:N] ({})).(generate^i) ).

          42. convergent::@=some lim (Kleene_sequence)

            Convergence is guaranteed for all grammars when the substitutions increase the length of the strings. It can be shown that if the generation process converges at all then it tends to a unique limit which is the required minimum fixed point[Manes & Arbib 86, Moll et al. 88 ].

          43. (ManesArbib86)|-if convergent then generated=lim[i:0..]([n:N]({}).(generate^i)).

            ...[parsing, see later and Aho & Ullman]

            }=::CF_GRAMMAR

            Normally, in MATHS and Language Reference Manuals, we use the grammar to determine N and T:

          44. CFG::=$
            Net{
              A CFG G is a 3-tuple (N, T, P) as defined in CF_GRAMMAR [above] which is normal and complete, with N as the set of non-terminals, T as the set of terminals, and P as the set of productions.

            1. G:: CF_GRAMMAR.grammar and normal, and complete,
            2. N::=pre(m(G)),
            3. T::=V~N.
            4. |-P in N -> @#V.

            }=::CFG.

          3.2.3 Dictionaries

          A dictionary (Chapter 2) permits intersections and complements in definitions - so, for example:

          Therefore

        4. (above)|- (dict1): B={b^m ! c^m || n=0..},
        5. (above)|- (dict2): P={a^n ! b^m ! c^m || n, m=0..}.
        6. (above)|- (dict3): A={a^n ! b^n || n=0..},
        7. (above)|- (dict4): Q={a^n ! b^n ! c^m || n, m=0..}.
        8. (dict2, dict4)|- (dict5): L={a^n ! b^n ! c^n || n=0..*}. The last result shows that a dictionary with an intersection can describe a language that is not context free.

          3.2.4 Acceptors

          Define (temporarily) an acceptor as a relation R between strings of symbols that accepts string i iff i R "" .
        9. I::=Input Symbols,
        10. #I::=Input strings,
        11. @(#I, #I)::=relations processing input strings.

        12. For R:@(#I,#I), accepted_by(R)::= {x:#I || x R () }.

          The get some input relation, x? is defined by

        13. For x:I, x? ::@(#I,#I)= rel [i, i':#i] ( i=x ? i' ) [compare Lam & Shankar 90].

          It follows that

        14. (above)|-"a" ("a"? ) (),
        15. (above)|-for no x:#I~{"a"} ( x("a"? ) () ),
        16. (above)|-accepted_by(("a"? )) = {"a"}.
        17. (above)|-"b" ("b"? ) (),
        18. (above)|-"ab" ("a"? )"b" ("b"? ) (),
        19. (above)|-"ab" ("a"? ; "b"? ) (),
        20. (above)|-{"ab"} = accepted_by ( "a"?; "b"? ).


        21. (above)|-"aba" ("a"? )"ba" ("b"? )"a" ("a"? ) ().
        22. (above)|-"aba" ("a"? ; "b"? ; "a"? ) ().

          Notice that if R is a finite relational expression containing only (;), (|), (do) and x? then R represents the behavior of a non-deterministic finite state acceptor(FSA). Hence there is an equivalent deterministic FSA. Similarly in reverse, for each FSA there is a finite relational expression made from x?, (|), (do) and (|).

          It is obvious that the usual top-down parser will take a context free MATHS grammar and construct a program that accepts language. Each definition is a regular expression. There is a simple transformation of the dictionary into a set of definitions of relations that model the parsing of the input by the grammar.

          Table of Mapping from Dictionary to Program


          Table
          DictionaryExampleRelation Notes
          definitionaEBNFdefiner bC_aEBNFdefiner BB is the transform of b.
          terminaltt?t is removed from front of i
          non_terminalaC_aC_a is a relation that consumes all of a
          sequencea b c... A; B; C; ...Where a, b, c...transform to A, B, C,...
          selection(a|b|c)(A|B|C|...)Where a, b, c...transform to A, B, C, ...
          iteration#ado(A)Where a transforms to A

          (Close Table)
          For example
           	P::=( a P b | #c)
          becomes
           	C_P::=(a?; C_P; b? | do(c?))
          by applying the above transformations.

          To show

        23. |- (correct): P=accepted_by(C_P),
        24. take ==> and <== in turn.

          Proof of correct


            (correct1): P ==>accepted_by(C_P).

            Let i:P,

            then either i in #c or for some p:P( i=a ! p ! b). In the first case, i (do( c? ))() and so i is acceptable to C_P. In the second case, i=a ! p ! b and so if p is acceptable to C_P then so is i. By induction we conclude that if i in P then i in accepted_by(C_P).

          (Close Let )


          (correct2): accepted_by(C_P)==> P.
          Let

            Now consider a string i that is acceptable to C_P. It is therefore either accepted by 'do(c?)' or by (a?; C_P; b?). In the first place, i is in #c and so in P. In the second place i is accepted by C_P iff it starts with an "a" and terminates with a "b" and the middle is accepted by C_P. By a simple induction if p in accepted_by(C_P) then p in P.

          (Close Let )

        25. (correct1, correct2)|-result.

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

        Proving that the translation of a grammar into a top-down parser always produces a relation that accepts exactly the language described by the grammar is a straight forward induction on the structure of the expressions. The translation is a homomorphism between the two semi_rings.

        In practice a programmer implementing an accepting relation can reduce the amount of backtracking by adding conditions like the following:

      1. For a in #Character, a.next::=for some y(i=a ! y).
      2. For A in @#Character, A.next::=for some x, y(i=x ! y and x in A).
      3. else::=the previous alternative failed to complete.
      4. For example if the grammar P::=#A B then the mapping of dictionaries to programs above gives:
      5. C_P::=do(C_A); C_B. But if we know that no prefix of a string in B is a prefix of a string in A then:
      6. C_P= while(A.next ) (C_A); C_B, Since|-(while1): (A.next; C_A)=C_A. and|-(while2): (not (A next); B)=B.

        A CFL is accepted by a non-deterministic PDA, where a PDA(Push-Down-Automata) has the following structure:

        It is easy to show that if R is defined by a simple recursion (like a context free grammar) then it can be implemented as a non-deterministic PDA.

        3.2.5 Acceptors & Dictionaries

        Next extend the construction of acceptors for grammars to acceptors for dictionaries including intersections. Consider the intersection (&R) of two or more simple acceptors R1, R2, R3, ... . This relation succeeds on those strings that are accepted by all of them.
        Let
        1. R1, R2, ... : @(#I,#I).
        2. |-accepted_by(R1 & R2 &...) ={x:#i || x (R1 & R2 & ...) () }
        3. ={x:#I || x R1 () and x R2 () and ...}
        4. ={x:#I || x R1 () } & {x:#I || x R2 () } & ...
        5. =accepted_by (R1) & accepted_by( R2) & ...

        (Close Let )
        The parallel composition of the acceptors for a set of dictionaries accepts the intersection of languages defined by the dictionaries [ Hemendinger 90 has a similar result for Ada Tasks]. Therefore by adding the following mappings we get an acceptor for a MATHS dictionary with intersections and complements:


        Table
        DictionaryRelation Notes
        intersectiona&b&c... A&B&C&... Where a,b,c...translate to A,B,C,...
        complementa~b A ~ BWhere a and b translate to A and B.

        (Close Table)

        For instance consider:


      7. |-L={a^n b^n c^n || n=0..}.

        Converting this dictionary into an acceptor with two processes gives:

      8. acceptorL::=following
        Net
        1. C_L::=C_P & C_Q,
        2. C_P::=do(a?); not a next; C_B,
        3. C_B::=(b?; C_B; c? | else),
        4. C_Q::=C_A; do(c?); end,
        5. C_A::=(a?; C_A; b? | else).

        (End of Net)

        L accepts a string i iff both C_P and C_Q relate i to (). Hence C_L accepts P&Q. If C_L accepts a string then the string is in P&Q.

        So, dictionaries define languages that are recognized by networks of CFG acceptors. Hemendinger shows that similar rules can be used for deriving grammars that model the communications that can occur between two Ada tasks [Hemendinger 90]. Notice that it is easy to transform acceptors into automata that report at each step whether or not the input is currently acceptableand then connect these to an "and-gate":

        This kind of structure - a Directed Acyclic Graph(DAG) of simple automata is found in naturally occurring recognisers - eyes, ears, and brains. Gelernter would call it a trellis. It is known that any finite state automata can be decomposed into such a DAG of simple finite state automata and delay machines - where a simple automata is one that has a "simple group"[Hartmenis and Stearns]. However, there are mathematically simple automata of arbitray size and complexity and so this result is not very helpful. Further it does not help us to understand what can be done by networks of recognizers that have stacks in them. This is the next topic.

        3.2.6 Power of MATHS

        There is no limit to the expressive power of MATHS as a syntactic meta-language because it permits definitions like:
      9. L::={a || W(a)} for any well formed expression W. For example,
      10. L::={a^(n^2) || n=0..}, is a context sensitive language. The following language is clearly not even computable.
      11. L(s0)::={ a:#I || for some n:Nat ( (UTM^n)(s0, a) ==>{(HALT, x)||x:#I} }
      12. where `UTM is a relation that simulates one step of a Universal Turing Machine`.

        A simple context free dictionary has a comparatively simple top-down acceptor. The correspondence has proved its value in practical projects[ DDD]. Intersections in the dictionary lead to a network of parallel recognizers. Two questions arise:

      13. - How many parallel processes (intersections) might be required?
      14. - What languages can not be handled by n parallel processes(intersections)?

        These are the topics for section 3. Section 4 shows how dictionaries are used and gives several examples.

      . . . . . . . . . ( end of section 3.2 On the Power of Data Directed Methods) <<Contents | End>>

      3.3 Grammar Theory

        3.3.1 Concurrent and communicating grammars

        Concurrent and communicating grammars are important because if a language is described as the intersection of n grammars ( of a given type G say which is accepted by automata of type A ) then the language is accepted concurrently by n automata of the type A . Thus n is an upper bound on the number of communicating sequential processes needed to recognize, parse, or process the language. Further if the automata are in some sense efficient then there will be an efficient (in the same sense) n processor solution. Concurrent definitions imply cooperating sequential processes that form networks that can be efficiently implemented.

        The family of languages defined by these grammars is a superset of the Boolean closure of the family of context free languages and a proper subset of the context sensitive languages.

        Defining a language as the intersection of several grammatical constraints is not new - Constrained Expressions are expressive and based on simple regular expressions [Dillon et al 86]. Hehner and Silverberg[83] use the term "Communicating Grammars" for a set of grammars with some terminals and non-terminals occurring in both. The model here is simpler - I propose the terms "concurrent context free grammars" (CCFG) for the dictionary model proposed here, and "concurrent context free languages"(CCFLs) for the family of languages defined by CCFGs. The Turing project used explicit intersections [Holt & Cordy 88]. Hemendinger notes that Ada tasks have communication patterns that are CCFLs[Hemendinger 90].

        3.3.2 Formal Model

        This is a more abstract model than CFG above and has an explicit initial symbol (I) and set of non-context free definitions(J).

        CCFG = CG and context_free.

      1. CG::=Concurrent_Grammars,
      2. Concurrent_Grammars::=
        Net{
        1. T::=terminals,
        2. terminals::Sets,
        3. N::=non_terminals
        4. non_terminals::Sets,
        5. |-N&T={}.
        6. V::=Vocabulary,
        7. Voculary::=N | T,

        8. I::=Initial_Symbol,
        9. Initial_Symbol::N,
        10. J::@N,
        11. degree::Nat=|J|, J::={ j1 , j2 , j3 , ..., j[degree]}.

        12. D::=dictionary.
        13. dictionary::N ->expression(V).
        14. D(I)= j1 & j2 &j3 &...&j[degree].
        15. context_free::@=for all n:N~{I}( D(n) in regular_expression(V)),
        16. G::=(N,V,I,D),

        17. states::N -> @#V,
        18. P::N -> (states -> @#V)=map[n:N](map [s:states](`for p:N, substitute s(p) for p in D(n)`)),
        19. initial_state::=[n]({n}),
        20. |>::=rel [x,y:states](for some n:N(x(n'=P(n)(x) ) y)),
        21. |>*::=do(|>),
        22. Generated_language::={x(I) || x:(|>*(initial_state )) } & #T.

          Acceptors were introduced above and are formally defined in chapter 5. It is easy to show that these acceptors are the equivalent of PDA's (the stack handles recursion and vice-versa). Chapter 5 also defines stacks and the meaning of coupling between components.

        23. PDA::=...
        24. accepted_language::=...
        25. ... }=::CCG

          3.3.3 Intersections of CFLs

          I now describe a hierarchy of families of languages. Let CFL^0 be the regular languages and CFL^1 the context free languages. A language is in CFL^n if it is the intersection of n CFL^1 languages. A similar set of definitions can be created for any family of languages which is not closed under intersection. The context free dimension of a language L (CFD(L)) is the minimum n for which L is a CFL^n. Liu and Weiner defined CFL^k as the `k-intersection languages` - but failed to specify what the intersection of zero CFLs might mean. In this case by defining the regular languages as CFL^0 implies that if a language is the intersection of a CFL^p and CFL^q language then it is a CFL^(p+q) language.

          Liu and Weiner remark that trivially

        26. if n<m then CFL^n==>CFL^m and show that CFL2<>CFL1 by considering {a^n b^n c^n||n:0..}. Thus CFL1=>>CFL2 As another example consider
          Let
          1. L::=P&Q,
          2. P::=#a B #d, B::=(b B c|),
          3. Q::=A D, A::=(a A b |), D::=(c D d|).

            Clearly,

          4. (P)|-P={a^n1 ! b^n2 ! c^n3 ! d^n4 || n2=n3},
          5. (Q)|-Q={a^n1 ! b^n2 ! c^n3 ! d^n4 || n1=n2 and n3=n4}.

            Therefore,

          6. (-1, -2, L)|-L={a^n1 ! b^n2 ! c^n3 ! d^n4 || n1=n2=n3=n4}.

            Similarly

          7. {a^n ! b^n ! c^n ! d^n ! e^n || n:0..} in CFL^2,
          8. {a^n ! b^n ! c^n ! d^n ! e^n ! f^n || n:0..} in CFL^2,
          9. ...

          (Close Let )

          Liu & Wiener presented for all p>0 languages which belong in CFL^(p+1) and not CFL^p. This proves that for all p ( CFL^p=>>CFL^(p+1)) [Liu & Wiener 73, Hemendinger 90].

          For example the language

        27. {a^n1 ! b^n2 ! c^n3 ! a^n1 ! b^n2 ! c^n3 || n1,n2,n3:0..} in CFL^3 ~ CFL^2.

          It is interesting to note that all the other languages formed by permuting terms are all CFL^1 or CFL^2:

        28. {a^n1 ! b^n2 ! c^n3 ! b^n2 ! a^n1 ! c^n3 || n1,n2,n3:0..} in CFL^2 ~ CFL^1.
        29. {a^n1 ! b^n2 ! c^n3 ! c^n3 ! b^n2 ! a^n1 || n1,n2,n3:0..} in CFL^1 ~ CFL^0. etc.

          The first language exhibits two examples of what Jackson calls an "interleaving clash", and the next a single clash, the last has no clashes. I therefore conjecture that the number of interleaved groups is equal to one less than the context free dimension of the data.

          Liu and Weiner[73] use a correspondence between the context free dimension of a language and the dimensionality of an associated linear space in their proof. They note that determining the context free dimension of an arbitrary language is often difficult. Finding G:CCFG with degree n merely establishes an upper bound on the CF dimension of the language.

          There are well known polynomial time algorithms which recognize or parse a CFL^1 language. Hence CFL^n languages will be recognized by n parallel polynomial time algorithms - and so by a polynomial time algorithm that simulates the n parallel processes. The simple parallel structure proposed to handle intersections has no interaction between the processes. Each process is isolated from all others and conceptually has its own copy of the input. There is an implicit census taker waiting for all processes to accept their inputs before it reports success of the whole. This is an easy structure to implement in most high-level languages and well suited to modern programming styles with tasking and/or objects.

          There exist CSLs that are not CCFL. An example is {a^(n^2) || n:0..} which is a CSL. If it was a CFL^p for some p then it would be the intersection of p CFLs with a single terminal symbols. A CFL with a single non-terminal is regular and so the language must be the intersection of p regular languages. Therefore it is regular. However it is obviously irregular. Therefore

        30. {a^(n^2) || n:0.. } in CSL~CCFL.

          A similar argument shows that if L in CFL^p for some p, and t some terminal then

        31. L&#t in CFL^0=REG.

          CFL^n is accepted by n parallel non-deterministic PDAs. Hence it follows that CFL^n is closed under:

          1. Star
          2. Concatenation
          3. Inverse finite state transductions.
          4. Inverse homomorphism

          Hemendinger uses closure under Inverse homomorphism to construct an elegant proof that a language is in CFL^3~CFL^2 [page 753, Hemendinger 90].

          CFL^p is not closed under union but CCFL is because

        32. (A | B)&(C | D)=A&B | A&D | B&C | B&D so that the union of a CFL^p and a CFL^q is a CFL(p*q) when p,q>0.

          If we permit networks with a more general acceptance criteria - a boolean operation on the individuals then the number of PDA's required for the union of two such nets is the sum of the sizes of the two nets.

          Other results depend on an exemplary type of language - languages defined by linear constraints [Liu & Wiener 73]. Given an alphabet of N elements {a1,a2,a3,...,a[N]} and

        33. n::Nat0^N=(n1,n2,...n[N]),

          define a**n=![i:1..n](a[i]^n[i]).

          Given alphabet of N elements {a1,a2,a3,...,a[N]} and an integer linear map M:Int^N -> Int^p and vector j[1..p] then

        34. LL(M,j)={a**n || for some n:Nat0^N(M(n)=j)}.
        35. LinL::=img(LL) are the Linear Languages.
        36. Linear Languages map some languages into linear spaces
        37. If M is of rank r then ML(M,j) in CFL^r.
        38. Given alphabet of N elements A={a1,a2,a3,...,a[N]} define
        39. For a:A, Dup(a)::={a**n! a**n || for some n:Nat^N}
        40. |-Dup(a)==>{w ! w || w:#A}
        41. |-Dup(a) in CFL^N

          A countably infinite union of one set of CFL^m (m=1..) is {x! x || x:#@}. Now for finite p, {x! x || x:#@} is CSL~CFL^p. However

        42. {x!x || x:#@}={x!x || n:0.., x:@^n}= | [n:0..]{x!x || x:@^n} Now if x:@^n then x=0^p1! 1^p2 ! 0^p3 ... 0^p[m] where +(p)=n and m<=n.

          Therefore {x! x || x:@^n} is in CFL^m.

          Clearly then {x! x || x:#@(|x|<=n)} is also CFL^m , and so as m tends to infinity we get a closer and closer approximation to {x! x || x:#@ } which is a Context Sensitive Language(CSL).

          3.3.4 Embedded intersections

          The union of a CFL^p and a CFL^q is a CFL(p*q) when p,q>0. So if a dictionary contains an intersection which is not self embedding then there is a dictionary with that intersection at the top level.

          Philippe Schnoebelen circulated the Theory-Net on the BITNet(comp.theory on Usenet) with an interesting result equivalent to the observation that

        43. For A:Alphabet, L1,L2:CFL^0 & @#A,

        44. X::=L1 | (L2 & (A X)) defines the language
        45. X= | [n:0.. ] (L2 & (A L2) & (A^2 L2) & ( A^3 L2) & ... & ( A^n L1))

          and shows that this is a regular set.

          It also appears there is no additional power added to language definitions by allowing intersections to be used arbitrarily - it is enough that they be permitted at the top level.

          Lower level intersections in a grammar (which may be useful and convenient) are equivalent to allowing the network of PDAs to spawn new PDAs. We can get the same effect by keeping PDAs in a do-nothing loop until needed [cf pp81-88 of Baetan 90 by J A Bergstra]. It is clear that there is no limit to the number new PDAs. So allowing lower level intersections implies using either a growing network or a fixed network of finite but unbounded size.

          3.3.5 Multiple Grammars

          Unlimited networks are a simple extension to CCFL which allows definitions to have parameters in them. Details will be explored later but there are two extant examples of systems based on this model - Sakakibara's Extended Simple Formal Systems(ESFS) and JSD.

          Sakakibara's Extended Simple Formal Systems(ESFS) define a family of languages that lie between the CCFL and CSL [Sakakibara 90, p91]. Sakakibara also presents a Simple Formal System(SFS) which defines the language { a^(2^n) || n:Nat0}[Sakakibara 91]. This is clearly not definable in terms of a finite number of intersecting grammars. Using more advanced MATHS one of Sakakibara's SFSs would be written as Net{ P::#{a}->@, P(a), for all x:#{a}, if P(x) then P(x!x). }.

          Moreover, let

        46. sqr::#{a}->#{a}=(_)!(_) then by definition
        47. |-For A:@#{a}, sqr(A)= {x!x || x:A }

          and so this non-Chomskian grammar

        48. L::= a | sqr(L)

          defines L={ a^(2^n) || n:Nat0} by the usual iterative/topological model.

          The Simple Formal Systems [ defined Sakakibara 91 p84] can define a language that is not CCFL, and yet can not define {a^n ! b^n ! c^n || n:Nat} which is CCFL [evidence in proof of proposition 7 on p90 of Sakakibara 91].

          JSD (Jackson System Development) designs systems as a large network of objects that belong in a small number of "classes"[Jackson 78]. Each class has many similar but out of phase objects . In these designs, each dynamic object keeps an occurrence of an entity up to date [ See bibliography of JSP/JSD, Chapter 9]. It appears likely that these correspond to a subset of the CSLs.

        . . . . . . . . . ( end of section 3.3 Grammar Theory) <<Contents | End>>

        3.4 MATHS as a MetaLanguage

          3.4.1 Introduction

          Making a programming system is a part of Software Engineering. However it is a larger part than might be thought, since giving the user the power to write programs makes any system more useful at comparatively small cost. Further, much of formal specification is creating a formal language and defining its meaning. Finally, any program with input and/or output has an associated set of formal languages (the possible inputs and outputs) and these are often defined by EBNF. MATHS can be used as a powerful meta-language to define formal and computer languages.

          In essence the task is to define a relation that maps certain strings of symbols into a set of meanings. The pre-image of this relation is called the language. Ideally the syntax of the language is isomorphic to the structure induced on the language by the inverse of this relation. The co-domain of the relation forms the semantics of the language.

          The standard approach is to separate the description of the set of strings in the language (syntax) from determining their meaning (semantics). In most programming languages there are other techniques - a map from strings of characters into strings of "tokens" representing "lexemes", and a mapping of certain defined patterns into a standard language by a collection of "definitions" or "macros" are also defined.

          All languages of any size have been defined by several sets of rules that define and interpret the language. Typically there is a lexical description plus a set of syntax rules, and then some informal semantic and context dependant rules. Each set of rules gives a constraint on the design[Dasgupta 91 pp234-237,249-253,272-276]. Often the basic language is expanded by relations that add new strings to the language but present translation and transformation rules into the basic language. In MATHS we formalize this by assuming that a formal language can be defined by four sets of rules:
          Table
          StringsRules
          LexicalA Lexical grammar or Lexicon
          GrammaticalA set of Syntaxes
          MeaningfulA set of maps from Grammatical strings into Meanings
          DefinedDefinitions map Lexical strings into Meaningful strings

          (Close Table)
          Finally, since humans can handle informal descriptions and often prefer them when first meeting a topic or design there should be a set of informal definitions of every lexeme, non-terminal, denotation, and defined term. For example in C++:

        1. Lexicon includes
        2. keyword::lexeme= "asm" | ... .

        3. Grammar includes
        4. assembler_block::="asm" "{" #assembler_instruction "}".

        5. Glossary includes
        6. asm::gloss = `A lexeme that indicates the start of a block of assembler code`.

          3.4.2 Examples

            3.4.2.1 The Mod13 Code

            A minimal example is the problem of defining the set of numerical identifiers used by a company for its transactions. Each identifier is a string of decimal digits. The company wishes to detect if one digit has been inserted, deleted or changed. An elegant solution is to only use the numbers that are multiples of 13[Wagner & Putter 89, Peterson 91].


            Net

              Lexicon
            1. Uses Integers.
            2. Uses Set_Theory.
            3. digit::="0".."9".
            4. c::digit -> Nat0=the meaning of character (_) as a number,
            5. c::=("0"+> 0 | "1"+> 1 | "2"+> 2 | "3"+> 3 | "4"+> 4 | "5"+> 5 | "6"+> 6 | "7"+> 7 | "8"+> 8 | "9"+> 9).

              Syntax

            6. identifier::=#digit.
            7. Uses Integers.
            8. m::identifier -> Nat0=`meaning of a string of digitd(_)`::=map[d](+[i:1..|d|](c(d[i])*10^(|d|-i))).

              Semantics

            9. Uses Number_Theory. [Chapter 4 Logic. Section 8 STANDARD. 9 Other Systems.Number_theory]
            10. Meanings::=multiples(13)
            11. |-Meanings={13*n || n:0,1..}.
            12. |-(_*13) = map[n](n*13).
            13. |-Meanings =Nat0.(_*13).

              (=[13])::=equivalent modulo 13 ::= ( = mod do(_+13)).

            14. For n,m:Nat0, n =[13] m iff |n-m| in Meaning.

            15. meaningful::=Meanings./m.
            16. μ::meaningful ->Meanings =m o meaningful.


            17. |-meaningful=Nat0; (_*13); /μ.

              Pragmatics We show that the requirement that a single change in a digit can be detected has been met.


            18. |-For all p:Nat0, δ:(0..9)*10^p, if μ(δ)=[13]0 then δ=0.

              Proof
              Let

              1. p:Nat0, δ:(0..9)*10^p. μ(δ)=[13]0.
              2. q:Nat0.
              3. |-δ=13*q+0=13*q.
              4. ...
              5. |-δ=0

              (Close Let )
              end of proof

              So the meanings of any two meaningful identifiers are equivalent modulo 13:

            19. |-For all d,d':meaningful ( μ(d)=[13]μ(d'))....

              Now for all meaningful decimals d, if just the i.th digit is changed (to e say) then the result is not meaningful.

            20. |-for d:meaningful, i:pre(d), e:digit, d':=d~(i+>d[i])|(i+>e) ( d' in meaningful iff e=d[i]).

              Proof
              Let

              1. d:meaningful, i:|/d, e:digit, d'=(d~(i +>d[i]))|i +>e).
              2. d' in meaningful.
                μ(d')=μ(d)+(e-d[i])*10^(|d|-i).
              3. e-d[i]=0.
              4. ...
              5. |-e=d[i].

              (Close Let )
              end of proof

              Note: We had to explicitly list the meanings of the digits:

            21. |- c::=("0"+> 0 | "1"+> 1 | "2"+> 2 | "3"+> 3 | "4"+> 4 | "5"+> 5 | "6"+> 6 | "7"+> 7 | "8"+> 8 | "9"+> 9) because
            22. |[x:digit]("x"+>x) = ("x"+> 0 | "x"+> 1 | "x"+> 2 | "x"+> 3 |...) <> c.

            (End of Net)

            3.4.2.2 MATHS

            A second example is the MATHS formal definition that has both a lexer and a parser:

            The syntax of MATHS is defined by several grammars. The valid strings must fit all these grammars and the lexical constraints.

          3.4.3 Multi-Grammar Languages

          Grammars are a specialized form of formal documentation. A grammar is a set of definitions of names of sets of strings. A typical terminal might be a character, a data type, a name of an event, an object in a data base or data structure, a message type, etc... Each term defined in a grammar represents a set of sequences. Typically a non_terminal can define a language, a set of valid or possible files, a set of interesting patterns of events, a strategy for getting particular data from a data base or data structure, a trace of a program, a communications protocol, etc.

        7. LANGUAGE::=
          Net{
          1. Alphabet::Finite_Set,
          2. Lexicon::CF_GRAMMAR
          3. and
            Net{
              terminals::=character_string | name_of_character,
            1. source in #non_terminals,
            2. tokens in #non_terminals,
            3. lexeme in #non_terminals
              }.
          4. Syntax::@CF_GRAMMAR(Alphabet=>lexeme) and
            Net{
              terminals::= lexeme_name|character_string,
            1. source in #non_terminals}.
            2. Meanings::Sets,
            3. μ::=Denotation::source(Lexicon)& Grammatical <>-> Meanings,
            4. Meaningful::=/Denotation(Meanings).

            5. Standard::= (source(Lexicon) & Grammatical & Meaningful),
            6. Grammatical::= &{G.source || G:Syntax}.

            7. Definitions::@#Alphabet -> @#Alphabet,
            8. Language::= Standard./do(|(Definitions)),

              Since there is no effective procedure for deciding whether an arbitrary language defined by this technique is empty or not, it is necessary for the designer to always provide examples of strings in the language.

            9. Examples::@Language~{}.


            }=::LANGUAGE.

            Context free grammars have definitions solely in terms of regular expressions (made of #,|,. alone). MATHS is not limited to Chomskian grammars. Any set of simultaneous equations expressed in terms of set theory can define a unique language by using the smallest language that is a fixed point under the map formed by replacing defined terms by their definitions. As long as this substitution tends to only add longer strings to the sets, then there is a unique fixed point and so a unique language defined. An example of such a grammar is in section 3.3. However there is no reason to suppose that a general set of definitions like this is any sense efficient.

            3.4.5 Traps

            The problem of language design has to be separated from the problem of expressing the design. The language itself must be designed to avoid complexity, inconsistency, inefficiency, and ambiguity. The expression of the design as a set of definitions must be guided solely by a desire to find the clearest and simplest expression of the language. Usually a language designed by and for the 10Hz, glucose powered, 7_chunk massively parallel neural-endocrine network that humanity uses to handle language tends to be efficient on faster electronic computers. Languages form a paradigmatic model for software engineering[Chapter 1]. In place of defining syntax and semantics in a dictionary, a data processing system will need a data dictionary. The following heuristics apply to language design, data processing, and general software engineering.

            Complexity - A designer should seek to specify the data as precisely as possible in the simplest possible form, but as understood by the user. A canonical dictionary defines the set of terms that the user or client understands, no more, no less, and in a way acceptable to the client. Extra complexity should be avoided. If the client's problem turns out to be intractable, ambiguous, unsolvable, or not computable then the documentation should show this.

            Efficiency - A designer is sometimes permitted to change the language to make recognition, translation and interpretation efficient, but correctness is more important than efficiency. As a rule of thumb there should not be a search for a more efficient expression of a solution until a working, correct, complete, and easily modified prototype has been tested. Otherwise there is a temptation to describe a problem that can be solved efficiently, not the problem as specified by the user. Gross inefficiency, when caused by the user's or client's stated needs, can not be ignored. The cause must be identified, analyzed and discussed with the client or user.

            Inconsistency - the designer must exhibit a string defined by the system of definitions to show that the different constraints do not, rule out all possibilities.

            Ambiguity - the designer should not add to or diminish the ambiguity already present in the language (if any). Once documented it can be discussed and resolved in discussion with the client.

            3.4.6 Semantics

            The BNF definition of syntax has been understood and used with success throughout computing. There is less agreement about how meaning should be defined. Natural language is used in most standards(FORTRAN, COBOL, Ada 83, Ada 9X) but even those acknowledged best at writing semantics(for example Naur in Algol 60) failed to produce clean definitions. The Algol 68 report attempted to define the language by using a formal subset of a natural language.

            Another approach is to define an abstract machine and map statements in the language into changes in the state of the machine. IBM Viena, for example developed VDL. This has become VDM. A variation of this is to define a virtual machine that can interpret a simplified version of the language plus a translator from the language into the simplified form. The interpreter can then be implemented in software or hardware (BCPL and OCODE, Pascal and PCODE, Modular 2 and LILITH). This approach is called operational semantics.

            The axiomatic approach of Hoare associates statements in a programming language with inference rules allowing properties of the whole to be derived from the parts. Dijkstra's method specifies a rule for each elementary step and structure that calculates the weakest pre-condition necessary to guarantee a particular post-condition. This, in turn, lead to Gries calculational methods of program construction and proof. Theorists have demonstrated that it is possible to define most programming languages axiomatically. Axiomatic specifications have been published for Pascal. The Turing Project used this approach successfully. Similar ideas are used to specify ADTs. The axiomatic approach has the advantage of stating how to think about statements in a program without providing too many details.

            The denotational semantics movement comes from Strachey's work. Stoy and Scott provide 'denotations' that map parts of a programming language into a set of meanings. The meanings form a mathematical system called a function space - a set of functions with some idea of limit or approximation. The syntactic elements and structures of the language are mapped into elements and expressions in this abstract mathematical space of meanings. It is then necessary to show that one and only one meaning is given to each string in the language. This is easy when the rules are compositional and so follow the structure of the syntax of the language [Nielson & Nielson 92]. Compositional semantics is thus similar to DDD. This has developed into a feasible approach but has not been applied in any well known language. Scott has recommended using complete partially ordered sets and function spaces to model the meanings of languages [See his essay in ACM 86]. More recently Manes and Arbib propose using categories instead [ Manes & Arbib 86]. Another theory recommends using initial (free) algebras [Leeuwen 90].

            The different kinds of semantics are still used [Kok & Ruuten 90, Gumb 89, Nielson & Nielson 92 ]. All of them provide a relation between strings in the language and elements in a set. Call this the semantic domain. MATHS can be used as a notation with any of them - the symbolic logic component [in chapter 4] is suitable for specifying axioms for example, and the structures provides several models of virtual machines [Chapter 5].

            MATHS permits an alternative sequence where the desired semantics is stated first and a map is defined relating character strings to the semantics [cf Abowd Allen & Garlan 93]. The domain of definition of the map defines the language. The process is like the data base design methods of Chapter 1: (1) structures, (2) changes, (3)reports and displays. The conceptual model of the data is the semantic domain for the languages that access and manipulate the data [Guerevich 87].

            Example A city may have a data base of dog licenses. A normalized data base has a conceptual model with at least three entity types/tables/classes:

          5. Owner::= Net{name, address, phone ::#char,...},
          6. Dog::=Net{id, name, sex, color, description::#char,...}.
          7. Owns::=Net{license_no, owners_name, id, expiration_date::#char,...}.

            Semantic Space

          8. owners::Finite_set(Owner), dogs::Finite_set(Dog),
          9. ownership::Finite_set(Owns).
          10. for all n:owners.name, one x:owners (x.name=n).
          11. for all i:dogs.id, one x:dogs (x.id=i).
          12. for all n:owners.name, i:dogs.id, one x:owners (x.(name,id)=(n, i) ).

            Predicates

          13. For P:person, owner(P)::@=P in owners,
          14. For D:animal, dog(D)::@=D in dogs,
          15. For P:person, D:dogs, owns(P,D)::@=P owns D.

            Syntax This data can be represented in English by statements like

          16. "Shadow" is a dog.
          17. Dr.Botting is a person.
          18. Dr.Botting owns "Shadow".
          19. S::=dogs.name "is a dog." | owners.name "is a person." | owners.name "owns" dogs.name "." |
          20. dogs.name "is owned by" owners.name "." | ... . For all pd:owernship, pd.id.name owns pd.owners_name and pd.owners_name is owned by pd.id.name.

            3.4.7 Example - Binary

              Introduction

              The purpose of the following documentation is to illustrate how a linguistic approach fits into other specification approaches. It uses a very simple example - namely the binary number system.

              Contents

            1. lexicon
            2. syntax
            3. semantics
            4. pragmatics.

              Lexicon

            5. one::="1",
            6. zero::="0",
            7. bit::=one | zero.

              Syntax

            8. A binary number must have at least one bit and
            9. the first bit is sometimes special (sign bit).
            10. binary_number::=bit_1 #bit_n,

            11. bit_1::=bit,
            12. bit_n::=bit.
            13. Therefore
            14. |-binary_number ==> #bit
            15. |-for all b:binary_number, i:1..|b|(b(i) in bit)

              Semantics

            16. Use STANDARD.Serial
            17. [Chapter 4, Section 8]
            18. A binary number stands for a natural number
            19. - a member of the set Nat0={0,1,2,...}.
            20. Each bit in a binary number is weighted by a power of 2: for i:0.., w(i)::=2^(i-1).
            21. The meaning of a binary_number is determined by the map,
            22. μ::binary_number -> Nat0= (
              1. "0"+> 0
              2. |"1"+> 1
              3. |+> map[b](+((μ o b)*(w o (1..|b|))))
              )
            23. (above)|-+((μ o b)*(w o (1..|b|)))
            24. =(+[i:1..|b|](μ(b(i))*(2^(i-1))))

              It is easy to show that:

            25. (above)|-for all b:#bit ( μ("0"!b)=2*μ(b) ),
            26. (above)|-for all b:#bit ( μ("1"!b)=2*μ(b)+1 ).

              Therefore

            27. (above)|-for all a,b:binary_number(μ(a!b)=μ(a)+(2^|a|)*μ(b).

              Binary is an exact 1 to 1 coding of the numbers,

            28. (above)|-μ in binary_number---Nat0.

              Pragmatics

              We could now proceed to design some pragmatic (useful) objects. As a sample here is an object that converts binary into natural numbers.

              We symbolize the standard input and output by "i" and "o" respectively. Notice that we need to make sure that we can recognize when the input ends.

            29. bin::$ Net{i:(binary_number end), o:Nat0, p:Process}.


            30. (above)|-bin.i in #(bit|end).
            31. (above)|-bin.o in Nat0.
            32. (above)|-bin.p in Process.

              (above) |-For I,O:Sets, S::=Net{i:#I, o:#O}, R:@(S,S), x:#i, y:#O, x+>(R)+>y::= ((i=>x!end, o=>()) R (i=>(), o=>y!end). [Chapter 5 ]

              Samples

            33. (i=>"0"!end, o=>()) bin.p (i=>(), o=>(0)) or:
            34. "0"+> (bin.p)+> (0)

            35. (i=>"1"!end, o=>()) bin.p (i=>(), o=>(1))
            36. "1"+> (bin.p)+> (1)

            37. (i=>"10"!end, o=>()) bin.p (i=>(), o=>(2))
            38. "10"+> (bin.p)+> (2)
            39. ... For all b:binary_number,
            40. b ->(bin.p)+> (μ(b))

              Specification


            41. |-For all b:binary_number,
            42. (i=>b!end, o=>()) bin.p (i=>(), o=>(μ(b))) The inputs and outputs are i and o the standard inputs and outputs of a filter. Since there is only one input and one output we will omit redundant stream identifiers in what follows so x?:i is written x?.

              Derivation

              Using the syntax as a basis for the structure of bin.p we have:
            43. bin.p::= ... Consume_bit_1;
            44. ... do Consume_bit_n;
            45. ... Consume_end;
            46. ... Produce_Nat0,
            47. Consume_bit_1::=0?;... | 1?;...,
            48. Consume_bit_n::=0?;... | 1?;...,
            49. Consume_end::= end?;...,
            50. Produce_Nat0::=... . Where the operations and internal objects are:
              Table
              OperationPlacement Notes .Row !n Produce_Nat0, for n:integer, !n ::= o'=o!n.
              n'=0 when bit_1="0" changes n to be 0.
              n'=1 when bit_1="1" changes n to be 1.
              n'=n*2when bit_n="0" doubles n.
              n'=n*2+1 when bit_n="1" doubles n and adds one.
              0?, 1?, end?when i[1]=0,1,or end

              (Close Table)
              for x:{1,0,end}, x? ::= i = x?i'.

              The process associated with bin is therefore

            51. bin.p::= (Consume_bit_1; do Consume_bit_n; end?; !n),
            52. Consume_bit_1::=(1?; n'=1 | 0?; n'=0),
            53. Consume_bit_n::=(1?; n'=2*n+1 | 0?; n'=2*n).

              hence,


            54. |-bin.p= (
              1. ( 1?; n'=1 | 0?; n'=0 );
              2. do (
                1. 1?; n'=2*n+1
                2. | 0?; n'=2*n
                )
              3. ;
              4. end?;
              5. !n
              ).

          . . . . . . . . . ( end of section 3.4 MATHS as a MetaLanguage) <<Contents | End>>

          3.5 Additional Techniques

            MATHS is more powerful than a typical meta-language since meta-linguistics is only a part of its targeted applications. Some of its features are both convenient to use and add little or nothing to the complexity of a recognizer or parser for languages defined. Others give rise to new ways to describe languages that are both natural and more powerful.

            3.5.1 Substitutions

          1. substitution::= "(" expression "where" tight_binding #("," tight_binding) ")" |"for" tight_binding #(","tight_binding) "(" expression ")".

            Both forms bind values to abbreviations for the range of a single expression. So these three formulas are equal

          2. (a*x^2+b*x+c where x:=3) = for x:=3( a*x^2+b*x+c ) = (9a + 3b +c).

            3.5.2 Partial Descriptions, Ellipsis, and Enthymemes

            When writing documentation it is usually easier to develop definitions piece meal rather than with all options, constraints, and complications at the same time. The tool for keeping this under control is the Ellipsis symbol ("..."). For example one technique is to start with a broad concept and then add more and more constraints. Thus if a term, t is defined as
          3. t::= A & B & C then we can quote as facts.
          4. |- t::=A &...
          5. |- t::=B &... It is convenient to allow these to be valid input into a documentation system:

          6. restriction::=described_term "::=" intersection "&...",

            A described term is always the name of a set of possibilities and so can have many descriptions. It must satisfy them all. If t::=S&... then t represents the largest subset S that is a subset of all other descriptions. A term with a definition can be quoted as a description. If declared, then a term that is described as a set of type S must be declared as type @S. Chapter 5 provides the semantics of definitions in general.

            It is best to start from a specific, easily understood subset of the problem and progress to more general forms[Botting 84b]. The development of error handling is an ubiquitous example:

          7. all_possible_data::=good_data | erroneous_data | other_data So is that of a compiler:
          8. compile::=compile_good_program | check_bad_program | reject_non_program Thus given that
          9. t::=A | B | C, then we can quote the following
          10. |- t::=A |...,
          11. |- t::=B |... .

            Again it should be possible to input a series of additional alternatives into a documentation processor, and have them, checked, appended, etc.

          12. additional_alternative::=described_term EBNF_definer selection "|..." Formally a set of additional alternatives are combined into a single definition where the term is defined as the union of the separate alternatives.

            It is incorrect to use more than one ellipsis on the same term.

          13. description::=additional_alternative | restriction

            These notations are conveniences. Formally they do not exist. They become a set of definitions that are created by either the intersection or union of all the descriptions.

            An incomplete argument is called an enthymeme[Aristotle?]. It is an argument with any contiguous set of steps replace by the ellipsis (...) symbol (see Chapter 5). Similarly the ellipsis can be used inside any set of documentation to hide a piece of irrelevant documentation from the reader/user. Online the three dots could react to being selected by expanding to show the details.

            A third form of incompleteness occurs when part of a sequence is left out. Similar - but much more informal - is the use of the ellipsis "..." in mathematical expressions :

          14. n*(n+1)/2 = 1+2+3+...+n as in the design of bin.p above. These can only be verified if they are accompanied with a formal expression that makes clear what is meant (Examples occur through out this book).

            3.5.3 Macros

            Functions mapping sets of strings into sets of strings are useful and efficient when defining programming languages. The following are used in chapter 4 and 5, and useful in most programming language definitions:
          15. macro::=@#A->@#A,
          16. macro2::=@#A><@#A->@#A.

          17. O::macro= ((_)|). --Option
          18. B::macro= ("(" (_) #("," (_)) ")" ). --Bracketed list
          19. L::macro2= ( (1st) #( (2nd) (1st))). --List
          20. N::macro= ( (_) #(_)). --Number of
          21. P::macro=(_) | "(" (_) #("," (_) ) ")". --Parameter pack
          22. R::macro=(_) | "(" (identifier "=>" |) (_) #( "," (identifier "=>" | ) (_)) ")" . -- Record values

            A dictionary that uses the above functions is equivalent to a longer dictionary without them. In general a dictionary that contains functions defined in terms of regular expressions of simpler functions is equivalent to a grammar with expressions containing N(arguments) replaced by the equivalent expression. Such functions defined are called "macros."

            Definitions that include parameters are useful for defining and specifying maps and relations. Sets of definitions that include parameters are called Logical Grammars [ Abramson & Dahl 89 ]. A more general form of dictionary is the W- Grammar, or Two-level Grammar or Van-Wijngarten Grammar that contributed to the demise of Algol 68 yet is alive as a tool for documenting data structures[Gonnet & Tompa, Gonnet & Baeza-Yates 91]. MATHS as a whole has the power of a logic programming language [Ballance et al 90]

            3.5.4 Parameterized Grammars

            The idea of a macro-like facility can be taken further because a piece of documentation can be created and named which has both declarations and definitions[ introduced in Chapter 2 Section 6.6, defined Chapter 5]. For example, we can define the idea of an UNARY operator u, as a symbol which can be put in front or after its argument a:
          23. UNARY::=Net{ u::#A, a::@#A, e::= a | u a | a dot u }. Given this definition then the following MATHS statement,
          24. UNARY( u=>"sqrt", a=>term, e=>expression) generates the following documentation:
          25. expression::= term | "sqrt" term | term dot "sqrt".

            A common example is when a symbol for a function f can be used as an infix operator between strings described by s to give strings described by 'S", For example: "+" is an inifx operator acting on products to give expressions is written

          26. INFIX(f=>"+", s=>product, S=>expression) which is short for
          27. expression::= "+" P(product) | P(product) dot "+" | "(" L(product, "+") ")", because,
          28. INFIX::=Net{ f:#A, s:@#A, S:= f P(s) | P(s) dot f | "(" L(s, f) ")" }.

            So,

          29. INFIX(f=>"<", s=>expression, S=>relation) means
          30. relation::= "<" P(expression) | P(expression) dot "<" | "(" L(expression, "<" ) ")".

            Another extension handles a common form of definition:

          31. `A wff is a propositional variable
          32. or " (" W ")" where W is any wff
          33. or W1 "and" W2 where W1 and W2 are wffs
          34. or W1 "or" W2 where W1 and W2 are wffs
          35. or "not" W where W is any wff.
          36. ` MATHS:
          37. wff::= propositional_variable
          38. | {" (" W ")"|| W: wff }
          39. | {W1 "and" W2 || W1,W2: wff}
          40. | {W1 "or" W2 || W1, W2:wff}
          41. | { "not" W || W: wff}. or using the prefixed operators defined in chapter 2, section 8 (also in chapter 4):
          42. wff::@#( propositional_variable | "(" | ")" | "and" | "or" | "not" ),
          43. wff = propositional_variable
          44. | |[W: wff] ( "(" W ")" )
          45. | |[W1,W2: wff ] (W1 "and" W2)
          46. | |[W1, W2:wff ] (W1 "or" W2 )
          47. | |[W: wff] ( "not" W ). Clearly this form of definition is more powerful than the simple techniques of section 3 and 4 since
          48. L::= a | |[x:L](x ! x) defines
          49. L={ a^(2^n) || n:0.. }.

            This technique leads to a way to express the context dependencies found programming languages such as Ada:

          50. labeled_loop::= | { ( L ":" "loop" #( S | "exit" L "when" C ";" ) "end loop" L ";") ||
          51. L:loop_ids, S:statement , C:condition }

            Further, suppose that we have already defined declaration(V), usage(V), and no_ref(V) as the strings in a language which (1) declare or introduce V, (2) make use of V, and (3) don't refer to V respectively then:

          52. For V:variable, valid_wrt(V)::=#no_ref(V) declaration(V) #(usage(V) | no_ref(V) ), describes all sequences of components where V is declared before it is used - and is NOT re-declared. Further,
          53. |-&(valid_wrt) = & [V:variable] valid_wrt(V). Hence
          54. block::="begin" ( &(valid_wrt ) & (statement # (";" statement )) "end", defines a block with all its variables declared exactly once before they are used. This is a common context sensitivity in programming languages. MATHS handles it well. Finally the '&'s in the definition imply that the parser would be structured as a number of parallel parsers, all with the same structure. This form concurrency is very easy to handle in both theory [Hoare 79 & 85] and in practice [Jackson 75, Andre Banatre & Routeau 81, Cameron 89].

            3.5.5 Grammars that Imply Semantics

            It is possible to use MATHS to define both the syntax and the semantics of a language simultaneously by defining terms which do not represent strings, but represent both a set of strings and a set of meanings at the same time. This is somewhat experimental at this time [Abramson & Dahl 89]. A technique that is used in practice is to simultaneously define several structures and correspondences between them [Mamrak et al 93]. Tagged Context Free Grammars can parse input and encode it in a relational data base [Mark & Cochrane 92]. If general operations are associated with each component in a grammar then we have something like JSP [see chapter 6, DDD in Chapter 9]. If the operations are just serial I/O the result is very like Aho and Ullman's translation systems. Attribute grammars specify equations that are solved in the process of parsing. The result is a loss of modularity and efficiency however [Dueck & Cormack 90].

            3.5.7 Mapping Semantics into Syntax

            Now suppose that we have already defined a semantic model of meanings (M) and we define a map that generates strings encoding the meanings ( like a pretty printer outputs a readable version of an internal list structure in LISP):
          55. generate::M ->@#char, then
          56. Language::= |generate.

            If generate is a (1)-(1) map then

          57. parse::= the parsing operation ::= /generate.

            It is possible to start by defining the semantics of a language, show how to encode the meanings as character strings, and so derive both a parser and a description of the syntax automatically [compare Wagner 90b, Abowd Allen & Garlan 93].

            3.5.8 Syntactic/Semantic Packages

            We can define packages of reusable syntax and semantics at one time. For example, in MATHS (as in mathematics) there are two kinds of infix operators - those that are like the plus sign and those like the less_than sign:
          58. 1+2+3=(1+2)+3.
          59. 1<2<3 = (1<2) and (2<3).

            These two types are called serial and parallel respectively in MATHS. Here is the syntactic/semantic definition of serial and parallel operators in terms of strings, types and a relationship linking strings to meanings.

          60. SERIAL_PARALLEL::=
            Net{
            1. Uses SEMANTICS.
            2. |- SEMANTICS::=Net{... [Compare chapter 5, Section 2.8]
            3. For x:: #lexeme, T::Types, v::T, symbol(x, T, v)::@=`symbol x in T means v `. ...
            4. For x, T, v, unique_symbol(x, T, v)::= symbol(x,T,v) and for one v:T(symbol(x, T, v)).
            5. For x, T, if unique_symbol(x, T, v) then x.T::T= the[v:T](symbol(x, T, v)).
            6. For x,y, T, x equivalent(T) y::@= (x.T = y.T).
            7. }.
            8. Used_in Theory_of_Types, TYPE, EXPRESSION[Chapter 5]. (maps) |-For T:Types, associative(T)::={f:T><T->T || for all x,y,z:T(f(f(x,y),z)=f(x, f(y,z)) }.


            9. (strings)|-For T:Types, n:2.., a:T^n, front(a) ! last(a) = a, front(a) =(a1, a2, ..., a[n-1]).

            10. SERIALITY::=
              Net{
              1. INFIX(f, s, S), [Section 5.4 above].
              2. T::Types,
              3. g::associative(T).
              4. unique_symbol(f, T><T->T, g).
              5. E::@#A=S | s dot f | f P(s).

              6. We wish to associate a unique value of Type T to each string in E
              7. First the formal equivalent of
              8. for a,b:T, a g b = (a,b).g = g(a,b),
              9. for a,b,c:T, a g b g c= (a,b,c).g = g(a,b,c)=g(g(a,b),c),
              10. for n:3.., a:T^n, g(a) = a.g = g( g(front(a)), a(n)).
              11. For a,b:s, symbol( a f b, T, g(a.T,b.T)).
              12. For a,b,c:s, symbol( a f b f c, T, g(g(a.T,b.T), c.T).
              13. For a,b,c:s, symbol( f"(" a "," b "," c ")" , T, g(g(a.T,b.T), c.T) ).
              14. |-For a,b,c:s, a f b f c equivalent(T) f"(" a "," b "," c ")".

              15. For a:S, b:s, if symbol( a, T, v) then symbol( a f b, T, g(v, a.T) ).
              16. For n:1.., a:s^n, b:s, if symbol(a,T,v) then symbol( f "(" a ! b")" , T, g(v, b.T) ).
              17. |-For s:S, one v:T, symbol(s, T, v).

              18. Next establish the formal version of
              19. for a:T, a.g = g(a) = a.
              20. For a:s, symbol(a"."f, T, a.T) and symbol(f"("a")", T, a.T).
              21. |-For e:E, one v:T, symbol(e, T, v).


              22. |-if units(g) then one units(g).
              23. if units(g) then for n:=(), g(n)=(n).g=the units(g).
              24. |-if units(g) then for e:E|"()", one v:T, symbol( e, T, v).


              }=::SERIALITY.

            11. For E,e,f,g,t, SERIAL(E, e,f,g,t)::=SERIALITY(T=>t, s=>e, f=>f, g=>g, E=>E).

              Example - SERIAL(disjunction, conjunction, "or", or, @)

              Clearly the formal and precise statements that a given symbol string s, in a given context T, has a particular value v (symbol( s, T, v) ) are a translation of the informal definition... and in the next example the formal translation is ommitted:

            12. PARALLELISM::=
              Net{
              1. INFIX. [Section 5.4 above]
              2. T::Types, g:: T><T->@.
              3. symbol( f, T><T->@, g).
              4. For a,b:T, a g b = (a,b).g = g(a,b).
              5. For a,b,c:T, a g b g c= (a,b,c).g = g(a,b,c)=g(a,b)and g(b,c).
              6. for n:4.., a:T^n, g(a) = a.g = g ( g(front(a)) and g(a(n-1),a(n) ) ).

              }=::PARALLELISM.

            13. For E,e,f,t, PARALLEL(E,e,f,g,t)::=PARALLELISM(T=>t, s=>e, f=>f,g=>g, S=>E).

              Example - PARALLEL( equivalences, implication, "iff", iff, @).

              For T:Types, R:@(T, T), r:#A, if symbol (r, @(T, T), R ) then

            14. PARALLEL(relational_proposition, expression(T),r, R, @).

              A more general form is given in Chapter 4, Section 2.2 - predicates [LPC].


            }=::SERIAL_PARALLEL.

            Note. It is tempting but incorrect to assert `for all Types T, x:T (symbol("x", T, x))`. However, "x" is a string with the same ASCII character "x" in it whatever the variable x currently represents and the formula therefore asserts that the character "x" means everything in T!

          . . . . . . . . . ( end of section 3.5 Additional Techniques) <<Contents | End>>

          3.6 Applications in MATHS

            3.6.1 MATHS_Lexemes

            Uses BINARY_CODE. [ section 6.4 ]

          1. For C:@character, non(C)::= character not C,
          2. For c:character, non(c)::= non({c}).

          3. lexer::= (i=>{lexer_input}, o=>{ lexer_output, contents},...). Note - i is short for inputs and o for outputs.

          4. lexer_input::= #line,
          5. line::= (directive | #(lexeme | whitespace) ) EOLN,
          6. lexer_output::= # lexeme,
          7. contents::=# directive_information,

          8. lexeme::= non_punctuation_lexeme | punctuator,
          9. non_punctuation_lexeme::= symbol | identifier | char_string | other_language_string | back_slashed_symbol,
          10. char_string::= quotation #( escaped_char | non(quotation) ) quotation,
          11. escaped_char::= backslash character,
          12. identifier::= # id_character,
          13. other_language_string::= (open_quote # non(open_quote) open_quote ),

            This allows any piece of natural language to placed into MATHS text and left undisturbed as lexical element. MATHS is designed so that formulae can be translated into the user's terminology or relate to another formal language. A formula can be defined to be an other_language_string with bound variables. The translation may be replace the variables by other strings (as in the λ calculus). Two other special forms are used to describe maps and sets of strings in a natural way:

          14. analysed_other_language_string::=open_quote # (bound_variable | lexeme~bound_variable) open_quote | other_language_map | other_language_syntax | other_language_parser.

          15. other_language_map::=open_quote # (function_symbol | lexeme~function_symbol) open_quote.
          16. function_symbol::=|[t1,t2:Type]variable(t1^t2).
          17. Examples::={ the (1st) sat on the (2nd), the parents of (_), ...}

          18. other_language_syntax::= open_quote # ( BNF_symbol | lexeme~ BNF_symbol ) open_quote.
          19. BNF_symbol::= less_than identifier greater_than.

            Example

          20. grep <options> <regular expression> <files>.
          21. other_language_parser::= open_quote # ( BNF_symbol | BNF_pair | lexeme~ BNF_pair~BNF_symbol ) open_quote.
          22. BNF_pair::=less_than identifier colon identifier greater_than.

            Example

          23. ( <car:list> <cdr:list> ). BNF-style brackets (brockets, ⟨ , ⟩) are not used outside these special strings unless they are escaped since the less-than and greater-than symbols are used for other purposes. See l_bnf and r_bnf below.

          24. back_slashed_symbol::= back_slash #non(whitespace_character) & (nroff | TeX | AMSTeX | ...),

            MATHS has half-a-dozen special brackets represented with backslashes, but permits the use of nroff, troff, TEX, and AMSTeX symbols for non-ascii characters such as Greek letters and mathematical symbols(For example α, Α, ∈, Σ, ∪,...).

          25. whitespace::= # whitespace_character,
          26. symbol::= symbol_character # symbol_character ~ (# symbol_character dot),
          27. symbol_character::= equals | lessthan | greaterthan | tilde | asterisk | plus | minus | ampersand | bar | slash | colon | dot,

            Group_chars can be used together or alone(examples: =>, ->,|-, ||). At different points in a piece of documentation different groups are defined. If whitespace is omitted then even a sophisticated context dependant syntactic analysis will fail to divide a group up into meaningful sub_groups.

          28. id_character::= letter | under_line | prime | digit,
          29. prime::= apostrophe,

          30. punctuator::= brackets_etc | comma | semicolon | hash | dollar | at_sign | circumflex | percent | query | exclamation | period, Punctuators tend to be used by themselves.
          31. brackets_etc::=l_brace | r_brace | l_bracket | r_bracket | l_parenthesis | r_parenthesis | l_bnf | r_bnf | l_semantic | r_semantic | l_meta | r_meta.

          32. period::= dot whitespace, Notice that a "." that is inside a string, or is not followed by white space is not a period but a group character.

          33. l_bnf::=backslash "<". r_bnf::=backslash ">".
          34. l_semantic::=backslash "[". r_semantic::=backslash "]".
          35. l_meta::=backslash "{". r_meta::=backslash "}". -- these are not used since in TeX "\{" symbolises "{" etc.

          36. left::= l_parenthesis | l_brace | l_bracket | l_bnf | l_semantic | l_meta,

          37. right::= r_parenthesis | r_brace | r_bracket | r_bnf | r_semantic | r_meta.

          38. left_right_pair::@(lexeme,lexeme)= l_parenthesis r_parenthesis | l_brace r_brace
          39. | l_bracket r_bracket | l_bnf r_bnf | l_semantic r_semantic | l_meta r_meta.


          40. |-pre(left_right_pair)=left and post(left_right_pair)=right.

          41. whitespace_character::= SP| HT | CR | LF | FF | VT|...,

          42. formula_in_a_different_language::= other_language_string.

            The type of a formula in a different language has to be determined by its context - either in a definition ( L::Sets=Elevators) or by using a type as a function - my uncles.@people or @people(my uncles).

            3.6.2 Structure of Documentation

            MATHS is not a markup language. Marking up a text for publication should be a service provided by a MATHS support environment. However a recent paper has shown that source code documentation (1) organized in a book like structure (chapters, sections,...), (2) Printed with italics or boldface indicating defined terms, and (3) not laid out in the traditional indented style is significantly easier to understand than the norm for source code [Baecker & Marcus 90, Oman & Cook 90, Van Wyk 86-88]. Therefore MATHS lets the user indicate the format, structure and content of a piece of documentation by using directives. Information about these named parts, their scope etc is produced by the lexical analysis process as a contents list for the document. Each item in the contents list comes from a directive and has the level number, an identifier (a name or number)and a position in the text ( line or character numbers, possibly a unique tag ).

            The rest of this section is based on the definitions in the MATHS manuals. [ notn_5_Form.html ]

            MATHS allows, but does not define, directives like those found in the roff family of text preparation systems.

          43. directive::= blank_line | O(".Open" | ".Close" | ... )#("." format) whitespace name eoln,
          44. blank_line::=#whitespace eoln,
          45. format::=#non(whitespace),
          46. name::=#non(EOLN),
          47. directive_information::=(level_number | ) ( name | sequence_number ) position_in_text.

            The name part of a directive enables the parts of the input to be referred to by name. The name normally applies to until the next name. If prefixed by an ".Open" then it extends down to the matching ".Close". The Open/close directives increase and decrease, respectively, the level of the piece of the document.

            Formats describe a desired high-level look of parts of the text but do not specify detailed fonts, layouts, etc. These formats contribute to the readability of MATHS without changing its formal meaning. Thus given an outline, with directives either blank or looking like this ".Open name" and ".Close name" and a decision about the desirable format for each level then the formats can be inserted automatically to make a first draft. The formats can be removed to abstract the outline. Local software can be developed to translate formats plus syntax analysis into \TEX, nroff/troff, and Postscript for the house style. Translation to a SGML form such as HTML can be automated.

            Example Formats Abstract, ASCII, As-is, Chapter_heading, Code, Digraph, Diagram, DFD, Equation, ERD, Example, Exercise, Experiment, Interview, Figure, Footnote, Graphic, Head_line, Joke, List, Matrix, Motivation, Name, Note, Observation, Outline, Paragraph, Quote, Reference, Remark, See_also, Section_head, SADT, Source, Spec, Subject, Table, VDM, Verbatum, Z. A collection of formats can be given for a piece of text indicating inclusion of multiple views of the same data. A formatting directive can be put in front of a definition to indicate a desirable presentation [Chapter 5] for that definition. Further the ".See" directive indicates a hypertext link (using the Universal Resource Locator (URL) format). Finally special directoves indicate the place to collect, generate, or include information in place of the directive:

            Example Insertions Index, Include, Bibliography, Contents, Cross_references, Company_Logo, Time_stamp, Date_line, By_line, Used_by, Address, Copywriter, Disclaimer, Author_Signature, Author_portrait, . . .,

            The ideal support system for MATHS will include automatic content lists, and outlines, plus indexes and cross-reference lists of definitions and declarations. In interactive mode it will allow selective searching and viewing of documents as an outline and with hypertext links. It will automatically prepare highly readable hardcopy in the "house style" while preserving the hidden ASCII code.

            3.6.3 Names

            Documentation gives names to things. A natural name is an unabbreviated phrase in a natural language with spaces replaced by an underline symbol. It will be constructed from words that are in a dictionary of that language. However to keep formula and proofs manageable, short algebraic "variables' or symbolic names are used [MacLennan 79].

            A MATHS environment needs to be able to keep an index of names that are current. As a general convention natural names should have a wider scope than variables.

          48. indexed::finite@name, the index is a set of names, partitioned into
          49. indexed>=={bound_names, declared_names, defined_names, used_identifier}, A name that is not in the index is free:
          50. free_names::=name ~ indexed.

          51. name::= symbolic_name | natural_identifier,
          52. variable::= symbolic_name | variable_structure,
          53. variable_structure::= R(variable) |P(variable), where
          54. For X:@#lexeme,
          55. R(X)::="(" identifier "=>" X #( comma identifier "=>" X) ")",
          56. P(X)::= "(" X #( comma X } ")".

          57. symbolic_name::= (mathematical_symbol #(subscript|superscript)) &
          58. (bound_symbolic_name | non_bound_symbolic_name),

            At each point in a piece of documentation there exists a set of bound symbolic names (in the current index). Bindings, definitions and declarations add to this set. Variables are removed at the end of their scope. At the start no names are bound.

            A binding always creates a new variable or name - even when the symbol or identifier is already bound. The old meaning is recovered at the end of the new symbols scope. Variables are uniquely identified by their name and the place where they were bound.

          59. mathematical_symbol::= letter | group | back_slashed_symbol | (identifier & mathematical),

            A mathematical symbol can be a character in another alphabet represented, in ASCII, by a word - typically prefixed by a backslash. Notice that in keeping with mathematical tradition single character identifiers are used for local variables. Identifiers like 'sin', 'cos', 'abs', 'sinh', 'asin', 'sqrt', 'pr', 'id'... etc can also be found in mathematical dictionaries, and can be used as mathematical symbols. Significantly they are not typeset as variables however (in italics). Thus there is an exception to the rule that names that are words must be in a standard dictionary. A (short) dictionary of mathematical words can therefore be included as part of a document - and a tool should be made that scans a document and extracts names that are defined but are not in the standard dictionary.

          60. subscript::= digit # digit | "[" expression"]", subscripts should be type set below the line.
          61. superscript::= prime. Re-use is easier when natural names are used. However algebraic abbreviations are needed inside a piece of documentation. Hence it is wise to have two names for all ideas that can be referred to by other people. The short one for local algebraic use and a long one is for the users of the documentation. Note that identifiers that are bound within a formula and so local must be algebraic variables.
          62. natural_identifier::= word #(underline word)
          63. & (declared_identifier | defined_identifier | unknown_identifier) The words should exist in a standard a dictionary of the user's and client's natural language or can be numbers. The use of underline to link words is incompatible with TEX conventions for mathematical typesetting. A preprocessor that outputs TEX must therefore escape underlines within natural identifiers. It will also have to indicate formatting of sub- and super-scripts.

            Strings like "I" and "a" are ambiguous - they are both in the English dictionary and are algebraic variables. Within a formal piece of documentation variables are taken to be algebraic variables. Within informal commentary most characters are taken to be comments - unless they are enclosed in reversed_quotes ("`").

            3.6.4 ASCII Codes

            Here is part of the MATHS handbook that documents the ASCII code - the complete document includes the ASCII names(HT,LF,VV,...), numerical coding and the symbols in C and Ada programs[cf Vassiliou & Orenstein 92].

          64. ASCII_CODE::=
            Net{
              ...(definitions of control codes deleted) Definition Definitions using term (Notes) ---------------------------------------------------
            1. SP::=" ", sequence, whitespace (E)
            2. exclam::="!", concatenation, put, push (E)
            3. quotation::="\"", character_string
            4. sharp::=hash::="#", phase, Types, any_number_of, sequence_of
            5. dollar::="$", documentation, structures, set
            6. percent::="%", n-tuples, lists(M,P,E)
            7. ampersand::="&", intersection(E)
            8. apostrophe::="'", prime, id_character, Dynamic Predicates, ADA (E)
            9. left_parenthesis::="(", expression(E,M,P,N)
            10. right_parenthesis::=")", expression(E,M,P,N)
            11. star::="*", group, expression(E,P,N)
            12. plus::="+", group, expression(E,M,P,N)
            13. comma::=",", extension, bindings, lists, parameters(E,M,P)
            14. minus::="-", group, arrows, expression(M,P,N)
            15. dot::=".", group, expression(M,P,E,N), see period below
            16. slash::=divide::="/", converse relation, quotient(M,P,N)
            17. colon::=":", group, declaration, definition,
            18. binding,infix(P,E)
            19. semicolon::=";", punctuator, relation, ADA, C, BNF, PDL(P,E)
            20. less_than::="<", group, arrows, ORDER(M,P,N)
            21. equal::="=" , group, arrows, assignment, logic.equality(M,P,NN)
            22. greater_than::=">", group, arrows, ORDER(M,P,N)
            23. query::="?", get, pop, prefix (E)
            24. at_sign::="@", collection,logic.collection, Type
            25. l_bracket::="[", subscript
            26. backslash::="\", escaped_character, backslashed_symbol
            27. r_bracket::="]", subscript
            28. circumflex::="^", Types, Logic.Maps, superscript
            29. underline::="_", name, id_character
            30. grave::="`", formula_in_a_different_language(E)
            31. l_brace::="{", set, item, structure, documentation
            32. bar::="|", union
            33. where_symbol::="||", set
            34. r_brace::="}", set, item, structure, documentation
            35. tilde::="~" , group, logic.Set.complement
            36. period::="." whitespace, A dot followed by white space is a period.

              Notes

            37. E - English punctuation symbol
            38. M - Mathematical symbol
            39. P - Used in most High Level Programming Languages
            40. N - Not in ASCII package in Ada reference Manual ...
            41. group - See Section 6.1, page 118 above. }=::ASCII_CODE

            . . . . . . . . . ( end of section 3.6 Applications in MATHS) <<Contents | End>>

            3.7 Meaning of Recursion

              3.7.1 Recursion

              In the absence of recursion (direct or indirect) the meaning of MATHS definitions are in terms of well known mathematics. Few practical problems have complex recursion and left and right recursive definitions (such as 'A::=x y z A|...' and 'A::=A x y z|...') are more naturally expressed in terms of the '#' operation. For example in the whole of data processing only BOMP(Bill Of Materials Program) is naturally recursive. However in computer science recursion is ubiquitous - trees, lists, recursive functions,... Recursion arises naturally in defining languages and data structures however. A set of recursive definitions may or may not define a unique solution. Section 7.2 is an annotated bibliography of papers that establish a theory of convergence for sets of strings. The theory proves the uniqueness of the language defined by a context free grammar. This is a paradigm for other recursive forms.

              Here is an example:

            1. FACTORIAL::=Net{ Use INTEGERS. |-For A:Finite_Set(Nat0), *A =Π{ a:Nat0 | a A}.
            2. -- Integers include mathematical induction:-
            3. |-INDUCTION=following
              Net
              1. Net{
                  P:Nat0->@, P(1), for k:Nat0, if P(k) then P(k+1).
                1. |-for all n:Nat0(P(n))

                (End of Net)

              2. For n:Nat0, n!::=n factorial::=if n>1 then n*(n-1)! else 1.
              3. |- (fac): n!=*(1..n).
                Let

                1. (*)|- (fac1): *(1..1)=*{1}=1=1!.
                2. ()|- (fac2): for all n:Nat0 , if n!=*(1..n) then (n+1)!=*(1..n+1),
                  Let
                  1. n!=*(1..n).
                  2. ()|-(n+1)!=(n+1)*(n!)=(n+1) * (*(1..n)).
                  3. ()|-*(1..n+1)=*(1..n || {n+1})=*(1..n)*(n+1)=(n+1) * (*(1..n)).
                  4. ()|-(n+1)!=*(1..n+1)

                  (Close Let )
                3. INDUCTION(P=>map[n]( n!=*(1..n)) ).

                (Close Let )
              4. ... }=::FACTORIAL

                The above shows how the special theory of integers contains an assumption that leads to proving that a definition has meaning. Sometimes instead of an induction axiom there is a model of convergence and limits - a topology. Scott's work on domains points to a theory which assigns meanings to recursive definitions in general. Details will be presented in Chapter 5. Section 7.2 is a survey of the publications that establish theories enabling the existence and uniqueness of solutions to recursive equations in MATHS grammars.

                3.7.2 Topology and Syntax

                Here is a partial annotated bibliography of theories of convergence for sets of strings. These work by establishing a measure of the difference between the objects generated by a grammar or set of definitions or iterative process. This is shown to be a metric - in the mathematical sense (not a software metric![Fenton 94]). Brower's theorem shows that contracting maps on metric spaces tend to a unique fixed point of the map. The idea of using a topology to establish convergence, and the original model date back to Schutzenburger's work in the 60's[ Schutzenburger 62a & 62b]. By 1963 a specific algebra and metric space had been developed for discussing context free grammars. The algebra was that of semi-rings of power series [Chomsky and Schutzenberger 63]. A recent paper has re-constructed a combined Kleene-Schutzenburger Theorem [Sakarovitch 86].

                In '67 Eli Shamir published a major theorem which uses the theory developed by Schutzenburger [Shamir 67]. He refers to Chomsky and Schutzenberger and uses a similar definition. He uses the idea that the coefficients of the power series generated by a grammar become constant as the iteration proceeds.

                A conference at Asilomar in California (1966) seems to have included early attempts to use topology in computer science[Bill Nico(CSU Fresno), Personal communication]. An expert on topological semigroups [J.M.Day] gave invited lectures which lead to a burst of publications on the theory of languages and automata. Arbib's book[Arbib 68] publishes some of the papers including one by E. Shamir [pp329-341] and J.M. Day's "Expository Lectures on Topological Semigroups" [pp269-294]. Shamir's paper refers to Schutzenberger's papers [1962, 1963] and avoids topology. Day's chapter is a presentation of topology and semigroups with no visible computer science. The appendix lists other 40 or 50 other papers from the conference that were published in "Math System Theory", "Computer and System Science", and "Information and Control" during 1967 through 1978 including Shamir's 1967 paper.

                S. Eilenberg's Magnum Opus(Eilenberg 74) is algebraic. He starts(Chapter VI) by assuming a total finite and infinite summation function. He credits Schutzenberger [1962] for the introduction of power series. Eilenberg has a tantalizing phrase(p158) "Subsequent publications of Schutzenberger and several of his associates..." but doesn't mention who or where they were... . Research discovered Schutzenberger's group was/is at the LITP in Paris University ( 2 place Jussieu Paris 7505, France). Names included: Dominique Perrin, Michel Fliess, Jean Berstel, M Nivat etc, who have proceeded to interesting work on infinite strings[for example Nivat & Perrin 84]. In this a sequence of equivalence relations are defined and hold between power series when the coefficients of all words of length n or less are equal. They define limits in terms of the equivalences. The LITP group contributed much to Leeuwen's 1990 Handbook.

                Salomaa and Soittola[1978] is a good survey of the whole area of formal power series as of 1978. They define the metric space on the power series by

              5. if x=y then d(x,y)=0
              6. else d(x,y)=2^- diff(x,y),
              7. where diff(x,y)=min {length(w) || not (Coef(x,w)=Coef(y,w)) },
              8. where Coef(x,w) = coefficient of word w in power series x. -(1) Also see W Kuich and A Salomaa [1986]. Salomaa's chapter in "The Handbook of Theoretical Computer Science" [Volumes B, Chapter 3, Leeuwen 90] is an up to date summary of the theory of grammars and power series.

                A graduate text by Manes and Arbib[1986] uses categories, posets, and metric spaces to prove that sundry iterative and recursive processes define a unique object. They describe a metric on languages without using power series [pp212, Chapter 9, section 1, paragraph 6]. They give Padulo & Arbib [1974] and Bloom[1983] as sources. Bloom uses metrics and Banach's theorem to prove convergence in a space of infinitely long strings of characters.

                A similar formula to (1) above is given by E-E Doberkat [pages of 289-302 of Main et al. 88]. Several other papers in this conference use topological ideas[Main et al. 88]. For example: Reed and Roscoe's paper uses

              9. d(x,y)=inf {2^(- t) || for some t:Time , where for all t'<t, x(t')=y(t')
                }.
              They state that this is a complete (ultra-)metric for a timed version of CSP. Similar results have been published for Process Algebra [p9 of Baetan 90 by J A Bergstra &J W Kop].

              3.7.3 Topology of Semantics

              Dana Scott's Turing award lecture is an introduction to this area [ACM 87]. Manes and Arbib give many rigorous examples of this form of reasoning. Mili et al. have a clear presentation of the theory [ Mili et al. 89]. The purpose is to establish the necessary and sufficient conditions for a set of definitions to define unique meanings. Typically this is a case of showing that an iterative approximation gets as close as we please to a particular value, which happens to be the fixed point of a recurrence relation equivalent to the set of definitions. Kleene's theorem is an early special case [Kleene 56]. The Tarski- Knaster theory of complete partial orders has proved to be very useful in recent years [Tarski 53]. Gordon Plotkin applied this to construct a domain of sets and mappings [Plotkin 76]. To model recursive data structures one of the more complex "power domains" are needed[Schmidt 86].

              The connection with Dana Scott's use of topological function spaces as semantic domains with the topology of languages has been investigated in the last 10 years or so - apparently starting with a "Continuous Lattices" conference (1973?) which resulted in a book by that name published by Springer Verlag. Melton and Schmidt state that the Scott topology is the Tychonoff topology on the function space (the weakest one with continuous function application) [Mellor 1985]. Brower's theorem has been used to show that many types of constructed objects have sets with a natural metric [Bloom 83]. Similar techniques are used to compare semantics for concurrent systems[Kok & Ruuten 90]. Appendix 1.GENESYS defines a natural metric for sets of constructable objects.

            . . . . . . . . . ( end of section 3.7 Meaning of Recursion) <<Contents | End>>

            3.8 Review

              3.8.1 Summary

              I have shown that adding the intersection operator to EBNF makes EBNF more powerful, but parsing and recognition stay within modern programming technology. This provides a reason for Jackson's use of parallelism and system network diagrams(Chapter 6). I have defined both normal and concurrent grammars. I have argued that languages should be defined as the intersection of lexical, syntactic and semantic constraints, and extended by definitions. I have also shown how using other formal systems within the EBNF model leads naturally to more powerful ways to define languages. I included examples taken from the definition of MATHS. I have shown that this approach brings syntax closer to semantics. I have also given examples of how a formal description of the problem domain and the syntax of the data leads to the structure and function of the programs needed in the domain. However, it appears that some further extensions are needed to permit logical and set theoretic definitions.

              3.8.2 Conclusions

              (1) The structure of a process with a single input can be determined from a description of the syntax and semantics of the input. (2) The syntax and semantics of the input to a process can be determined by documenting the user's and clients' language (3) Standard grammar theory needs logic and set theory to be useful.

              3.8.3 Preview

              In the next chapter (chapter 4) I present a MATHS model of the logic needed to talk about the semantics of problem domains and formal specifications. In chapter 5 I show how grammar theory, logic, and set theory are combined into a theory of documentation covering analysis through to specification and design. In chapter 6 I fit these discoveries into current methodologies.

            . . . . . . . . . ( end of section 3.8 Review) <<Contents | End>>

          . . . . . . . . . ( end of section Chapter 3 Grammars) <<Contents | End>>

        End