正本：FormalLab/Foundation/UntypedLambdaCalculus.lean

第4章：非型付きラムダ計算——束縛・代入・簡約#

関数適用は、どの規則によって「計算」になるのでしょうか。また、関数本体へ引数を代入するとき、変数の意味を誤って変えないためには何が必要でしょうか。

これまで使ってきた関数抽象と適用を、今度は研究対象となる小さな言語として定義します。 Lean自身にも fun x => t と関数適用がありますが、Leanの式を使うことと、ラムダ計算の構文・規則を研究することは別です。この章ではLeanをメタ言語 （定義と証明を書く側の言語）、ラムダ計算を対象言語（定義される側の言語）として分離します。自由変数と束縛変数、捕獲を避ける代入、β簡約を順に定義し、最外の簡約を一段実行できるところまで進みます。この区別により、「Leanが実行した」と「定義した計算規則が許した」を混同しません。

名前付き構文で変数束縛を表す#

非型付きラムダ計算の項は、次の三形だけです。

変数 x
適用 t u
抽象 λ x. t

BNFに近い標準記法では、項の集合を次の文法で生成します。

t,u ::= x \mid t\,u \mid \lambda x.t.

この式は任意の文字列を項と認めるのではありません。右辺の三つの生成法を有限回使って得られる構文木だけを項とする帰納的定義です。適用は左結合、抽象の本体は右端まで延びるという規約により、 $t\,u\,v$ は $(t\,u)\,v$ 、 $\lambda x.t\,u$ は $\lambda x.(t\,u)$ と読みます。

抽象 λ x. t で、λ x は本体 t に現れる x を束縛します。その有効範囲を スコープと呼びます。たとえば λ x. x y では最初の x は束縛されていますが、 y は自由です。λ x. λ x. x の最後の x は内側の束縛子を参照します。

束縛変数の名前だけを一貫して替えても項の意味は変わりません。 λ x. x と λ y. y を同じとみなす規約が α同値（α-equivalence）で、名前を替える操作が α変換です。ただし λ x. y の自由な y を x に替えることは α変換ではありません。

名前を捨て、束縛の距離を記録する#

α同値を毎回商で扱う代わりに、ここでは de Bruijn添字を使います。変数は名前でなく、それを束縛するラムダまでの距離を自然数で記録します。0 は最も近い束縛子、 1 はその一つ外側です。

名前付き項	de Bruijn添字
$\lambda x.x$	$\lambda.0$
$\lambda x.\lambda y.x$	$\lambda.\lambda.1$
$\lambda x.\lambda y.y$	$\lambda.\lambda.0$

変換は内側から当て推量するのではなく、変数の出現位置から外へ向かって束縛子を数えます。たとえば λ x. λ y. x y の本体では、x から対応する λ x までに内側の λ y を一つ越えるので 1、y は直近の束縛子を指すので 0 です。したがって全体は λ. λ. 1 0 になります。この方法なら、λ a. λ b. a b も同じ構文へ変換されます。

これでα同値な項は文字通り同じ構文木になります。一方、添字のずれを正しく管理する責任が代入の定義へ移ります。

非型付きラムダ計算の生の項。var n の n はde Bruijn添字である。

Leankernel-checked counterpartL68–71

inductive Term where
  | var : Nat → Term
  | app : Term → Term → Term
  | lam : Term → Term

恒等関数 λ x. x。

Leankernel-checked counterpartL74–74

def identity : Term := .lam (.var 0)

第一引数を返す関数 λ x. λ y. x。

Leankernel-checked counterpartL77–77

def constant : Term := .lam (.lam (.var 1))

閉項と開項#

自由変数を一つも持たない項を閉項、持つ項を開項と呼びます。深さ depth の束縛子の内側では、depth より小さい添字だけが束縛済みです。次の判定関数は構文木を再帰的に調べます。

term が外側に depth 個の束縛子を仮定して閉じているか判定する。

