Rodin Handbook





 
Previous: Sets Up: Mathematical Notation Next: Arithmetic Rodin User’s Handbook v.2.8

3.3.5 Relations

3.3.5.1 Pairs and Cartesian product

$\mapsto $

|->

Pair

$\mathbin \times $

**

Cartesian product

Description

$\textsf{E}\mapsto \textsf{F}$ denotes the pair whose first element is $\textsf{E}$ and second element is $\textsf{F}$.

$\textsf{S}\mathbin \times \textsf{T}$ denotes the set of pairs where the first element is a member of $\textsf{S}$ and second element is a member of $\textsf{T}$.

Definition

$\textsf{S}\mathbin \times \textsf{T}\mathrel {\widehat=}\{ ~ x\mapsto y~ |~ x\in \textsf{S}\land y\in \textsf{T}~ \} $

Types

$\textsf{E}\mapsto \textsf{F}\in \alpha \mathbin \times \beta $ with $\textsf{E}\in \alpha $ and $\textsf{F}\in \beta $.
$\textsf{S}\mathbin \times \textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$.

WD

$\mathcal{L}(\textsf{E}\mapsto \textsf{F})\mathrel {\widehat=}\mathcal{L}(\textsf{E})\land \mathcal{L}(\textsf{F})$
$\mathcal{L}(\textsf{S}\mathbin \times \textsf{T})\mathrel {\widehat=}\mathcal{L}(\textsf{S})\land \mathcal{L}(\textsf{T})$


3.3.5.2 Relations

$\mathbin \leftrightarrow $

<->

Relations

$\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$

<<->

Total relations

$\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$

<->>

Surjective relations

$\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$

<<->>

Total surjective relations

Description

$\textsf{S}\mathbin \leftrightarrow \textsf{T}$ is the set of relations between the two sets $\textsf{S}$ and $\textsf{T}$. A relation consists of pairs where the first element is of $\textsf{S}$ and the second of $\textsf{T}$. $\textsf{S}\mathbin \leftrightarrow \textsf{T}$ is just an abbreviation for $\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S}\mathbin \times \textsf{T})$.

A total relation is a relation which relates each element of $\textsf{S}$ to at least one element of $\textsf{T}$.

A surjective relation is a relation where there is at least one element of $\textsf{S}$ for each element of $\textsf{T}$ such that both are related.

Definition

$\textsf{S}\mathbin \leftrightarrow \textsf{T}\mathrel {\widehat=}\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S}\mathbin \times \textsf{T})$
$\textsf{S}\mathbin {\leftarrow \mkern -14mu\leftrightarrow }\textsf{T}\mathrel {\widehat=}\{ ~ r~ |~ r\in \textsf{S}\mathbin \leftrightarrow \textsf{T}\land \mathop {\mathrm{dom}}\nolimits (r) = \textsf{S}~ \} $
$\textsf{S}\mathbin {\leftrightarrow \mkern -14mu\rightarrow }\textsf{T}\mathrel {\widehat=}\{ ~ r~ |~ r\in \textsf{S}\mathbin \leftrightarrow \textsf{T}\land \mathop {\mathrm{ran}}\nolimits (r) = \textsf{T}~ \} $
$\textsf{S}\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }\textsf{T}\mathrel {\widehat=}(\textsf{S}\mathbin {\leftarrow \mkern -14mu\leftrightarrow }\textsf{T}) \land (\textsf{S}\mathbin {\leftrightarrow \mkern -14mu\rightarrow }\textsf{T})$

Types

For $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ for each operator $\mathbin {\Box }$ of $\mathbin \leftrightarrow $, $\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$:
$\textsf{S}\mathbin {\Box }\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta ))$

WD

$\mathcal{L}(\textsf{S}\mathbin {\Box }\textsf{T}) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \mathcal{L}(\textsf{T})$ for each operator $\mathbin {\Box }$ of $\mathbin \leftrightarrow $, $\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$.


3.3.5.3 Domain and Range

$\mathop {\mathrm{dom}}\nolimits $

dom

Domain

$\mathop {\mathrm{ran}}\nolimits $

ran

Range

Description

If $r$ is a relation between the sets $\textsf{S}$ and $\textsf{T}$, the domain $\mathop {\mathrm{dom}}\nolimits (\textsf{r})$ is the set of the elements of $\textsf{S}$ that are related to at least one element of $\textsf{T}$ by $\textsf{r}$.

Likewise the range $\mathop {\mathrm{ran}}\nolimits (\textsf{r})$ is the set of elements of $\textsf{T}$ to which at least one element of $\textsf{S}$ relates by $\textsf{r}$.

