Further, the work done abstract data types and the fact that a lot of computer ideas are already known to be abstract algebras, means that MATHS needs a way to cope with expressions from any abstract algebra.
Large Expressions
As MATHS developed I added the ability to create multiline expressions
for certain types of object using the MATHS directive notation
.Tag
.Close.TagThese have proved very useful:
| Tag | Type | Notes |
|---|---|---|
| Set | Sets | Each paragraph defines an element in the set |
| List | %X | A numbered n-tple or vector. One item per paragraph. Numbered 1,2,3,... |
| Table | @(...) | A relation defined as a set of n-tples |
| Etc |
Why Infix Operators
The immense popularity of infixed
binary operators (like + and *) means MATHS can not insist on functional
notation. However the elegant power of functional languages like LISP and
ML imply that their ideas - lambda abstraction for exmple - need to
encorporated. So
1 * 2is a valid expression, but means the same as
*(1, 2)
Why Priorities for Operators
If you think 1+2*3 equals 9 then you are using the wrong priorities
and doing the addition before the multiplication.
1 + 2 * 3is a valid expression, but means the same as
+(1, *(2,3))We set priorities simply to avoid expressions that end like this:
)))))))))))))))))))))))))))))))Further rules like the British rule:
Priorities are an excepted part of almost all programming languages.
Effect of ASCII
MATHS is committed to express ideas directly in ASCII rather
than encoding the written and printed look-and-feel. So the notation in
expands in
some unusual directions. In particular because ASCII does not
have graphic characters there is a need for
Need for Serial and Parallel Operators
When mathematicians invented matrices, quaternions, and vector analysis
they created a way of handling complex objects in very simple ways. This
lead to a generalized form of "bulk operation" in APL and later in FP.
Several papers and texts in the last 10 years have been espousing notations that are an extention of the traditional Σ and Π notations of mathematics. Drawing on the traditional notations, Donald Knuth's extensions in his "Art of Computer Programming", The λ calculus, and quantifiers in logic, these writers are proposing various uniform notations for quantification, summation, products, etc.
So there is a need for rules for expressions handle the large number associative infix operations that are also used to apply to vectors, sets, and series of elements - here the standard MATHS solution: Serial and Parallel Operators is unique and powerful.
MATHS is not the only notational system invented with similar generalisations of the Σ and Π notation. They are quite common in Computer Science. Apl had them. Knuth tinkers with Σ and Π. Unity and Z have their forms. Gries and Scheiner have their versions.
Inheritted Features
Expressions in MATHS follow a more general syntax than expressions in a
programming language. Expressions include ideas borrowed from both
mathematics and several other unnatural languages:
Mathematics Inverse functions, composition,...
ADA overloading, meaning determined by types.
APL Functions that operate on sets, vectors, and lists
POP equivalent Prefix and postfix forms
Church, ISWIM functions as results of expressions - '\lambda'
ML, FP Higher order functions
OOP Inheritance and polymorphism, `multimethods`
Z Schematic expressions summarizing logical systems
. . . . . . . . . ( end of section Introduction) <<Contents | End>>
Recognizing an expression.
Just about any string of words and symbols is a possible expression... but
to be meaningful it must follow special rules.
MATHS uses an explicit multiple pass or co-routine grammatical description.
(E2): A second cut needs a set of operators - those symbols that only make
sense when accompanying other symbols - and defines whether an expression
is functional.
(E3): A final process checks whether the balanced
applicative expression is correctly type, and also infers the types in
cases of ambiguity.
The definition of balanced is used to define an expression and a gloss (an definition in a glossary).
Notice that MATHS permits expressions like "[0..1.23)" where a l_bracket is balanced by a r_parenthesis. This is because these expressions are in use in mathematics.
sin(x), /sin(x), +x, -x, ...
x.sin, 4.th, x./sin, x.+
x+y, (x*y)=(4*3), ...
.Note Non-uniform abstractions, extensions, and mappings are older than the uniform bindings. In time they may become deprecated and then, perhaps removed from MATHS. This depends on which notations become used the most.
Bindings tie a mathematical or algebraic variable to a localized meaning - in other words to a type. Conventional abreviation - if a variable is in a binding, without a set or type attached to it, then it gets back the type of its previous usage in the text.
In a loose binding, if the type is omitted then the newly bound variable has the same type as it's previous use in the document.
The following indicate equivalent syntactic forms:
Experimental Notation June 1999
I'd to find out the implications of allowing a set of bindings
to include propositions so that
Note. I've already extended well formed formulae in formal pieces of documentation to include something like this.
Bound variables are arbitrary
The meaning of an expression is not changed if a binding and its expression
are changed systematically by replacing one variable by another as
long as the new variable isn't free in the expression:
Free Variables
Associated with each functional expression is a set of variables that are
used in that expression and not bound in it - the free variables. The
rules are simple but hard to express:
For example, if free maps and expression into a set of free variables and bound maps into the bound variables then we have:
So,
Net
Free and bound variables have to watched carefully in substitution (Substitution). So when substituting for a variable only the free occurences can be replaced. Further when the substituted expression contains a free variable that is also bound in the expression, then the bound variable must be changed to a different one.
The simple binding scheme creates an abstraction that can be used to define functions, maps, relations, sets, ...
Type checking
The syntax above allows expressions to be recognised, delimited, and
roughly parsed. Further parsing depends on the types of the symbols in the
expression. A formal model of expressions has been developed in the theory
of types which sorts out questions of precedence and the like
[ types.html ]
Here is a summary of that documentation:
First the notation for applying a function to an expression:
A similar rule holds for functions that require several arguments:
Finally, for any function with two arguments,
Parentheses can be omitted, at risk of ambiguity. Similarly commas and periods can be replaced by whitespace - but the list must be delimited by parentheses, braces, or brackets ({[]}).
Serial operators can also be used with the uniform_binder notation:
If f has a unit(u), then f({})=u. Note. f has a unit(u) iff for all x ( (x f u)=(u f x)=x ).
The following theorem follows for commutative serial operators (+) with an
unit 0 and inverse (-) on finite
sets S1 and S2:
Note.
. . . . . . . . . ( end of section Serial Operators) <<Contents | End>>
Parallel Operators
All relations - operators of type @^(T1><T1) except and, or` are PARALLEL
operators:
Examples of PARALLEL operators are iff, =, are, <,<=,<>,!=, >=,==>,>==, ->,...
Thus, if f:@^(T1><T1) is PARALLEL then f in (#T1)->@, but if f is SERIAL then f in (#T1)->T1.
Notice the special cases:
If you have a strong feeling one way or another about using "||" or " . " in these kinds of expressions please send me EMail. The ultimate form adopted will be determined by what people want. EMail by clicking "Contact" at the top_of_page. with subject: MATHS: Dots or Bars.
Precedence and Typing
Strong typing is used in MATHS (but not programming languages) to resolve
some apparent ambiguities:
Rules of precedence can resolve other ambiguities. Given that both f,g:T><T->T then it is not imediately clear whether
In the first case we write that f takes precedence over g, and in the second that g takes precedence over f.
The following precedences are predefined in MATHS - to follow established mathematical conventions:
Finally when o:X->(A->B) an expression like x.o(a) is parsed as (x.o)(a) rather than x.(o(a)). This convention is chosen so that we can have:
Substitution
Given a map (set of pairs: x+>y ) M that associates variable
symbols and names with meanings and an expression e then `substitute(M,
e) replaces each free occurrence of a variable in e that is also in M`
by its associated value in M. It does not replace bound occurrences
however. For example:
Roughly we have these rules to defines substitution:
Some care must be taken when M substitutes an expression that contains a free variable into an expression that binds that variable. For example:
However, the order of substitution is not defined and so only Ms can be used where the order does not matter. This means that no elementary substitution can insert a variable that is being replaced in a different elementary substitution. for example For example
Combinations of Maps
MATHS defines several shorthand forms for what are called `higher order
functions` in other languages. However, the forms have been chosen to
generalize mathematical usage and also express ideas that are often need in
formal specifications.
A map is a relation and so it is a set(of pairs) and so has different meanings depending on the types of the arguments, and the context of the resulting value. In particular, functions are extended to sets, lists and maps:
Some expressions describe relations. They use these operators "/", "o", "do", "&", "not", "|", ";" etc. They are best written as postfix operators on elements and sets:
.Dangerous_bend
Conditions for an expression to be unambiguous
Functions connect expressions of different types. Some expressions are
generic or polymorphic in the sense that the types of the parts of the
epression depend on the choice of actual types to replace certain symbolic
ones. This not a problem. The type is ambiguous when there are two ways to
assign types to the parts of an expression so that it gives different
meanings.
Example
--f---> B ---g---
/ \
A C
\ /
--f---> D ---g---There are two paths from that fit the sequence (f,g). There is only one that fits (f, B, g). Hence f(g(a)) and g o f are ambigous but g o B o f is not.
However if the previous diagram commutes so that g o B o f = g o D o F then the ambiguity as more apparent than real.
Theory for assigning types
The nodes/vertices are data types and the arcs/edges are
operators/functions.
Find all ways of interpreting an expression written in postfix form. Data
types
can be used to indicate the type of an expression.
Given a finite digraph with nodes/vertices N and edges/arcs E which has been labelled with symbols from an alphabet A. Node n:N has an unique label f(n) in A. Edge e:E has a possibly non-unique label g(e) in A or a null/empty string. The sets of labels on the nodes and arcs do not overlap. Notice - unique node labels, but non-unique and perhaps null edge labels.
.Road_work_ahead Given a path/sequence of arcs p=((n1,n2),(n2,n3),....)
Given w find ps that fit w and show thare are not two ps that fit w with the same number of nulls.
. . . . . . . . . ( end of section Conditions for expression to be unambiguous) <<Contents | End>>
. . . . . . . . . ( end of section Expressions in 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