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

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

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

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

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

1. 変数 `x`
2. 適用 `t u`
3. 抽象 `λ 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` に替えることは
α変換ではありません。
-/

namespace FormalLab.Foundation.UntypedLambdaCalculus

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

α同値を毎回商で扱う代わりに、ここでは **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添字である。 -/
inductive Term where
  | var : Nat → Term
  | app : Term → Term → Term
  | lam : Term → Term

/-- 恒等関数 `λ x. x`。 -/
def identity : Term := .lam (.var 0)

/-- 第一引数を返す関数 `λ x. λ y. x`。 -/
def constant : Term := .lam (.lam (.var 1))

/-!
## 閉項と開項

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

/-- `term` が外側に `depth` 個の束縛子を仮定して閉じているか判定する。 -/
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

/-- 自由変数を持たないことの計算可能な判定。 -/
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` だけ持ち上げる。 -/
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)

/-- 項を一つの新しい束縛子の内側へ安全に運ぶ。 -/
def shift (term : Term) : Term := shiftAbove 1 0 term

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

/-- de Bruijn添字による、変数捕獲を避ける代入。 -/
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)` になってしまいます。
-/

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だけを一段縮約する。 -/
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は探しません。したがってこれは完全な評価器
でも、正規形判定器でもありません。
-/

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

/-- β縮約と構文の各位置での縮約を閉じた、一段簡約関係です。 -/
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?` が成功したとき、その結果は一段簡約関係でも到達できます。 -/
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` がラムダ項について表す一段簡約とを、それぞれの入力・出力を挙げて比較します。
-/

end FormalLab.Foundation.UntypedLambdaCalculus