compiler-construction - プログラム解析とモノトーン関数

Question

プログラム分析を実行するときの単調関数の目的を誰か説明してもらえますか?

今ハンキンの「プログラム解析の原理」を読んでいるのですが、その目的がよくわかりません。

定義上、単調関数とは、集合 S のすべての要素 x と y について、x <= y => f(x) <= f(y) の場合、任意の関数です。

Answer 1

Knaster -Tarski 不動点定理は次のように述べています。

L を完全な格子とし、f : L → L を順序保存関数とします。このとき、L における f の不動点の集合も完全な格子です。

L 内の f の不動点の集合は完全な格子であるため、L 内に f の最小不動点が存在します。さらに、無数の他の不動点が存在する可能性があります。

プログラム解析で不動点が重要なのはなぜですか? ラティス L が抽象的なプログラム状態上にある場合、ループのセマンティクスの固定点 f は、帰納的不変量を論理的に表すか、またはセットで、特定のプログラム位置でのプログラム状態のセットを表し、そこからプログラムを実行するその状態セット内の状態から開始して同じ場所に戻るプログラム位置は、その状態セット内の状態を生成します。これらの状態セット (または帰納的不変条件) は、抽象的な解釈が見つけようとするものです。

抽象的な解釈の直感的な説明については、Cousot, P. and Cousot, R.: Static Determination of Dynamic Properties of Programsという論文を強くお勧めします。ISOP 1976。「有名な」Cousot と Cousot '77論文よりも前のものですが、高度な数学にはあまり詳しくありません。