ASCII Symbols for the Abstract Machine Notation

NOTE: If your browser does not support tables, click here.
RELATIONS
SYMBOL MEANING Cardinality Optionality
Domain Range Domain Range
<-> relation  many many optional optional
+-> partial function many one optional optional
--> total function many one mandatory optional
+->> partial surjection many one optional mandatory
-->> total surjection many one mandatory mandatory
>+> partial injection one one optional optional
>-> total injection one one mandatory optional
>->> bijection  one one mandatory mandatory
 
LOGIC
SYMBOL MEANING 
&  logical and, conjunction 
or  logical disjunction 
=>  logical implication, implies 
<=>  logical equivalence, if and only if 
not  logical negation 
!  universal quantification, for all 
#  existential quantification, there exists 
=  equality 
/=  inequality 
==  rewrite rule 
|->  ordered pair, maplet 
z\A non-freeness of z in A
 
SETS
SYMBOL MEANING 
:  set membership, belongs to, element of 
/:  set non-membership 
<:  set inclusion, subset of 
/<:  set non-inclusion 
*  Cartesian product 
\/  set union 
/\  set intersection 
-  set difference 
{}  empty set, null set 
POW  powerset 
POW1  set of all non-empty subsets 
FIN  set of all finite subsets 
FIN1  set of all non-empty finite subsets 
{E}  singleton set 
{E,F}  enumerated set 
union  generalised union 
inter  generalised intersection 
UNION(z).(P | E)  generalised union 
INTER(z).(P | E)  generalised intersection 
card  set cardinality 
 
NATURALS
SYMBOL MEANING 
>  strict inequality, greater than 
<  strict inequality, less than 
>=  inequality, greater than or equal 
<=  inequality, less than or equal 
NAT  set of natural numbers 
NAT1  set of non-zero natural numbers 
max  maximum 
min  minimum 
+  addition, plus 
-  difference, minus 
*  product 
/  division 
mod  remainder of integer division 
..  interval 
SIGMA  summation 
PI  product 
 
RELATIONS
SYMBOL MEANING 
dom domain of relation 
ran co-domain (or range) of relation
; relational composition
circ relational composition
id identity relation 
<| domain-restriction
|> range-restriction
<<| anti-domain-restriction
|>> anti-range-restriction
r~ inverse 
r[s] image 
<+ overriding 
+> overriding
>< direct product
|| parallel product
iterate(r,n) iteration 
closure(r) reflexive transitive closure
prj1 projection 
prj2 projection
%(z).(P | E) lambda abstraction
f(x) function application
 
SEQUENCES
SYMBOL MEANING 
<> empty sequence
seq(S) set of finite sequences over S
iseq(S) set of injective sequences over S
seq1(S) set of non-empty sequences over S
perm(S) set of bijective sequences over S
^ sequence concatenation
-> prepend 
<- append
[E] singleton sequence
[E,F] sequence enumeration
size sequence size
rev sequence reverse
/|\ sequence projection (prefix)
\|/ sequence projection (suffix)
first first sequence element
last last sequence element
tail sequence tail
front sequence front
conc generalised concatenation
 
AMN SUBSTITUTIONS
SYMBOL MEANING 
x:=E simple substitution
x,y:=E,F simultaneous substitution
x::E membership postconditioned substitution
x: P general postconditioned substitution
S ; T substitution S followed by substitution T
skip no-substitution
oo <-- op(ii) parameterised substitution with input ii, output oo
 
GENERALISED SUBSTITUTIONS
SYMBOL MEANING 
[S]P substitution application to a predicate P
[x:= E]F simple substitution on expression F
P | S pre-conditioning of S by P
P ==> S guarding of S by P
S [] T choice between S and T
@z.S unbounded choice
 

 
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: 22 Feb 2002