The mathematical model of a language is a set of strings. The strings must be sequences of zero or more symbols taken froma finite set often called an alphabet.
See also
Grammar
A Grammar defines a language and imposes a stucture on the strings
in that language. Chomski invented a model for how grammars work.
A grammar describes (explicitly) rules for generating a correct
strings in a given language. If well chosen each string in the language
can be generated in essentially only one way. This way of generating
the string defines the structure of the string - how it is parsed.
No useful languages are context free - so more general form of grammars are needed. However CFGs are the commonest form of grammar use din practice.
Parameters are used to indicate correspondences across sequences, etc.
Example
Let
By default you can assume that a sequence is parsed as an array or list (of type #X for some X). Parameterized items become mappings from parameters to content(of type X<>->Y). For more, see [ notn_2_Structure.html ] [ Definitions in notn_14_Docn_Semantics ] [ notn_13_Docn_Syntax.html] , for an example of a how the formal grammar of MATHS maps into a structured objet.
Lexical
Tags should be put on sequences to indicate fields in the tokens generated
by an associated lexer. A lexer is built by associating character
input(lazy), token output and conditions with the grammar. All that is
needed is to define the special non_terminal 'lexeme'.
.Example
GRAMMAR and
The tags indicate fields in tokens input by the formatter and placed in sequence in the context of the untagged strings. A formatter is built by associating token input, character output and conditions with the grammar. The special non terminal 'output' needs to be defined.
For example:
A translation can be defined by giving two corresponding grammars. One defines the input, and the other the output. Tags indicate corresponding strings in the two grammars.
More sophisticated is to simultaneously define both the input and the output at the same time. Here each definition doesn't define a set of strings, but does define a set of pairs of strings (equivalent therefore to a relationship between two languages). A simple version of this idea will be found in Aho and Ullman Volume 1.
A parser constructs a data structure that encodes the input sequence. Each non_terminal in the grammar will have its own associated type of object in this data structure. A particular input is encoded as a set of objects which in generalwill not be a tree but a directed acyclic graph(dag). In MATHS a simple formal model is two simultanously define the abstract and the concrete syntax - (expression, expressions) ::@#Alphabet><Sets=(f:function e:delimitted | e:delimitted f:function,$ {f:functions, e:expressions}).
Clearly this involves much redundancy and so a convenient abreviation is to place the abstract syntax imediately folling the concrete syntax:
Thus sequence with tags leads to an object with tags identifying the components in it plus a special set of pointer tags identifying the object of which this object is part.
In (A|B|C|...) only one object will constructed, but it will be one of the alternative types indicated. The alternatives may or may not have overlapping component types.
In a concurrent expression the tags should all be distinct. From A & B & C ... The object is constructed by all parsings and so each concurrent part must have its own distinct tags. Thus each concurrent parsing operates on its part of the tpl, which can be implemented as a separately locked record. Thus the exact timing of the concurrent parsing is irrelevant.
In (A~B) it is assumed that B will be attempted before hand, and if it fails then its n-tpl is removed and/or replace by the n-tple (if any) described in A.
By extending the concept of simultaneous definitions two a n-ary relation between sets of input, outputs and objects a formal version of JSP is developed.
GRAMMAR(Alphabet=>Events, terminal=>Events, non_terminal::= (Pattern|Entity(|"."Role))
Grammars with embedded operations are programs.
A grammar can have operations embedded in it but they then become non-deterministic data driven programs. In this case each definition (formally) defines two sets - a language and a relation. Strings in the language also satisfy the relation.
Thus if U=$ Net{level:Nat0, S:@variables, bound_symbols:@Net{name:variable, at:Nat0, type:Types}} then we can describe the parsing of a set of bindings be a grammar on (@#Char, @(J,U)), with the properties that
(A,R) (B,S) = (A B, R;S),
(A,R)|(B,S)=(A|B,R|S),
(A,R)~(B,S)=(A~B,R~S),
and #(A,R) =(#A, do(R)).
So (binding, note) ::=|[v:variable](v, not v in S;v|:S),
(bindings, bind) ::=("",level'=level+1;S'={}) (binding, note) #((comma,Id) (binding, note)) ":" |[s:set](s,save(S,s)),
[ Data directed Design] .
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 = Net{radius:Positive Real, center:Point}.
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