Leankernel-checked counterpartL88–92

def isClosedAt (depth : Nat) : Term → Bool
  | .var index => decide (index < depth)
  | .app function argument =>
      isClosedAt depth function && isClosedAt depth argument
  | .lam body => isClosedAt (depth + 1) body

自由変数を持たないことの計算可能な判定。

Leankernel-checked counterpartL95–99

def isClosed (term : Term) : Bool := isClosedAt 0 term

example : isClosed identity = true := rfl
example : isClosed (.var 0) = false := rfl
example : isClosed constant = true := rfl

捕獲を避ける代入#

名前付き項で (λ x. t) u を簡約するとき、素朴に文字を置換すると自由変数が別のラムダに捕獲されることがあります。たとえば x を y で置き換える際、途中に λ y があれば、引数に元からあった自由な y の意味が変わります。これを 変数捕獲と呼びます。

de Bruijn表現では、束縛子の内側へ項を運ぶたび、自由変数の添字を一つ増やします。この操作を shift（持ち上げ）と呼びます。cutoff 未満の添字は内側の束縛子を指すので動かしません。

cutoff 以上の自由な添字を amount だけ持ち上げる。

Leankernel-checked counterpartL115–120

def shiftAbove (amount cutoff : Nat) : Term → Term
  | .var index =>
      if cutoff ≤ index then .var (index + amount) else .var index
  | .app function argument =>
      .app (shiftAbove amount cutoff function) (shiftAbove amount cutoff argument)
  | .lam body => .lam (shiftAbove amount (cutoff + 1) body)

項を一つの新しい束縛子の内側へ安全に運ぶ。

Leankernel-checked counterpartL123–123

def shift (term : Term) : Term := shiftAbove 1 0 term

substitute index replacement body は、body の index 番の変数を replacement で置き換え、その束縛子を一つ除きます。対象より大きい添字を一つ下げるのは、束縛子を除いた後の距離を補正するためです。ラムダの下へ入ると、対象添字と置換項をともに持ち上げます。この二つを同時に行うことが捕獲回避の核心です。

de Bruijn添字による、変数捕獲を避ける代入。

Leankernel-checked counterpartL133–141

def substitute (index : Nat) (replacement : Term) : Term → Term
  | .var found =>
      if found < index then .var found
      else if found = index then replacement
      else .var (found - 1)
  | .app function argument =>
      .app (substitute index replacement function)
        (substitute index replacement argument)
  | .lam body => .lam (substitute (index + 1) (shift replacement) body)

次の式で置換項 .var 0 は自由変数です。ラムダの内側へ入った後も .var 1 のままなので、内側の束縛子へ捕獲されません。誤った素朴な代入なら .lam (.var 0) になってしまいます。

Leankernel-checked counterpartL148–149

example :
    substitute 0 (.var 0) (.lam (.var 1)) = .lam (.var 1) := rfl

この例を一段ずつ追います。置換対象 0 を求めてラムダの下へ入ると、外側から見た対象は 1 になります。同時に、自由な置換項 .var 0 は shift によって .var 1 になります。本体で見つかった .var 1 をこの持ち上げ済みの項に替えるため、結果は .lam (.var 1) です。結果の変数は依然として自由であり、ラムダに捕獲されていません。

三つの添字分岐にもそれぞれ理由があります。

found < index：より内側の束縛子を指すので変更しない。
found = index：探していた変数なので置換項へ替える。
index < found：消える束縛子より外側を指すので距離を一つ縮める。

この不変条件を理解せずコードだけ暗記すると、ラムダの下での持ち上げや添字の減算が恣意的に見えてしまいます。

β簡約：適用を代入へ変える#

β簡約（beta-reduction）の中心規則は

(\lambda x.t)\,u\longrightarrow_\beta t[x:=u]

