Merge branch 'main' of https://github.com/abap34/abap34.com

public/posts/jci_04.html

@@ -1116,7 +1116,7 @@ <h4 id="1065">1. <span class="math-inline"> \( \text{Instr} \) </span></h4><br>
 &x := 1, \\
 &x := 1 + y, \\
 &\text{goto 1}, \\
-&\text{if } x < 10 \text{ goto inst}, \\
+&\text{if } x < 10 \text{ goto 2}, \\
 &\vdots \\
 \}
 \end{align*}
@@ -1141,33 +1141,40 @@ <h4 id="1075">2. <span class="math-inline"> \( A, \leq \) </span></h4><br>次は
     "title":"3. <span class="math-inline"> \( ![.!] \) </span>"
 });
 </script>
-<h4 id="1169">3. <span class="math-inline"> \( ![.!] \) </span></h4><br>構文は 3種類に分かれているわけですが、それぞれについて考えればいいです。<br>[代入]<br><span class="inline-code"> <code>x := expr</code> </span> としたとき、 <span class="math-inline"> \( x \) </span> 以外の変数の状態は変わりません。<br>右辺に現れるのが全て定数( <span class="math-inline"> \( \neq \bot \) </span>) であれば <span class="inline-code"> <code>x</code> </span> も定数になりますから、  <span class="math-inline"> \( s' = ![x := \text{expr}!](s) \) </span> は次のようになります。<br><div class="math-block"> \[ 
+<h4 id="1169">3. <span class="math-inline"> \( ![.!] \) </span></h4><br>構文は 3種類に分かれているわけですが、それぞれについて考えればいいです。<br>[代入]<br><span class="inline-code"> <code>x := expr</code> </span> としたとき、 <span class="math-inline"> \( x \) </span> 以外の変数の状態は変わりません。<br>右辺に現れるのが全て定数( <span class="math-inline"> \( \neq \bot \) </span>) であれば <span class="inline-code"> <code>x</code> </span> も定数になりますから、  <span class="math-inline"> \( s' = ![\text{var} := \text{expr}!](s) \) </span> は次のようになります。<br><br><div class="math-block"> \[ 
+
+a = 
+\begin{cases}
+\text{expr} & \text{右辺がすべて定数かつその結果が expr の値} \\
+\bot & \text{otherwise}
+\end{cases}
+
+ \] </div><br>として、<br><div class="math-block"> \[ 
 
 s'(x) = \begin{cases}
-\text{expr の値} & x = \text{右辺がどちらも定数} \\
-\bot & x = \bot \text{ が右辺に含まれる} \\
+\text{a} & x = \text{\text{var}} \\
 s(x) & \text{otherwise}
 \end{cases}
 
  \] </div><br><br>[goto]<br>何も変わらないです。<br><br>[条件つき goto]<br>何も変わらないです。<br><br><script>page_contents.push({
     "type":"H4",
-    "id":"1203",
+    "id":"1208",
     "title":"4. <span class="math-inline"> \( a_0 \) </span>"
 });
 </script>
-<h4 id="1203">4. <span class="math-inline"> \( a_0 \) </span></h4><br>初期状態は全ての変数が <span class="math-inline"> \( \top \) </span> です。 元記事によれば元論文が間違っているとのことです。自分が一から読んでいたら気がつけないだろうことなので、ありがたいです。。。<br><br><script>page_contents.push({
+<h4 id="1208">4. <span class="math-inline"> \( a_0 \) </span></h4><br>初期状態は全ての変数が <span class="math-inline"> \( \top \) </span> です。 元記事によれば元論文が間違っているとのことです。自分が一から読んでいたら気がつけないだろうことなので、ありがたいです。。。<br><br><script>page_contents.push({
     "type":"H2",
-    "id":"1212",
+    "id":"1217",
     "title":"まとめ ！？"
 });
 </script>
-<h2 id="1212">まとめ ！？</h2><br>こうして今回の問題設定をデータフロー解析の形式的定義に落とし込むことができました。<br><br>次回は実際にこれを解くアルゴリズムを紹介します。<br><br><script>page_contents.push({
+<h2 id="1217">まとめ ！？</h2><br>こうして今回の問題設定をデータフロー解析の形式的定義に落とし込むことができました。<br><br>次回は実際にこれを解くアルゴリズムを紹介します。<br><br><script>page_contents.push({
     "type":"H2",
-    "id":"1221",
+    "id":"1226",
     "title":"今日の一曲"
 });
 </script>
-<h2 id="1221">今日の一曲</h2><br><iframe width="560" height="315" src="https://www.youtube.com/embed/D0W44Z3D3wo?si=kvQ68VsF5tg-C5lC" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen></iframe><br><div class="footnote"><span class="footnote-def" id="label_1"><a href="#ref_1">[1]</a> 分野によって入れ替わることもあるみたいです。 <url> <a href="https://x.com/__pandaman64__/status/1321404812332654592">参考</a> </url></span></div>
+<h2 id="1226">今日の一曲</h2><br><iframe width="560" height="315" src="https://www.youtube.com/embed/D0W44Z3D3wo?si=kvQ68VsF5tg-C5lC" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen></iframe><br><div class="footnote"><span class="footnote-def" id="label_1"><a href="#ref_1">[1]</a> 分野によって入れ替わることもあるみたいです。 <url> <a href="https://x.com/__pandaman64__/status/1321404812332654592">参考</a> </url></span></div>
 
             <hr>