- Form of a grammar
- Meaning of a grammar
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- T::Sets=given set of terminal symbols.
The terms used to talk about the language - forming its meta-language - are separate set of symbols(N), that does not overlap with T,

- N::Sets=given set of nonterminal symbols
- |- (disjoint): T & N = {}.
A grammer generates the strings in its language by replace non-terminal symbols by terminal ones. This is why we use the tem terminal vs non-terminal.

The grammar has a vocabulary V made up of symbols in either T or N.

- V::= T | V.
The vocabulary V is split into the
terminals or elements (T) and the defined terms or nonterminals (N).
The rules describe a collection of operations or functions that take a string of symbols from both N and T and changes it to another one. The rules only apply when the string has at least one non-terminal and typically replace it by a string of terminals and nonterminals.

Context free grammars ( CFG ) have rules are expressed as a definition of a single nonterminal as a string of terminals and nonterminals: example

L::=a L b.

for example. The mapping substitutes the nonterminal by the string. For example the above rule describes a mapping/function/operation that can do things like the following:**Table**Before After L a L b a L b a a L b b a a L b b a a a L b b b ... ...

(Close Table)

A MATHS grammar gives each term n in N, a formula that defines n in terms of the nonterminals m1,m2,... (which may include n itself) and some terminals(D[n](m1,m2,...)), using the following operations "(&|~#)".In the above example defines "L" in terms of "a", "b", and "L". So the L-rule is to replace a string x by "a" x "b". Thus:

- For all x, D["L"](x) = "a" x "b". or
- D["L"] = λ[x:V]( "a" x "b").
Notice that this implies that D["L"] is automatically defined on sets of strings:

- D["L"] = λ[A:@V]( { y:@V || for some x:A (y = "a" x "b")}).
# Meaning of a grammar

Each terminal and nonterminal represents a set of strings of symbols in an alphabet or vocabulary.

There are several models of strings and some have been translated into MATHS [ intro_strings.html ] [ logic_6_Numbers..Strings.html ] [ math_61_String_Theories.html ] [ math_62_Strings.html ] [ math_66_SuperStrings.html ] But for now I assume in the theory of grammars that strings are generated by starting with an empty string ("") and a putting symbols (in T) onto it using concatenation operation (!).

The pre-defined operations of union('|'), intersection ('&'), complementation ('~'), concatenation, and iteration (#) on sets of strings: I treat a string as a set when the context requires it. A string s is cast into the singleton set {s} when necessary.

- For s:string, s::sets of strings = { s }.
For A,B: sets of strings,

- A B ={c || c=a!b and a in A and b in B},
- A & B ={c || c in A and c in B},
- A | B ={c || c in A or c in B},
- A ~ B ={c || c in A and not( c in B) }.
.Note { x || P} is short for the set of x such that P is true. [ intro_sets.html ] [ logic_30_Sets.html ] [ logic_32_Set_Theory.html ]

The Kleene closure operator (#) can be read "zero or more of" and can be defined as the smallest set of strings that contains the null string and the results of concatentaing one of the elements of the set onto the closure:

- #A =least{ X || X=({""} | A X) }.
'#' could be defined many other ways. In MATHS it is a standard
operator.
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:

- For all n:N, M(n) = D[n](M(m1),M(m2),M(m3),...),
For example, the grammar

- Net{ L:="" || a L b } defines L to be the smallest set of strings such that
- M(L)={""}| {c || for some x in M(L) (c =a!x!b)}
This definition does not tell us how to find the M's, neither does it prove that they exist nor whether they are unique. Finally the term 'smallest' has not been defined. It can be shown, for a wide class of grammars (see later) that we can get as complete a listing of the M's as we like by a simple process:

- Initially, for n:N do M(n)={}.
- Iteration the following steps as often as you want:

Net

For example, with - Initially, for n:N do M(n)={}.
- { L:=""| a L b }
gives as successive approximations to M(L) as the following sets:

Net- {}
- {""}|a{}b = {""}
- {""}|a{""}b = {"","ab"}
- {""}|a{"","ab"}b = {"","ab","aabb"}
- {""}|a{"","ab","aabb"}b = {"","ab","aabb","aaabbb"}
- {""}|a{"","ab","aabb","aaabbb"}b =
- {"","ab","aabb","aaabbb","aaaabbb"}
- ...

(End of Net)

It seems intuitively obvious that these sets are `tending towards a limit`: - M(L)={a^n!b^n||n:0..}.
The reason that these seem to converge to M(L) is that we have to look at longer and longer examples of strings in L to find one that has not been generated by the iteration. The discrepancy between the iterates and M(L) are getting longer and longer - More formally, if we itterate long enough, then the iterates will match the limit up to any preselected length.

# Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

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

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

# Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.For a more rigorous description of the standard notations see

- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

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