Definition

$\mathop {\mathrm{dom}}\nolimits (\textsf{r}) \mathrel {\widehat=}\{ ~ x~ |~ \exists y~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\mapsto y\in \textsf{r}~ \} $
$\mathop {\mathrm{ran}}\nolimits (\textsf{r}) \mathrel {\widehat=}\{ ~ y~ |~ \exists x~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\mapsto y\in \textsf{r}~ \} $

Types

$\mathop {\mathrm{dom}}\nolimits (\textsf{r})\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\mathop {\mathrm{ran}}\nolimits (\textsf{r})\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$.

WD

$\mathcal{L}(\mathop {\mathrm{dom}}\nolimits (\textsf{r})) \mathrel {\widehat=}\mathcal{L}(\textsf{r})$
$\mathcal{L}(\mathop {\mathrm{ran}}\nolimits (\textsf{r})) \mathrel {\widehat=}\mathcal{L}(\textsf{r})$


3.3.5.4 Domain and Range Restrictions

$\mathbin \lhd $

<|

Domain restriction

$\mathbin {\lhd \mkern -14mu-}$

<<|

Domain subtraction

$\mathbin \rhd $

|>

Range restriction

$\mathbin {\rhd \mkern -14mu-}$

|>>

Range subtraction

Description

The domain restriction $\textsf{S}\mathbin \lhd \textsf{r}$ is a subset of the relation $\textsf{r}$ that contains all of the pairs whose first element is in $\textsf{S}$. $\textsf{S}\mathbin {\lhd \mkern -14mu-}\textsf{r}$ is the subset where the pair’s first element is not in $\textsf{S}$.

In the same way, the range restriction $\textsf{r}\mathbin \rhd \textsf{S}$ is a subset that contains all of the pairs whose second element is in $\textsf{S}$ and $\textsf{r}\mathbin {\rhd \mkern -14mu-}\textsf{S}$ is the set where the pair’s second element is not in $\textsf{S}$.

Definition

$\textsf{S}\mathbin \lhd \textsf{r}\mathrel {\widehat=}\{ ~ x\mapsto y~ |~ x\mapsto y\in \textsf{r}\land x\in \textsf{S}\} $
$\textsf{S}\mathbin {\lhd \mkern -14mu-}\textsf{r}\mathrel {\widehat=}\{ ~ x\mapsto y~ |~ x\mapsto y\in \textsf{r}\land x\not\in \textsf{S}\} $
$\textsf{r}\mathbin \rhd \textsf{S}\mathrel {\widehat=}\{ ~ x\mapsto y~ |~ x\mapsto y\in \textsf{r}\land y\in \textsf{S}\} $
$\textsf{r}\mathbin {\rhd \mkern -14mu-}\textsf{S}\mathrel {\widehat=}\{ ~ x\mapsto y~ |~ x\mapsto y\in \textsf{r}\land y\not\in \textsf{S}\} $

Types

$\textsf{S}\mathbin \lhd \textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{S}\mathbin {\lhd \mkern -14mu-}\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$
$\textsf{r}\mathbin \rhd \textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{r}\mathbin {\rhd \mkern -14mu-}\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$

WD

$\mathcal{L}(\textsf{S}\mathbin {\Box }\textsf{r})\mathrel {\widehat=}\mathcal{L}(\textsf{S})\land \mathcal{L}(\textsf{r})$ for each operator $\mathbin {\Box }$ of $\mathbin \lhd $, $\mathbin {\lhd \mkern -14mu-}$, $\mathbin \rhd $, $\mathbin {\rhd \mkern -14mu-}$


3.3.5.5 Operations on relations

$\mathbin ;$

;

Relational forward composition

$\circ $

circ

Relational backward composition

$\mathbin {\lhd \mkern -9mu-}$

<+

Relational override

$\mathbin \| $

||

Parallel product

$\mathbin \otimes $

><

Direct product

$\mbox{}^{-1}$

~

Inverse

Description

An element $x$ is related by $\textsf{r}\mathbin ;\textsf{S}$ to an element $y$ if there is an element $z$ such that $\textsf{r}$ relates $x$ to $z$ and $\textsf{S}$ relates $z$ to $y$.

$\textsf{s}\circ \textsf{r}$ can be written as an alternative to $\textsf{r}\mathbin ;\textsf{s}$. This reflects the fact that $f(g(x)) = (f\circ g)(x)$ holds for two functions $f$ and $g$.

