Sections 4, 5, 6 and 7 discuss new ways to define languages in preparation for defining a complete documentation system in chapter 5.
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>>
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.
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:
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].
Syntax.
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:
We now define the meaning of the set of productions constructed from a particular type of grammar:
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.
The generated language is smallest invariant language or fixed language under repeated substitution:
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 ].
...[parsing, see later and Aho & Ullman]
}=::CF_GRAMMAR
Normally, in MATHS and Language Reference Manuals, we use the grammar to determine N and T:
Therefore
The get some input relation, x? is defined by
It follows that
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.
Dictionary | Example | Relation Notes | |
---|---|---|---|
definition | aEBNFdefiner b | C_aEBNFdefiner B | B is the transform of b. |
terminal | t | t? | t is removed from front of i |
non_terminal | a | C_a | C_a is a relation that consumes all of a |
sequence | a 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 | #a | do(A) | Where a transforms to A |
P::=( a P b | #c)becomes
C_P::=(a?; C_P; b? | do(c?))by applying the above transformations.
To show
(correct2): accepted_by(C_P)==> P.
Let
. . . . . . . . . ( 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:
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.
Table
Dictionary | Relation Notes | |
---|---|---|
intersection | a&b&c... A&B&C&... Where a,b,c...translate to A,B,C,... | |
complement | a~b A ~ B | Where a and b translate to A and B. |
For instance consider:
Converting this dictionary into an acceptor with two processes gives:
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.
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:
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>>
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].
CCFG = CG and context_free.
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.
Liu and Weiner remark that trivially
Clearly,
Therefore,
Similarly
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
It is interesting to note that all the other languages formed by permuting terms are all CFL^1 or CFL^2:
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
A similar argument shows that if L in CFL^p for some p, and t some terminal then
CFL^n is accepted by n parallel non-deterministic PDAs. Hence it follows that
CFL^n is closed under:
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
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
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
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
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).
Philippe Schnoebelen circulated the Theory-Net on the BITNet(comp.theory on Usenet) with an interesting result equivalent to the observation that
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.
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
and so this non-Chomskian grammar
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>>
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
Strings | Rules |
---|---|
Lexical | A Lexical grammar or Lexicon |
Grammatical | A set of Syntaxes |
Meaningful | A set of maps from Grammatical strings into Meanings |
Defined | Definitions map Lexical strings into Meaningful strings |
Net
Syntax
Semantics
(=[13])::=equivalent modulo 13 ::= ( = mod do(_+13)).
Pragmatics We show that the requirement that a single change in a digit can be detected has been met.
Proof
Let
So the meanings of any two meaningful identifiers are equivalent modulo 13:
Now for all meaningful decimals d, if just the i.th digit is changed (to e say)
then the result is not meaningful.
Proof
Let
Note: We had to explicitly list the meanings of the digits:
The syntax of MATHS is defined by several grammars. The valid strings must fit all these grammars and the lexical constraints.
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.
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.
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.
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:
Semantic Space
Predicates
Syntax This data can be represented in English by statements like
It is easy to show that:
Therefore
Binary is an exact 1 to 1 coding of the numbers,
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.
(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 ]
Operation | Placement 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*2 | when 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 |
The process associated with bin is therefore
hence,
. . . . . . . . . ( end of section 3.4 MATHS as a MetaLanguage) <<Contents | End>>
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.
Both forms bind values to abbreviations for the range of a single expression. So these three formulas are equal
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:
Again it should be possible to input a series of additional alternatives into a documentation processor, and have them, checked, appended, etc.
It is incorrect to use more than one ellipsis on the same term.
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 :
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]
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
So,
Another extension handles a common form of definition:
This technique leads to a way to express the context dependencies found programming languages such as Ada:
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:
If generate is a (1)-(1) map then
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].
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.
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:
Example - PARALLEL( equivalences, implication, "iff", iff, @).
For T:Types, R:@(T, T), r:#A, if symbol (r, @(T, T), R ) then
A more general form is given in Chapter 4, Section 2.2 - predicates [LPC].
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>>
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:
Example
Example
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 α, Α, ∈, Σ, ∪,...).
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.
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).
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.
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.
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.
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.
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.
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 ("`").
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].
Notes
. . . . . . . . . ( end of section 3.6 Applications in MATHS) <<Contents | End>>
Here is an example:
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.
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
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
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>>
. . . . . . . . . ( end of section 3.8 Review) <<Contents | End>>
. . . . . . . . . ( end of section Chapter 3 Grammars) <<Contents | End>>