です。左辺のように直ちに簡約できる部分項を 簡約可能式（redex; reducible expressionの略）、右辺をその contractum と呼びます。次の関数は項全体の最外部がβ-redexである場合だけ一段縮約します。どのredexを先に選ぶかという評価戦略は、規則そのものとは別問題なので、ここでは内部を探索しません。

最外部のβ-redexだけを一段縮約する。

Leankernel-checked counterpartL183–190

def contractHead? : Term → Option Term
  | .app (.lam body) argument => some (substitute 0 argument body)
  | _ => none

example : contractHead? (.app identity constant) = some constant := rfl
example :
    contractHead? (.app constant identity) = some (.lam identity) := rfl
example : contractHead? identity = none := rfl

二つ目の例は、名前付きなら (λ x. λ y. x) (λ z. z) です。最外β-redexを縮約すると、外側の x が恒等関数で置き換わり、結果は λ y. (λ z. z) になります。 de Bruijn表現では some (.lam identity) がその構文です。contractHead? はこの一段だけを実装し、引数やラムダ本体の内側にあるredexは探しません。したがってこれは完全な評価器でも、正規形判定器でもありません。

一段簡約関係は探索関数より多くの選択を残す#

β縮約と構文の各位置での縮約を閉じた、一段簡約関係です。

Leankernel-checked counterpartL203–211

inductive Step : Term → Term → Prop where
  | beta (body argument : Term) :
      Step (.app (.lam body) argument) (substitute 0 argument body)
  | appFunction {function function' argument : Term} :
      Step function function' → Step (.app function argument) (.app function' argument)
  | appArgument {function argument argument' : Term} :
      Step argument argument' → Step (.app function argument) (.app function argument')
  | lamBody {body body' : Term} :
      Step body body' → Step (.lam body) (.lam body')

contractHead? が成功したとき、その結果は一段簡約関係でも到達できます。

Leankernel-checked counterpartL214–226

theorem contractHead?_sound {term reduct : Term}
    (contracted : contractHead? term = some reduct) : Step term reduct := by
  cases term with
  | var index => simp [contractHead?] at contracted
  | lam body => simp [contractHead?] at contracted
  | app function argument =>
      cases function with
      | var index => simp [contractHead?] at contracted
      | app left right => simp [contractHead?] at contracted
      | lam body =>
          simp [contractHead?] at contracted
          subst reduct
          exact .beta body argument

Step は項の任意の位置にあるredexを一つ選べる関係なので、同じ項から異なる二項へ進めることがあります。これに対して contractHead? は最外部だけを調べ、成功時の出力を一つに決める関数です。上の定理は関数の出力が関係の許す一歩であることを述べますが、逆は成り立ちません。ラムダ本体や引数だけが縮約できる場合、 Step は進めても contractHead? は none を返します。

標準的な両立閉包は、β規則に次の三規則を加えたものです。

\frac{t\to_\beta t'}{t\,u\to_\beta t'\,u} \qquad \frac{u\to_\beta u'}{t\,u\to_\beta t\,u'} \qquad \frac{t\to_\beta t'}{\lambda x.t\to_\beta\lambda x.t'}.

これらは「どこでも一段進めてよい」ことを定めます。正規順序や値呼びのような評価戦略は、この複数の候補から一つを選ぶ追加規則です。

法則、戦略、正規形を区別する#

β-redexを含まない項を β正規形と呼びます。正規順序と適用順序、名前呼びと値呼びは、どのredexをいつ縮約するかを決める戦略です。同じβ規則を使っても、停止性や途中経過は戦略で変わります。非型付きラムダ計算には停止しない閉項があります。典型例 (λ x. x x) (λ x. x x) は一段後に自分自身へ戻ります。

η規則 λ x. f x →η f（x が f に自由出現しない場合）は、関数を適用結果だけで観察する外延的な見方を表します。β規則が関数適用の計算を述べるのに対し、η規則は関数について何を同じとみなすかを強めます。両者を一語の「簡約」で混同しません。

