Rodin User’s Handbook v.2.4: Typing

3.3.7 Typing

$\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$

oftype

of type

Description

$\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha$ is an expression that has exactly the value of $\textsf{E}$ but its type is specified by the type expression $\alpha$ (3.3.1.1).

$\mathsf{\textsf{E}}$ is restricted to expressions whose type does not depend on an argument of that expression. These are the constant relations $\mathop {\mathrm{id}}\nolimits$ , $\mathop {\mathrm{prj}_1}\nolimits$ , $\mathop {\mathrm{prj}_2}\nolimits$ and the empty set $\emptyset$ .

Another location where the operator can be used is the declaration of bound variables in quantifiers and patterns in lambda expressions. Each identifier can be followed by $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ and the identifier’s type.

Definition

$\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha = \textsf{E}$

Types

$\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha \in \alpha$ with $\textsf{E}\in \alpha$

WD

$\mathcal{L}(\textsf{E}\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\alpha ) \mathrel {\widehat=}\mathcal{L}(\textsf{E})$

Example

The predicate $\emptyset =\emptyset$ is not correctly typed in Event-B because the types of $\emptyset$ are not inferable. A valid alternative would be:
$(\emptyset \mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathbb Z}) = \emptyset$

The predicate $\exists x,y ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\neq y$ is not correctly typed because the types of $x$ and $y$ cannot be inferred: A valid alternative (for integers) is:
$\exists x\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathbb Z},y ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\neq y$

The following lambda expression uses the $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ operator:
$(\lambda x\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathbb Z}\mapsto y\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}\mathord {\mathrm{BOOL}}~ |~ x>0 ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x+1)$
An arguably more readable version without the use of $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ is:
$(\lambda x\mapsto y ~ |~ x>0 \land y\in \mathord {\mathrm{BOOL}}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x+1)$