The relational overwrite $\textsf{r}\mathbin {\lhd \mkern -9mu-}\textsf{s}$ is equal to $\textsf{r}$ except all entries in $\textsf{r}$ whose first element is in the domain of $\textsf{s}$ are replaced by the corresponding entries in $\textsf{s}$.

The parallel product $\textsf{r}\mathbin \| \textsf{s}$ relates a pair $x\mapsto y$ to a pair $m\mapsto n$ when $\textsf{r}$ relates $x$ to $m$ and $\textsf{s}$ relates $y$ to $n$.

If a relation $\textsf{r}$ relates an element $x$ to $y$ and $\textsf{s}$ relates $x$ to $z$, the direct product $\textsf{r}\mathbin \otimes \textsf{s}$ relates $x$ to the pair $y\mapsto z$.

The inverse relation $\textsf{r}^{-1}$ relates an element $x$ to $y$ if the original relation $\textsf{r}$ relates $y$ to $x$.

Definition

$\textsf{r}\mathbin ;\textsf{s}\mathrel {\widehat=}\{ ~ x \mapsto y~ |~ \exists z~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x \mapsto z \in \textsf{r}\land z \mapsto y\in \textsf{s}~ \} $
$\textsf{r}\circ \textsf{s}\mathrel {\widehat=}\textsf{s}\mathbin ;\textsf{r}$
$\textsf{r}\mathbin {\lhd \mkern -9mu-}\textsf{s}\mathrel {\widehat=}\textsf{s}\mathbin {\mkern 1mu\cup \mkern 1mu}(dom(\textsf{s})\mathbin {\lhd \mkern -14mu-}\textsf{r})$
$\textsf{r}\mathbin \| \textsf{s}\mathrel {\widehat=}\{ ~ (x\mapsto y)\mapsto (m\mapsto n)~ |~ x\mapsto m\in \textsf{r}\land y\mapsto n\in \textsf{s}~ \} $
$\textsf{r}\mathbin \otimes \textsf{s}\mathrel {\widehat=}\{ ~ x\mapsto (y\mapsto z)~ |~ x\mapsto y\in \textsf{r}\land x\mapsto z\in \textsf{s}~ \} $
$\textsf{r}^{-1} \mathrel {\widehat=}\{ y\mapsto x~ |~ x\mapsto y\in \textsf{r}~ \} $

Types

$\textsf{r}\mathbin ;\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \gamma )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta \mathbin \times \gamma )$
$\textsf{r}\circ \textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\gamma \mathbin \times \alpha )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta \mathbin \times \gamma )$
$\textsf{r}\mathbin {\lhd \mkern -9mu-}\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$
$\textsf{r}\mathbin \| \textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (~ (\alpha \mathbin \times \gamma )\mathbin \times (\beta \mathbin \times \delta )~ )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\gamma \mathbin \times \delta )$
$\textsf{r}\mathbin \otimes \textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times (\beta \mathbin \times \gamma ))$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{s}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \gamma )$
$\textsf{r}^{-1}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta \mathbin \times \alpha )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$

WD

$\mathcal{L}(\textsf{r}\mathbin {\Box }\textsf{s})\mathrel {\widehat=}\mathcal{L}(\textsf{r})\land \mathcal{L}(\textsf{s})$ for each operator $\mathbin {\Box }$ of $\mathbin ;$, $\circ $, $\mathbin {\lhd \mkern -9mu-}$, $\mathbin \| $, $\mathbin \otimes $
$\mathcal{L}(\textsf{r}^{-1})\mathrel {\widehat=}\mathcal{L}(\textsf{r})$


3.3.5.6 Relational image

$[\ldots ]$

[…]

Relational image

Description

The relational image $\textsf{r}[\textsf{S}]$ are those elements in the range of $\textsf{r}$ that are mapped from $\textsf{S}$.

Definition

$\textsf{r}[\textsf{S}] \mathrel {\widehat=}\{ ~ y~ |~ \exists x~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\in \textsf{S}\land x\mapsto y\in \textsf{r}~ \} $

Types

$\textsf{r}[\textsf{S}]\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ with $\textsf{r}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$

WD

$\mathcal{L}(\textsf{r}[\textsf{S}])\mathrel {\widehat=}\mathcal{L}(\textsf{r})\land \mathcal{L}(\textsf{S})$


3.3.5.7 Constant relations

$\mathop {\mathrm{id}}\nolimits $

id

Identity relation

$\mathop {\mathrm{prj}_1}\nolimits $

prj1

First projection

