簡約と変換

簡約

$\lambda$ 抽象を引数に適用した結果は、束縛変数に引数を代入して計算する。

このステップを β 簡約と呼び、$(\tLam{x}{A}{t})\;s$ の形の部分項を β 簡約基（beta-redex）と呼ぶ。第 II 部ではさらに二種類のステップを加えた。定義を展開する δ 簡約（第 7 章）と、構成子に対して再帰子を走らせる ι 簡約（図 7.1 と 9.1、および 第 8 章 の一般規則）である。各ステップは項の内部のどこで行ってもよいものとし、いずれかの種類の一回のステップを $\to$ と書く。どのステップも適用できない項は正規形にある。たとえば $\mathit{Id} = \tLam{X}{\Sort{0}}{X}$ とすると、

であり、最後の項は正規形である。内側の簡約基を先に簡約しても同じ結果に至る。

変換

定義的等価は変換（conversion）とも呼ばれ、束縛変数の名前を除いて同じ結果に計算される項どうしを同一視する。

$s \conv t$ を判定するために、カーネルは両方の項を正規化し、結果を $\alphaeq$ で比較する。この手続きは二つの事実に依拠している。

• 簡約は合流的であり、簡約の順序が違っても、異なる正規形に至ることはない。したがって $s \conv t$ が成り立つのは、$s$ と $t$ の正規形が α 同値であるとき、かつそのときに限り、巧妙なステップ列を探し回る必要はない。
• 型の付くすべての項は正規形を持つので、正規化は停止する。これは本書の体系で成り立つが、深い定理である（強正規化、第 14 章）[Barendregt 1992]。

実用的なカーネルは簡約ステップ数にも上限を設け、バグがあっても無限ループに陥らないようにする。本書の実装は 20,000 ステップで停止し、「reduction fuel exhausted」というエラーを出す。

データとしての計算規則

図 7.1 と 9.1 では ι 規則を一本ずつ別々の等式として書いており、これを見ると、新しい帰納型ごとにカーネルに新しい簡約コードが要るように思えるが、そうではない。カーネルは ι 規則を再帰子の隣にデータとしてシグネチャに保存し、一つのコードがすべての帰納型に対してそれを適用する。

各再帰子の項目は、大前提の位置、つまりどの規則を適用するかをその構成子が決める引数の位置と、その帰納型の構成子を記録する。各構成子について、カーネルは先頭の引数のうちいくつがパラメータ（規則はこれを無視する）で、いくつがフィールド（規則はこれを引き渡す）か、そしてどのフィールドが再帰的かを知っている。本書の再帰子のうち三つについて、そのデータと、結果として得られる右辺を次に示し、$\lambda$ の型注釈は省略する。

右辺は、大前提より前の引数を取り、次に構成子のフィールドを取る。たとえば $\NatRec{u}\;M\;z\;s\;(\suc\;n)$ は二番目の規則を選び、

