十二

Twelfは、カーネギーメロン大学のFrank PfenningとCarsten Schürmannによって開発された論理フレームワークLFの実装です。^{[1]これは、}論理プログラミングとプログラミング言語理論の形式化に使用されます。

最も単純な Twelf プログラム (「シグネチャ」と呼ばれる) は、型ファミリ(関係) の宣言とそれらの型ファミリに含まれる定数の集合です。たとえば、以下は自然数の標準的な定義で、 はzゼロを表し、 はs後続演算子を表します。

nat :タイプ。  

z : nat . s : nat -> nat .  
    

ここでnatは型であり、 およびzはs定数項です。依存型付けシステムとして、型は項によってインデックス付けすることができ、より興味深い型ファミリーの定義が可能になります。次に、加算の定義を示します。

プラス: nat -> nat -> nat -> type 。        

plus_zero : { M: nat }プラスM z M 。      

plus_succ : { M: nat } { N: nat } { P: nat }プラスM ( s N ) ( s P ) <-プラスM N P 。    
                 
             

型ファミリは、となる3 つの自然数、、plusの関係として読み取られます。次に、関係を定義する定数を指定します。定数はを示します。量指定子は、 「型 のすべてについて」と読み取ることができます。 MNPM + N = Pplus_zeroM + 0 = M{M:nat}Mnat

定数 はplus_succ、2 番目の引数が他の数値の後続数である場合の の場合を定義しますN(パターン マッチングを参照)。結果は の後続数でP、 はとPの合計です。この再帰呼び出しは、 で導入されたサブゴール を介して行われます。矢印は、操作的には Prolog の として、または論理的含意 ("M + N = P の場合、M + (s N) = (s P)") として、または型理論に最も忠実に、定数の型("型 の項が与えられた場合、型 の項を返す") として理解できます。 MNplus M N P<-:-plus_succplus M N Pplus M (s N) (s P)

{M:nat}Twelf は型の再構築を特徴とし、暗黙的なパラメータをサポートしているため、実際には、通常、上記の (など) を明示的に記述する必要はありません。

これらの単純な例では、LF の高階機能や定理チェック機能は示されていません。含まれる例については、Twelf ディストリビューションを参照してください。

Twelf シグネチャは、検索手順を介して実行できます。そのコアは、高階で依存型であるためPrologよりも洗練されていますが、純粋な演算子に制限されています。Prolog 実装でよく見られるカットやその他の論理外演算子 ( I/O を実行するための演算子など) は存在しないため、実用的な論理プログラミングアプリケーションには適さない可能性があります。Prolog のカット規則の一部の用途は、特定の演算子が決定論的な型ファミリに属する​​ことを宣言することで取得でき、再計算を回避できます。また、λPrologと同様に、Twelf はHorn 節を遺伝的 Harrop 式に一般化します。これにより、論理的に十分に根拠のある操作概念である新規名生成と節データベースのスコープ拡張が可能になります。

Twelf は現在、主に数学、特にプログラミング言語のメタ理論を形式化するためのシステムとして使用されています。そのため、CoqやIsabelle / HOL / HOL Lightと密接に関連しています。ただし、これらのシステムとは異なり、Twelf の証明は通常、手作業で開発されます。それにもかかわらず、Twelf が優れている問題領域では、自動化された汎用システムよりも Twelf の証明の方が短く、開発が容易な場合が多くあります。

Twelf に組み込まれているバインディングと置換の概念により、プログラミング言語とロジックのエンコードが容易になります。これらの言語とロジックのほとんどはバインディングと置換を利用しており、多くの場合、高階抽象構文(HOAS) を通じて直接エンコードできます。この場合、メタ言語のバインダーはオブジェクト レベルのバインダーを表します。したがって、型保存置換やアルファ変換などの標準定理は「無料」で提供されます。

Twelf は、さまざまなロジックやプログラミング言語を形式化するために使用されてきました (例は配布物に含まれています)。大規模なプロジェクトには、Standard MLの安全性の証明、^[2] CMU の基礎的な型付きアセンブリ言語システム、 ^[3]プリンストンの基礎的な証明付きコードシステムなどがあります。

Twelf は Standard ML で書かれており、Linux および Windows 用のバイナリが利用可能です。2006 年現在^{[アップデート]}、主にカーネギーメロン大学で活発に開発されています。^{[更新が必要]}

• 証明補助者のリスト

• 公式サイト、Wiki