|
|-> |
Pair |
|
** |
Cartesian product |
denotes the pair whose first element is
and second element is
.
denotes the set of pairs where the first element is a member of
and second element is a member of
.
with
and
.
with
and
.
|
<-> |
Relations |
|
<<-> |
Total relations |
|
<->> |
Surjective relations |
|
<<->> |
Total surjective relations |
is the set of relations between the two sets
and
. A relation consists of pairs where the first element is of
and the second of
.
is just an abbreviation for
.
A total relation is a relation which relates each element of to at least one element of
.
A surjective relation is a relation where there is at least one element of for each element of
such that both are related.
For and
for each operator
of
,
,
,
:
for each operator
of
,
,
,
.
|
dom |
Domain |
|
ran |
Range |
If is a relation between the sets
and
, the domain
is the set of the elements of
that are related to at least one element of
by
.
Likewise the range is the set of elements of
to which at least one element of
relates by
.
and
with
.
|
<| |
Domain restriction |
|
<<| |
Domain subtraction |
|
|> |
Range restriction |
|
|>> |
Range subtraction |
The domain restriction is a subset of the relation
that contains all of the pairs whose first element is in
.
is the subset where the pair’s first element is not in
.
In the same way, the range restriction is a subset that contains all of the pairs whose second element is in
and
is the set where the pair’s second element is not in
.
and
with
and
and
with
and
for each operator
of
,
,
,
|
; |
Relational forward composition |
|
circ |
Relational backward composition |
|
<+ |
Relational override |
|
|| |
Parallel product |
|
>< |
Direct product |
|
~ |
Inverse |
An element is related by
to an element
if there is an element
such that
relates
to
and
relates
to
.
can be written as an alternative to
. This reflects the fact that
holds for two functions
and
.
The relational overwrite is equal to
except all entries in
whose first element is in the domain of
are replaced by the corresponding entries in
.
The parallel product relates a pair
to a pair
when
relates
to
and
relates
to
.
If a relation relates an element
to
and
relates
to
, the direct product
relates
to the pair
.
The inverse relation relates an element
to
if the original relation
relates
to
.
with
and
with
and
with
and
with
and
with
and
with
for each operator
of
,
,
,
,
|
[…] |
Relational image |
The relational image are those elements in the range of
that are mapped from
.
with
and
|
id |
Identity relation |
|
prj1 |
First projection |
|
prj2 |
Second projection |
is the identity relation that maps every element to itself.
is a function that maps a pair to its first element. Likewise
maps a pair to its second element.
,
and
are generic definitions. Their type must be inferred from the environment.
for an arbitrary type
.
and
for arbitrary types
and
.
The assumption that a relation is irreflexive can be expressed by:
|
+-> |
Partial functions |
|
–> |
Total functions |
|
>+> |
Partial injections |
|
>-> |
Total injections |
|
+->> |
Partial surjections |
|
–>> |
Total surjections |
|
>->> |
Bijections |
A partial function from to
is a relation that maps an element of
to at most one element of
. A function is total if its domain contains all elements of
, i.e. it maps every element of
to an element of
.
A function is injective (is an injection) if two distinct elements of are always mapped to distinct elements of
. It is also equivalent to say that the inverse of an injective function is a also a function.
A function is surjective (is a surjection) if for every element of there exists an element in
that is mapped to it.
A function is bijective (is a bijection) if it is both injective and surjective.
,
for each operator
of
,
,
,
,
,
,
:
For each operator of
,
,
,
,
,
,
:
|
(…) |
Function application |
The function application yields the value for
of the function
. It is only defined if
is in the domain of
and if
is actually a function.
with
and
with
being the type of
.
|
% |
Lambda |
is a function that maps an “input”
to a result
such that
holds.
is a pattern of identifiers, parentheses and
which follows the following rules:
An identifier is a pattern.
An identifier , followed by an
operator is a pattern (See 3.3.7 for more details).
A pair is a pattern if
and
are patterns.
is pattern if
is pattern.
In the simplest case, is just an identifier.
with
,
being a predicate and
.
A function that returns the double value of a natural number:
The dot product of two 2-dimensional vectors can be defined by: