Syntropy Type view Object diagrams/mechanisms Statecharts Logic Value types Glossary

Logic

Definitions and declarations

Definition of LHS as syntactically equivalent to RHS.
x : T Declaration of identifier x to stand for a member of the set T (which may be a type name or any expression yielding a set).
x, y : T Equivalent to x : T, y : T
( ) Groups terms in expressions

Logic

true, false Logical constants
not P Negation: ‘not P’.
Conjunction: ‘P and Q’
Disjunction: ‘P or Q’
Implication: ‘P implies Q’ or ‘if P then Q’
Equivalence: ‘P is logically equivalent to Q’ or ‘P if and only if Q’
Conditional: ‘if P then Q else R’.
Universal quantification: ‘for all x in set S, P holds’.
Existential quantification: ‘there exists an x in S such that P holds’.
Unique existence: ‘there exists a unique x in S such that P holds’.
Equality between terms.

Sets

Set membership: ‘t is a member of S’.
* not (t * S)
Set inclusion: ‘every member of S is also in T’.
{ } The empty set.
The set containing the terms t1 through tn
#S Size of the set S
set of S Powerset: set of all subsets of S.
The set containing exactly those x in S for which P holds.
Given declarations D, the set of t’s for which P holds.
Given declarations D, the set of t’s.
Ordered tuple of elements
Set union.
Set difference.
Set intersection.
Distributed set union. Given SS is a set of sets with members taken from S, ‘the union of all the members of all the sets’
Cartesian product: The set of all 2-tuples such that the first component is a member of S and the second a member of T.
sum S The numerical sum all of the elements of the set S.

Also defined over sequences and bags.
min S Minimum of a set (or sequence or bag)
max S Maximum of a set (or sequence or bag)

Functions

The set of total functions from S to T.

Bags

Mathematically, a bag is treated as a function mapping elements of the bag to positive integers, representing the number of times the element appears in the bag.

bag of T The set of bags whose elements are drawn from set T.
#X The number of elements in bag X
The empty bag
The bag containing x1, x2...,xn with the frequency in which they occur in the list.
members X The set formed from the elements of bag X.

Sequences

Mathematically, a sequence is treated as a function mapping positive integers, representing position in the sequence, to elements of the sequence.

seq of T The set of sequences whose elements are drawn from set T.
#A The length of sequence A
The empty sequence
The sequence containing a1, a2..., and an
The sequence formed by concatenating the sequence A with the sequence B.
A(n) The nth element of sequence A.
members A The set formed from the elements of A.
items A The bag of items contained in the sequence A.
head A The first element of a sequence or nil if the sequence is empty.
last A The last element of a sequence or nil if the sequence is empty.
tail A All but the head of a sequence.
front A All but the last of a sequence.

Sorted sequences

The sorted sequence formed by inserting element e into the sorted sequence S, following the sort rule for S.

Objects

a in Q True if the object a is in state Q, false otherwise.


Comments, corrections to jdaniels@cix.co.uk