$\mathop {\mathrm{prj}_2}\nolimits $

prj2

Second projection

Description

$\mathop {\mathrm{id}}\nolimits $ is the identity relation that maps every element to itself.

$\mathop {\mathrm{prj}_1}\nolimits $ is a function that maps a pair to its first element. Likewise $\mathop {\mathrm{prj}_2}\nolimits $ maps a pair to its second element.

$\mathop {\mathrm{id}}\nolimits $, $\mathop {\mathrm{prj}_1}\nolimits $ and $\mathop {\mathrm{prj}_2}\nolimits $ are generic definitions. Their type must be inferred from the environment.

Definition

$\mathop {\mathrm{id}}\nolimits \mathrel {\widehat=}\{ ~ x\mapsto x~ |~ \mathord {\top }~ \} $
$\mathop {\mathrm{prj}_1}\nolimits \mathrel {\widehat=}\{ ~ (x\mapsto y)\mapsto x~ |~ \mathord {\top }~ \} $
$\mathop {\mathrm{prj}_2}\nolimits \mathrel {\widehat=}\{ ~ (x\mapsto y)\mapsto y~ |~ \mathord {\top }~ \} $

Types

$\mathop {\mathrm{id}}\nolimits \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \alpha )$ for an arbitrary type $\alpha $.
$\mathop {\mathrm{prj}_1}\nolimits \in \mathop {\mathbb P\hbox{}}\nolimits ((\alpha \mathbin \times \beta )\mathbin \times \alpha )$ and $\mathop {\mathrm{prj}_1}\nolimits \in \mathop {\mathbb P\hbox{}}\nolimits ((\alpha \mathbin \times \beta )\mathbin \times \beta )$ for arbitrary types $\alpha $ and $\beta $.

WD

$\mathcal{L}(\mathop {\mathrm{id}}\nolimits )\mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathop {\mathrm{prj}_1}\nolimits )\mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathop {\mathrm{prj}_2}\nolimits )\mathrel {\widehat=}\mathord {\top }$

Example

The assumption that a relation $r$ is irreflexive can be expressed by:
$r\mathbin {\mkern 1mu\cap \mkern 1mu}\mathop {\mathrm{id}}\nolimits =\emptyset $


3.3.5.8 Sets of functions

$ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $

+->

Partial functions

$\mathbin \rightarrow $

–>

Total functions

$ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $

>+>

Partial injections

$\mathbin \rightarrowtail $

>->

Total injections

$ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $

+->>

Partial surjections

$\mathbin \twoheadrightarrow $

–>>

Total surjections

$\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $

>->>

Bijections

Description

A partial function from $\textsf{S}$ to $\textsf{T}$ is a relation that maps an element of $\textsf{S}$ to at most one element of $\textsf{T}$. A function is total if its domain contains all elements of $\textsf{S}$, i.e. it maps every element of $\textsf{S}$ to an element of $\textsf{T}$.

A function is injective (is an injection) if two distinct elements of $\textsf{S}$ are always mapped to distinct elements of $\textsf{T}$. 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 $\textsf{T}$ there exists an element in $\textsf{S}$ that is mapped to it.

A function is bijective (is a bijection) if it is both injective and surjective.

Definition

$\textsf{S} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \textsf{T}\mathrel {\widehat=}\{ ~ f ~ |~ f\in \textsf{S}\mathbin \leftrightarrow \textsf{T}\land (\forall e,x,y \mathord {\mkern 1mu\cdot \mkern 1mu}e\mapsto x\in f \land e\mapsto y\in f \mathbin \Rightarrow x=y) ~ \} $
$\textsf{S}\mathbin \rightarrow \textsf{T}\mathrel {\widehat=}\{ ~ f ~ |~ f\in \textsf{S} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \textsf{T}\land \mathop {\mathrm{dom}}\nolimits (f) = \textsf{S}~ \} $
$\textsf{S} \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } \textsf{T}\mathrel {\widehat=}\{ ~ f ~ |~ f\in \textsf{S} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \textsf{T}\land f^{-1} \in \textsf{T} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \textsf{S}~ \} $
$\textsf{S}\mathbin \rightarrowtail \textsf{T}\mathrel {\widehat=}(\textsf{S} \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } \textsf{T}) \mathbin {\mkern 1mu\cap \mkern 1mu}(\textsf{S}\mathbin \rightarrow \textsf{T})$
$\textsf{S} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } \textsf{T}\mathrel {\widehat=}\{ ~ f ~ |~ f\in \textsf{S} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \textsf{T}\land \mathop {\mathrm{ran}}\nolimits (f) = \textsf{T}~ \} $
$\textsf{S}\mathbin \twoheadrightarrow \textsf{T}\mathrel {\widehat=}(\textsf{S} \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } \textsf{T}) \mathbin {\mkern 1mu\cap \mkern 1mu}(\textsf{S}\mathbin \rightarrow \textsf{T})$
$\textsf{S}\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } \textsf{T}\mathrel {\widehat=}(\textsf{S}\mathbin \rightarrowtail \textsf{T}) \mathbin {\mkern 1mu\cap \mkern 1mu}(\textsf{S}\mathbin \twoheadrightarrow \textsf{T})$

