proofglyph

Proofglyph の証明検査

Proofglyph の .pg ファイルでは、型と証明項を最小限の記号列で記述します。検査器はその記号列を読み込み、各証明項が指定された型を持つかを検証します。検査の体系は、LF（Logical Framework）の型理論である λΠ 計算（依存型付きラムダ計算）に基づいています。

LF は、多様な論理の構文・推論規則・証明を依存型付きラムダ計算上で統一的に表現・検証するためのメタ言語です。Robert Harper、Furio Honsell、Gordon Plotkin が論文 A Framework for Defining Logics（1987 / 1993）において提案しました。

自然演繹やシーケント計算、集合論など、論理体系ごとに記号や推論規則は異なります。LF では、これらを「シグネチャ」と呼ばれる定数宣言の列として定義します。検査器はその宣言をもとに、関数の引数・戻り値の型、変数のスコープ、型の同値性を判定します。

例えば高水準言語 Hieratic では、命題の型 Prop と、命題からその証明の型への写像 Prf（カインド Prop -> Type）を次のように宣言します。命題 P は型 Prop を持ち、その証明は型 Prf P を持つ項として表現されます。このコードをコンパイルして Proofglyph 形式で検査します。

axiom Prop : Type;
axiom Prf : Prop -> Type;
axiom P : Prop;
theorem identity (p : Prf P) : Prf P := p;

このコードをコンパイルすると、次の .pg が生成されます。

*:
#0*>:
#0:
#1#2@#1#2@>#1#2@$0\!

上記の Proofglyph コードにおいて、#0 は Prop、#1 は Prf、#2 は P を指します。演算子 : で前提（公理）を登録し、最後の ! で identity の型と証明項を検査して登録します。

定理 identity は「P の証明を受け取ってそのまま返す関数」です。引数として P の証明を必要とするため、これは P を無条件に証明したのではなく、含意 P → P に相当する仮定付きの証明です。自然演繹における仮定の導入と解消が、ラムダ計算における関数の引数受け取りとラムダ抽象に対応しています。

Prf P は、命題 P の値に依存する型（依存型 / 型族）です。forall (P : Prop), Prf P -> Prf P は、任意の命題 P とその証明を受け取り、同じ命題の証明を返す関数の型を表します。Hieratic では forall 構文を用いて、引数の値に依存する関数型（依存積型 / Π型）を記述します。

対象論理の全称量化子を All : (U -> Prop) -> Prop と宣言すると、「すべての x について F x」という命題は All (fun (x : U) => F x) と表現できます。このように、対象論理の変数束縛を LF のラムダ束縛で表現する手法を HOAS（Higher-Order Abstract Syntax） と呼びます。Proofglyph の内部表現では de Bruijn インデックス を採用し、変数名の違い（α 同値性）の吸収や変数捕獲を防ぐ代入を安全かつ決定論的に行います。

型検査器の役割は、宣言された前提のもとで証明項が指定された型を持つかを機械的に確かめることです。前提（公理系）自体の無矛盾性や、記述した規則が意図した対象論理を正確に捉えているかは、型検査器の保証範囲外です。LF の元論文では、対象論理の構文・演繹木と LF の正準項の 1 対 1 対応が「適合性（Adequacy）」として証明されています。

Proofglyph のカーネルは、Π型、λ項、関数適用、ソート（Type / Kind）、変数、不透明な定数のみを扱う最小構成です。型の同値判定には β 簡約のみを用います。論理の推論規則や公理はすべて前提として宣言し、証明項は明示的に記述します（自動証明探索、タクティクス、暗黙引数などの機能はありません）。

言語仕様

Hieratic（.ht）は変数名や定数名を用いて人間が読み書きしやすい形式で記述する高水準言語であり、Proofglyph（.pg）は型と証明項を最小限の記号列で記述するスタック指向の中間言語です。Hieratic で記述されたコードは Proofglyph へとコンパイルされ、カーネルによって型検査されます。Proofglyph を直接入力して検査することも可能です。

