Concrete semantics of binary operator

[leporia]

Your Name

Andrea Lepori

Question

During the lecture we defined the following for the concrete semantics of the binary operator

but I'm quite confused as $[[E_1]](m)$ and $[[E_2](m)$ are a sets ($\wp(\mathbb{Z})$) hence the signature of the operator should be
$\wp(\mathbb{Z}) \to \wp(\mathbb{Z}) \to \wp(\mathbb{Z})$

But then homework 3 we defined it as

which makes a lot more sense and is much more useful for proving the soundness of abstract binary operators.

Hence my question is can we always used the definition served in homework 3? If not how should we prove the soundness of abstract binary operators using the definition showed in the slides?

[KihongHeo]

Hi.

• $[[E]] \in \mathbb{Z} \to \mathbb{Z} \to \mathbb{Z}$ and $[[E]]_{\wp} \in \wp(\mathbb{Z}) \to \wp(\mathbb{Z})\to \wp(\mathbb{Z})$ are different.
• Sorry for the confusion. I changed the lecture slide but forgot to fix it for the homework. Both of them are okay to prove the soundness. But I used the former because the latter introduces unnecessary garbage information. (guess what)

[leporia]

Thanks for the answer. I'm sorry I've missed the difference. It now makes much more sense.
From my understanding then the following should hold
$\{[[E]](m)\} = [[E]]_{\wp}(\{m\})$