となり、これを β 簡約すると図 7.1 の二番目の等式の右辺になる。同様に、$\EqRecDep{u,v}$ の唯一の規則は $\EqRecDep{u,v}\;A\;a\;M\;m\;b\;(\refl{u}\;A'\;c)$ に対して発火する。構成子 $\refl{u}$ は二つのパラメータ $A'$ と $c$ を持ち、フィールドを持たないので、右辺は $A\;a\;M\;m\;b$ だけを受け取って $m$ を返す。

弱頭正規形と正規化

アルゴリズム 12.1 は、アルゴリズム 5.1 が未定義のまま残した三つの関数を定義する。$\Whnf$ と $\Normalize$ はどちらも項を背骨（spine）$h\;a_1 \cdots a_n$、つまり適用ではない頭部 $h$ に $n \ge 0$ 個の引数を適用したものとして見る（第 2 章）。どの項もこの分解をちょうど一つ持つ。

Whnf(t):
  loop:
    write t as a spine h a_1 ... a_n
    if h = λ(x : A). b and n ≥ 1:                               -- beta
        t ← (b[x ↦ a_1]) a_2 ... a_n
    else if h = c and (c : C := d) ∈ Σ:                         -- delta
        t ← d a_1 ... a_n
    else if h = c is a recursor with major position p ≤ n:      -- iota
        k b_1 ... b_j ← Whnf(a_p)
        if k is a constructor of c's inductive type with q parameters:
            t ← rhs_k a_1 ... a_{p-1} b_{q+1} ... b_j a_{p+1} ... a_n
        else return t                                           -- stuck, e.g. on a variable
    else return t

Normalize(t):
  t ← Whnf(t)
  if t = Π(x : A). B:  return Π(x : Normalize(A)). Normalize(B)
  if t = λ(x : A). b:  return λ(x : Normalize(A)). Normalize(b)
  else write t as a spine h a_1 ... a_n and return h Normalize(a_1) ... Normalize(a_n)

IsDefEq(s, t):
  return  · ; · ⊢ Normalize(s) =α Normalize(t)                  -- Figure 11.1

$\Whnf$ は項の頭部でのみ簡約し、そこに適用できる規則がなくなるまで続け、結果が弱頭正規形である。$\lambda$ や $\Pi$ の内側、行き詰まった頭部の引数の中は決して見ない。呼び出し側が型の最も外側の形だけを必要とするとき、たとえば $\Infer$ の適用の場合で $\Pi$ が欲しいときには、これで十分であり、完全な正規化より安くつく。$\Normalize$ はまず弱頭正規形を計算し、次に直下の部分項をすべて正規化する。たとえば $t = \tLam{h}{\mathit{Id}\;P}{h}$ とし、$\mathit{Id}$ を上のとおりとすると、

である。$t$ の頭部は引数のない $\lambda$ なのに対し、$\Normalize$ は注釈 $\mathit{Id}\;P$ の中まで進むからだ。同様に $\Whnf(\mathit{Id}\;(\mathit{Id}\;P \to P)) = \mathit{Id}\;P \to P$ であり、定義域はまだ正規形でないものの、すでに $\Pi$ の形が見えている。どちらも下で確認でき、頭部に適用できるステップはないのに、正規形は異なる。

$\Whnf$ の三つの場合には次の性質がある。

• ι の場合は $\Nat$、$\Eq{}$、$\mathsf{Tree}$ への言及を一切含まず、大前提の位置と構成子のデータをシグネチャから読む。これは一度書けば終わりで、以後、新しい帰納型が加えるのはデータの行であってコードではない。
• 大前提は、計算の後で初めて構成子になることがあるので、規則を参照する前に弱頭正規形にする。第 7 章の $2 + 1$ では、大前提は数字 $1 = \suc\;\zero$ で、すでに構成子であるが、$\mathit{double}\;(1 + 1)$ では大前提は $1 + 1$ であり、$\Whnf$ がまずこれを $\suc\;(1 + 0)$ にする。
• 大前提が構成子にならなければ、たとえば変数であれば、項は行き詰まり（stuck）、そのままの形にとどまる。$0 + n$ が簡約されないのはこのためである（第 9 章）。

$\mathit{double}$ を第 7 章のとおりとして、$\mathit{double}\;(1 + 1)$ に対する $\Whnf$ の動作をその場で計算した結果を示す。簡約されるのは常に頭部だけだが、大前提の簡約が内側の計算を強いる。

def add : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) m (fun (k : Nat) => fun (r : Nat) => Nat.succ r) n
def double : Nat -> Nat := fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) Nat.zero (fun (k : Nat) => fun (r : Nat) => Nat.succ (Nat.succ r)) n

whnf と記されたステップが内側の計算であり、再帰子は大前提が構成子であることを要求するので、まず $1 + 1$ を頭部で簡約する。最終的な弱頭正規形には、行き詰まった内側の再帰子がまだ残っており、その下に示す正規形は、$\Normalize$ が内側へ進み続けて得るものである。

本書の $\IsDefEq$ は、実装を単純にするため両辺を完全に正規化するが、実用的なカーネルは代わりに、両辺を弱頭正規形にして頭部を比較し、必要なときだけ引数を調べる。この遅延比較なら、頭部がすでに異なる大きな項を最後まで正規化せずに済む。型の付く項に対して三つの関数がすべて停止することは、強正規化によって保証される。

コードでは

normalize_with_fuel には触れておくべき細かい点が一つある。引数の正規化が頭部に新しい簡約基を露わにすることがあるので、適用の関数部と引数を正規化した後、組み立て直した項に対してもう一度 whnf を呼ぶ。行き詰まった再帰子の適用で、大前提が自身の引数を正規化して初めて構成子になる場合、頭部をもう一度簡約しなければならない。この再検査がなければ is_def_eq はいくつかの等しさを見逃し、src/proof.rs のテスト conversion_renormalizes_exposed_redex がこれを守っている。

演習