.Open 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
Set::Sets.
op::infix(Set).
for all a,b,c:Set( a op (b op c) = (a op (b op c)).
.Close.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:
variable ":" set_expression
Name_of_Type variable
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:
name ":" ":" Set_expression.
name ":" ":" "=" expression.
name ":" ":" set_expression "=" expression.
name ":" ":" "=" "following".
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
name::= symbolic_name | natural_identifier,
A MATHS environment needs to be able to keep an index of names that are
current.
index :: @name, the index is a set of names, partitioned into
|- index>=={bound_names, declared_names, defined_names, used_identifier},
A name that is not in the index is free:
free_names::=name~index.
variable::= symbolic_name | variable_structure,
variable_structure::= R(variable) | P(variable).
.Box
.See http://www/dick/maths/math_64_Meta_Macros.html
|- For X:@#lexeme,
R(X) ::="(" #(X comma) identifier "=>" X #( comma identifier "=>" X)
")",
P(X) ::= "(" X #( comma X ) ")".
.Close.Box
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
.See ./notn_12_Expressions.html#Free Variables
for more examples.
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.
subscript::= digit # digit | "[" expression"]",
subscripts should be type set below the line.
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
.Key dynamic
variable and can be contrasted with the remaining `static` variables. For
example in
.As_is x'+y
both `x` and `y` are free but `x` is dynamic and `y` is static.
(For more
see
.See ./notn_12_Expressions.html#Free Variables
,
.See ./intro_dynamics.html
,
.See ./math_14_Dynamics.html
, and
.See ./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.
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 \TeX subscripting. A preprocessor that outputs \TeX 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:
.As_is |- tweedle_dee <> tweedle_dum.
.Close Names