ソフトウェアエンジニアのためのLean証明の解剖

ソフトウェアエンジニアのためのLean証明の解剖 目次 はじめに 最近、計算理論の教科書から、有限オートマトンを使ってある言語の性質を証明するという問題に取り組みました。非形式的な証明は、オートマトンを構築し、それがその言語を認識することを示す単純な構成的証明です。これはプログラム検証と似ているため、証明を形式化するには何が必要かを見るのは興味深いと思いました。 形式証明を終えた後、ソフトウェアエンジニアにシステムのプロパティを形式的に証明するために何が必要かについての良い洞察を提供できると考え、それを書き出すことにしました。 この投稿を分かりやすくしようと努めました。TypeScriptやRustのようなモダンな静的型付けプログラミング言語、バイナリ算術、基本的な命題論理、帰納的証明に慣れているなら、ついていけるはずです。 背景: DFAと正規言語 DFAと正規言語に慣れている場合は、次のセクションにスキップしても構いません。 有限オートマトンは、固定されたメモリを持つ計算の理論的モデルを提供します。理論だけでなく、有限オートマトンは重要な実用的な応用もあります。例えば、有限オートマトンはパーサーや正規表現に関連しており、かつてバグがインターネットの大部分をダウンさせたこともありました。 決定性有限オートマトン (DFA) 決定性有限オートマトン (DFA) は、固定された有限の状態セットを持ち、一度に1つのシンボルを左から右へ入力として読み取る機械です。各シンボルで、決定的な遷移関数を使用して状態を更新します。最後のシンボルの後、機械は受理状態（入力が受理される）にあるか、そうでないか（入力が拒否される）のいずれかです。 -?[0-9]+ のような単純な正規表現を書いたことがあるなら、DFAを構築したことがあります。この正規表現は、12や-123のような整数リテラルに一致し、対応するDFAは次のようになります（矢印は次の状態につながるシンボルで注釈が付けられています）。 デシマル整数リテラルのDFA、デッドステートを含む このDFAには4つの状態があります。 開始: これは最初の文字を処理する前の開始位置です。開始状態は受理状態ではないため、空文字列は拒否されます。 符号: 開始状態の-文字を検出すると、符号状態に移動します。符号文字はオプション（-?）なので、開始状態から直接数字にジャンプして符号状態をスキップすることもできます。文字列の終わりにこの状態にある場合、文字列は拒否されます。 数字: 数字文字（[0-9]）を検出すると、開始状態または符号状態から数字状態に移動します。数字状態にいて再び数字文字を検出した場合、数字状態に留まります。数字状態はこのDFAの唯一の受理状態です。入力文字列を処理した後、この状態にある場合、DFAはその文字列を受理します。 デッド: 数字以外の文字（先頭にマイナス記号がない場合）を検出すると、この状態に入ります。文字列の終わりにデッド状態にある場合、DFAはその文字列を拒否します。デッド状態に入ると、そこから抜け出せなくなるため、このDFAのデッド状態はシンクです。 機械の入力シンボルのセットは、ΣΣΣのセットによって定義されます。この正規表現の例では、Σ={−,0,1,2,…,9}です。 正規言語 言語とは文字列（単語とも呼ばれる）のセットであり、DFAがその中の文字列のみを受け入れる場合、その言語は正規と呼ばれます。正規言語を認識することは、入力とともにメモリ量が増加しない計算問題のクラスです。 正規言語には有用な閉包特性があります。2つの正規言語の和集合と共通部分は正規であり、補集合と（私たちにとって重要な）逆転も正規です。 言語が正規であることを証明する標準的な方法は、DFAを構築し、それがその言語のみを受け入れることを示すことです。 集合内包表記を使用して言語AAAを記述できます。 A={ w∈Σ∗∣P(w) } Σ∗はΣのシンボルのすべての可能な連結によって作成された文字列のセットを意味し、P(w)は文字列wが言語に含まれるために満たさなければならない条件です。 この表記法を正規表現の例 -?[0-9]+ に適用してみましょう。Σ∗には、"", "123", "-111", "2-625-"などの文字列が含まれ、P(w)は「wは空ではなく、負の符号を含まない。ただし、wが2文字以上の場合、その最初の文字は負の符号である可能性がある」と定義できます。 問題 解決する問題は、Michael Sipser著『Introduction to the Theory of Computation, 3rd ed.』からのものです。 1.32 Σ3={[000],[001],[010],…,[111]}とする。 Σ3は高さ3の0と1の列のセットであり、Σ3上の文字列は3行のビットを決定します。各行を2進数として読むと、次のように定義されます。 B={ w∈Σ3∗∣P(w) } ここで、P(w)はwの最下行がwの上の2行の合計に等しいという命題です。 BBBが正規であることを示してください。（ヒント: BRB Rで作業する方が簡単です。） 問題は、通常の文字[a-z]の代わりに、3ビットの列からなる変わったアルファベットを定義しています。したがって、"apple", "banana"などの文字列で構成される言語ではなく、言語は011 001 100のような2次元ビット文字列で構成され、最初の列が最初の「文字」などとなります。 文字列が言語に含まれるかどうかを判断するルールは、文字列の最初の2行を加算し、それらが3番目の行と一致するかどうかを確認することです。 例えば、次の文字列は言語に含まれます。 011 # x行: 最初の加算数は10進数で3 001 # y行: 2番目の加算数は10進数で1 100 # z行: 合計は4であり、3 + 1に等しい しかし、次の文字列は言語に含まれません。 01 # x行: 最初の加算数は10進数で1 00 # y行: 2番目の加算数は0 11 # z行: 合計は3であり、1 + 0に等しくない このような言語は最初は奇妙に見えるかもしれませんが、認識するのは実際には簡単です。x+y=zという方程式を確認するだけで、文字列が言語に含まれるかどうかを判断できます。課題は、任意に長い文字列に対して固定されたメモリ量でこれを実行する必要があることです。 解決策 トリックは、手で数字を加算する方法を思い出すことです。最下位桁から最上位桁に向かって作業します。前の列から次の列に持ち越されるのはキャリーだけです。 しかし、DFAは左から右に読み取り、問題は最上位ビットを最初に提示します。そのため、BBBを直接認識しません。代わりに、その逆転であるBRB Rを認識するDFAを構築します。これは、BBBの文字列を逆順に書いたものであり、機械は最下位桁を最初に目にします。 BRB Rを認識するDFAを構築できれば、BRB Rが正規言語であると結論付けることができます。BRB Rの逆転がBBBであるため、正規言語の逆転の閉包特性を使用して、BBBも正規であると結論付けることができ、これで解決策が完了します。 加算算術 列ごとに算術を実行する際、加算方程式を使用して各ステップの合計ビットを計算します。 xi⊕yi⊕cin=zi ここで、xi,yiは加算ビット、ziは合計ビット、iは現在の列のインデックス、cinは前のステップからの入力キャリーです。次のステップの出力キャリー、coutは次のように計算します。 cout=(xi∧yi)∨(cin∧(xi⊕yi))