What is the denotation for identifiers?

Question

I am trying to understand what is the domain for denotational semantics.

Right now the way I understand denotational semantics is that given some syntax of a program that maps to some mathematical object that represents its meaning. e.g. for example give some arithmetic expression AExp the denotation $[\_]:AExp \to (State \rightharpoondown Int)$ :

$$ [ 1 + x ]\sigma = 1+x $$

if the state is $\sigma = \{ x:2\}$ then:

$$ [ 1 + x ]\sigma = 3 $$

So indeed given the syntax AExp using the state we can fully determine what the integer should be returned.

I also understand the denotations for statements $[\_]:State \rightharpoondown State $ which makes a lot of sense since that states the state of the program to the next after executing some code in the statement. e.g. $[\{ \}] = 1_{identity}$ the empty statement does not change the state so:

$$ [\{ \}](\sigma) = [\{ \}]\sigma = 1_{identity}(\sigma) = \sigma $$

But I can't figure out what the type should be for the denotation for identifiers. From the notes I am reading CS522 I see this:

$$ x\in Identifier \implies [\sigma] = \sigma(x) $$

which intuitively makes sense but I am having difficulties matching it to the fact that denotaitons should be CPO (Complete Partial Sets). How is the above a CPO? (or the poset, the technicality of existence of LUB/sumpremum is not that important to me). I can't see the POSET.

I guess I am not 100% how the other two are also CPOs...any enlightening comments?

Answer 1

But I can't figure out what the type should be for the denotation for identifiers.

That is because you are implicitly tracing the denotation function $⟦\_⟧$. It might get easier to see the type if you explicitly trace the denotation function by tagging them appropriately. $⟦x + y⟧_{AExp}\sigma = ⟦x⟧_{AExp}\sigma + ⟦y⟧_{AExp}\sigma$.

Similarly, if you have an boolean expression with identifiers, for example: $$⟦a_1 < a_2⟧_{BExp}\sigma = \begin{cases} True &\text{if} ⟦a_1⟧_{AExp}\sigma < ⟦a_2⟧_{AExp}\sigma\\ False &\text{if} ⟦a_1⟧_{AExp}\sigma \geq ⟦a_2⟧_{AExp}\sigma\\ \bot &\text{otherwise} \end{cases}$$

In this case $\sigma : Identifier \rightharpoondown Int$. The type of $\sigma$ would also be implicitly traced by the denotation function because, the object language construct makes it obvious. You can, if you want to be even more pedantic, carry around a tuple of $\sigma$'s, one for each type of variable lookup. So, if your language has integer variables and boolean variables, your $\sigma = (\sigma_{Int}, \sigma_{Bool})$ and the correct component would be chosen depending on which $⟦\_⟧$ is being used.

I guess I am not 100% how the other two are also CPOs...any enlightening comments?

Now, the poset structure is on the co-domain of the denotation function i.e. if you have a denotation $⟦\_⟧_{Stmt}$ the signature of the poset structure will be $(\alpha: State \rightharpoondown State, \preceq, \bot)$ similarly for $⟦\_⟧_{AExp}$ the structure poset structure would be $(\alpha: State \rightharpoondown Int, \preceq, \bot)$, where $\preceq$ allows you to compare the amount of information contained by the information bearers $\alpha$, as explained on pg 159-160 in the notes you have linked.