Mathematical Notation

See the `B-Method Abstract Machine Notation Summary' for a full treatment of the mathematical notation.

Contents

Notes on operator binding

Compound formulae (e.g. A => B & C) are given an unambiguous interpretation by the operator binding rules:
  1. All operators bind to the left (are left-associative) except ``.'' which binds to the right.
  2. Each symbol (e.g. &) is given a priority, and the highest priorities bind strongest,

    3. e.g. A => B & C is equivalent to A => (B & C).
  3. In case of equal priority the leftmost operator binds the strongest,

    4. e.g. A & B & C <=> (A & B) & C.
The priorities of infix operators are listed in the table below.

Infix Operator Priorities

        Priority          Operator

         10                .      
          3                mod  *  /
          2                -  +
          1                ..
          0                /\  \/  |->
          0                <|  <<|  |>  |>>  <+  +>  ><  circ
          0                ^  ->  <-  /|\  \|/
          0                <  <=  >  >=  /=  /:
         -1                <->  -->  +->
         -1                >->  >+>  +->>  >->>  -->>
         -1                <--  ,
         -2                <:  <<:  /<:  /<<:
         -2                :=
         -4                =  ==  :  <=>  ::
         -5                &  or
         -6                =>  ==>
         -7                ;  ||  []
         -8                |
A full list of priorities is found in the B Toolkit Symbol Table, $BKIT/BLIB/AMNSYMBOL.

Predicates

Let z be a Variable List, x Variable, E and F be Expression Lists, P and Q be Predicates, and S, T be Sets. z\E means that there are no free occurrences in E of the variables in z.

General Predicates

P & Q
Conjunction: ``P and Q''.
P => Q
Implication: ``P implies Q'' or ``if P then Q''.
not(P)
Negation: ``Not P''.
!z.(Q => P)
Universal quantification: ``For all z where Q, P''. The predicate Q must, for each variable x in the list z, contain a constraining predicate, i.e. x: S, x <: S, x <<: S or x = E, where z\S, z\E.
P or Q
Disjunction: ``P or Q''.
P <=> Q
Equivalence: ``P is equivalent to Q''. An abbreviation for (P => Q) & (Q => P).
#z.P
Existential quantification: ``For some z, P holds''. The predicate Q must, for each variable x in the list z, contain a constraining predicate, i.e. x: S, x <: S, x <<: S or x = E, where z\S, z\E.

Predicates on Expressions

E = F
Equality: E equals F.
E /= F
Inequality: E is not equal to F.

Expressions

Let E and F be Expressions.
E,F
Expression list.
E |-> F
Ordered pair (maplet).

Sets

Let z be a Variable List, P be a Predicate, E and F be Expressions, and S and T be sets.
E : S
Set membership: the predicate ``E belongs to S'' or ``E is an element of S''.
E /: S
Set non-membership: the predicate ``E does not belong to S'', i.e. not(E: S).
S <: T
Set inclusion: the predicate ``S is included in T'', i.e. ``every element of S is also an element of T''.
S /<: T
Set non-inclusion: the negation of the predicate S <: T.
S <<: T
Strict set inclusion: the predicate ``S is included in T, but is not equal to T''.
S /<<: T
String set non-inclusion: the negation of the predicate S <<: T.

Set Expressions

{z | P}
Set comprehension: the subset such that P. The predicate P must, for each variable x in the list z, contain a constraining predicate, i.e. x: S, x <: S, x <<: S or x = E, where z\S, z\E.
{z | z: S & P}
Set comprehension: the subset of S such that P.

e.g. {x,y | x,y: S*T & P}.
S * T
Cartesian product: the set of Ordered Pairs whose first component is from S and second component is from T.
POW(S)
Power set: set of all subsets of S.

x: POW(S) <=> x <: S.
S \/ T
Set union: the set of elements which are elements of S or T.
S /\ T
Set intersection: the set of elements which are elements of S and T.
S - T
Set difference: the set of elements which are elements of S, but not of T.
{}
Empty set: the set with no elements.
POW1(S)
Non-empty subset: Set of all non-empty subsets of S.

POW1(S) = POW(S) - {}.
FIN(S)
Finite subsets: Set of all finite subsets of S.
FIN1(S)
Non-empty finite subsets: Set of all non-empty finite subsets of S.

FIN1(S) = FIN(S) - {}.
{E}
Singleton set: Provided that E is not an Expression List, and E: S, {E} is a singleton set: {x | x: S & x = E}.
{E,F}
Set enumeration: Provided that F is not an Expression List, this is the set with elements from {E} together with element F. {E,F} = {E} \/ {F}.

Note that F is an element of {(E,F)}, while E |-> F is the single element of {E |-> F}.
union(U)
Generalised union: the generalised union of a set U of subsets of S (U: POW(POW(S))). union(U) = {x | x: S & #s.(s: U & x: s)}.
inter(U)
Generalised intersection: the generalised intersection of a set U of subsets of S (U: POW(POW(S))). inter(U) = {x | x: S & !s.(s: U => x: s)}.
UNION(z).(P | E)
Generalised union of the sets E where z satisfies P. For each variable x in the list z, P must contain a constraining predicate of the form x: S, x <: S, x <<: S or x = F with z\s, z\F.

!z.(P => E <: T) => UNION(z).(P | E) = {x | x: T & !z.(P => x: E)}.
INTER(z).(P | E)
Generalised intersection of the sets E where z satisfies P. For each variable x in the list z, P must contain a constraining predicate of the form x: S, x <: S, x <<: S or x = F with z\s, z\F.

!z.(P => E <: T) => INTER(z).(P | E) = {x | x: T & #z.(P & x: E)}.

Natural Numbers

A Natural Number (i.e. a non-negative integer) is an Expression, and the Natural Numbers form an infinite set. Let m and n be Natural Numbers, E and F be Expressions, and P be a Predicate.

Predicates on Natural Numbers

m > n
Strict inequality: m is greater than n.
m < n
Strict inequality: m is less than n.
m >= n
Inequality: m is greater than or equal to n.
m <= n
Inequality: m is less than or equal to n.

Natural Number Expressions

NAT
The set of natural numbers.
NAT1
The set of non-zero natural numbers.
min(S)
Minimum of a non-empty subset, S, of NAT.
max(S)
Maximum of a non-empty finite subset, S, of NAT.
m+n
Addition: the sum of m and n.
m-n
Difference: the difference of m and n (defined for m >= n).
m*n
Product: the product of m and n.
m/n
Division: the integer division of m by n.
m mod n
Remainder: the remainder of the integer division of m by n.
n .. m
Interval: the set of non-negative integers between n and m inclusive.
card(S)
Cardinality: the cardinality of the finite set S: the number of elements in S.
SIGMA(z).(P | E)
Set summation: the sum of values of the natural number expression E, for z such that P holds. For each variable x in the list z, P must contain a constraining predicate of the form x: S, x <: S, x <<: S or x= F, where z\S, z\F.
PI(z).(P | E)
Set product: the product of values of the natural number expression E, for z such that P holds. For each variable x in the list z, P must contain a constraining predicate of the form x: S, x <: S, x <<: S or x= F, where z\S, z\F.

Relations

A Relation is a set of Ordered Pairs. Therefore, any set operation may also be applied to Relations. Let S, T, U and V be sets, and r, r1, r2 be relations from S to T, and let E and F be Expressions. Also let s <: S and t <: T.

Relational Expressions

S <-> T
Relation: Set of relations from S to T. Equivalent to POW(S * T).
dom(r)
Domain of r:

The set {x | x: S & #y.(x,y: r)}.
ran(r)
Range of r:

The set {y | y: T & #x.(x,y: r)}.
p;q
Relational composition: Composition of relations p and q, where p: S <-> T and q: T <-> U.

The set {x,z | x,z: S * U & #y.(y: T & x,y: p & y,z: q)}. Also denoted by q circ p.
q circ p
Composition of relations q and p. The same as p;q.
id(S)
Identity on S.

The set {x,y | x,y: S * S & x = y}.
s <| r
Restriction of r by s. Also known as domain restriction. The relation formed from r by keeping only the pairs where the first element is in s.

The set {x,y | x,y: r & x: s}.
r |> t
Co-restriction of r by t. Also known as range restriction. The relation formed from r by keeping only those pairs where the last element is in t.

The set {x,y |x,y: r & y: t}.
s <<| r
Anti-restriction of r by s. Also known as domain subtraction. The relation formed from r by keeping only those pairs where the first element is in the complement of s.

The set {x,y | x,y: r & x: S-s}.
r |>> t
Anti-co-restriction of r by t. Also known as range subtraction. The relation formed from r by keeping only those pairs where the last element is in the complement of t.

The set {x,y | x,y: r & y: T-t}.
r~
Inverse of r. The relation formed from r by interchanging the elements of each pair.

The set {y,x | y,x: T * S & x,y: r}.
r[s]
Image of set s under relation r.

The set consisting of all those elements related to some element in the set s through relation r.
The set {y | y: T & #x.(x: s & x,y: r)}
r1 <+ r2
Overriding of r1 by r2.

The set (dom(r2) <<| r1) \/ r2.
r1 +> r2
Overriding of r2 by r1.

The set r2 <+ r1.
p >< q
Direct product of p and q, where p: S <-> U and q: S <-> V.

The set {x,(y,z) | x,(y,z): S * (U * V) & x,y: p & x,z: q}.
p || q
Parallel product of p and q. where p: S <-> T and q: V <-> U.

The set {(x,y),(m,n) | (x,y),(m,n): (S*T) * (V*U) & (x,m: p & y,n: q)}.
iterate(r,n)
The nth iterate of r (where n: NAT), i.e. r composed with itself n times (defined only for r: S <-> S).

iterate(r,0) = id(S) and iterate(r,n+1) = r;iterate(r,n).
closure(r)
The reflexive transitive closure of r (defined only for r: S <-> S).

closure(r) = UNION(n).(n: NAT | iterate(r,n)).
prj1(S,T)
Projection: prj1(S,T) = {(x,y),z | (x,y),z: (S*T)*S & z = x}.
prj2(S,T)
Projection: prj2(S,T) = {(x,y),z | (x,y),z: (S*T)*T & z = y}.

Functions

A Function is a Relation with the additional property that each element of the domain is related to a unique element in the range. Any operation applicable to Relations may also be applied to Functions. Let S and T be sets, z a Variable List, E be an Expression, and P be a predicate.
S +-> T
Set of partial functions from S to T (also known as `many-to-one relations').

