diff --git a/LeanByExample/Declarative/Axiom.lean b/LeanByExample/Declarative/Axiom.lean index 97c73bb3..98158c8b 100644 --- a/LeanByExample/Declarative/Axiom.lean +++ b/LeanByExample/Declarative/Axiom.lean @@ -119,7 +119,7 @@ end quot --# 実際に証明していきます。一般に証明を理解するためには、前提を確認することが大切です。「商の公理を使用しなくても、前提として等しいことが分かっているものは何か」をまず確認しましょう。前提として利用できる事実には、次の２つがあります： -* 関数 `f` とラムダ式 `fun x => f x` は等しい。（これは **η 簡約(eta reduce)** と呼ばれます） +* 関数 `f` とラムダ式 `fun x => f x` は等しい。（これは **η 簡約(eta reduce)** と呼ばれる簡約ルールより従います） * 関数 `f` と、「関数 `f` を適用する関数」は等しい。 実際に、公理を一切使わずにこれは証明できます。 diff --git a/LeanByExample/Declarative/Class.lean b/LeanByExample/Declarative/Class.lean index 0ff45b7a..10b450db 100644 --- a/LeanByExample/Declarative/Class.lean +++ b/LeanByExample/Declarative/Class.lean @@ -1,6 +1,6 @@ /- # class -`class` は型クラスを定義するためのコマンドです。型クラスを用いると、複数の型に対して定義され、型ごとに異なる実装を持つような関数を定義することができます。例えば「和を取る操作」のような、`Nat` や `Int` や `Rat` など複数の型に対して同じ名前で定義したい関数を作りたいとき、型クラスが適しています。 +`class` は **型クラス(type class)** を定義するためのコマンドです。型クラスを用いると、複数の型に対して定義され、型ごとに異なる実装を持つような関数を定義することができます。例えば「和を取る操作」のような、`Nat` や `Int` や `Rat` など複数の型に対して同じ名前で定義したい関数を作りたいとき、型クラスが適しています。 -/ namespace Class --# /-- 証明なしのバージョンのモノイド。 @@ -74,7 +74,7 @@ def instMonoid'Nat : Monoid' Nat where #check (Monoid.e : {α : Type} → [_self : Monoid α] → α) -/- これは**インスタンス暗黙引数**と呼ばれるもので、この場合 Lean に対して `Monoid' α` 型の項を自動的に合成するよう指示することを意味します。また、型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを、**型クラス解決**と呼びます。-/ +/- これは **インスタンス暗黙引数(instance implicit)** と呼ばれるもので、この場合 Lean に対して `Monoid' α` 型の項を自動的に合成するよう指示することを意味します。また、型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを、 **型クラス解決(type class resolution)** と呼びます。-/ /- ## outParam 足し算を表現する型クラスを自分で定義してみましょう。名前は `Plus` としてみます。足し算は自然数の和 `Nat → Nat → Nat` のように、同じ型の中で完結する操作として定義されることが多いものですが、より一般的に `α → β → γ` で定義されるものとしてみます。 diff --git a/LeanByExample/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean index 835dcdcc..b56fc3a0 100644 --- a/LeanByExample/Declarative/Infix.lean +++ b/LeanByExample/Declarative/Infix.lean @@ -11,7 +11,7 @@ scoped infix:60 " ⋄ " => Nat.mul #guard 2 ⋄ 3 = 6 -/- `:` の後に付けている数字はパース優先順位で、高いほど結合するタイミングが早くなります。等号 `=` のパース優先順位は 50 であることを覚えておくと良いかもしれません。-/ +/- `:` の後に付けている数字は **パース優先順位(parsing precedence)** で、高いほど結合するタイミングが早くなります。等号 `=` のパース優先順位は 50 であることを覚えておくと良いかもしれません。-/ -- 等号より微妙にパース優先順位が高い scoped infix:51 " strong " => Nat.add diff --git a/LeanByExample/Declarative/Notation.lean b/LeanByExample/Declarative/Notation.lean index feab1222..f0590600 100644 --- a/LeanByExample/Declarative/Notation.lean +++ b/LeanByExample/Declarative/Notation.lean @@ -34,7 +34,7 @@ set_option pp.notation false end /- ## パース優先順位 -`notation` で記法を定義するときに、その記法の他の演算子などと比べたパース優先順位(parsing precedence)を数値で指定することができます。パース優先順位が高い演算子ほど、他の演算子より先に適用されます。言い換えれば、パース優先順位を正しく設定することにより、括弧を省略しても意図通りに式が解釈されるようにすることができます。 +`notation` で記法を定義するときに、その記法の他の演算子などと比べた **パース優先順位(parsing precedence)** を数値で指定することができます。パース優先順位が高い演算子ほど、他の演算子より先に適用されます。言い換えれば、パース優先順位を正しく設定することにより、括弧を省略しても意図通りに式が解釈されるようにすることができます。 -/ /-- 結合が弱い方。中身は足し算 -/ diff --git a/LeanByExample/Declarative/Syntax.lean b/LeanByExample/Declarative/Syntax.lean index 07885767..2e492e93 100644 --- a/LeanByExample/Declarative/Syntax.lean +++ b/LeanByExample/Declarative/Syntax.lean @@ -57,7 +57,7 @@ using the `set_option diagnostics true` command. #check_failure (1 + 1 = 2 as Nat) end --# -/- パース優先順位(parsing precedence)を設定することで、どの構文から順に解釈されるかを指定することができ、問題を修正できることがあります。このあたりは [`notation`](./Notation.md) コマンドと同様です。 -/ +/- **パース優先順位(parsing precedence)** を設定することで、どの構文から順に解釈されるかを指定することができ、問題を修正できることがあります。このあたりは [`notation`](./Notation.md) コマンドと同様です。 -/ section --# -- 十分低いパース優先順位を設定する diff --git a/LeanByExample/Type/List.lean b/LeanByExample/Type/List.lean index cf9704f4..f1cd4d1e 100644 --- a/LeanByExample/Type/List.lean +++ b/LeanByExample/Type/List.lean @@ -1,6 +1,6 @@ /- # List -`List` は**連結リスト**を表す型です。 +`List` は **連結リスト(linked list)** を表す型です。 Lean では次のように再帰的に定義されています。 -/ @@ -59,7 +59,7 @@ end Hidden --# /- ## 高階関数 -「関数を引数に取る関数」や「関数を返す関数」のことを、**高階関数**と呼ぶことがあります。`List` 名前空間には様々な高階関数が定義されています。 +「関数を引数に取る関数」や「関数を返す関数」のことを、**高階関数(higher-order function)** と呼ぶことがあります。`List` 名前空間には様々な高階関数が定義されています。 ### map diff --git a/LeanByExample/Type/Prop.lean b/LeanByExample/Type/Prop.lean index 2f3aee2d..46c7ced7 100644 --- a/LeanByExample/Type/Prop.lean +++ b/LeanByExample/Type/Prop.lean @@ -7,7 +7,7 @@ #check (1 + 1 = 2 : Prop) #check (1 + 1 = 3 : Prop) -/- ## Curry Howard 同型対応 +/- ## カリー・ハワード同型対応 Lean では、各命題 `P : Prop` は再び型になっています。これは通常の数学では考えないことなので慣れないとわかりにくいのですが、言い換えれば命題 `P` の項というものを考えることができます。 @@ -20,12 +20,12 @@ Lean では、各命題 `P : Prop` は再び型になっています。これは -- 項に名前を付けた def one_and_one_eq_two : 1 + 1 = 2 := rfl -/- 実は、いま構成した `1 + 1 = 2` という型の項は `1 + 1 = 2` の証明になっています。実際のところ、命題 `P : Prop` の証明とは、Lean においては項 `h : P` そのものです。このことを強調するために、**証明項**という呼び方をすることもあります。-/ +/- 実は、いま構成した `1 + 1 = 2` という型の項は `1 + 1 = 2` の証明になっています。実際のところ、命題 `P : Prop` の証明とは、Lean においては項 `h : P` そのものです。このことを強調するために、 **証明項(proof term)** という呼び方をすることもあります。-/ -- さっき構成した証明項で証明ができる example : 1 + 1 = 2 := one_and_one_eq_two -/- このように命題を型として、証明を項として実装できるのは、そもそも直観主義論理と型付きラムダ計算の間に **Curry Howard 同型対応**が存在するからです。簡単に言えば、論理と計算（プログラム）は出自は全く異なるものの何故か同じ構造を持っており、同じものであると見なせるということです。-/ +/- このように命題を型として、証明を項として実装できるのは、そもそも直観主義論理と型付きラムダ計算の間に **カリー・ハワード同型対応(correspondence)** が存在するからです。簡単に言えば、論理と計算（プログラム）は出自は全く異なるものの何故か同じ構造を持っており、同じものであると見なせるということです。-/ /- ## 命題論理 [`Bool`](#{root}/Type/Bool.md) には真と偽に対応する `true` と `false` という項がありますが、`Prop` では真偽は `True` と `False` で表されます。 diff --git a/LeanByExample/Type/Syntax.lean b/LeanByExample/Type/Syntax.lean index 7f820d96..e9af1339 100644 --- a/LeanByExample/Type/Syntax.lean +++ b/LeanByExample/Type/Syntax.lean @@ -36,7 +36,7 @@ inductive Syntax where (val : Name) (preresolved : List Syntax.Preresolved) : Syntax --#-- --- **Syntax の定義の変更を確認するためのコード** +-- Syntax の定義の変更を確認するためのコード /-- info: inductive Lean.Syntax : Type number of parameters: 0 diff --git a/LeanByExample/Type/Type.lean b/LeanByExample/Type/Type.lean index b9dd50fe..9e22e899 100644 --- a/LeanByExample/Type/Type.lean +++ b/LeanByExample/Type/Type.lean @@ -38,11 +38,11 @@ example : Sort (u + 1) = Type u := rfl /- ## なぜ Type : Type ではないのか 何故このような仕様になっているのでしょうか。可算無限個の宇宙を用意するよりも `Type : Type` とした方が簡単ではないでしょうか？実は、`Type : Type` となるような型理論を採用すると矛盾が生じてしまいます。 -これは **Girard のパラドックス** と呼ばれる有名な結果です。しかし Girard のパラドックスを直接説明しようとすると準備が多く必要になるので、ここでは Girard のオリジナルの議論を追うことはせず、代わりに濃度による簡潔な議論を紹介します。 +これは **ジラールのパラドックス(Girard's paradox)** と呼ばれる有名な結果です。しかしジラールのパラドックスを直接説明しようとすると準備が多く必要になるので、ここではジラールのオリジナルの議論を追うことはせず、代わりに濃度による簡潔な議論を紹介します。 以下証明を説明します。仮に `Type` が `Type` の項だったとしましょう。このとき `α := Type` とすることにより、ある `Type` の項 `α` を選べば、全射 `f : α → Type` を作れることがわかります。したがって、任意の型 `α : Type` に対して関数 `f : α → Type` が全射になることはありえないことを示せばよいことになります。 -これは Cantor の定理の単射バージョンに帰着して示すことができます。 +これは **カントールの定理(Cantor's theorem)** の単射バージョンに帰着して示すことができます。 -/ open Function diff --git a/LeanByExample/TypeClass/CoeSort.lean b/LeanByExample/TypeClass/CoeSort.lean index e6692b09..4d601834 100644 --- a/LeanByExample/TypeClass/CoeSort.lean +++ b/LeanByExample/TypeClass/CoeSort.lean @@ -60,7 +60,7 @@ local instance : Coe FinCat Type := ⟨fun S ↦ S.base⟩ #check_failure (Two → Two) end --# -/- しかし、これは「`Coe` では型宇宙への変換は扱えないから」ではありません。`Coe` と `CoeSort` では型強制が呼ばれるタイミングが異なるからです。`Coe` は「ある型の**項**が期待される場所に、異なる型の項が来た時」にトリガーされますが、`CoeSort` は「**型**が期待される場所に型が来ていないとき」にトリガーされます。 +/- しかし、これは「`Coe` では型宇宙への変換は扱えないから」ではありません。`Coe` と `CoeSort` では型強制が呼ばれるタイミングが異なるからです。`Coe` は「ある型の項が期待される場所に、異なる型の項が来た時」にトリガーされますが、`CoeSort` は「型が期待される場所に型が来ていないとき」にトリガーされます。 実際、`Coe` を使っても `Type` への型強制は定義することができます。 -/ diff --git a/LeanByExample/TypeClass/GetElem.lean b/LeanByExample/TypeClass/GetElem.lean index 899625d0..ff932edd 100644 --- a/LeanByExample/TypeClass/GetElem.lean +++ b/LeanByExample/TypeClass/GetElem.lean @@ -42,7 +42,7 @@ instance : GetElem (MyList α) Nat α (fun as i => i < as.length) where #guard Three[2] = 3 /- ## インデックスアクセスの種類 -コレクション `as` に対して、`i` 番目の要素を取得すると書きましたが、**i 番目の要素があるとは限らない**という問題があります。これに対処するには様々な方法がありえますが、中でも以下のものは専用の構文が用意されています。 +コレクション `as` に対して、`i` 番目の要素を取得すると書きましたが、`i` 番目の要素があるとは限らないという問題があります。これに対処するには様々な方法がありえますが、中でも以下のものは専用の構文が用意されています。 * `as[i]`: インデックス `i` が範囲内であることの証明を自動で構成する。`i` が変数になっていて具体的に計算できないときでも、ローカルコンテキスト内に `i` が範囲内であることの証明があれば動作する。 * `as[i]?`: 返り値を [`Option`](#{root}/Type/Option.md) に包む。範囲外の場合は `none` を返す diff --git a/LeanByExample/TypeClass/README.lean b/LeanByExample/TypeClass/README.lean index aa4b793b..f9f1d269 100644 --- a/LeanByExample/TypeClass/README.lean +++ b/LeanByExample/TypeClass/README.lean @@ -1,6 +1,6 @@ /- # 型クラス -型クラスとは、和や積、逆数を取る演算など、複数の型に対してそれぞれのやり方で実装されるような演算を定義するものです。 +**型クラス(type class)** とは、和や積、逆数を取る演算など、複数の型に対してそれぞれのやり方で実装されるような演算を定義するものです。 型クラスは主に [`class`](#{root}/Declarative/Class.md) コマンドで定義され、インスタンスを宣言するには [`instance`](#{root}/Declarative/Instance.md) コマンドを使用します。 -/