[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng ] / [R J Botting] / [ ] / notn_11_Names
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue May 19 06:47:20 PDT 2009

# Names

## Idea

Documentation gives names to things. This may be its most important function.

Algebra and natural languages have two different paradigms for creating names[Gr??, SIGPLAN]. Thus "x" is clearly an algebraic name, and "cats" an English name. Programming languages do not include a list of valid English words because they predate the existence of spelling checkers and because of the divine right of programmers to confuse their colleagues.

MATHS allows both to be used in formulae. A natural MATHS name is an unabbreviated phrase in a natural language with spaces replaced by an underline symbol. It will be constructed from words that are in a dictionary of that language. However to keep formula and proofs manageable, short algebraic variables or symbolic names are needed.

## Style Guide

Use algebraic or symbolic names for variables bound inside a definition or formula(local). Use natural identifiers when they are declared in a piece of documentation and shared across two or more formulae (public). Avoid short global identifiers unless you are working with complex formula and proofs or the identifier is already in use.

## Example

Net
1. Set::Sets.
2. op::infix(Set).
3. for all a,b,c:Set( a op (b op c) = (a op (b op c)).

(End of Net)

In the above Set, op are public and a,b, and c are local. The words "Sets", "infix" are defined in the STANDARD MATHS package. Words like "for" and "all" are part of the MATHS language.

## Introduction to Syntax

A local or private name is always introduced by a private/local declaration or definition with the following syntax:
1. variable ":" set_expression
2. Name_of_Type variable
3. variable ":=" expression These forms are used inside expressions and inside summaries of extended pieces of documentation.

A public name, or parameter needs to be easy to retrieve or spot by eye. They are always introduced (defined or declared) by using two colons:

4. name ":" ":" Set_expression.
5. name ":" ":" "=" expression.
6. name ":" ":" set_expression "=" expression.
7. name ":" ":" "=" "following".
8. name ":" ":" set_expression "=" "following".

The above forms are used inside documents and should be interspersed with comments. The keyword "following" above means that the following closed piece of document forms the expression.

## Development of Syntax of names

9. name::= symbolic_name | natural_identifier,

A MATHS environment needs to be able to keep an index of names that are current.

10. index::@name, the index is a set of names, partitioned into
11. |-index>=={bound_names, declared_names, defined_names, used_identifier},

A name that is not in the index is free:

12. free_names::=name~index.

13. variable::= symbolic_name | variable_structure,

14. variable_structure::= R(variable) | P(variable).
[ math_64_Meta_Macros.html ]
1. |-For X:@#lexeme,
2. R(X)::="(" #(X comma) identifier "=>" X #( comma identifier "=>" X) ")",
3. P(X)::= "(" X #( comma X ) ")".

15. symbolic_name::= (mathematical_symbol #(subscript|superscript)) & (bound_symbolic_name | non_bound_symbolic_name),

At each point in a piece of documentation there exists a set of bound symbolic names (the current index). Bindings, definitions and declarations add to this set. Variables are removed at the end of their scope. At the start no names are bound.

A binding always creates a new variable or name - even when the symbol or identifier is already bound. The old meaning is recovered at the end of the new symbols scope. Variables are uniquely identified by their name and the place where they were bound. Compare [ notn_12_Expressions.html#Free Variables ] for more examples.

16. mathematical_symbol::= letter | symbol | back_slashed_symbol | (identifier & mathematical),

A mathematical symbol can be a character in another alphabet represented, in ASCII, by a word - typically prefixed by a backslash. Notice that in keeping with mathematical tradition single character identifiers are used for local variables. Identifiers like 'sin', 'cos', 'abs', 'sinh', 'asin', 'sqrt', 'pr', 'id'... etc can also be found in mathematical dictionaries, and can be used as mathematical symbols. Significantly they have not been typeset in italics as variables however. Thus there is an exception to the rule that names that are words must be in a standard dictionary. A (short) glossary of mathematical words can therefore be included as part of a document - and a tool should be made that scans a document and extracts names that are defined but are not in the standard dictionary.

17. subscript::= digit # digit | "[" expression"]", subscripts should be type set below the line.

18. superscript::= prime. In MATHS a prime ("'") can be used to indicate the future value of a variable. A free variable that appears in an expression with a prime is said to be a dynamic variable and can be contrasted with the remaining static variables. For example in
` 		x'+y`
both x and y are free but x is dynamic and y is static. (For more see [ notn_12_Expressions.html#Free Variables ] , [ intro_dynamics.html ] , [ math_14_Dynamics.html ] , and [ math_75_Programs.html ] )

To make reuse easier, natural names whose scope is larger than a single formula. This is especially true for ideas that someone else may want to remember.. Some f these can be given internal algebraic abbreviations are used inside a piece of documentation.

19. natural_identifier::= word #(underline word) & (declared_identifier | defined_identifier | unknown_identifier)

The words should exist in a standard a dictionary of the user's and client's natural language. The use of underline to link words is incompatible with ΤΕΧ subscripting. A preprocessor that outputs ΤΕΧ must therefore escape underlines within natural identifiers. It will also have to insert formatting of sub- and super-scripts.

Strings like "I" and "a" are ambiguous - they are both in the English dictionary and are algebraic variables. Within a formal piece of documentation they are taken to be algebraic. Within informal commentary they are taken to be words. However, inside a comment, a reverse quotes should enclose a formula. Identifiers of defined terms may be preceded by a dollar sign to indicate a cross-reference or hypertext link. Note. This is not really necessary outside comments if suitable tools are available for interpreting formulae.

## Dangerous Bend

Notice that it is easy to assume that different names refer to different (unequal) object. In MATHS it may be necessary to add some explicit assumptions that names are different:
` 		|- tweedle_dee <> tweedle_dum.`

. . . . . . . . . ( end of section Names) <<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.