Types

$\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$, $\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ for each operator $\mathbin {\Box }$ of $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $, $\mathbin \rightarrow $, $ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $, $\mathbin \rightarrowtail $, $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $, $\mathbin \twoheadrightarrow $, $\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $:
$\textsf{S}\mathbin {\Box }\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta ))$

WD

For each operator $\mathbin {\Box }$ of $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $, $\mathbin \rightarrow $, $ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $, $\mathbin \rightarrowtail $, $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $, $\mathbin \twoheadrightarrow $, $\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $:
$\mathcal{L}(\textsf{S}\mathbin {\Box }\textsf{T}) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \mathcal{L}(\textsf{T})$



3.3.5.9 Function application

$(\ldots )$

(…)

Function application

Description

The function application $\textsf{f}(\textsf{a})$ yields the value for $\textsf{a}$ of the function $\textsf{f}$. It is only defined if $\textsf{a}$ is in the domain of $\textsf{f}$ and if $\textsf{f}$ is actually a function.

Definition

$\textsf{a}\mapsto \textsf{f}(\textsf{a})\in \textsf{f}$

Types

$\textsf{f}(\textsf{a})\in \beta $ with $\textsf{f}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $\textsf{a}\in \alpha $

WD

$\mathcal{L}(\textsf{f}(\textsf{a}))\mathrel {\widehat=}\mathcal{L}(\textsf{f})\land \mathcal{L}(\textsf{a})\land \textsf{f}\in \alpha \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \beta \land \textsf{a}\in \mathop {\mathrm{dom}}\nolimits (\textsf{f})$ with $\mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ being the type of $\textsf{f}$.


3.3.5.10 Lambda

$\lambda $

%

Lambda

Description

$(\lambda ~ \textsf{p}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ )$ is a function that maps an “input” $\textsf{p}$ to a result $\textsf{E}$ such that $\textsf{P}$ holds.

$\textsf{p}$ is a pattern of identifiers, parentheses and $\mapsto $ which follows the following rules:

  • An identifier $x$ is a pattern.

  • An identifier $x$, followed by an $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ operator is a pattern (See 3.3.7 for more details).

  • A pair $\textsf{a}\mapsto \textsf{b}$ is a pattern if $\textsf{a}$ and $\textsf{b}$ are patterns.

  • $(\textsf{a})$ is pattern if $\textsf{a}$ is pattern.

In the simplest case, $\textsf{p}$ is just an identifier.

Definition

$(\lambda ~ \textsf{p}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ ) \mathrel {\widehat=}\{ ~ \textsf{p}\mapsto \textsf{E}~ |~ \textsf{P}~ \} $

Types

$(\lambda ~ \textsf{p}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ )\in \mathop {\mathbb P\hbox{}}\nolimits (~ \alpha \mathbin \times \beta ~ )$ with $\textsf{p}\in \alpha $, $\textsf{P}$ being a predicate and $\textsf{E}\in \beta $.

WD

$\mathcal{L}(\lambda ~ \textsf{p}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ )~ \mathrel {\widehat=}~ \forall \textsl{Free}(\textsf{p})~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \mathcal{L}(\textsf{P})\land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))$

Example

A function $double$ that returns the double value of a natural number:
$double = (\lambda x~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\in \mathord {\mathbb N}~ |~ 2\cdot x)$

The dot product of two 2-dimensional vectors can be defined by:
$dotp = (\lambda ~ (a \mapsto b)\mapsto (c \mapsto d)~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ a\in \mathord {\mathbb Z}\land b\in \mathord {\mathbb Z}\land c\in \mathord {\mathbb Z}\land d\in \mathord {\mathbb Z}~ |~ a\cdot c+b\cdot d~ )$



Previous: Sets Up: Mathematical Notation Next: Arithmetic  
Rodin User’s Handbook v.2.8 : Reference : Mathematical Notation : Relations