第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 の中だけで使える局所名を導入します。これを束縛と呼び、その有効範囲がスコープです。

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

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

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

受け取った項をそのまま返す恒等関数です。

Leankernel-checked counterpartL70–71

def identity {α : Type} (x : α) : α :=
  x

最初の値を保存し、次の入力を無視して返す定数関数です。

Leankernel-checked counterpartL74–75

def constant {α : Type} {β : Type} (x : α) : β → α :=
  fun _ => x

f の出力を g の入力へ渡す関数合成です。

Leankernel-checked counterpartL78–80

def compose {α : Type} {β : Type} {γ : Type}
    (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)

合成を入力へ適用すると、中間結果を順に渡す計算へ戻ります。

Leankernel-checked counterpartL83–85

theorem compose_apply {α β γ : Type} (g : β → γ) (f : α → β) (x : α) :
    compose g f x = g (f x) :=
  rfl

三関数の合成は、各入力でどちらに括っても同じ計算になります。

Leankernel-checked counterpartL88–91

theorem compose_assoc_pointwise {α β γ δ : Type}
    (h : γ → δ) (g : β → γ) (f : α → β) (x : α) :
    compose h (compose g f) x = compose (compose h g) f x :=
  rfl

関数 f を同じ入力へ二回適用します。

Leankernel-checked counterpartL94–95

def applyTwice {α : Type} (f : α → α) (x : α) : α :=
  f (f x)

型から合成を導出する#

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

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

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

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

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

二つの自然数を受け取る関数。型は Nat → (Nat → Nat) と読む。

Leankernel-checked counterpartL117–118

def add : Nat → Nat → Nat :=
  fun left => fun right => left + right

add の第一引数だけを与えて得た、一引数関数。

Leankernel-checked counterpartL121–126

def addThree : Nat → Nat :=
  add 3

#check add
#check add 3
#eval addThree 4

出力

FormalLab.Foundation.Functions.add : Nat → Nat → Nat

出力

add 3 : Nat → Nat

出力

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

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

Leankernel-checked counterpartL136–138

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

出力

@identity : {α : Type} → α → α

出力

FormalLab.Foundation.Functions.compose {α β γ : Type} (g : β → γ) (f : α → β) : α → γ

出力

結合の向きを読む#

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

\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 で閉じる計算段階を分けて注釈します。

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