Concrete Semantics 정의[5강 슬라이드]

[bongjunj]

이름 Your Name

장봉준

질문 Question

$[[ x := E ]]_\wp$가 잘못 정의되었습니다.
우선 $[[E]]_\wp$는 m(memory)가 아니라 M(set of memory)를 입력으로 받는데
$[[E]]_{\wp}(m)$ 로 표기되어 있습니다.

그리고 합집합 기호가 implicit하게 들어가있는 것 같은데, 오해를 불러일으킬 수 있습니다.
아래와 같이 표기하는 게 맞아보입니다.

$$\lambda M. \bigcup_{m \in M} \{ m \{ x \mapsto v \} ~|~ v = [[ E ]](m) \}$$

번역본 Translated Version

The definition of $[[ x := E ]]_\wp$ is incorrect.

First, $[[E]]_\wp$ takes a set of memories (M) as input, not a single memory (m), yet it is written as $[[E]]_{\wp}(m)$.

Additionally, the union symbol seems to be implicit, which can be misleading. It should be written as follows:

$$\lambda M. \bigcup_{m \in M} \{ m \{ x \mapsto v \} ~|~ v = [[ E ]](m) \}$$

[duncan020313]

지적해 주신 내용이 맞습니다. 다만, 조건 제시법의 방식으로 작성하는 것이 좀 더 적절해 보입니다.

$$\lambda M. \{ m \{ x \mapsto v \} ~|~ v = [[ E ]](m), m \in M \}$$

---

You are correct. However, it seems more appropriate to write it using set-builder notation.

$$\lambda M. \{ m \{ x \mapsto v \} ~|~ v = [[ E ]](m), m \in M \}$$

[KihongHeo]

Thanks.