Exercise 7.3: order of logical steps for L-evaluation of *z

Hello,

in the solution to exercise 7.3 C0p - Basics the expression L[*z]\sigma (I don’t know what the latex shortcut for the special bracket is) is immediately transformed into R[z]\sigma without proving that the later term is an address. Obviously the following calculation of R[z]\sigma proves this, however reading the equations from left to right we are using something before we have established it.

This seems like something a student might do in the exam (because it is fast and it is done in the lecture/exercises) and then get points deducted for it.

Also the & operator in this solution doesn’t render correctly.

This is the justification. To be formally correct, one should add the justification explicitly at the end (a small sentence, nothing fancy).

Screenshot_2022-07-28_20-14-46
The \LaTeX version looks fine to me.

Screenshot_2022-07-28_20-15-24
The ampersands also appear in the HTML version. (Although with escape characters for \LaTeX.)

Note:
A very useful tool for \LaTeX symbols is Detexify.
The [\![ bracket is \llbracket from the stmaryrd package.
But this is not supported in (the forum subset of) MathJax. Instead you can hack it together with -0.5 spaces $[\![$.

3 Likes