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.
.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-tuple or vector. One item per paragraph. Numbered 1,2,3,... |
Table | @(...) | A relation defined as a set of n-tuples |
Etc |
1 * 2is a valid expression, but means the same as
*(1, 2)
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 accepted part of almost all programming languages.
For more see [ Serial Operators ] below.
However if an operator (-) is not associative then a-b-c may mean a-(b-c) or (a-b)-c and is best avoided.
Several papers and texts in the last 10 years have been espousing notations that are an extension 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 generalizations 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 Sheider have their versions.
For more see [ Serial Operators ] and [ Parallel Operators ] below.
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>>
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 abbreviation - 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:
Note. I've already extended well formed formulas in formal pieces of documentation to include something like this.
For example, if free maps an 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 occurrences 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, ...
x < x' <= a*x.states that x will grow but, that its growth is limitted by the constant (stable) a. The expression
x' = x +1,expresses the operation of adding one to x.
One can define
Net
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:@T:
Note.
. . . . . . . . . ( end of section Serial Operators) <<Contents | End>>
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. Or use the "Hole" below.
[click here if you can fill this hole]
Rules of precedence can resolve other ambiguities. Given that both f,g:T><T->T then it is not immediately 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:
(standard_priorities):
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:
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
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:
Note that care is needed when these expressions are used with generic relations where the type of the value can not be determined. Fr example trying to use /Card(3) to express the set of all sets with three elements` is ambiguous and the type of object needs defining: /Card[Int](3) -- sets of 3 integers.
.Dangerous_bend
Second, The parsing with most obvious, visible, or simplest explanation is taken.
Third, some expressions have a deliberately generic type.
Further, a function, f say extends from operating on integers to lists:
We might argue that the following has two meanings:
First, directly distribute the + inside the list
Second, treat the + as a function of a list and then as infix
The first is the correct parsing and evaluation, because it's explanation is simpler.
Something similar happens with union (|) and intersection (&) when applied to sets of sets of sets( the kind of expressions discussed in Principia Mathematica in section *42):
As rule MATHS selects the most obvious parsing.
Notice that sets of sets don't have the same problem:
--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 ambiguous 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.
These are extremely convenient but have to e used with care to avoid ambiguity and possible paradoxes.
For example, the operation that gives the size of a set, Card(S) is generic -- it can be applied to any set of objects. The null set {} is generic -- it is a subset of some type but the precise type has to be determined from the context. Similarly, operator overloading gives rise to functions that can be applied to many different types of object: (+), for example, is used to add numbers but can also add lists/vectors of numbers:
So definitions like
defines a function example: T1->T2 that apply to any types of objects. They can be also applied in reverse /example:T2->@T1 without ambiguity.
.DangerousBend However, consider the following kind of definition, for a fixed, given type T,
This clearly defines the type of the expression one_way_example(e) for each e:T1.expression, and so defines the map one_way_example: T1->T. But it does not define an inverse mapping because the codomain (T) is fixed and so we can not determine the correct T1 in terms of the T. One example of this was the Card function which has values in the natural numbers (including 0) Nat0 and so the inverse /Card(2) does not define the type of the set. To handle cases where we must include the type as an argument in a definition like this:
Now we can precisely describe the sets of Boolean values with two elements as
The following kinds of definition (for a given global T like Nat) is context dependent because the meaning will depend on where it appears.
As long as context_dependent_example is used where it's conext demands a particular type then this is valid. The inverse function /context_dependent_example also has a well defined type T2->@T and so for any x:T2 /context_dependent_example(x) ∈ @T another well defined type.
A more complex example occurs with generic relations defined like this:
When used with two arguments the type is well defined. However, this relation can not be treated as a set of pairs without the types being defined
Further, knowing the type of x in generic_relation(x) or y in /generic_relation(y) does not help us define the type of the expression -- further disambiguation is needed.
On the other hand homogenous generic relations defined like this:
do define the types in expressions like homogeneous_generic_relation(x) and /homogeneous_generic_relation(y) precisely.
Given a finite digraph with nodes/vertexes N and edges/arcs E which has been labeled 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 there 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>>
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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see [ home.html ]
For a more rigorous description of the standard notations see