This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
Relations
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



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: 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 2dimensional vectors can be defined by:
