.Open Expressions in MATHS
.Open Introduction
. Why expressions
An short way of expressing calculations is needed. In general some
simple yet effective way of expressing algebraic expressions is needed to
document software requirements, specifications, and code. They have a 200
year history of algebraic expressions or formulas
helping us to express and solve problems.
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 multi-line expressions
for certain types of object using the MATHS directive notation
.As_is .Tag
.As_is .Close.Tag
These have proved very useful:
.Table Tag Type Notes
.Row Set Sets Each paragraph defines an element in the set
.Row List %X A numbered n-tuple or vector. One item per paragraph.
Numbered 1,2,3,...
.Row Table @(...) A relation defined as a set of n-tuples
.Row Etc
.Close.Table
. 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 example - need to
incorporated. So
.As_is 1 * 2
is a valid expression, but means the same as
.As_is *(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.
.As_is 1 + 2 * 3
is a valid expression, but means the same as
.As_is +(1, *(2,3))
We set priorities simply to avoid expressions that end like this:
.As_is )))))))))))))))))))))))))))))))
Further rules like the British rule:
BODMAS::mnemonic="Brackets, Division, Multiplication, Addition, Subtraction",
have been a part of algebraic expressions since for many decades.
Priorities are an accepted part of almost all programming languages.
. MATHS does not predefine general associativity
If an operator (+) is associative then MATHS defines
a+b+c = a+(b+c) = (a+b)+c.
For more see
.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.
. 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
.Box
Operators identified by multi-character identifiers
The ability to define operators locally
The need for operator overloading and polymorphism.
.Close.Box
. 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 extension of the traditional \Sigma and \Pi
notations of mathematics. Drawing on the traditional notations, Donald
Knuth's extensions in his "Art of Computer Programming", The \lambda
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 \Sigma and \Pi notation. They are quite common in Computer
Science. APL had them. Knuth tinkers with \Sigma and \Pi. Unity
and Z have their forms. Gries and Sheider have their versions.
For more see
.See Serial Operators
and
.See Parallel Operators
below.
. Inherited 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:
.As_is Mathematics Inverse functions, composition,...
.As_is ADA overloading, meaning determined by types.
.As_is APL Functions that operate on sets, vectors, and lists
.As_is POP equivalent Prefix and postfix forms
.As_is Church, ISWIM functions as results of expressions - '\lambda'
.As_is ML, FP Higher order functions
.As_is OOP Inheritance and polymorphism, `multimethods`
.As_is Z Schematic expressions summarizing logical systems
.Close Introduction
. 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.
.Box
(E1): A string of lexemes that is not terminated by a $comma or $period
occurring outside parentheses of some kind or other, can be expression. But
an expression can not contain a $comma or $period outside of parentheses.
MATHS therefore uses punctuation to recognized `balanced` expressions.
(E1)|-(E1a): By default a sentence, or a comma terminated phrase is a weak
kind of expression.
(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.
.Close.Box
expression::= $balanced & $functional & $types_ok.
BALANCE::=following.
.Net
This uses the lexemes defined in the MATHS Lexicon
.See http://www/dick/maths/notn_10_Lexicon.html
For example
comma::=",".
.See http://www/dick/maths/notn_10_Lexicon.html#comma
period::= "." whitespace.
.See http://www/dick/maths/notn_10_Lexicon.html#period
A period is a dot followed by a whitespace. So "1.2" and
"java.awt" have no period in them. This is borrowed from COBOL.
left::= "{" | "(" | "[" | ...,
.See http://www/dick/maths/notn_10_Lexicon.html#left
right::= "}" | ")" | "]" | ...,
.See http://www/dick/maths/notn_10_Lexicon.html#right
The definition of $balanced is used to define an $expression and a `gloss`
(an definition in a glossary).
balanced::= #(lexeme ~ ( $comma | $period | left | right) | $quantified | $schematic ).
quantified::=( $for_symbol #( $comma | $balanced )|) $schematic.
schematic::= left $sentence #( $period $sentence ) right.
sentence::=$clause #( $comma $clause).
clause::=$balanced.
for_symbol::="for" | "For".
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.
.Close.Net
FUNCTIONALITY::=following
.Net
If we are given the set of currently defined operators then we can further
parse an expression according to these rules:
lexeme::Sets,
operator:: @lexeme.
LEXICON::=http://www/dick/maths/notn_10_Lexicon.html#LEXICON,
Use $LEXICON.
SYNTAX::=http//www/dick/maths/math_11_Standard#SYNTAX,
(SYNTAX)|- For X:@#lexeme,
O(X) ::= (X | ),
P(X) ::= "(" X #( $comma X ) ")",
R(X) ::="(" identifier "=>" X #( $comma identifier "=>" X) ")",
N(X) ::= (X #X).
functional::= $prefix | $infix | $postfix,
prefix::=$N( (slash |) operator) delimited,
.As_is sin(x), /sin(x), +x, -x, ...
postfix::=delimited (dot| "./") operator #( $O(slash) operator),
.As_is x.sin, 4.th, x./sin, x.+
infix::= delimited #( (operator | omitted_operator ) delimited),
.As_is x+y, (x*y)=(4*3), ...
omitted_operator::=whitespace.
In MATHS one infix operator can be left out without ambiguity -- as long
as a complete list of operators is available. Normally
this symbolizes the concatenation of two sets of strings. The operator
itself shown as "( )". In looser expressions with a natural sentence
structure white space also acts as an omitted_operator.
delimited::= $abstraction | $mapping_form | $extension | $definite_description | $quantified | $non_punctuation_lexeme | $uniform_binding,
uniform_binding::= operator $scheme.
scheme::=`defined in the MATHS Lexicon`,
.See http://www/dick/maths/notn_10_Lexicon.html#scheme
abstraction::=#( $binder $bindings ) $P( $functional ) $right.
Some uniform bindings also act as abstractions.
extension::= $l_brace $bindings $double_bar $functional $r_brace.
Some uniform bindings also act as extensions.
mapping_form::= $l_parenthesis $O( $operation | $function_name |
$under_score ) $r_parenthesis.
Some uniform bindings also act as mapping_forms.
.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.
operation::=$operator | $under_score $operator $delimited | $delimited $operator $under_score.
Symbols like (1st), (2nd), (rest), (!), (_+1), (2*_) indicate functions.
(_) is short for an identity function of some type or other.
So (+) is an unambiguous symbol for the map that adds values together.
definite_description::= "the" $l_parenthesis $bindings $double_bar $functional ( $double_bar $functional |).
There is a uniform version of definite descriptions.
quantified ::=("for"|"For") $bindings l_parenthesis $functional r_parenthesis.
Again there is a uniform binding notation for quantified expressions.
binder::= $O("map") | "rel" | "the" | "set",
A binder introduces a new meaning for one or more variables. It
is said to `bind` them.
bindings::= $binding | l_bracket $binding #($comma $binding) r_bracket,
The brackets are needed to enclose the commas in the list.
They are helpful even when not necessary.
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.
loose_binding::= variable $O(colon $functional ) | set_name variable $O(
"where" functional ).
tight_binding::=variable ":=" $functional.
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.
binding::= variable $O(colon $functional | ":=" $functional) | $set_name
$variable $O( "where" $functional).
The following indicate equivalent syntactic forms:
For set_name S,variable v, (S v) ::=( v:S ).
For set_name S, proposition P, variable v, (S v where P) ::= (v:{v:S||P}).
. Experimental Notation June 1999
I'd to find out the implications of allowing a set of bindings
to include propositions so that
For set_name S, proposition P, variable v, ( v:S,P) ::= (v:{v:S||P}).
Some of the implications of this freedom are not clear. Here
are some examples:
+[i:Nat, 0<=i<17](i*i).
Note. I've already extended well formed formulas 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:
map[x](x+1) = map[y](y+1),
map[z](x*z) = map[y](x*y) <>map[x](x*x).
. 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:
.Box
Any term used in an expression is a free variable of that expression if it
is not bound in a surrounding expression.
A term used in an expression is a bound variable if it is bound in that
expression.
.Close.Box
The binding essentially hides the variable from expressions that contain
the expression in which the variable is bound. In the subexpressions an
expression appears free. However a binding is always local, so an original
meaning can be overridden locally and then the original can reappear - in the
usual way (as in C, C++, the lambda calculus, Algol 60, and the integral calculus).
For example, if `free` maps an expression into a set of free variables
and `bound` maps into the bound variables then we have:
free(1) = {},
free(1+2+3)={},
free(x+1)={x},
bound(x+1)={},
bound(map[x](x+1)) = {x},
free(map[x](x+1)) = { }.
So,
.Net
free:expression->@variable,
|-free(constant) ={},
|-free(variable) ={variable},
|-free(variable') ={variable},
|-free(e1 op e2) =free(e1) | free(e2),
|-free(fun(e)) =free(e),
|-free(map[variable:Type](e)) = free(e)~{variable},
...
.Hole
bound:expression->@variable,
|-bound(constant) ={},
|-bound(variable) ={},
|-bound(variable') ={},
|-bound(e1 op e2) =bound(e1) | bound(e2),
|-bound(fun(e)) =bound(e),
|-bound(map[variable:Type](e)) = bound(e)|{variable},
...
.Hole
.Close.Net
The full treatment of binding and free variable depends on the
existence and position of globally defined symbols, see
.See ./notn_11_Names.html#name
for more.
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, ...
.Close.Net
. Dynamic Variables
Dynamic variables are used in MATHS to express change. They lead to a natural and
logical model of programs. A dynamic variable is free variable that appears in
an expression with a prime superscript. All occurences are of the same variable, but if
at least one of them has one or more primes after it then variable is said to be dynamic.
The remaining free variables are said to be static. When a predicate (an expression
that is true or false) has dynamic vriables then it is interpretted as defining a change.
The static variables require the addition of a "Framing condition" that they do not change.
For example
.As_is x < x' <= a*x.
states that x will grow but, that its growth is limitted by the constant (stable) `a`.
The expression
.As_is x' = x +1,
expresses the operation of adding one to x.
One can define
.Net
dynamic:expression->@variable,
|-dynamic(e) ==> free(e) & primed(e).
|-primed(constant) ={},
|-primed(variable') ={variable},
|-primed(variable) ={},
|-primed(e1 op e2) =primed(e1) | primed(e2),
...
.Hole
.Close.Net
. Type checking
The syntax above allows expressions to be recognized, 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
.See http://www/dick/maths/types.html
Here is a summary of that documentation:
First the notation for applying a function to an expression:
For f:(T1^ T2).expression, e2:T2.expression, f(e2) :: T1.expression.
For f:(T1^ T2).expression, e2:T2.expression, (e2).f:: T1.expression.
For f:(T1^ T2).expression, e2:T2.expression, f(e2)=(e2).f.
A similar rule holds for functions that require several arguments:
For e1:T1.expression, e2:T2.expression, ..., f:T1^ (T2><...), f(e2,e3,...) :: T1.expression.
For e1:T1.expression, e2:T2.expression, ..., f:T1^ (T2><...), (e2,e3,...).f :: T1.expression.
For e1:T1.expression, e2:T2.expression, ..., f:T1^ (T2><...), f(e2,e3,...) = (e2,e3,...).f .
Finally, for any function with two arguments,
For e3:T3.expression, e2:T2.expression, f:T1^ (T2>), (e2 f e3) :: T1.expression.
For e3:T3.expression, e2:T2.expression, f:T1^ (T2>), (e2 f e3) = f(e2, e3) = (e2,e3).f.
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 ({[]}).
.Open Serial Operators
Some associative operators of type f:T1^ (T1>) are designated to be
SERIAL operators. If `f:T1^(T1>T1:
f(e1,e2,...) =e1 f e2 f e3...=(e1,e2,e3,...).f,
and
f(e1) = e1.
. Common Serial Operators
Examples of serial operators are (and) (or) (&) (|) (!) (+) (*). This is
a simplification of the notation proposed and implemented by Iverson in APL
and that of Bachus's FP operations. Notice the special cases:
For x:#@, and(x) =` all elements in x are true`,
For x:#@, or(x) =` some elements in x are true`,
For T:Types, x:#@T, &(x) =` the intersection of all elements in x`,
For T:Types, x:#@T, |(x) =` the union of all elements in
x`,
For x:#Numbers, +(x) =` the sum of all elements in x`,
For x:#Numbers, *(x) =` the product of all elements in x`,
For x:#%T, !(x) =`the concatenation of elements in x`.
Serial operators can also be used with the $uniform_binder notation:
+( i:Nat || odd(i), i <= N || i ) = N^2
+( i:Nat . odd(i), i <= N . i ) = N^2
. Serial Commutative Operations on Sets
A commutative serial operator like addition, multiplication, intersection,
conjunction, union, and disjunction can operate on sets without ambiguity,
however this may or may not have a pre-defined value when the set is not
finite. So we have:
For SERIAL(f), if f in commutative(A), f :: ((@A)~{{}}) <>->T1.
-- f is not always defined on all subsets of A.
For f, f :: ((Finite_sets(A)~{{}}) ->T1.
-- f is defined for all finite nonempty subsets of A.
For all f, f{a} = a.
For f, S1,S2:Finite_sets(A)~{{}}, if S1 & S2 ={} then f( S1 | S2) = f( S2 | S1) = f( S2 ) | f(S1).
-- On finite subsets the sum of a disjoint union is the sum of the sums of the parts.
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:
|-(decomp): +( S1 | S2 ) = +(S1) + +(S2) - +(S1&S2).
Note.
.Close Serial Operators
. Parallel Operators
All relations - operators of type @^(T1>,!=, >=,==>,>==, ->,...
Thus, if f:@^(T1>@, but if f is SERIAL
then f in (#T1)->T1.
Notice the special cases:
.Box
iff(x) = `x is a list of equivalent logical values`,
=(x) = `x is list of identical elements`,
!=(x) = `x is list of elements with no adjacent equal elements`,
<=(x) = `x is sorted into increasing order`,
<(x) = `x is sorted into increasing order and has no equal elements`,
=>>(x) = `x is an ascending chain of subsets`,
->(x) = `the elements in x are connected by mappings`.
.Close.Box
. Uniform Binders
The following definitions are based on Gries's uniform binding notation:
.Box
op( x:T || P || E) ::= op[x:(set[x:T](P))](E).
op( x:T || E) ::= op[x:T](E).
op( x:T ) ::= op[x:T](x).
.Close.Box
.Note
A new experimental form uses sentences and periods rather than the double_bar.
.Box
op( x:T . P . E) ::= op[x:(set[x:T](P))](E).
op( x:T . E) ::= op[x:T](E).
op( x:T ) ::= op[x:T](x).
.Close.Box
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.
.Hole
. Precedence and Typing
Strong typing is used in MATHS (but not programming languages) to resolve
some apparent ambiguities:
x + y > z
can not be interpereted as
+(x,>(y,z))
because `+` does not accept an expression of type `@` as an argument. A
fundamental assumption in MATHS notation is that we have an intelligent
reader - one that can resolve this kind of apparent ambiguity.
Rules of precedence can resolve other ambiguities. Given that both
`f,g:T>T` then it is not immediately clear whether
x f y g z
is to be read as
(first): (x f y) g z = g(f(x,y),z) =((x,y).f,z).g
or
(second): x f (y g z) = f(x, g(y,z))=(x,(y,z).g).f.
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):
(*) and (/) take precedence over (+) and (-)
(and) and (not) take precedence over (or)
(&), (;), (o), (!) and (~) take precedence over (|)
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:
4.th(x) =x(4).
. 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:
substitute( (a+>1 | b+>2 ) , 2*a+b+map[a:real](b+1+a) ) =
2*1+2+map[a:real](2+1+a) =
5+map[a:real](a+3)=
5+map[x:real](x+3) = 8+(_).
Roughly we have these rules to defines substitution:
substitute((v+>a) , e) = a.map[v](e).
substitute((v+>a)|A, e) = a.map[v](substitute(A, e))=substitute(A,
a.map[v]( e)).
Some care must be taken when `M` substitutes an expression that contains
a free variable into an expression that binds that variable. For
example:
substitute((x->(y+1)), map[y](2*x+y) ) = map[z](2*(y+1)+z)
substitute((x->(y+1)), map[y](2*x+y) ) <> map[y](2*(y+1)+y)
Because the `y` in `y+1` is `captured by the `map[y]`.
However, the order of substitution is not defined and so only `M`s 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
substitute( (x+>x+y | y+>x*y), x+y )
could mean
substitute( (y+>x*y), x+y+y ) = x+2*x*y
or
substitute( (x+>x+y), x+x*y ) = (x+y)+(x+y)*y = x+y+x*y+y*y.
Hence `substitute( M, e )` is defined and can be used only when `M` does
not include pairs `x+>e1` and `y+>e2` where `y` is free in `e1` or `x` is
free in `e2`.
. 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.
|- For f:T1^T2, g:T2^T3, f(g) = g o f = f;g = map x:T3( ((x).f).g ) in T1^
T3
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:
For f:T1^ T2, E1:@T1.expression, E2:@T2.expression, f(E2)=(E2).f ={x:T1 || for some y:E2( f(y) ) }.
For f:T1^T2, E1:#T1.expression, E2:#T2.expression, f(E2)=(E2).f = map i:1..|E2|( f(E2[i]) ) = E2.f = f o E2.
For f:T1^T2, e1:expression(T1), E1:@T1.expression, /f(e1) = (e1)./f = {x:T2 || f(x)=e1}.
For f:T1^T2, e1:expression(T1), E1:@T1.expression, /f(E1) = (E1)./f = {x:T2 || for some y:E1(x in y ./ f) }.
Some expressions describe relations. They use these operators "/", "o",
"do", "&", "not", "|", ";" etc. They are best written as postfix operators
on elements and sets:
For e1:expression(T1), E1:(@T1).expression, R:@(T1,T2), e1.R in expression(@T2).
For e1:expression(T1), E1:(@T1).expression, R:@(T1,T2), E1.R in expression(@T2).
For e2:expression(T2), E1:(@T2).expression, R:@(T1,T2), e2./R in expression(@T1).
For e2:expression(T2), E1:(@T2).expression, R:@(T1,T2), E2./R in expression(@T1).
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.
For f, R:@(T1,T2), R mod f:@(T1,T1) ::= rel x,y(x.f R y.f).
For f, R:@(T1,T2), (= mod f) = rel [x,y] (x.f=y.f).
. Equivalences
For e1:expression(T1), E1:expression(@T1), f:@(T1,T2), e1/f = ((e1).f)./f.
For e1:expression(T1), E1:expression(@T1), f:@(T1,T2), E1/f = {y/f:T2||for some y:E1 }.
.Dangerous_bend
e1 / f <> e1 ./ f
.Open Conditions for an expression to be unambiguous
. Rules for ambiguities
First, the types of subexpressions can block parsings.
Second, The parsing with most obvious, visible, or simplest explanation
is taken.
Third, some expressions have a deliberately generic type.
. Generic expressions
Functions connect expressions of different types. Some expressions are
generic or polymorphic in the sense that the types of the parts of the
expression depend on the choice of actual types to replace certain symbolic
ones. This not a problem.
. Ambiguities from overloaded symbols
When an expression has two different parsings because of definitions of
functions and operators then the most visible interpretation is taken.
As an example the '+' operator is infix and $SERIAL, So
+(1,2,3) = 1+2+3 = 6.
Further, a function, `f` say extends from operating on integers to
lists:
f(1,2) = (f(1), f(2)).
We might argue that the following has two meanings:
+( (1,2) , (3,4))
First, directly distribute the + inside the list
+( (1,2) , (3,4)) = (1,2) + (3,4) = ( 1+3, 2+4) = (4,6)
Second, treat the + as a function of a list and then as infix
+( (1,2) , (3,4)) = ( +(1,2), + (3,4)) = ( 1+2, 3+4) = (3,7).
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):
|{ {{1,2} , {2,3}}, {{1,2},{3,5}} } =
{{1,2} , {2,3}} | {{1,2},{3,5}} = {{1,2}, {2,3}, {3,5}}
|{ {{1,2} , {2,3}}, {{1,2},{3,5}} } <>
{ |{{1,2} , {2,3}}, |{{1,2},{3,5}} } = {{1,2,3}, {1,2,3,5}}.
As rule MATHS selects the most obvious parsing.
Notice that sets of sets don't have the same problem:
|{ {1,2} , {2,3} } = {1,2} | {2,3} = {1,2,3},
|{ {1,2} , {2,3} } <> {|{1,2}, |{2,3}} -- meaningless.
. Ambiguity from missing type information
The type of an expression is ambiguous when there are two
-- equally simple -- ways to
assign types to the parts of an expression so that it gives different
meanings.
. Example g o f
.As_is --f---> B ---g---
.As_is / \
.As_is A C
.As_is \ /
.As_is --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.
. Generic Operations and Templates
The MATHS type system permits the definition of constants and operations whose meaning and the type implicitly depends on the arguments when it is used. In Ada these would be `generic` and in C++ `templates`. In `Principia Mathematica` they would be said to be `typically ambiguous`. And in language theory they would have `context dependent` semantics (and syntax).
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:
(1,2)+(3,4) = (4,6).
So definitions like
For Types T1,T2, x:T1, example(x)::T2.
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,
For Types T1, x:T1, one_way_example(x)::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:
For Types T1, x:T1, explicitly_typed_example [T](x)::T=....
Now we can precisely describe the sets of Boolean values with two elements as
/Card[@](2) = { {false, true} }.
The following kinds of definition (for a given global T like `Nat`) is context dependent because the meaning will depend on where it appears.
For T2, x:T, context_dependent_example(x)::T2=....
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) \in @T` another well defined type.
A more complex example occurs with generic relations defined like this:
For Types T1, T2, generic_relation::@(T1,T2) = ... .
For Types T1, T2, x:T1, y:T2, (x generic_relation y)::@ =... .
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
generic_relation.@(Real, Nat0),
for example.
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:
For Types T, homogeneous_generic_relation::@(T,T) = ... .
For Types T, x, y:T, (x homogeneous_generic_relation y)::@ =... .
do define the types in expressions like `homogeneous_generic_relation(x)` and `/homogeneous_generic_relation(y)` precisely.
. Theory for assigning types
The nodes/vertexes 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/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),....)
and a word w=(w1,w2,w3,...) in #A then p fits w iff
either both p and w are empty
or w is empty and all g(p(i)) are null
or w1=f(n1) and w2=g(n1,n2) and ((n2,n3),....) fits (w3,...)
or w1=g(n1,n2)<>null and ((n2,n3),....) fits (w2,...)
or g(n1,n2)=null and ((n2,n3),....) fits (w1,...).
Given `w` find `p`s that fit `w` and show there are not two `p`s that fit
`w` with the same number of nulls.
.Close Conditions for expression to be unambiguous
.Close Expressions in MATHS