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

public/posts/jci_04.html

@@ -1088,7 +1088,7 @@ <h3 id="369">抽象解釈による定数畳み込み: 問題設定</h3><br>以
     "title":"データフロー解析の形式的定義"
 });
 </script>
-<h3 id="950">データフロー解析の形式的定義</h3><br>このあと具体的なアルゴリズムに入る前に、もう少し解こうとしている問題をもう少し一般化して定式化してみます。<br>今回解きたい問題は、以下のように定義される 「データフロー解析」 と呼ばれる問題として捉えることができます。<br><br><div class="definition"><span class="strong"> <strong>データフロー解析 (Data Flow Analysis)</strong> </span><br><br>命令全体の集合を <span class="math-inline"> \( \text{Instr} \) </span> 、プログラムの状態全体の集合を <span class="math-inline"> \( A \) </span> とする。<br><span class="math-inline"> \( \text{Instr} \) </span> は <br><ul><li>代入 </li><li>goto</li><li>条件つき goto</li></ul><br>のいずれかに属する命令の集合。<br><br>ここで、以下のような四つ組 <span class="math-inline"> \( (P, L, ![.!], a_0) \) </span> を考える:<br><ul><li><span class="math-inline"> \( P = I_1, I_2, \cdots, I_n \in \text{Instr} \) </span>: プログラム (命令の有限列)</li><li><span class="math-inline"> \( L = (A, \leq) \) </span>: 有限束</li><li><span class="math-inline"> \( ![.!] \in \text{Instr} \to (A \to A) \) </span>: 各命令の作用</li><li><span class="math-inline"> \( a_0 \in A \) </span>: 初期状態</li></ul><br>このとき、データフロー解析は以下のような問題を解くことである:<br><br><span class="math-inline"> \( \text{Pred}_P: \{1, 2, \cdots, n\} \to 2^{\{1, 2, \cdots, n\}} \) </span> を<br><div class="math-block"> \[ 
+<h3 id="950">データフロー解析の形式的定義</h3><br>このあと具体的なアルゴリズムに入る前に、もう少し解こうとしている問題をもう少し一般化して定式化してみます。<br>今回解きたい問題は、以下のように定義される 「データフロー解析」 と呼ばれる問題として捉えることができます。<br><br><div class="definition"><span class="strong"> <strong>データフロー解析 (Data Flow Analysis)</strong> </span><br><br>命令全体の集合を <span class="math-inline"> \( \text{Instr} \) </span> 、プログラムの状態全体の集合を <span class="math-inline"> \( A \) </span> とする。<br><span class="math-inline"> \( \text{Instr} \) </span> は <br><ul><li>代入 </li><li>goto</li><li>条件つき goto</li></ul><br>のいずれかに属する命令の集合。<br><br>ここで、以下のような四つ組 <span class="math-inline"> \( (P, L, ![.!], a_0) \) </span> を考える:<br><ul><li><span class="math-inline"> \( P = I_1, I_2, \cdots, I_n \in \text{Instr} \) </span>: プログラム (命令の有限列)</li><li><span class="math-inline"> \( L = (A, \leq) \) </span>: 有限束</li><li><span class="math-inline"> \( ![.!] \in \text{Instr} \to (A \to A) \) </span>: 各命令の作用を表す単調関数  ※</li><li><span class="math-inline"> \( a_0 \in A \) </span>: 初期状態</li></ul><br>このとき、データフロー解析は以下のような問題を解くことである:<br><br><span class="math-inline"> \( \text{Pred}_P: \{1, 2, \cdots, n\} \to 2^{\{1, 2, \cdots, n\}} \) </span> を<br><div class="math-block"> \[ 
 
 j \in \text{Pred}_P(i) \Leftrightarrow 
 I_j \in \{ \text{goto i}, \text{条件つき goto i} \} \text{ または } j = i - 1  \ かつ\  I_i \neq \text{goto}
@@ -1097,19 +1097,19 @@ <h3 id="950">データフロー解析の形式的定義</h3><br>このあと具
 
 s_i = \prod_{j \in \text{Pred}_P(i)} ![I_j!](s_j) \quad (i = 1, 2, \cdots, n) 
 
- \] </div><br>を満たす最大の解 <span class="math-inline"> \( s_1, s_2, \cdots, s_n \) </span> を求めよ。<br></div><br>少し補足をします。<br><ul><li>状態 <span class="math-inline"> \( s \in A \) </span> のときに 命令 <span class="math-inline"> \( I \) </span> を実行したときの状態は <span class="math-inline"> \( ![I!](s) \) </span> です (記法の確認です)</li><li><span class="inline-code"> <code>\bigsqcap</code> </span> が MathJax で使えなかったので <span class="math-inline"> \( \prod \) </span> で代用しています。交わりの意味です。</li><li><span class="math-inline"> \( \text{Pred}_P(i) \) </span> はややこしくなっていますが、要は命令 <span class="math-inline"> \( I_i \) </span> の直前になりうる命令のインデックスの集合になります。</li><li>つまり、 連立方程式の各方程式はつまるところ「ありうる直前命令からの実行結果の全ての交わり」と言うことになります。</li><li>元記事や <url> <a href="https://www.semanticscholar.org/paper/A-Graph-Free-Approach-to-Data-Flow-Analysis-Mohnen/5ad8cb6b477793ffb5ec29dde89df6b82dbb6dba?p2df">元論文</a> </url> では <span class="math-inline"> \( L \) </span> を その交わりと結びで定義していますが、ここでは準備に合わせて <span class="math-inline"> \( (A, \leq) \) </span> としています。</li><li>順序関係が <span class="math-inline"> \( A \) </span> 上で定まっていることに注意しましょう。 (後述します)</li></ul><br><br><br><script>page_contents.push({
+ \] </div><br>を満たす最大の解 <span class="math-inline"> \( s_1, s_2, \cdots, s_n \) </span> を求めよ。<br></div><br>少し補足をします。<br><ul><li>状態 <span class="math-inline"> \( s \in A \) </span> のときに 命令 <span class="math-inline"> \( I \) </span> を実行したときの状態は <span class="math-inline"> \( ![I!](s) \) </span> です (記法の確認です)</li><li><span class="inline-code"> <code>\bigsqcap</code> </span> が MathJax で使えなかったので <span class="math-inline"> \( \prod \) </span> で代用しています。交わりの意味です。</li><li><span class="math-inline"> \( \text{Pred}_P(i) \) </span> はややこしくなっていますが、要は命令 <span class="math-inline"> \( I_i \) </span> の直前になりうる命令のインデックスの集合になります。</li><li>つまり、 連立方程式の各方程式はつまるところ「ありうる直前命令からの実行結果の全ての交わり」と言うことになります。</li><li>元記事や <url> <a href="https://www.semanticscholar.org/paper/A-Graph-Free-Approach-to-Data-Flow-Analysis-Mohnen/5ad8cb6b477793ffb5ec29dde89df6b82dbb6dba?p2df">元論文</a> </url> では <span class="math-inline"> \( L \) </span> を その交わりと結びで定義していますが、ここでは準備に合わせて <span class="math-inline"> \( (A, \leq) \) </span> としています。</li><li>順序関係が <span class="math-inline"> \( A \) </span> 上で定まっていることに注意しましょう。 (後述します)</li></ul><br>※ 元論文には "monotone semantic functional" と書いてあるんですが、 <span class="math-inline"> \( \text{Instr} \) </span> には順序が定まっていないように見えるので、少し謎です。意味がわかる方がいれば教えてください。<br><br><br><script>page_contents.push({
     "type":"H3",
-    "id":"1057",
+    "id":"1061",
     "title":"定数畳み込みの形式的定義"
 });
 </script>
-<h3 id="1057">定数畳み込みの形式的定義</h3><br>実際に今回の問題をこの定義に落とし込みます。<br><br>上から行きましょう。<br><script>page_contents.push({
+<h3 id="1061">定数畳み込みの形式的定義</h3><br>実際に今回の問題をこの定義に落とし込みます。<br><br>上から行きましょう。<br><script>page_contents.push({
     "type":"H4",
-    "id":"1065",
+    "id":"1069",
     "title":"1. <span class="math-inline"> \( \text{Instr} \) </span>"
 });
 </script>
-<h4 id="1065">1. <span class="math-inline"> \( \text{Instr} \) </span></h4><br>ちゃんと定義したければ BNF とかを書けばいいと思いますがいったんふわっと書くと<br><div class="math-block"> \[ 
+<h4 id="1069">1. <span class="math-inline"> \( \text{Instr} \) </span></h4><br>ちゃんと定義したければ BNF とかを書けばいいと思いますがいったんふわっと書くと<br><div class="math-block"> \[ 
 
 \begin{align*}
 \text{Instr} =\  &\{ \\
@@ -1123,25 +1123,25 @@ <h4 id="1065">1. <span class="math-inline"> \( \text{Instr} \) </span></h4><br>
 
  \] </div><br>みたいな集合です。全ての要素はそれぞれ 代入, goto, 条件つき goto のどれかただ一つに属することに注意してください。<br><script>page_contents.push({
     "type":"H4",
-    "id":"1075",
+    "id":"1079",
     "title":"2. <span class="math-inline"> \( A, \leq \) </span>"
 });
 </script>
-<h4 id="1075">2. <span class="math-inline"> \( A, \leq \) </span></h4><br>次はプログラムの状態 <span class="math-inline"> \( A \) </span> とその順序関係 <span class="math-inline"> \( \leq \) </span> です。<br>今回の設定では変数の状態以外に特に状態はありませんから、<br><span class="math-inline"> \( X \) </span> を変数の集合、 <span class="math-inline"> \( C \) </span> を変数の状態の集合として<br><span class="math-inline"> \( A = X \to C \) </span> とすればいいでしょう。<br><br>今さらっと <span class="math-inline"> \( C \) </span> を導入しましたが、ここが (多分自分が思うに) キモです。 これの中身をどうするかが抽象解釈の設計の本質パート (ではないかとと素人ながら) 思います.<br><br>というのもこの部分こそが調べたい性質のためにプログラムを抽象化するパートだからです。<br><br>例えば今回の場合、次のような集合と順序関係を考えることによって抽象化します。<br><br><span class="math-inline"> \( L = \{ \bot, 1, 2, 3, \cdots, \top \} \) </span> として、 <span class="math-inline"> \( \leq \) </span> を次のように定義する:<br><div class="math-block"> \[ 
+<h4 id="1079">2. <span class="math-inline"> \( A, \leq \) </span></h4><br>次はプログラムの状態 <span class="math-inline"> \( A \) </span> とその順序関係 <span class="math-inline"> \( \leq \) </span> です。<br>今回の設定では変数の状態以外に特に状態はありませんから、<br><span class="math-inline"> \( X \) </span> を変数の集合、 <span class="math-inline"> \( C \) </span> を変数の状態の集合として<br><span class="math-inline"> \( A = X \to C \) </span> とすればいいでしょう。<br><br>今さらっと <span class="math-inline"> \( C \) </span> を導入しましたが、ここが (多分自分が思うに) キモです。 これの中身をどうするかが抽象解釈の設計の本質パート (ではないかとと素人ながら) 思います.<br><br>というのもこの部分こそが調べたい性質のためにプログラムを抽象化するパートだからです。<br><br>例えば今回の場合、次のような集合と順序関係を考えることによって抽象化します。<br><br><span class="math-inline"> \( L = \{ \bot, 1, 2, 3, \cdots, \top \} \) </span> として、 <span class="math-inline"> \( L \) </span> 上の順序関係 <span class="math-inline"> \( \leq \) </span> を次のように定義します:<br><div class="math-block"> \[ 
 
-\bot \leq x \leq \top \quad (x \in \{ 1, 2, 3, \cdots \})
+l_i \leq l_j \Leftrightarrow l_i = l_j \text{ または } l_i = \bot \text{ または } l_j = \top
 
  \] </div><br>このとき <span class="math-inline"> \( (L, \leq) \) </span> は束です。 <br><br>図にすると<br><figure><img src="jci_04/image-1.png" ><figcaption>元記事より</figcaption></figure><br>みたいな感じです。<br><span class="math-inline"> \( \bot, \top \) </span> はそれぞれ次のような意味です。 <span class="footnote-ref"><sup id="ref_1"><a href="#label_1">[1]</a></sup></span><br><ul><li><span class="math-inline"> \( \bot \) </span>: 定数でない</li><li><span class="math-inline"> \( \top \) </span>: 未定義</li></ul><br><br>このような状態 <span class="math-inline"> \( C \) </span> を設定することで、実際の実行から、「定数かどうか && 定数ならその値」を考える抽象的な解釈に落とし込まれるわけです！ (たぶん)<br><br>例えば (そんなもんが役に立つのかはさておき) 単に「定数かどうか」だけ調べるのであれば <span class="math-inline"> \( C = \{ \bot, c, \top \} \) </span>  みたいな感じでいいのだと思います。<br><br>なお、注意する点として、 <span class="strong"> <strong>データフロー解析の問題設定においてはあくまでも束をなのは 各変数でなく状態 <span class="math-inline"> \( A \) </span>　と <span class="math-inline"> \( A \) </span> 上の順序です。</strong> </span><br>したがって <span class="math-inline"> \( A \) </span> 上の順序関係を考える必要があります。<br>が、そこまで大変でなく単に次のようにすればいいです。<br><div class="math-block"> \[ 
 
 a_i \leq a_j \Leftrightarrow \forall x \in X, a_i(x) \leq a_j(x)
 
  \] </div><br>これが束をなすのは論理関数のときと同じような感じでわかります！　<br><script>page_contents.push({
     "type":"H4",
-    "id":"1169",
+    "id":"1175",
     "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' = ![\text{var} := \text{expr}!](s) \) </span> は次のようになります。<br><br><div class="math-block"> \[ 
+<h4 id="1175">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}
@@ -1158,23 +1158,23 @@ <h4 id="1169">3. <span class="math-inline"> \( ![.!] \) </span></h4><br>構文
 
  \] </div><br><br>[goto]<br>何も変わらないです。<br><br>[条件つき goto]<br>何も変わらないです。<br><br><script>page_contents.push({
     "type":"H4",
-    "id":"1208",
+    "id":"1214",
     "title":"4. <span class="math-inline"> \( a_0 \) </span>"
 });
 </script>
-<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({
+<h4 id="1214">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":"1217",
+    "id":"1223",
     "title":"まとめ ！？"
 });
 </script>
-<h2 id="1217">まとめ ！？</h2><br>こうして今回の問題設定をデータフロー解析の形式的定義に落とし込むことができました。<br><br>次回は実際にこれを解くアルゴリズムを紹介します。<br><br><script>page_contents.push({
+<h2 id="1223">まとめ ！？</h2><br>こうして今回の問題設定をデータフロー解析の形式的定義に落とし込むことができました。<br><br>次回は実際にこれを解くアルゴリズムを紹介します。<br><br><script>page_contents.push({
     "type":"H2",
-    "id":"1226",
+    "id":"1232",
     "title":"今日の一曲"
 });
 </script>
-<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>
+<h2 id="1232">今日の一曲</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>