トゥエルフは、 カーネギーメロン大学のフランク・フェニングとカーステン・シュールマンによって開発された論理フレームワークLFの実装です。[ 1 ]論理プログラミングとプログラミング言語理論の形式化に使用されます
はじめに
最も単純な意味では、12進プログラム（「シグネチャ」と呼ばれる）は、型ファミリー（リレーション）の宣言と、それらの型ファミリーに含まれる定数の集合です。例えば、以下は自然数の標準的な定義であり、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_succ2 番目の引数が他の数値の後続数である場合の の場合を定義します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)
12 個の特徴は型の再構築であり、暗黙的なパラメータをサポートしているため、実際には、通常、上記の (など) を明示的に記述する必要はありません{M:nat}。
これらの単純な例では、LF の高階機能や定理検証機能は示されていません。Twelf ディストリビューションに含まれる例については、Twelf ディストリビューションを参照してください。
用途
論理プログラミング
Twelfシグネチャは検索手続きを介して実行できます。そのコアは高階で依存型であるためPrologよりも洗練されていますが、純粋演算子に制限されています。Prologの実装によく見られるカットやその他の論理外演算子（ I/Oを実行するための演算子など）はないため、実用的な論理プログラミングアプリケーションには適さない可能性があります。Prologのカットルールの一部の用途は、特定の演算子が決定論的な型族に属することを宣言することで得られ、再計算を回避できます。また、λPrologと同様に、Twelfはホーン節を遺伝的ハロップ式に一般化します。これにより、論理的に十分な根拠のある操作概念である新規名生成と節データベースのスコープ付き拡張が可能になります
数学の形式化
12進法は現在、主に数学、特にプログラミング言語のメタ理論を形式化するシステムとして使用されています。そのため、 RocqやIsabelle、HOL、HOL Lightと密接に関連しています。しかし、これらのシステムとは異なり、12進法の証明は通常、手作業で開発されます。それにもかかわらず、12進法が得意とする問題領域においては、12進法の証明は、自動化された汎用システムよりも短く、開発が容易な場合が多いです
Twelf に組み込まれた束縛と置換の概念は、束縛と置換を利用するプログラミング言語やロジックのエンコードを容易にします。これらの言語やロジックの多くは、束縛と置換を利用しており、多くの場合、高階抽象構文(HOAS) を通じて直接エンコードできます。この場合、メタ言語のバインダーはオブジェクトレベルのバインダーを表します。そのため、型保存置換やアルファ変換といった標準的な定理が「無償」で提供されます。
Twelfは、様々な論理やプログラミング言語の形式化に利用されてきました（サンプルは配布物に含まれています）。大規模なプロジェクトとしては、Standard MLの安全性証明[ 2 ]、CMUの基礎的な型付きアセンブリ言語システム[ 3 ] 、プリンストンの基礎的な証明付きコードシステムなどがあります。
実装
TwelfはStandard MLで記述されており、LinuxとWindows用のバイナリが利用可能です。2006年現在、主にカーネギーメロン大学で活発に開発されています
参照
参考文献
- ^ Pfenning, Frank; Carsten Schürmann (1999年7月).システムの説明: Twelf - 演繹システムのためのメタ論理的枠組み(PDF) . 第16回国際自動演繹会議 (CADE-16) の議事録. 2019年5月8日閲覧
- ^ Lee, Daniel; Karl Crary; Robert Harper (2007年1月). Towards a Mechanized Metatheory of Standard ML (PDF) . Proceedings of the Symposium on the Principles of Programming Languages 2007. Nice , France . 2007年2月8日閲覧.
- ^ Crary, Karl (2003).基礎的な型付きアセンブリ言語に向けて(PDF) . 2003年プログラミング言語の原理に関するシンポジウム議事録. 2007年2月8日閲覧.
外部リンク
- 公式サイト、Wiki
