3.3.5 Relations

3.3.5.1 Pairs and Cartesian product

 |-> Pair ** Cartesian product
Description

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 .

Definition

Types

with and .
with and .

WD

3.3.5.2 Relations

 <-> Relations <<-> Total relations <->> Surjective relations <<->> Total surjective relations
Description

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.

Definition

Types

For and for each operator of , , , :

WD

for each operator of , , , .

3.3.5.3 Domain and Range

 dom Domain ran Range
Description

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 .

Definition

Types

and with .

WD

3.3.5.4 Domain and Range Restrictions

 <| Domain restriction <<| Domain subtraction |> Range restriction |>> Range subtraction
Description

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 .

Definition

Types

and with and
and with and

WD

for each operator of , , ,

3.3.5.5 Operations on relations

 ; Relational forward composition circ Relational backward composition <+ Relational override || Parallel product >< Direct product ~ Inverse
Description

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 .

Definition

Types

with and
with and
with and
with and
with and
with

WD

for each operator of , , , ,

3.3.5.6 Relational image

 […] Relational image
Description

The relational image are those elements in the range of that are mapped from .

Definition

Types

with and

WD

3.3.5.7 Constant relations

 id Identity relation prj1 First projection prj2 Second projection
Description

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.

Definition

Types

for an arbitrary type .
and for arbitrary types and .

WD

Example

The assumption that a relation is irreflexive can be expressed by:

3.3.5.8 Sets of functions

 +-> Partial functions –> Total functions >+> Partial injections >-> Total injections +->> Partial surjections –>> Total surjections >->> Bijections
Description

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.

Definition

Types

, for each operator of , , , , , , :

WD

For each operator of , , , , , , :

3.3.5.9 Function application

 (…) Function application
Description

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.

Definition

Types

with and

WD

with being the type of .

3.3.5.10 Lambda

 % Lambda
Description

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.

Definition

Types

with , being a predicate and .

WD

Example

A function that returns the double value of a natural number:

The dot product of two 2-dimensional vectors can be defined by: