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}

ExampleUsing 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:

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

Solution.

• Liam O'Connor

1. \llbracket \mathsf {proc}\ c \rrbracket _\mathcal {E}\ \sigma \ =\ \llbracket c \rrbracket _\mathcal {C}
2. \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 ).

ExampleA 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.