Mathematical Notation

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

Notes on operator binding

Compound formulae (e.g. A => B & C) are given an unambiguous interpretation by the operator binding rules:

All operators bind to the left (are left-associative) except ``.'' which binds to the right.
Each symbol (e.g. &) is given a priority, and the highest priorities bind strongest,
e.g. A => B & C is equivalent to A => (B & C).
In case of equal priority the leftmost operator binds the strongest,
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