/-!
# 第2章：関数・適用・合成

前章では閉じた式を定義して計算しました。しかし数学の多くは、具体的な値一つではなく、
任意の入力から出力を作る同じ手続きを扱います。二倍、後者関数、恒等写像は、入力を与える
まで値が決まらないという点で共通しています。その共通の形が関数です。

本章では関数をグラフや対応表として仮定せず、入力を束縛するラムダ抽象、入力を渡す適用、
出力を次の入力へ渡す合成から組み立てます。型 `A → B` を読んだだけで必要な入力と得られる
出力を追跡できることが、後の論理、ラムダ計算、関手を学ぶ基礎になります。

## 入力から出力への依存を対象にする

集合論的な記法では関数を $f:A\to B$ と書き、各 $a\in A$ にただ一つの $f(a)\in B$ を
対応させます。型理論では対応のグラフを先に構成するのではなく、入力 $a:A$ から出力
$f\,a:B$ を作る項として関数を扱います。

* **作る**：`λx : A. t` は入力 `x` を束縛するラムダ抽象。
* **使う**：`f x` は関数 `f` の入力 `x` への適用。
* **つなぐ**：`f : A → B` と `g : B → C` から `g ∘ f : A → C` を作る。

ラムダ計算の関数は一引数です。`A → B → C` は右結合して `A → (B → C)` と読み、最初の
入力を与えると、次の入力を待つ関数が返ります。

## 関数型・ラムダ抽象・適用の三項を読む

関数を「入力と出力の対応表」と考えることは有限集合では便利ですが、Leanで関数を
使うための基本像としては狭すぎます。関数も一つの項であり、次の二規則で特徴づけます。

$$
\frac{\Gamma,x:A\vdash t:B}
     {\Gamma\vdash \lambda x:A.\,t:A\to B}\;{\to}\mathrm I
\qquad
\frac{\Gamma\vdash f:A\to B\qquad\Gamma\vdash a:A}
     {\Gamma\vdash f\,a:B}\;{\to}\mathrm E
$$

左は関数の**導入**、右は関数の**除去**です。導入では仮の入力に対する出力を作り、
除去では実際の入力を与えます。$(\lambda x.\,t)\,a$ は $t$ の自由な $x$ を $a$ で置き換えて
計算します。この計算を「非型付きラムダ計算」でβ簡約として対象言語の側から分析します。

$$
(\lambda x:A.\,t)\,a\;\longrightarrow_\beta\;t[x:=a].
$$

置換 $t[x:=a]$ は、$t$ に既にある束縛変数を誤って捕獲しないように行います。型付け規則は項を作れる条件、
β規則は作った項が一段でどう計算するかを述べており、役割が異なります。

## 束縛とスコープ

`fun x => body` の `x` は、新しい値を計算する命令ではなく、`body` の中だけで使える
局所名を導入します。これを**束縛**と呼び、その有効範囲がスコープです。

```text
fun x => x + 1
    └───────┘  この範囲の x は入力を指す
```

外側に同じ名前があっても、内側の束縛が優先されます。名前自体ではなく、どの束縛子を
参照するかが意味を決めます。


-/

namespace FormalLab.Foundation.Functions

/-! ## 恒等関数・定数関数・合成を定義する -/

/-- 受け取った項をそのまま返す恒等関数です。 -/
def identity {α : Type} (x : α) : α :=
  x

/-- 最初の値を保存し、次の入力を無視して返す定数関数です。 -/
def constant {α : Type} {β : Type} (x : α) : β → α :=
  fun _ => x

/-- `f` の出力を `g` の入力へ渡す関数合成です。 -/
def compose {α : Type} {β : Type} {γ : Type}
    (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)

/-- 合成を入力へ適用すると、中間結果を順に渡す計算へ戻ります。 -/
theorem compose_apply {α β γ : Type} (g : β → γ) (f : α → β) (x : α) :
    compose g f x = g (f x) :=
  rfl

/-- 三関数の合成は、各入力でどちらに括っても同じ計算になります。 -/
theorem compose_assoc_pointwise {α β γ δ : Type}
    (h : γ → δ) (g : β → γ) (f : α → β) (x : α) :
    compose h (compose g f) x = compose (compose h g) f x :=
  rfl

/-- 関数 `f` を同じ入力へ二回適用します。 -/
def applyTwice {α : Type} (f : α → α) (x : α) : α :=
  f (f x)

/-!
## 型から合成を導出する

`compose` の本体を暗記する必要はありません。求める型を一段ずつ使えば復元できます。

1. 結果は `α → γ` なので、まず `fun x => ...` として `x : α` を仮定する。
2. `f : α → β` へ `x` を渡すと `f x : β` を得る。
3. `g : β → γ` へそれを渡すと `g (f x) : γ` を得る。
4. 仮定した `x` を閉じれば `fun x => g (f x) : α → γ` になる。

型は完成品を検査するだけでなく、次に何を作るべきかを案内しています。

## 複数引数は一引数関数の反復である