*:
*:
#0#1>:
#0#1>#0#2$0@\!

axiom A : Type;
def id (x : A) : A := x;

def id : A -> A := fun (x : A) => x;

import "commons/logic/propositional.ht";

実行できる証明例（Hieratic）

以下の各例は単独で実行可能です。「エディタで試す」をクリックすると、エディタの内容が該当コードに置き換わり、コンパイルと型検査が実行されます。

axiom A : Type;
def id (x : A) : A := x;
theorem keep (x y : A) : A := x;

axiom A : Type;
axiom B : Type;
axiom C : Type;
theorem compose (ab : A -> B) (bc : B -> C)
  (x : A) : C := bc (ab x);

axiom A : Type;
axiom B : A -> Type;
theorem dependent_id (x : A) (y : B x) : B x := y;

axiom Prop : Type;
axiom Prf : Prop -> Type;
axiom Imp : Prop -> Prop -> Prop;
axiom imp_i (P Q : Prop) :
  (Prf P -> Prf Q) -> Prf (Imp P Q);
axiom imp_e (P Q : Prop) :
  Prf (Imp P Q) -> Prf P -> Prf Q;
theorem self_imp (P : Prop) : Prf (Imp P P) :=
  imp_i P P (fun (p : Prf P) => p);
theorem apply_self (P : Prop) (p : Prf P) : Prf P :=
  imp_e P P (self_imp P) p;

axiom A : Type;
axiom B : A -> Type;
axiom a : A;
axiom b : B a;
theorem beta : (fun (x : A) => B x) a := b;

収録されている数学の証明

エディタ上部の「証明例」ドロップダウンから、命題論理、等式の性質、自然数（ペアノ公理）、整除性、二項定理、素数の無限性、$\sqrt{2}$ の無理性、フェルマーの小定理、ラッセルのパラドックス（普遍集合の非存在）などを選択できます。依存する前提宣言を含めて展開され、選択した主要定理が検査結果の先頭に表示されます。

証明項の書き方ガイド

基本型、型族、公理、推論規則はすべて axiom として宣言します。これらはシグネチャ上の前提となります。導出したい結論を証明する際は theorem（または def）を用います。結論そのものを axiom で宣言してしまうと、証明ではなく単なる仮定になってしまう点に注意してください。

axiom A : Type;
axiom B : Type;

型 A -> B -> A の項を構成するには、x : A と y : B を引数として受け取り、型 A の項を返す関数を記述します。関数本体として x を返せば、この型を満たす証明項となります。

theorem first (x : A) (y : B) : A := x;
// 同じ宣言を引数の省略形なしで書くと：
// theorem first : A -> B -> A :=
//   fun (x : A) (y : B) => x;

項 f : A -> B が存在する場合、x : A に対する関数適用 f x によって型 B の項が得られます。依存型理論に基づく規則では、命題や対象に関する引数も明示的に渡す必要があります。たとえば「例」タブの imp_e P P (self_imp P) p では、対象となる 2 つの命題 P, P、含意の証明 self_imp P、そして前提の証明 p を順番に渡しています。

Hieratic を編集した後は「コンパイルして検査」を押してください。検査に成功した宣言は、以降の証明から名前で参照できるようになります。複雑な証明は補題ごとに theorem として分割し、依存順（トポロジカル順）に並べます。エディタの入力を変更すると前回の検査結果はクリアされるため、編集完了後に再度検査を実行してください。

エラーの読み方と対処法

定義（def）を使用する際の注意

def id (x : A) : A := x; を登録しても、定数は不透明（opaque）として扱われるため、id a は a へと定義的に簡約されません。型レベルの計算で β 簡約を利用したい場合は、定数呼び出しではなくインラインのラムダ式を直接記述します。式の変形や等価性の移送には、定義の展開ではなく等式に関する証明項（置換規則など）を使用します。