項の言語

5 種類の項

核となる言語は小さな依存型理論であり、その項は次の文法で生成される。

ここで $u$ は自然数、$x$ は変数名である。各形には役割がある。

• $\Sort{u}$ は宇宙（universe）、すなわち要素がそれ自体型であるような型で、数 $u$ はそのレベルである。$\Sort{0}$ は命題の宇宙である。宇宙が一つではなく階層全体になっている理由は第 13 章で説明する。
• $x$ は変数であり、その意味は現れる文脈、すなわちそれを囲む $\lambda$ か $\Pi$ の束縛子か、型付け文脈の仮定から決まる。
• $\tPi{x}{A}{B}$ は $\Pi$ 型、第 1 章の依存関数型である。$x : A$ を受け取って型 $B$ のものを返す関数の型であり、$B$ は $x$ に言及してよい。
• $\tLam{x}{A}{t}$ は $\lambda$ 抽象で、型 $A$ の引数 $x$ を受け取って $t$ を返す関数である。
• $t\;s$ は $t$ の $s$ への適用である。

この文法は型と項を区別せず、命題 $\tPi{P}{\Sort{0}}{P \to P}$ もその証明 $\tLam{P}{\Sort{0}}{\tLam{p}{P}{p}}$ も、同じ 5 つの構成子から組み立てた項である。

この二つの項を木として見ると文法が共有されていることが目に見え、どの節点も 5 つの構成子のどれかで、$\Pi$ や $\lambda$ の節点に付いた名前はそれが束縛する変数である。節点をクリックすればそれが表す部分項が見えるし、別の項を入力してもよい。

項が妥当な型であるかどうかは構文的な性質ではなく、型検査器が決める。項が型であるのは、その項自身の型が宇宙であるとき、そのときに限る（第 5 章）。

記法の約束

本書では次の文字を一貫して使う。

項を読みやすくするために、三つの略記を使う。

->。 $B$ が $x$ に言及しないとき、$\tPi{x}{A}{B}$ を $A \to B$ と書く。したがってふつうの関数型は依存関数型の特別な場合であり、含意は全称量化の特別な場合である。実装では、-> の束縛子は予約された名前 _ である。

結合性。 適用は左に、-> は右に結合する。

カリー化。 二引数の関数とは、一つ目の引数を受け取って、二つ目を待つ関数を返す関数である。たとえば $\tLam{a}{A}{\tLam{b}{B}{a}}$ は型 $A \to B \to A$ を持ち、これを $x : A$ と $y : B$ に適用することを次のように書く。

二つの結合性の約束は噛み合うように決めてあり、型 $A \to B \to C$ のカリー化された関数を $f\;a\;b$ と適用するとき、どちらの側にも括弧は要らない。

束縛とスコープ

$\tLam{x}{A}{t}$ と $\tPi{x}{A}{B}$ において、変数 $x$ は束縛されており、そのスコープは本体 $t$ または $B$ であり、注釈 $A$ はスコープの外にある。$\tLam{x}{x}{x}$ では、注釈の中の $x$ は項の外にある何かを指し、本体の $x$ は引数を指す。自分を束縛する束縛子のスコープの中にない変数の出現は自由である。たとえば $\tLam{x}{P}{f\;x\;y}$ では、変数 $P$、$f$、$y$ が自由で、$x$ が束縛されている。

束縛変数については、本書全体で重要になる事実が二つあり、どちらも第 11 章で形式化する。

1. 束縛変数の名前には意味がなく、$\tLam{x}{A}{x}$ と $\tLam{y}{A}{y}$ は同じ関数である。束縛変数の名前だけが異なる項を α 同値（alpha-equivalent）と呼び、カーネルはそれらを等しいものとして扱わなければならない。
2. 変数を項で置き換える操作は型付け規則にも計算にも必要だが、その際に自由変数をうっかり同じ名前の束縛子の下に持ち込んではならない。これを正しく行うことを捕獲回避代入（capture-avoiding substitution）と呼ぶ。

どちらの事実も述べるのは簡単だが、どちらも実際の証明検査器で本物のバグを引き起こしてきたからこそ、一章を割いている。

コードでは

同じファイルには、入れ子の Box::new 呼び出しなしで項を書けるように、小さな構成関数も用意してある。var("x")、const_term("Nat")、app(f, a)、pi("x", a, b)、lam("x", a, b)、そして pi("_", a, b) を作る arrow(a, b) である。さらに三つの補助関数が、本章の約束をそのままコードにしている。

/// f a_1 ... a_n   (left-associated application)
pub fn apps(f: Term, args: impl IntoIterator<Item = Term>) -> Term {
    args.into_iter().fold(f, app)
}

/// Pi (x_1 : A_1) ... Pi (x_k : A_k). tail   (a telescope of binders)
pub fn telescope(binders: &[(String, Term)], tail: Term) -> Term {
    binders.iter().rev().fold(tail, |body, (name, ty)| pi(name, ty.clone(), body))
}

/// Decomposes t into its spine: a head that is not an application, and its arguments.
/// f a b  becomes  (f, [a, b]);  a non-application becomes  (t, []).
pub fn spine(t: &Term) -> (Term, Vec<Term>) {
    match t {
        Term::App(f, a) => {
            let (head, mut args) = spine(f);
            args.push((**a).clone());
            (head, args)
        }
        _ => (t.clone(), vec![]),
    }
}

apps と spine は互いに逆であり、apps(h, args) が左に入れ子になった適用 $h\;a_1 \cdots a_n$ を組み立て、spine がそれを再びばらす。第 12 章の簡約エンジンは項をこの背骨（spine）の形で見るので、今のうちに慣れておいてほしい。入れ子の項 $((f\;a)\;b)\;c$ の頭部は $f$、引数は $[a, b, c]$ である。各適用の関数側をたどって下りていくと頭部に着き、途中で集めた引数を内側から外側へ読めば正しい順序になる。

本書全体で使う .leanmini スクリプトの表層構文では、同じ項を Sort 0、forall (x : A), B、A -> B、fun (x : A) => b と書き、適用は並置で表す。完全な文法は付録 Eにある。

演習

goal forall (P : Sort 0), forall (Q : Sort 0), P -> Q -> P
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (p : P) => fun (q : Q) => p
qed