[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci ] / [R J Botting] / [ ] / intro_characters
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Nov 16 11:12:00 PST 2007

# Introduction to Syntax of MATHS

## Special Characters

 @	prefix: Subsets of/Subsets defined by/SetOf
 @	prefix: Relations between...
 @	 - also  @={true,false}
 %	prefix: Numbered sequences of
 #	prefix: Strings of | any number of
 \$	prefix: Set/tuple defined by documenting its structure and properties
 &	infix and prefix: intersection of sets
 |	infix and prefix: union of sets, alternative forms of syntax a la BNF
 ^	infix and prefix: Power, superscript
 !	infix and prefix: Concatenation  of sequences/strings/files/lists/...
 ?	Prefix/postfix items  to sequences/strings/...
 :>=-<	Used to build identifiers: arrows, operators, etc
 *	infix and prefix: Multiplication
 +	infix and prefix: Addition
 -	infix and prefix: subtraction and negate
 \	Nroff  or TEX symbols for strange characters: \Sigma
 {....}	Sets defined by extension(listing) or intension(property)
 ()	Algebraic precedence, function parameters, lists
 []	Lower/subscript/\lambda/Schema
 /	infix: division
 / 	prefix: inverts functions and relations.
 ,	separate parameters, elements in lists, sets, schema,...
 .	infix: apply.  Also separates sentences in schema.
 ::=     is defined to be the same as
 ::      is declared to be of type
 :       has type
 |-      It is asserted that....  It is assumed,  or It can be shown

For more see [ notn_10_Lexicon.html ] , and [ math.syntax.html ] or below.

## Lexemes

Here is a quick list of key words used in MATHS
key wordpurpose
CloseTerminate the last Net, Set, Let, List, Open
For, forIntroduses quantifiers: all, some, 1, 0..1, ...
funFunction
LetIntroduces a temporary assumption used to prove something else
ListStart an ordered sequential list
mapIndicates a map, function, λ
NetIntroduces a collection of variables and constraints
OpenOpen a subsection of the document
relRelation
RowAn n-tpl of items separated by tabs in a Table
Set, setIntroduces an unordered set of items
TableA table: an relation defined as a set of rows

## TeX Symbols

Maths permits the TeX convention of putting "\" before a word to indicate a symbol. Some of these are handled correctly when mapped to HTML, see [ ../samples/tex2html.html ] for the mapping.

## Syntax

A MATHS document has many pieces,
1. document::= #piece_of_documentation.

Some pieces are sections (see Structure) and other are elementary:

2. piece_of_documentation::= section | elementary_documentation.
3. elementary_documentation::=#(formal | break | directive | gloss | (label| ) comment ).
4. formal::=formula | formal_definition | declaration | assertion.
5. definition::=formal_definition | gloss.
6. formal_definition::=(for_clause (condition | ) | )term"::"(context | )"="expression ender,
 		pi ::real= 3.14159.
 		paragraph_tag ::= "<p>".
7. gloss::= term "::"(context | )"=" (balanced ~ expression) ender.
 		pi ::real= ratio of circumference divided by radius.
8. balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
9. ender::= "." | ",".
10. declaration::= (for_clause (condition | ) | )term"::"context.
11. assertion::=axiom | theorem.
12. formula::= indentation ( label | ) well_formed_formula.
13. axiom::= (indentation | ) "|-"( label | ) well_formed_formula.
14. theorem::= (| indentation ) ( evidence ) "|-" ( label | ) well_formed_formula.
15. label::= "(" identifier "):".
16. context::=expression describing a type or set of possibilities.
17. break::= blank line.
18. indentation::=a tab at the start of the line followed by spaces and tabs.
19. paragraph_indentation::= a space indicates an item, element, or bullet point.

For more see [ math.syntax.html ] and [ notn_13_Docn_Syntax.html ] and [ notn_14_Docn_Semantics.html ] and [ notn_15_Naming_Documentn.html ]

## Structure

21. section::=simple_section | open_close_section | local_section. simple_section::= header_line #(paragraph | blank_line | insertion).

22. header_line::="." white_space name #whitespace eoln,

25. open_close_section::= |[H:name](open(H) #piece_of_documentation close(H))
26. open::syntax->syntax=".Open" SP (_) eoln,
27. close::syntax=".Close" O(SP (_)) eoln.

28. local_section::= |[T:"." type_of_section]( T eoln #piece ".Close" T eoln).
29. type_of_section::= {"Let", "Net", "Box", "List", "Set", "Table", ...}.

## Expressions

(expressions): All functions can be used in prefix, postfix, and infix form. Functions are overloaded. In particular predefined operators are apply to sequences and sets. Some are serial (for example +(1,2,3)=1+2+3), while others act in a parallel (for example <(1,2,3)=1<2 and 2<3 and 3<4).

For more see [ notn_11_Names.html ] and [ notn_12_Expressions.html ]

. . . . . . . . . ( end of section Introduction to Syntax of MATHS) <<Contents | End>>

# 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

1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

# Glossary

2. 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).
3. given::reason="I've been told that...", used to describe a problem.
4. given::variable="I'll be given a value or object like this...", used to describe a problem.
5. goal::theorem="The result I'm trying to prove right now".
6. goal::variable="The value or object I'm trying to find or construct".
7. 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.
8. hyp::reason="I assumed this in my last Let/Case/Po/...".
9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.