The terms used to talk about the language - forming its meta-language - are separate set of symbols(N), that does not overlap with T,
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.
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:
| 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 |
| ... | ... |
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:
Notice that this implies that D["L"] is automatically defined on sets of strings:
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 A,B: sets of strings,
.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 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 example, the grammar
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:
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