The set {r | r : S <-> T & (r~;r) <: id(T)}.
S --> T
Set of total functions from S to T.

The set {f | f : S +-> T & dom(f) = S}.
S >+> T
Set of partial injections from S to T (also known as `one-to-one relations').

The set {f | f : S +-> T & f~ : T +-> S}.
S >-> T
Set of total injections from S to T.

The set S >+> T /\ S --> T.
S +->> T
Set of partial surjections from S to T.

The set {f | f: S +-> T & ran(f)=T}.
S -->> T
Set of total surjections from S to T.

The set S +->> T /\ S --> T.
S >->> T
Set of bijections from S to T.

The set S -->> T /\ S >-> T.
%z.(z: S & P | E)
Function construction. The function {x,y | z: S & y=E & P} where y\E and y\P, with domain {z | z: S & P}.
%z.(P | E)
Function construction. The predicate P must, for each variable x in the list z, contain a constraining predicate i.e. x: S, x <: S, x <<: S or x = E, with z\S, z\E.
f(x)
For x: dom(f), f(x) denotes the value of the function f at x, i.e. x |-> f(x): f.

Sequences

A sequence over a set S is a function from NAT to S whose domain is an interval 1..n for some natural number n. Let s, t be sequences of elements from S, e be an element of S, and E and F be expressions.
<>
The empty sequence.
seq(S)
The set of finite sequences of elements from S.
seq1(S)
The set of finite non-empty sequences of elements from S. seq1(s) = seq(s) - {<>}.
iseq(S)
The set of injective sequences of elements from S. iseq(S) = seq(S) /\ (NAT1 >+> S).
perm(S)
The set of bijective sequences of elements from a finite set S. A sequence belonging to perm(S) is said to be a `permutation' of S. For finite S, perm(S) = 1..card(S) >->> S.
s^t
The concatenation of sequences s and t.
e -> s
The sequence formed by prepending e to s.
s <- e
The sequence formed by appending e to s.
[E]
Provided that E is not an Expression List, [E] is the singleton sequence with element E, i.e [E] = E -> <>.
[E,F]
Provided F is not an Expression List, then this is [E] with F appended. Equivalent to [E] <- F.
size(s)
The size of the finite sequence s.
rev(s)
The reverse of s.
s /|\ n
The sequence obtained from s by retaining only its first n elements, where n <= size(s).
s \|/ n
The sequence obtained by removing the first n elements of s, where n <= size(s).
first(s)
The first element of the non-empty sequence s.
last(s)
The last element of the non-empty sequence s.
tail(s)
The sequence s with its first element removed (s must be non-empty).
front(s)
The sequence s with its last element removed (s must be non-empty).
conc(s)
The generalised concatenation of a sequence of sequences, s. For a sequence t, conc(<>) = <> and conc(s <- t) = conc(s)^t.

Variables, Variable Lists and Identifiers

A Variable is an Identifier. An Identifier is a string of length 2 or more of alphanumeric characters ( a to z, A to Z, 0 to 9 ASCII codes) or underscore `_', with at least one letter. An Upper Case Identifier is an Identifier made only from upper case letters and underscore. An Infix operator is either a string of non-alphanumeric characters (excluding `_' ``' `$' and `?') or an Identifier declared as an Infix Operator in the AMN Symbol Table, e.g. `mod'.

Let z be a Variable List and x be a Variable.

z,x
((z,x)) is a Variable List.

Generalised Substitutions

Let x be a Variable, z be a variable List, P and R be predicates, E and F be Expressions, and S, T be Generalised Substitutions.
[S]P
A predicate obtained by replacing the variables in P according to the rules below.
[x:= E]F
An expression obtained by replacing all free occurrences of x in F by E.
z\A
Non-freeness: z is not free in E, i.e. there are no free occurrences of z in the Predicate or Expression A.
x:= E
Simple substitution. Substitute E for x in a Predicate or Expression formula. (Note that the applicability of a simple substitution on a formula is limited by non-freeness conditions when the formula is a quantified expression or a set comprehension).
x,y:= E,F
Simultaneous substitution. Substitute several Expressions for several Variables.
x:=E || y:=F
Simultaneous substitution. A form equivalent to the above simultaneous substitution.
P | S
Pre-conditioning of S by P. [P | S]R = P & [S]R.
P ==> S
Guarding of S by P. [P ==> S]R = P => [S]R.
S [] T
Choice between S and T. [S [] T]R = [S]R & [T]R.
@z.S
Unbounded choice. [@z.S]R = !z.[S]R
S;T
Sequencing. [S;T]R = [S][T]R.
skip
No-op.
 
A full on-line help listing is available in the Contents Page
Also available in the form of a complete Index.
Blogo © B-Core (UK) Limited, Last updated: 25/08/99