3.1. 関数（Functions）🔗

関数型は Lean の組み込み機能です。 関数 （function）とはある型の値（ 定義域 、domain）から別の型の値（ 値域 、range）へとマッピングし、 関数型 （function type） は関数の定義域と値域を指定します。

関数型には2種類あります：

依存的 （dependent）

依存関数の型はパラメータに明示的に名前を付け、関数の値域はこの名前を明示的に参照することができます。型は値から計算できるため、依存関数はその引数に応じて任意の数の異なる型の値を返すことができます。 依存関数は集合の添字付き積に対応するため、 依存積 （dependent product）と呼ばれることもあります。

非依存的 （non-dependent）

非依存関数の型はパラメータの名前を含まず、提供される特定の引数によって値域が変わることはありません。

依存関数型

関数 two はどの引数で呼び出されるかに応じて異なる型の値を返します：

def two : (b : Bool) → if b then Unit × Unit else String := fun b => match b with | true => ((), ()) | false => "two"

関数の本体は if...then...else... と書くことができません。なぜならこの書き方は Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match と同じように型を絞り込まないからです。

Lean のコア言語では、すべての関数型は依存的です：非依存関数型はパラメータ名が値域内に出現しない依存関数型のことです。さらに、パラメータ名が異なる2つの依存関数型について、パラメータ名をリネームしたものが等しい場合、これら2つは definitionally equal になります。しかし、Lean のエラボレータは非依存関数のパラメータにローカル束縛を導入しません。

依存・非依存関数の definitional equality

型 (x : Nat) → String と Nat → String は definitionally equal です：

example : ((x : Nat) → String) = (Nat → String) := rfl

同様に、型 (n : Nat) → n + 1 = 1 + n と (k : Nat) → k + 1 = 1 + k は definitionally equal です：

example : ((n : Nat) → n + 1 = 1 + n) = ((k : Nat) → k + 1 = 1 + k) := rfl
非依存関数は変数を束縛しない

配列のすべての要素が0でないことを示す以下の文においては、依存関数が必要です：

def AllNonZero (xs : Array Nat) : Prop := (i : Nat) → (lt : i < xs.size) → xs[i] ≠ 0

これは配列アクセスのためのエラボレータが、インデックスが範囲内にあることの証明を必要とするためです。非依存バージョンの文では、この仮定は導入されません：

def AllNonZero (xs : Array Nat) : Prop := (i : Nat) → (i < xs.size) → failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid xs : Array Nat i : Nat ⊢ i < xs.sizexs[i] ≠ 0 
failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
xs : Array Nat
i : Nat
⊢ i < xs.size

コア型理論には 暗黙 パラメータの機能はありませんが、関数型にはパラメータが暗黙かどうかの表示があります。この情報は Lean のエラボレータに使用されますが、コア型理論における型チェックや definitional equality には影響しないため、コア型理論についてだけ考える場合は無視しても構いません。

暗黙・明示の関数型の definitional equality

型 {α : Type} → (x : α) → α と (α : Type) → (x : α) → α は最初のパラメータが一方が暗黙的で他方では明示的でありながら definitionally equal です。

example : ({α : Type} → (x : α) → α) = ((α : Type) → (x : α) → α) := rfl

3.1.1. 関数抽象（Function Abstractions）

Lean の型理論では、関数は変数を束縛する 関数抽象 （function abstraction）を使用して作成されます。 様々なコミュニティでは、関数抽象は Alonzo Church の記法に由来する ラムダ式 としても知られており、グローバル環境で名前を定義する必要がないことから 無名関数 （anonymous function）としても知られています。 関数を適用すると、 β簡約 によって結果が求められます：引数でその束縛変数を置換します。コンパイルされたコードでは、これは正格に行われます：引数はすでに値でなければなりません。型チェックの際には、このような制約はありません；definitional equality における等式の理論では、どのような項でもβ簡約が許可されます。

Lean の 項の言語 では、関数抽象は複数のパラメータを取ったりパターンマッチを使ったりすることができます。これらの機能はコア言語ではより単純な操作に変換され、変換された関数抽象はすべて正確に1つのパラメータを取ります。すべての関数が抽象に由来するわけではありません： 型コンストラクタ ・ コンストラクタ ・ 再帰子 は関数型を持ちえますが、関数抽象だけでは定義できません。

3.1.2. カリー化（Currying）🔗

Lean のコア型理論では、すべての関数は定義域の要素をそれぞれ値域の単一の要素にマッピングします。言い換えれば、すべての関数は正確に1つのパラメータを必要とします。複数のパラメータを持つ関数は、高階関数を定義することで実装されます。これは最初のパラメータを与えると、残りのパラメータを期待する新しい関数を返します。このエンコーディングは カリー化 （currying）と呼ばれ、Haskell B. Curry にちなんで命名されました。関数を定義し、型を指定し、それを適用するための Lean の構文は、複数パラメータの関数のような錯覚を引き起こしますが、エラボレーションの結果には単一パラメータの関数のみが含まれます。

