計算可能な関数のロジック

計算可能関数の論理（LCF）は、1970年代初頭にスタンフォード大学とエジンバラ大学のロビン・ミルナーと共同研究者によって開発された対話型の自動定理証明器であり、以前にダナ・スコットによって提案された計算可能関数の論理の理論的基礎に基づいています。LCF システムの作業では、汎用プログラミング言語MLが導入され、ユーザーが定理証明戦術を記述できるようになり、代数データ型、パラメトリック多態性、抽象データ型、例外がサポートされました。

システム内の定理は、特別な「定理」抽象データ型の用語です。ML の抽象データ型の一般的なメカニズムにより、定理は、定理抽象型の操作によって指定された推論規則のみを使用して導出されます。ユーザーは、定理を計算するために任意の複雑な ML プログラムを作成できます。定理の有効性は、そのようなプログラムの複雑さに依存せず、抽象データ型の実装の健全性と ML コンパイラの正確さによって決まります。

LCF アプローチは、明示的な証明証明書を生成するシステムと同様の信頼性を提供しますが、証明オブジェクトをメモリに格納する必要はありません。Theorem データ型は、システムの実行時の構成に応じて、証明オブジェクトをオプションで格納するように簡単に実装できるため、基本的な証明生成アプローチを一般化します。定理の開発に汎用プログラミング言語を使用するという設計上の決定は、記述されたプログラムの複雑さに応じて、同じ言語を使用して段階的な証明、決定手順、または定理証明器を記述できることを意味します。

基礎となるMLコンパイラの実装は、信頼できるコンピューティングベースに追加されます。CakeML ^[1]の作業により、正式に検証されたMLコンパイラが生まれ、これらの懸念の一部が軽減されました。

定理証明は、その正しさが広範囲に分析されている決定手順と定理証明アルゴリズムから恩恵を受けることが多い。LCFアプローチでこれらの手順を実装する簡単な方法は、結果を直接計算するのではなく、システムの公理、補題、推論規則から常に結果を導き出す手順を必要とする。より効率的な可能性のあるアプローチは、式を操作する関数が常に正しい結果を返すことを証明するためにリフレクションを使用することである。^[2]

その後の実装には Cambridge LCF があります。その後のシステムでは、ロジックを簡略化して部分関数ではなく全体関数を使用するようになり、HOL、HOL Light、さまざまなロジックをサポートするIsabelle 証明支援システムが生まれました。2019 年現在、Isabelle 証明支援システムには LCF ロジックの実装である Isabelle/LCF がまだ含まれています。