jci 05 publish

assets/modern-light.css

@@ -47,6 +47,13 @@ body {
     padding-right: 20px;
 }
 
+.sidebar {
+   /* スクロールバーを表示 */
+    overflow-y: auto;
+    height: 100vh;
+    padding-right: 10px;
+}
+
 .content {
     order: 2;
     padding: 20px;
@@ -63,6 +70,7 @@ body {
 }
 
 
+
 .article-header {
     padding-top: 30px;
     margin: 10px;
@@ -122,8 +130,7 @@ body {
 
 .math-inline {
     display: inline-grid;
-    overflow-x: hidden;
-    ;
+    overflow: hidden !important;
 }
 
 mjx-container {
@@ -143,7 +150,9 @@ h2 {
 
 img {
     max-width: 100% !important;
-    height: auto;
+    display: block;
+    margin-left: auto;
+    margin-right: auto;
 }
 
 @media (max-width: 1200px) {
@@ -475,6 +484,8 @@ pre code {
     color: #e43e3ee0;
 }
 
+
+
 .success,
 .info,
 .warning,

posts/jci_04.md

@@ -250,32 +250,6 @@ $$
 
 (※ 仕様を読んだり示したりしたわけではなく、そう思っているだけなのでご存じの方がいたら教えてください)
 
-### 完備束
-
-:::definition
-
-**完備束 (Complete Lattice)**
-
-束 $(L, \leq)$ が任意の部分集合に対して上限と下限が存在するとき、完備束であるという。
-
-:::
-
-ここで、高さが有限な束は完備束です。証明は [平井広志, 数理情報学のための束論 Lattice Theory for Mathematical Informatics](https://www.math.nagoya-u.ac.jp/~hirai.hiroshi/papers/lattice20211108.pdf) に書いてあります。 (実はもう少し条件を緩めて、 最小元が存在する $L$ の任意の区間の鎖が有限長、までで完備束になりますがここでは省略します)
-
-
-このシリーズで出てくる束は全て有限の高さなので完備束になります。
-
-完備束であることの嬉しい性質として、不動点に関する以下の性質があります。
-
-:::definition
-クナスタ・タルスキの不動点定理 (Knaster-Tarski Fixed Point Theorem)
-
-完備束 $(L, \leq)$ と $f: L \to L$ を考える。
-
-ここで、 $f$ が単調ならば $f$ は不動点をもち、さらに不動点の集合は完備束をなす。
-:::
-
-この定理は、このあと出てくる求解アルゴリズムで活躍します、
 
 ---
 
@@ -405,14 +379,20 @@ end
 
 </div>
 
-
 ### データフロー解析の形式的定義
 
 このあと具体的なアルゴリズムに入る前に、もう少し解こうとしている問題をもう少し一般化して定式化してみます。
 
 今回解きたい問題は、以下のように定義される 「データフロー解析」 と呼ばれる抽象解釈によって解ける問題の一つとして捉えることができます。
 
 
+データフロー解析は、簡単に言えば次のような問題を解くことです。
+
+- **命令 $i$ の直前/直後の抽象状態として、最も具体的なものを求めよ。**
+
+実際に計算機上で解くために、形式的に定義してみましょう。
+
+
 :::definition
 **データフロー解析 (Data Flow Analysis)**
 
@@ -437,7 +417,6 @@ $\text{Instr}$ は
 
 このとき、データフロー解析は以下のような問題を解くことである:
 
-
 $\text{Pred}_P: \{1, 2, \cdots, n\} \to 2^{\{1, 2, \cdots, n\}}$ を
 
 $$
@@ -451,16 +430,17 @@ $$
 s_i = \prod_{j \in \text{Pred}_P(i)} ![I_j!](s_j) \quad (i = 1, 2, \cdots, n) 
 $$
 
-を満たす最大の解 $s_1, s_2, \cdots, s_n$ を求めよ。
+を満たす最大の解 $s_1, s_2, \cdots, s_n$ を求めよ
 
 :::
 
 少し補足をします。
 
 - 状態 $s \in A$ のときに 命令 $I$ を実行したときの状態は $![I!](s)$ です (記法の確認です)
 - `\bigsqcap` が MathJax で使えなかったので $\prod$ で代用しています。交わりの意味です。
-- $\text{Pred}_P(i)$ はややこしくなっていますが、要は命令 $I_i$ の直前になりうる命令のインデックスの集合になります。
 - つまり、 連立方程式の各方程式はつまるところ「ありうる直前命令からの実行結果の全ての交わり」と言うことになります。
+- $\text{Pred}_P(i)$ はややこしくなっていますが、要は命令 $I_i$ の直前になりうる命令のインデックスの集合になります。
+  - 果たしてこれは最初に書いた「命令 $i$ の直前/直後の抽象状態として、最も具体的なものを求めよ」に対応する妥当な定義でしょうか？実はとても議論の余地、というか抜けがあります。次回の記事で議論するので、一旦ここは置いておいてください。
 - 元記事や [元論文](https://www.semanticscholar.org/paper/A-Graph-Free-Approach-to-Data-Flow-Analysis-Mohnen/5ad8cb6b477793ffb5ec29dde89df6b82dbb6dba?p2df) では $L$ を その交わりと結びで定義していますが、ここでは準備に合わせて $(A, \leq)$ としています。
 - 順序関係が $A$ 上で定まっていることに注意しましょう。 (後述します)