3.1.3. 外延性（Extensionality）🔗

Lean における関数の definitional equality は 内包的 （intensional）です。つまり、この definitional equality は、束縛変数のリネームと 簡約 によって 構文上 （syntactically）で定義されます。大まかに言えば、これは2つの関数が同じアルゴリズムを実装していれば definitionally equal であるということを意味し、定義域の等しい要素を値域の等しい要素にマッピングしていれば等しいという通常の数学的な等値性の概念とは異なります。

definitional equality は型チェッカで使用されるため、予測可能であることが重要です。内包的な等価性の構文的特徴によって、それをチェックするアルゴリズムが適切に指定できます。外延的な等価性のチェックには、関数の等価性に関する本質的に任意の定理を証明する必要があり、それをチェックするアルゴリズムの明確な仕様はありません。このため、外延的な等価性は型チェッカに向きません。その代わりに関数の外延性は、2つの関数が等しいという 命題 を証明する時に推論原理として利用できるようになっています。

束縛変数の簡約とリネームに加えて、 η同値 （η-equivalence）と呼ばれる外延性の1つの限定された形式をサポートします。これは、ある関数とその本体が引数に適用されている抽象と等しいことを指します。 f の型が (x : α) → β x であるとすると、 f は fun x => f x と definitionally equal です。

関数について推論するとき、定理 funextいくつかの内包的な型理論とは異なり、 funext は Lean における定理です。これは quotient 型を使って証明できます。 または対応するタクティク funext もしくは ext を使用して、2つの関数が等しい入力を等しい出力にマッピングする場合に等しいことを証明することができます。

🔗
funext.{u, v} {α : Sort u} {β : α → Sort v}
    {f g : (x : α) → β x}
    (h : ∀ (x : α), f x = g x) : f = g

Function extensionality is the statement that if two functions take equal values every point, then the functions themselves are equal: (∀ x, f x = g x) → f = g. It is called "extensionality" because it talks about how to prove two objects are equal based on the properties of the object (compare with set extensionality, which is (∀ x, x ∈ s ↔ x ∈ t) → s = t).

This is often an axiom in dependent type theory systems, because it cannot be proved from the core logic alone. However in lean's type theory this follows from the existence of quotient types (note the Quot.sound in the proof, as well as the show line which makes use of the definitional equality Quot.lift f h (Quot.mk x) = f x).

3.1.4. 全域性と停止（Totality and Termination）🔗

関数は Lean.Parser.Command.declaration : commanddef を使って再帰的に定義することができます。Lean の論理の観点から、すべての関数は 全域 （total）です。これは関数が定義域の各要素を値域の要素に有限時間でマッピングすることを意味します。 プログラミング言語のコミュニティによっては、異なる意味で 全域 という用語を使用するものもあり、その場合、関数がハンドルされていないケースによってクラッシュしなければ全域と見なされますが、非停止は無視されます。 全域関数の値はすべての型が正しい引数に対して定義され、パターンマッチでケースが漏れて停止に失敗したりクラッシュしたりすることはありません。

Lean の論理モデルはすべての関数を全域関数と見なしますが、Lean は実用的なプログラミング言語でもあり、ある種の「逃げ道」を用意しています。停止することが証明されていない関数は、その値域が空でないことが証明されている限り Lean の論理で使用することができます。これらの関数は Lean の論理では未解釈の関数として扱われ、その計算動作は無視されます。コンパイルされたコードでは、これらの関数は他の関数と同様に扱われます。そうではない関数は unsafe とマークされることがあります；これらの関数は Lean の論理では全く使用することができません。 partial と unsafe 関数定義 の節で再帰関数を使ったプログラミングの詳細があります。

同様に、配列への範囲外アクセスなど、コンパイルされたコードではランタイムに失敗するはずの操作は、結果の型が inhabited であることが分かっている場合にのみ使用することができます。これらの操作の結果、Lean のロジックでは型の住人が任意に選ばれます（具体的には、その型の Inhabited インスタンスで指定されたもの）。

パニック

関数 thirdChar は配列の3番目の要素を取り出します。配列の要素が2個以下の場合はパニックします：

def thirdChar (xs : Array Char) : Char := xs[2]!

#['!'] と #['-', 'x'] の（存在しない）3番目の要素は等しいです。なぜなら、どちらも同じ任意に選ばれた文字を返すからです：

example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl

実際、どちらも 'A' に等しく、これは偶然にも Char のデフォルトのフォールバックです：

example : thirdChar #['!'] = 'A' := rfl example : thirdChar #['-', 'x'] = 'A' := rfl