1
$\begingroup$

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?

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.