Definition. Set isomorphism [dm-000B]

Liam O'Connor

Two sets $A$ and $B$ are isomorphic, written $A \simeq B$ , iff a bijection exists between them.

Backlinks

Recursively defined semantic domains [dt-0007]

Liam O'Connor

Suppose we extend our notion of expressions in the $\mathcal {C}$ language with parameterless higher-order procedures: $\begin {array}{l} \mathcal {E}\; \Coloneqq \; \cdots \mid \mathsf {proc}\ \mathcal {C}\\ \mathcal {C}\; \Coloneqq \; \cdots \mid x \end {array}$

Example. Using higher-order procedures

Liam O'Connor

We can store procedures in variables, so the program: $\mathit {inc} := (\mathsf {proc}\ a := a + 1); \mathit {inc}; \mathit {inc}$ has the same effects on the variable $a$ as the program: $a := a + 1; a := a + 1$

For our denotational semantics, our domains now take this form ( $\textcolor {blue}{\text {blue}}$ parts are new vs. Example [dt-0004]), where $\uplus$ denotes disjoint union: $\begin {array}{lcl} \mathbf {E} & \triangleq & \Sigma \rightarrow \mathbb {Z}\textcolor {blue}{\ \uplus \ \mathbf {C}}\\ \mathbf {B} & \triangleq & \Sigma \rightarrow \mathbb {B} \\ \mathbf {C} & \triangleq & \Sigma \rightarrow \Sigma \\[0.2em] \Sigma & \triangleq & \mathcal {V} \rightarrow \mathbb {Z}\textcolor {blue}{\ \uplus \ \mathbf {C}} \end {array}$

Exercise. [dt-000P]

Liam O'Connor

Give a semantics to the $\mathsf {proc}$ construct:

$\llbracket \mathsf {proc}\ c \rrbracket _\mathcal {E}\ \sigma \ =\ ?$
$\llbracket x \rrbracket _\mathcal {C}\ \sigma \ =\ ?$

Solution.

Liam O'Connor

$\llbracket \mathsf {proc}\ c \rrbracket _\mathcal {E}\ \sigma \ =\ \llbracket c \rrbracket _\mathcal {C}$
$\llbracket x \rrbracket _\mathcal {C}\ \sigma \ =\ \sigma (x)(\sigma )$

Unfolding the definition of

\Sigma

, we end up with a recursive equation for the definition of

\mathbf {C}

:

\mathbf {C} \; = \; (\mathcal {V} \rightarrow (\mathbb {Z} \uplus \mathbf {C})) \rightarrow (\mathcal {V} \rightarrow (\mathbb {Z} \uplus \mathbf {C}))

Such equations have no set-theoretic solution, even if we weaken equality to mere set isomorphism (here notated

\simeq

).

Example. A simpler equation with no solution

Liam O'Connor

Consider the recursive equation $X = X \rightarrow \mathbb {B}$ . Cantor's theorem says that there is no set $X$ such that $X \simeq \mathcal {P}(X)$ (where $\mathcal {P}(X)$ is the power set of $X$ ), and seeing as $\mathcal {P}(X) \simeq (X \rightarrow \mathbb {B})$ it follows that $X = X \rightarrow \mathbb {B}$ has no solution.

Any kind of higher-order construct leads to such recursive domain equations.

Upshot.

Liam O'Connor

There are no (nontrivial) set-theoretic solutions to the recursive domain equations that arise from higher-order language constructs.

Related

Definition. Set bijection [dm-000A]

Liam O'Connor

A bijection between sets $A$ and $B$ is a one to one correspondence between their elements. That is, $R \subseteq A \times B$ is a bijection between $A$ and $B$ if, for each $x \in A$ , there is exactly one $y \in B$ such that $x\ R\ y$ , and vice versa.