`constant x` は値ではなく、次の入力を待つ関数です。関数を一引数へ適用した結果が再び
関数になるため、複数引数のように使えます。この表現を**カリー化**（currying）、一部の
引数だけを与えることを**部分適用**と呼びます。
-/

/-- 二つの自然数を受け取る関数。型は `Nat → (Nat → Nat)` と読む。 -/
def add : Nat → Nat → Nat :=
  fun left => fun right => left + right

/-- `add` の第一引数だけを与えて得た、一引数関数。 -/
def addThree : Nat → Nat :=
  add 3

#check add
#check add 3
#eval addThree 4

/-!
波括弧の `{α : Type}` は**暗黙引数**です。`identity 3` ではLeanが `3 : Nat` から
`α := Nat` を推論します。`@identity` と書くと暗黙引数も明示された型を観察できます。

暗黙引数は存在しない引数ではありません。通常はelaboratorが文脈から補う引数です。
推論できないときは明示する必要があり、`@` は全引数を観察・指定するために省略を解除します。
-/

#check @identity
#check compose
#eval applyTwice (fun n : Nat => n + 1) 3

/-!
## 結合の向きを読む

矢印は右結合し、適用は左結合します。

$$
\alpha\to\beta\to\gamma=\alpha\to(\beta\to\gamma),
\qquad f\,x\,y=(f\,x)\,y.
$$

この二規約が組み合わさるため、`f : α → β → γ` と `x : α` から `f x : β → γ`、さらに
`y : β` から `f x y : γ` と機械的に追えます。括弧を推測で補わず、型から復元します。

## 関数の記法が隠しているもの

この章では `Type` に属する型だけを使います。異なる宇宙階層をまたいで同じ定義を
再利用する**宇宙多相**は「宇宙階層と宇宙多相」で一般化します。合成の結合則のような関数同士の
等しさには、関数外延性が必要です。この原理は「等式、代入、外延性、一意存在」で導入します。

関数の本体が同じ計算をすることと、関数項が定義的に同じことも区別が必要です。
点ごとに同じ出力を返す二関数を等しいとする関数外延性は、単なる評価規則ではありません。

`compose_assoc_pointwise` は、任意の入力 $x$ で二つの合成結果が等しいことを `rfl` で検査します。これを
関数そのものの等式へ引き上げるには関数外延性が要ります。計算規則だけで証明できた点ごとの等式と、外延性原理を
使う関数等式を分けることで、後の圏論で必要な合成則の証明責任が見えます。

## 要点

関数型は入力型と出力型を指定し、ラムダ抽象が関数を作り、適用が関数を使います。β規則は適用された
ラムダ抽象を捕獲回避置換へ簡約します。
多引数関数は一引数関数の反復で、合成は中間型を一致させて導出できます。暗黙引数は
elaboratorが補う実在の引数です。

## 研究史と文献案内

関数概念はラムダ計算以前から解析学・集合論で発展し、19世紀には関数とその解析的表示を
区別する方向へ一般化されました。Churchの1940年の単純型理論 [CHU40] は型付きラムダ抽象を
論理体系へ組み込みます。現代の型付き関数の構文論は [TAPL02]、判断中心の提示は [PFPL16]、
proof theoryとの関係は [GLT89] を参照してください。

## 問題

### 合成の向きを型だけから復元する

`f : A → B` と `g : B → C` だけを与え、`compose g f` の本体を見ずにラムダ項を導いてください。
始域、中間型、終域を図に書き、入力 `x : A` がどの順で移るかを各適用の型判断とともに示します。
次に `compose f g` を同じ方法で診断し、どの二型が一致すれば例外的に型検査できるかも述べます。

数学的記法 `A \xrightarrow{f} B \xrightarrow{g} C`、ラムダ式 `λx. g (f x)`、Leanの `compose g f` を三行に並べ、各部分の対応を示してください。
解答は記法の暗記ではなく、中間型 `B` が合成の順序を一意に強制することを説明できれば完了です。

### カリー化と部分適用を実装と判断で区別する

`multiply : Nat → Nat → Nat` を定義し、`multiply 2` の型を予想してから
`doubleByMultiplication : Nat → Nat` として名前を与えます。二引数関数を一引数関数の反復で表すことと、
その関数に実際に一引数を与えることを、定義時と使用時の異なる操作として説明してください。

さらに暗黙引数を一つ持つ関数を作ります。カリー化、部分適用、暗黙引数の三者を比較表にします。
表には、構文上の引数、省略される引数、新しい関数値が生じる時点を記入してください。

### 合成の単位則を等式による証明とLean証明で対照する

任意の `f : A → B` について、`id ∘ f = f` と `f ∘ id = f` をまず等式列で証明します。関数の等しさを
点ごとの等しさへ帰着させ、任意の入力で両辺を計算してください。次に同じ証明をLeanで書き、
`funext` が担う段階と `rfl` で閉じる計算段階を分けて注釈します。

検証として、関数外延性を使わずに各点の等式だけを証明した場合、なぜ元の関数等式がまだ得られていないかを述べてください。
-/

end FormalLab.Foundation.Functions