Leanのデータとして対象言語を扱う#

.lam body はLean自身のラムダ抽象ではなく、対象言語の抽象を表す Term の構成子です。同様に shiftAbove と substitute はLeanのelaboratorやkernelによる代入ではなく、本章で明示的に定義した構文変換です。Leanはこれらの関数が全ての Term について定義され、例の等式が成り立つことを検査しますが、どの表現法を採用するかは対象言語のモデル化の選択です。

この構文モデルが表すもの#

この Term は型を持たない対象言語の構文です。Leanのkernelが受理する項でも、Leanの内部構文そのものでもありません。また、de Bruijn添字はラムダ計算の本質ではなく、 α同値と捕獲回避を機械的に扱う一つの表現法です。「単純型付きラムダ計算」では同じ生の項に単純型の 型判断を与え、どの項を受理するかを規則として定めます。

要点#

ラムダ計算の構文は変数・適用・抽象の三形からなる。
束縛は変数の意味を決め、α同値は束縛変数名の偶然を捨てる。
de Bruijn添字は名前を距離へ替える代わりに、代入時の添字管理を要求する。
β簡約は規則、Step はその両立閉包、評価戦略は候補の選択、正規形は候補がない状態である。
対象言語の項をLeanの帰納型として表すことで、構文操作そのものを定義・検査できる。

研究史と文献案内#

Churchは1932–1933年の論理体系で、関数抽象と変換規則を用いました。1936年には、ラムダ定義可能性を計算可能性の定式化へ用いました [CHU32, CHU33, CHU36]。現在「非型付きラムダ計算」と呼ぶ体系は、後世に整理された構文・変換の核です。de Bruijn添字は1972年、束縛変数名を使わない機械処理の記法として提案されました [DB72]。原論文の体系と本章で定義したLean上のモデルを同一視しません。

構文・代入・簡約を標準的な推論規則で学ぶには [TAPL02] を参照してください。proof theoryと正規化には [GLT89]、判断と動的意味論の関係には [PFPL16] が対応します。

問題#

名前付き項とde Bruijn添字を往復する#

λ x. λ y. x y と λ a. λ b. a b をde Bruijn添字へ翻訳し、両者が同じ構文になることを確かめてください。各添字から指される束縛子へ線を引き、束縛子が一つ増えるごとに同じ変数の番号がどう変化するかを説明します。

次に、単なるα変換、束縛を無視した不正な文字列置換、捕獲回避代入の三例を作ります。各例で自由変数集合を代入の前後に計算し、何が保存されなければならないかを判定基準にしてください。

シフトと代入の不変条件を一段ずつ追う#

substitute 0 (.var 2) (.lam (.app (.var 1) (.var 0))) を再帰呼出しごとに展開し、現在の深さ、置換対象の添字、 shiftAbove の cutoff、得られる部分項を表に記録してください。cutoff 未満の添字が現在の束縛子に属するため動かしてはならず、 cutoff 以上だけが自由変数または外側の束縛を指すことを、具体的な項の線図で示します。

対照として、このシフトを省略した素朴な代入を一つ書き、自由だった添字が新しいラムダに捕獲される最小の反例を作ってください。

簡約規則から評価器の探索方針を分離する#

β規則、一段簡約関係、評価戦略、β正規形をそれぞれ定義し、一つの項が複数のredexを持つ例で差を示してください。直下の関数位置、その後に引数位置を一段だけ探索する簡約関数を実装し、探索順を逆にした版と結果を比較します。

[DB72] の冒頭で無名記法が解決しようとする問題を確認し、原論文の記法と本章の Term、shiftAbove、substitute の対応を説明します。最後に、この Term がLean内に定義した対象言語のデータであり、Lean自身の項と同一ではない理由を説明してください。 Leanが関数 contractHead? を評価することと、Step がラムダ項について表す一段簡約とを、それぞれの入力・出力を挙げて比較します。