# What is the denotation for identifiers?

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?

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