[Skip Navigation] [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >> math.lexicon
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri May 12 10:09:54 PDT 2006


    Lexemes for MATHS

      Informal Introduction

      [ comp.text.ASCII.html ]
    1. digit::="0".."9",
    2. letter::=lower_case | uppercase,
    3. lower_case::="a".."z"
    4. upper_case::="A".."Z".

      There is a one-to-one correspondence between the lower case letters and the upper case letters. This is not exploited in the MATHS notation but recorded here for completeness and so people can use it in their own documents:

    5. to_upper::#char>->#char, map lower case into upper case.
    6. to_lower::#char>->#char, map upper case into lower case.
    7. ignore_case::#char>->@#char.

    8. eoln::= #whitespace (ASCII.CR | ASCII.LF) #whitespace.
    9. break::= eoln eoln #eoln, -- two or more eolns can break comments up into paragraph.
    10. indentation::= ASCII.HT #white_space_char, indicates a formula.
    11. paragraph_indentation::= ASCII.SP #white_space_char, indicates a break, item, bullet point, or element.

    12. quote::="\"", -- a backslash changes the meaning of the next char exactly as it does in ANSI C.
    13. backslash::="\\" -- as in C a backslash is an escape character and so two are needed to represent one.

      Formal statements are distinguished by the presence of the double colon some where in the line or else by white space character at the start of a line:

       	::=	is defined to be the same as
       	::	is declared to be a
      Indented formula can be labeled:
       		(label):	display and name a formula, if indented at start of line
       	(label):		Allows a label to be attached to an informal statemnt.
       	|-(label):	State an assumption or axiom.
       	(reasons)|-(label):	assert a provable theorem
      In a logically complete document for each provable theorem labeled l has a proof in a section headed ".Proof of l". All the steps in the proof are either standard (and well known) or are listed as reasons. The reasons will all be labels of formula that have appeared previous to the statemnt of the theorem.
       	|- yada::=		Indicates a definition has already been introduced.

      The ASCII characters "@#$ ^&|~" are used in place of written symbols used in discrete mathematics:

       	&	intersection
       	|	union/alternate syntaxes
       	~	complement
      [ logic_30_Sets.html ]
       	@	Subsets of/Subsets defined by
      [ logic_31_Families_of_Sets.html ]
       	#	Numbered sequences of
      [ logic_6_Numbers..Strings.html ] [ math_62_Strings.html ]
       	$	Structured Set/Set defined by documentation
      [ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ]

       	^	Power, raise up, superscript

      Parentheses, Brackets and Braces

      	{}	Sets, alternately use SET(...)
       	()	Order of operations, lists, sequences, function application
       	[]	Lower/subscript/map from, else use MAP[...]
       	\<...\>	BNF Brockets
       	\[...\]	Semantic brackets

      Additional non-ASCII symbols a described by using any of nroff or TEX code or by concatenating these symbols "~-*><:=." together. Here are some special arrows and crosses

       	+>	Maplet
      	->	Mappings and functions
      	<>->	Partial Mappings and functions
      	><	Cartesian and Cross Products

       	=>	Substitution

       	<=	Less than or equal
       	>=	greater than or equal
       	<>	not equal (Pascal and BASIC)

       	==>	subset
       	=>>	proper subset
       	>==	partitioning
      [ logic_30_Sets.html ]

      	||	"where" in intensional set descriptions {x:T || P}
      	.	"where" in intensional set descriptions {x:T. P}

      The slash("/") is used as a prefixed inversion/converse operator, rather than having "^{-1}" afterwards - it can be thought of as a generalised "root" symbol(sqrt=/(^2)), or possibly being short for "arc" (arcsin=/sin).

      Lists, strings, and sequences can be treated as functions. Functions as relations. For example (a,b,c) = ( 1+>a | 2+>b | 3+>c). Further they can be inverted, so that for example: /(a,b,c) = ( a+>1 | b+>2 | c+>3 ).

      All functions can used in prefix, postfix and infix form and are overloaded to also apply to sequences and sets of elements.

      However some functions have a serial interpretation (for example +(1,2,3)=1+2+3), while others have a parallel interpretation (for example <(1,2,3)=(1<2<3)=(1<2 and 2<3)). This obviates the need for special signs for the same operations(with apologies to Lagrange who was the first to use \Sigma where MATHS uses "+").

      Identifiers can be used for variables, constants, functions, operators etc. however there are two kinds of identifier. The mathemaatical is short and used locally in algebraic formula - for example "x", "\lambda", ... The others a longer and made up of words in the client's language. These have a wider scope and should indicate their meaning clearly, if at all possible. Here are some special identifiers with predefined meanings:

      	and	Boolean conjunction
      	or	Boolean inclusive disjunction
      	if	Start of conditional
       	then	Separates premise from conclusion in conditional
      	for	Introduces a series of quantifiers
       	all, some, one, no, 1,2,3,4,...	Quantifiers
       	not	Boolean complement
       	the	definite description of an object

      Formal Treatment

      [ notn_10_Lexicon.html ]

    . . . . . . . . . ( end of section Lexemes of MATH) <<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, and give them a name. 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.

    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 complete listing of pages by topic see [ home.html ]