diff --git a/GLOSSARY.md b/GLOSSARY.md index 8792022..9371b03 100644 --- a/GLOSSARY.md +++ b/GLOSSARY.md @@ -7,14 +7,17 @@ | angle bracket | 角括弧 | square bracketと同じ訳語にしているが、直後にコード例がある場合も多いため文脈で見分けられる想定 | | annotation | 注釈 | | | anonymous constructor | 匿名コンストラクタ | | +| assign | 割り当て | | | associativity | 結合性 | | | assumption | 仮定 | | | at most | 高々 | | | attribute | 属性 | | +| auto-bound | 自動的に束縛された | | | backtrack | バックトラック | 後戻りと書かれる場合あり | | base case | 基本ケース | | | bijection | 全単射 | | | binder | 束縛子 | | +| binding | 束縛 | | | boolean | 真偽値 | | | bound variable | 束縛変数 | | | box | ボックス化 | | @@ -46,10 +49,12 @@ | declaration | 宣言 | | | definition | 定義 | | | definitional (η-)equality | 定義上の(η)等価性 | | +| definition-like | 定義に類する | | | definitional proof irrelevance | 定義上の証明の無関係性 | | | dependent | 依存的 | 後ろに何も続かない場合 | | dependent function | 依存関数 | | | dependent type theory | 依存型理論 | | +| derivation | 導出 | | | deriving | 導出 | | | desugar | 脱糖 | | | disjointness | 不連結性 | | @@ -77,6 +82,7 @@ | extend | 拡張 | | | field | （構造体・クラスのメンバの意味）フィールド | | | field specifier | フィールド指定子 | | +| first-class | 第一級 | | | fixed point operator | 不動点演算子 | | | fixed-width integer | 固定幅 整数 | | | formalization | 形式化 | | @@ -94,7 +100,9 @@ | identifier | 識別子 | | | identifier component | 識別子要素 | | | identifier continuation character | 識別子継続文字 | | +| identity function | 恒等関数 | | | implicit parameter | 暗黙のパラメータ | | +| incompatible | 互換性 | | | index, indices | 添字 | | | induction | 帰納法 | | | induction hypothese | 帰納法の仮定 | | @@ -108,7 +116,7 @@ | injectivity | 単射性 | | | instance implicit parameter | インスタンスの暗黙のパラメータ | | | instances synthesize | インスタンス合成 | | -| instantiate | インスタンス化 | | +| instantiate, instantiation | インスタンス化 | | | intensional | 内包的 | | | interactive theorem prover | 対話型定理証明器 | | | interface | インタフェース | | @@ -120,9 +128,11 @@ | kind | 種 | | | laziness | 遅延 | | | language server | 言語サーバ | | +| least upper bound | 最小上界 | | | lemma | 補題 | | | letter | 文字 | | | letterlike | 文字様 | | +| level expression | レベル式 | | | longest match | 最長一致 | | | macro | マクロ | | | machine integer | 機械整数 | | @@ -133,6 +143,7 @@ | memoization | メモ化 | | | modifier | 修飾子 | | | monad | モナド | | +| monomorphism | モノ射 | | | motive | 動機 | | | multi-threading | マルチスレッド | | | mutually inductive | 相互帰納 | | @@ -155,13 +166,15 @@ | predicate | 述語 | | | pretty printer | プリティプリンタ | | | primitive | プリミティブ | | +| primitive recursion | 原始再帰 | | | product type | 直積型 | | | projection function | 射影関数 | | | proof checker | 証明チェッカ | | | proof state | 証明状態 | | | proof term | 証明項 | | | qualification | 修飾 | | -| quantify | 定量化 | | +| quantify | 量化 | | +| quantification | 量化子 | | | question mark | 疑問符 | | | quote | クォート | | | quotient type | 商型 | | @@ -180,6 +193,7 @@ | run-time | ランタイム | | | rule | 規則 | | | saturated application | 完全な適用 | 固定訳は無いように思われ、飽和では意味が分かりづらいため | +| schematic definition | スキーマ的定義 | | | scope | スコープ | | | separator | 区切り文字 | | | set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | | @@ -188,11 +202,13 @@ | side effect | 副作用 | | | signature | シグネチャ | | | single quote | シングルクォート | | +| singleton | 単集合 | | | soundness | 健全性 | | | square bracket | 角括弧 | | | specialization | 特殊化 | | | statement | 文 | | | strict implicit parameter | 厳格な暗黙のパラメータ | | +| strictly | （順序の意味で）狭義 | | | strictness | 正格 | | | strong induction | 強帰納法 | | | structure | 構造体 | | @@ -200,6 +216,7 @@ | subterm | 部分項 | | | subtype | 部分型 | | | subscript | 下付き文字 | | +| substitution | 置換 | | | syntactically | 構文上 | | | syntactic sugar | 構文糖衣 | | | syntax | 構文 | | @@ -222,6 +239,7 @@ | tree | 木 | | | trivial | 自明な | | | trust | 信頼 | | +| tuple | タプル | | | type class | 型クラス | | | type class instance synthesis | 型クラスインスタンス合成 | | | type signature | 型シグネチャ | | @@ -244,10 +262,13 @@ | 用語 | 備考 | | --- | --- | | choice node | | +| cumulative | | +| impredicativity, predicativity | | | packed array | System Verilogという言語にこの名前の文法要素がある？ | | strict positively, negatively | 自己言及される定義の分類、定訳は無い模様 | | prelude | | | relevant, irrelevant | 直訳して「関係・無関係」はわかりづらいと判断 | | subject reduction | TAPLに出てくる模様 | | subsingleton | | -| type ascription | Scala、Rustに同じ用語あり | \ No newline at end of file +| type ascription | Scala、Rustに同じ用語あり | +| well-typed | | \ No newline at end of file diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index eaa22ac..4497ca5 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -39,7 +39,7 @@ def ullrich23 : Thesis where /- #doc (Manual) "Elaboration and Compilation" => -/ -#doc (Manual) "エラボレーションとコンパイル" => +#doc (Manual) "エラボレーションとコンパイル（Elaboration and Compilation）" => %%% htmlSplit := .never %%% @@ -132,7 +132,7 @@ The next command is parsed and elaborated in this updated state, and itself upda # Parsing ::: -# パース +# パース（Parsing） :::comment Lean's parser is a recursive-descent parser that uses dynamic tables based on Pratt parsing{citep pratt73}[] to resolve operator precedence and associativity. @@ -191,7 +191,7 @@ Syntax extensions are described in more detail in {ref "language-extension"}[a d # Macro Expansion and Elaboration ::: -# マクロ展開とエラボレーション +# マクロ展開とエラボレーション（Macro Expansion and Elaboration） :::comment Having parsed a command, the next step is to elaborate it. @@ -248,7 +248,7 @@ While macro expansion occurs prior to elaboration for a given “layer” of the ## Info Trees ::: -## 情報木 +## 情報木（Info Trees） :::comment When interacting with Lean code, much more information is needed than when simply importing it as a dependency. @@ -278,7 +278,7 @@ This can be used to add information to be used by custom code actions or other u # The Kernel ::: -# カーネル +# カーネル（The Kernel） :::comment Lean's trusted {deftech}_kernel_ is a small, robust implementation of a type checker for the core type theory. @@ -311,7 +311,7 @@ The language implemented by the kernel is a version of the Calculus of Construct カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です： + 完全な依存型 + 相互に帰納的であったり、他の帰納的データ型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型 -+ {tech}[impredicative] ・定義上証明と irrelevant な {tech}[propositions] の拡張的 {tech}[universe] ++ {tech}[impredicative] ・定義上証明と irrelevant な {tech}[命題] の拡張的 {tech}[宇宙] + {tech}[predicative] なデータの宇宙の非蓄積な階層 * 定義上の計算規則を伴った {ref "quotients"}[商型] （Quotient type） + 命題上の関数外延性 {margin}[関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。] @@ -362,7 +362,7 @@ Lean の型理論には subject reduction の機能はなく、定義上の等 # Elaboration Results ::: -# エラボレーションの結果 +# エラボレーションの結果（Elaboration Results） :::comment Lean's core type theory does not include pattern matching or recursive definitions. @@ -371,7 +371,7 @@ Thus, the elaborator must translate definitions that use pattern matching and re This translation is additionally a proof that the function terminates for all potential arguments, because all functions that can be translated to recursors also terminate. ::: -Lean のコア型理論には、パターンマッチや再帰定義は含まれていません。その代わりに、場合分けとプリミティブな再帰の両方を実装するために使用できる低レベルの {tech}[再帰子] を提供します。したがって、エラボレータはパターンマッチと再帰を使用する定義から再帰子を使用する定義に変換する必要があります。この変換はさらに、関数がすべての潜在的な引数に対して停止することの証明でもあります。なぜなら再帰子へ翻訳されるすべての関数は停止するからです。 +Lean のコア型理論には、パターンマッチや再帰定義は含まれていません。その代わりに、場合分けと原始再帰の両方を実装するために使用できる低レベルの {tech}[再帰子] を提供します。したがって、エラボレータはパターンマッチと再帰を使用する定義から再帰子を使用する定義に変換する必要があります。この変換はさらに、関数がすべての潜在的な引数に対して停止することの証明でもあります。なぜなら再帰子へ翻訳されるすべての関数は停止するからです。 :::comment The translation to recursors happens in two phases: during term elaboration, uses of pattern matching are replaced by appeals to auxiliary functions that implement the particular case distinction that occurs in the code. @@ -655,7 +655,7 @@ For most workloads, the overhead of compilation is larger than the time saved by # Initialization ::: -# 初期化コード +# 初期化（Initialization） :::comment Before starting up, the elaborator must be correctly initialized. diff --git a/Manual/Language.lean b/Manual/Language.lean index beb68e7..a51ea8c 100644 --- a/Manual/Language.lean +++ b/Manual/Language.lean @@ -22,49 +22,103 @@ set_option pp.rawOnError true set_option linter.unusedVariables false +/- #doc (Manual) "The Lean Language" => +-/ +#doc (Manual) "Lean 言語について（The Lean Language）" => {include Manual.Language.Files} +# 型システム（The Type System） + +:::comment +-- エラーが発生するためタイトルのみ上下入れ替えている # The Type System {deftech}_Terms_, also known as {deftech}_expressions_, are the fundamental units of meaning in Lean's core language. -They are produced from user-written syntax by the {tech}[エラボレータ].elaborator +They are produced from user-written syntax by the {tech}[elaborator]. Lean's type system relates terms to their _types_, which are also themselves terms. Types can be thought of as denoting sets, while terms denote individual elements of these sets. A term is {deftech}_well-typed_ if it has a type under the rules of Lean's type theory. Only well-typed terms have a meaning. +::: + +{deftech}_項_ （term）は {deftech}_式_ （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは {tech}[エラボレータ] によってユーザが書いた構文から生成されます。Lean の型システムは項をその _型_ （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論のルールに従った型を持つ項は {deftech}_well-typed_ と言います。well-typed である項のみが意味を持ちます。 + +:::comment Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and `let`-bindings. -In addition to bound variables, variables in the term language may refer to {tech}[コンストラクタ]constructors, {tech}[型コンストラクタ]type constructors, {tech}[再帰子]recursors, {deftech}[defined constants], or opaque constants. +In addition to bound variables, variables in the term language may refer to {tech}[constructors], {tech}[type constructors], {tech}[recursors], {deftech}[defined constants], or opaque constants. Constructors, type constructors, recursors, and opaque constants are not subject to substitution, while defined constants may be replaced with their definitions. +::: + +項は依存型付きラムダ計算です；関数抽象・適用・変数・`let` 束縛を含みます。束縛変数に加えて、項言語の変数は {tech}[コンストラクタ] ・ {tech}[型コンストラクタ] ・ {tech}[再帰子] ・ {deftech}[defined constants] ・不透明な定数を参照することができます。コンストラクタ・型コンストラクタ・再帰子・不透明な定数は置換の対象にはなりませんが、定義された定数はその定義に置き換えることができます。 + +:::comment A {deftech}_derivation_ demonstrates the well-typedness of a term by explicitly indicating the precise inference rules that are used. Implicitly, well-typed terms can stand in for the derivations that demonstrate their well-typedness. Lean's type theory is explicit enough that derivations can be reconstructed from well-typed terms, which greatly reduces the overhead that would be incurred from storing a complete derivation, while still being expressive enough to represent modern research mathematics. This means that proof terms are sufficient evidence of the truth of a theorem and are amenable to independent verification. +::: + +{deftech}_導出_ （derivation）は使用される正確な推論規則を明示的に示すことで項の well-typed さを示します。暗黙的に、well-typed な項は、その well-typed であることを示す導出の代わりにすることができます。Lean の型理論は十分に明示的であるため、well-typed な項から導出を再構築することができ、完全な導出を保存することで発生するオーバーヘッドを大幅に削減することができるにもかかわらず、この理論は現代の研究数学を表現するに足る表現力を保ちます。これは、証明項が定理の真理の十分な根拠となり、独立した検証が可能であることを意味します。 + +:::comment In addition to having types, terms are also related by {deftech}_definitional equality_. This is the mechanically-checkable relation that equates terms modulo their computational behavior. Definitional equality includes the following forms of {deftech}[reduction]: +::: + +型を持つことに加えて、項は {deftech}_定義上の等価性_ （definitional equality）によっても関連付けられます。これは機械的にチェック可能な関係であり、計算動作に応じて項を等しくします。定義上の等価性には {deftech}[簡約] （reduction）の以下の形式が含まれます： + +:::comment : β (beta) Applying a function abstraction to an argument by substitution for the bound variable +::: + + : β (beta) + + 束縛された変数への置換によって、引数に関数抽象を適用する + +:::comment : δ (delta) Replacing occurrences of {tech}[defined constants] by the definition's value +::: + + : δ (delta) + + {tech}[defined constant] の出現箇所を定義の値で置き換える + +:::comment : ι (iota) Reduction of recursors whose targets are constructors (primitive recursion) +::: + + : ι (iota) + + コンストラクタをターゲットとする再帰子の簡約（原始再帰） + +:::comment : ζ (zeta) Replacement of let-bound variables by their defined values -::::keepEnv +::: + + : ζ (zeta) + + let 束縛変数を定義された値に置き換える + +:::::keepEnv ```lean (show := false) axiom α : Type axiom β : Type @@ -84,27 +138,50 @@ example : S.mk x.f1 x.f2 = x := by rfl export S (f1 f2) ``` +:::comment Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, {lean}`fun x => f x` is definitionally equal to {lean}`f`, and {lean}`S.mk x.f1 x.f2` is definitionally equal to {lean}`x`, if {lean}`S` is a structure with fields {lean}`f1` and {lean}`f2`. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence. -:::: +::: + +定義上の等価性には関数と単一コンストラクタの帰納型についてのη同値が含まれます。つまり、 {lean}`fun x => f x` は {lean}`f` に定義上等しく、 {lean}`S` がフィールド {lean}`f1` と {lean}`f2` を持つ構造体である時には {lean}`S.mk x.f1 x.f2` は {lean}`x` と定義上等価です。また証明の irrelevance も特徴づけ、同じ命題の2つの証明は定義上等価です。これは反射的・対称的・合同です。 + +::::: +:::comment Definitional equality is used by conversion: if two terms are definitionally equal, and a given term has one of them as its type, then it also has the other as its type. Because definitional equality includes reduction, types can result from computations over data. -::::keepEnv -:::Manual.example "Computing types" +::: + +定義上の等価性は変換にも用いられます：2つの項が定義上等しく、ある項がその一方を型として持つ場合、その項ももう一方を型として持ちます。定義上の等価性は簡約を含むため、データに対する計算から型が生じることがあります。 +:::::keepEnv +:::comment +::Manual.example "Computing types" +::: +::::Manual.example "型の計算" + +:::comment When passed a natural number, the function {lean}`LengthList` computes a type that corresponds to a list with precisely that many entries in it: +::: + +自然数を渡すと、関数 {lean}`LengthList` は正確にその数のエントリを持つリストに対応する型を計算します： + ```lean def LengthList (α : Type u) : Nat → Type u | 0 => PUnit | n + 1 => α × LengthList α n ``` +:::comment Because Lean's tuples nest to the right, multiple nested parentheses are not needed: +::: + +Lean のタプルは右側にネストしているため、複数のネストした括弧は必要ありません： + ````lean example : LengthList Int 0 := () @@ -112,7 +189,12 @@ example : LengthList String 2 := ("Hello", "there", ()) ```` +:::comment If the length does not match the number of entries, then the computed type will not match the term: +::: + +長さが項目数と一致しない場合、計算された型はその項と一致しません： + ```lean error:=true name:=wrongNum example : LengthList String 5 := ("Wrong", "number", ()) @@ -127,50 +209,111 @@ has type but is expected to have type LengthList String 3 : Type ``` -::: :::: +::::: -The basic types in Lean are {tech}[universes], {tech}[関数]function types, and {tech}[型コンストラクタ]type constructors of {tech}[帰納型]inductive types. -{tech}[Defined constants], applications of {tech}[再帰子]recursors, function application, {tech}[axioms] or {tech}[opaque constants] may additionally give types, just as they can give rise to terms in any other type. +:::comment +The basic types in Lean are {tech}[universes], {tech}[function] types, and {tech}[type constructors] of {tech}[inductive types]. +{tech}[Defined constants], applications of {tech}[recursors], function application, {tech}[axioms] or {tech}[opaque constants] may additionally give types, just as they can give rise to terms in any other type. +::: + +Lean の基本型は {tech}[宇宙] ・ {tech}[関数] 型・ {tech}[帰納型] の {tech}[型コンストラクタ] です。 {tech}[Defined constants] ・ {tech}[再帰子] の適用・関数適用・ {tech}[axioms] ・ {tech}[不透明な定数] のいずれかは他の型の項を生じさせることができるのと同様に、さらに型を与えることができます。 + {include Manual.Language.Functions} -## Propositions +## 命題（Propositions） %%% tag := "propositions" %%% +:::comment +-- エラーが出るため章タイトルの上下を入れ替えている +## Propositions +::: + +:::comment {deftech}[Propositions] are meaningful statements that admit proof. {index}[proposition] Nonsensical statements are not propositions, but false statements are. All propositions are classified by {lean}`Prop`. +::: + +{deftech}[命題] （propositioin）は証明を認める意味のある文です。 {index}[proposition] 無意味な文は命題ではありませんが、偽の文は命題です。すべての命題は {lean}`Prop` によって分類されます。 + +:::comment Propositions have the following properties: +::: + +命題は以下の性質を持ちます： + +:::comment : Definitional proof irrelevance Any two proofs of the same proposition are completely interchangeable. +::: + +: 定義上の証明の irrelevance + + 同じ命題の2つの証明は完全に交換可能です。 + +:::comment : Run-time irrelevance Propositions are erased from compiled code. +::: + +: ランタイムにおける irrelevance + + 命題はコンパイルされたコードからは消去されます。 + +:::comment : Impredicativity Propositions may quantify over types from any universe whatsoever. +::: + +: impredicativity + + 命題はあらゆる宇宙からの型に対して量化することができます。 + +:::comment : Restricted Elimination With the exception of singletons, propositions cannot be eliminated into non-proposition types. +::: + +: 制限された除去 + + 単集合を除いて、命題は非命題型に除去することができません。 + +:::comment : {deftech key:="propositional extensionality"}[Extensionality] {index subterm:="of propositions"}[extensionality] Any two logically equivalent propositions can be proven to be equal with the {lean}`propext` axiom. +::: + +: {deftech key:="propositional extensionality"}[外延性] {index subterm:="of propositions"}[extensionality] + + 論理的に同等な2つの命題は、 {lean}`propext` 公理によって等しいことが証明できます。 + {docstring propext} +:::comment ## Universes +::: + +## 宇宙（Universes） + +:::comment Types are classified by {deftech}_universes_. {index}[universe] Each universe has a {deftech (key:="universe level")}_level_, {index subterm := "of universe"}[level] which is a natural number. The {lean}`Sort` operator constructs a universe from a given level. {index}[`Sort`] @@ -178,14 +321,28 @@ If the level of a universe is smaller than that of another, the universe itself With the exception of propositions (described later in this chapter), types in a given universe may only quantify over types in smaller universes. {lean}`Sort 0` is the type of propositions, while each `Sort (u + 1)` is a type that describes data. +::: + +型は {deftech}_宇宙_ （universe）によって分類されます。 {index}[universe] 各宇宙には {deftech (key:="universe level")}_レベル_ （level）があり、これは自然数です。 {lean}`Sort` 演算子は与えられたレベルから宇宙を構築します。 {index}[`Sort`] ある宇宙レベルが他の宇宙レベルよりも小さい場合、その宇宙自体も小さいと言います。命題を除いて（この章で後述）、与えられた宇宙内の型はより小さい宇宙内の型に対してのみ量化することができます。 {lean}`Sort 0` は命題の型であり、各 `Sort (u + 1)` はデータを記述する型です。 + +:::comment Every universe is an element of every strictly larger universe, so {lean}`Sort 5` includes {lean}`Sort 4`. This means that the following examples are accepted: +::: + +すべての宇宙はすべての狭義に大きな宇宙の要素なので、 {lean}`Sort 5` は {lean}`Sort 4` を含みます。つまり、以下の例が認められます： + ```lean example : Sort 5 := Sort 4 example : Sort 2 := Sort 1 ``` +:::comment On the other hand, {lean}`Sort 3` is not an element of {lean}`Sort 5`: +::: + +一方で、 {lean}`Sort 3` は {lean}`Sort 5` の要素ではありません： + ```lean (error := true) (name := sort3) example : Sort 5 := Sort 3 ``` @@ -199,7 +356,12 @@ but is expected to have type Type 4 : Type 5 ``` +:::comment Similarly, because {lean}`Unit` is in {lean}`Sort 1`, it is not in {lean}`Sort 2`: +::: + +同様に、 {lean}`Unit` は {lean}`Sort 1` に存在するため、 {lean}`Sort 2` には存在しません： + ```lean example : Sort 1 := Unit ``` @@ -216,46 +378,92 @@ but is expected to have type Type 1 : Type 2 ``` +:::comment Because propositions and data are used differently and are governed by different rules, the abbreviations {lean}`Type` and {lean}`Prop` are provided to make the distinction more convenient. {index}[`Type`] {index}[`Prop`] `Type u` is an abbreviation for `Sort (u + 1)`, so {lean}`Type 0` is {lean}`Sort 1` and {lean}`Type 3` is {lean}`Sort 4`. {lean}`Type 0` can also be abbreviated {lean}`Type`, so `Unit : Type` and `Type : Type 1`. {lean}`Prop` is an abbreviation for {lean}`Sort 0`. +::: + +命題とデータは異なる使われ方をし、異なる規則に支配されるため、より便利に区別するために {lean}`Type` と {lean}`Prop` という省略形が用意されています。 {index}[`Type`] {index}[`Prop`] `Type u` は `Sort (u + 1)` の省略形であるため、 {lean}`Type 0` は {lean}`Sort 1` で {lean}`Type 3` は {lean}`Sort 4` です。 {lean}`Type 0` は {lean}`Type` と省略することもできるため、 `Unit : Type` および `Type : Type 1` です。 {lean}`Prop` は {lean}`Sort 0` の省略形です。 + ### Predicativity +:::comment Each universe contains dependent function types, which additionally represent universal quantification and implication. A function type's universe is determined by the universes of its argument and return types. The specific rules depend on whether the return type of the function is a proposition. +::: + +各宇宙は依存関数型を含んでおり、それはさらに全称量化子と含意を表します。関数型の宇宙は、引数の型と戻り値の型の宇宙によって決定されます。具体的な規則は、関数の戻り値が命題かどうかに依存します。 + +:::comment Predicates, which are functions that return propositions (that is, where the result type of the function is some type in `Prop`) may have argument types in any universe whatsoever, but the function type itself remains in `Prop`. In other words, propositions feature {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions (and all other types). -:::Manual.example "Impredicativity" +::: + +命題を返す関数である述語（つまり、関数の結果の型が `Prop` にある型である場合）は引数の型がどのような宇宙に会っても構いませんが、関数の型自体は `Prop` に留まります。言い換えると、命題は {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] な量化子を特徴づけます。というのも、命題はそれ自体、すべての命題（および他のすべての命題）についての文になりうるからです。 + +::::Manual.example "Impredicativity" +:::comment Proof irrelevance can be written as a proposition that quantifies over all propositions: +::: + +証明の irrelevance はすべての命題を量化する命題として書くことができます： + ```lean example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2 ``` +:::comment A proposition may also quantify over all types, at any given level: +::: + +命題はまた任意のレベルにおいてすべての型を量化することもできます： + ```lean example : Prop := ∀ (α : Type), ∀ (x : α), x = x example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x ``` -::: +:::: +:::comment For universes at {tech key:="universe level"}[level] `1` and higher (that is, the `Type u` hierarchy), quantification is {deftech}[_predicative_]. {index}[predicative]{index subterm := "predicative"}[quantification] For these universes, the universe of a function type is the least upper bound of the argument and return types' universes. -:::Manual.example "Universe levels of function types" +::: + +{tech key:="universe level"}[レベル] `1` 以上の宇宙（つまり、`Type u` の階層）では、量化子は {deftech}[_predicative_] です。 {index}[predicative]{index subterm := "predicative"}[quantification] これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。 + +:::comment +::Manual.example "Universe levels of function types" +::: +::::Manual.example "関数型の宇宙レベル" +:::comment Both of these types are in {lean}`Type 2`: +::: + +これらの型はどちらも {lean}`Type 2` に存在します： + ```lean example (α : Type 1) (β : Type 2) : Type 2 := α → β example (α : Type 2) (β : Type 1) : Type 2 := α → β ``` -::: +:::: -:::Manual.example "Predicativity of {lean}`Type`" +:::comment +::Manual.example "Predicativity of {lean}`Type`" +::: +::::Manual.example "{lean}`Type` の Predicativity" +:::comment This example is not accepted, because `α`'s level is greater than `1`. In other words, the annotated universe is smaller than the function type's universe: +::: + +`α` のレベルは `1` より大きいため、この例は許可されません。言い換えると、注釈された宇宙は実際の関数型の宇宙よりも小さいです： + ```lean error := true name:=toosmall example (α : Type 2) (β : Type 1) : Type 1 := α → β ``` @@ -267,13 +475,26 @@ has type but is expected to have type Type 1 : Type 2 ``` -::: +:::: +:::comment Lean's universes are not {deftech}[cumulative];{index}[cumulativity] a type in `Type u` is not automatically also in `Type (u + 1)`. Each type inhabits precisely one universe. -:::Manual.example "No cumulativity" +::: + +Lean の宇宙は {deftech}[cumulative] ではありません； {index}[cumulativity] これは `Type u` の型が自動的に `Type (u + 1)` にも存在するようにならないことを意味します。 + +:::comment +::Manual.example "No cumulativity" +::: +::::Manual.example "cumulativity ではない" +:::comment This example is not accepted because the annotated universe is larger than the function type's universe: +::: + +この例は注釈された宇宙が関数型の宇宙よりも大きいため、許可されません： + ```lean error := true name:=toobig example (α : Type 2) (β : Type 1) : Type 3 := α → β ``` @@ -285,28 +506,59 @@ has type but is expected to have type Type 3 : Type 4 ``` -::: +:::: +:::comment ### Polymorphism +::: + +### 多相性（Polymorphism） + +:::comment Lean supports {deftech}_universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[universe parameters]. These parameters can then be instantiated with universe levels when the constant is used. Universe parameters are written in curly braces following a dot after a constant name. -:::Manual.example "Universe-polymorphic identity function" +::: + +Lean は {deftech}_宇宙多相_ {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] （universe polymorphism）をサポートしており、Lean 環境で定義された定数は {deftech}[宇宙パラメータ] を取ることができます。これらのパラメータは定数が使用されるときに宇宙レベルでインスタンス化されます。宇宙パラメータは定数名の後のドットに続く波括弧で記述します。 + +:::comment +::Manual.example "Universe-polymorphic identity function" +::: +::::Manual.example "宇宙多相恒等関数" +:::comment When fully explicit, the identity function takes a universe parameter `u`. Its signature is: +::: + +完全に明示的な場合、恒等関数は宇宙パラメータ `u` を取ります。このシグネチャは以下になります： + ```signature id.{u} {α : Sort u} (x : α) : α ``` -::: +:::: +:::comment Universe variables may additionally occur in {ref "level-expressions"}[universe level expressions], which provide specific universe levels in definitions. When the polymorphic definition is instantiated with concrete levels, these universe level expressions are also evaluated to yield concrete levels. -::::keepEnv -:::Manual.example "Universe level expressions" +::: + +宇宙変数はさらに、定義の中で特定の宇宙レベルを提供する {ref "level-expressions"}[宇宙レベル式] の中で現れるかもしれません。多相定義が具体的なレベルでインスタンス化されるとき、これらの宇宙レベル式も具体的なレベルをもたらすために評価されます。 +:::::keepEnv +:::comment +::Manual.example "Universe level expressions" +::: +::::Manual.example "宇宙レベル式" + +:::comment In this example, {lean}`Codec` is in a universe that is one greater than the universe of the type it contains: +::: + +この例では、 {lean}`Codec` はそれが含む型の宇宙より1つ大きい宇宙に存在します： + ```lean structure Codec.{u} : Type (u + 1) where type : Type u @@ -314,8 +566,13 @@ structure Codec.{u} : Type (u + 1) where decode : Array UInt32 → Nat → Option (type × Nat) ``` +:::comment Lean automatically infers most level parameters. In the following example, it is not necessary to annotate the type as {lean}`Codec.{0}`, because {lean}`Char`'s type is {lean}`Type 0`, so `u` must be `0`: +::: + +Lean はほとんどのレベルパラメータを自動的に推論します。以下の例では、 {lean}`Char` の型は {lean}`Type 0` であるため、`u` は `0` でなければならないことから、 {lean}`Codec.{0}` と注釈する必要はありません。 + ```lean (keep := true) def Codec.char : Codec where type := Char @@ -328,15 +585,28 @@ def Codec.char : Codec where else failure ``` -::: :::: +::::: +:::comment Universe-polymorphic definitions in fact create a _schematic definition_ that can be instantiated at a variety of levels, and different instantiations of universes create incompatible values. -:::Manual.example "Universe polymorhism is not first-class" +::: + +宇宙多相な定義は、実際には様々なレベルでインスタンス可能な _スキーマ的定義_ （schematic definition）を作り出し、宇宙レベルの異なるインスタンス化は互換性のない値を作ります。 + +:::comment +::Manual.example "Universe polymorhism is not first-class" +::: +::::Manual.example "宇宙多相は第一級ではない" +:::comment This can be seen in the following example, in which `T` is a gratuitously-universe-polymorphic definition that always returns the constructor of the unit type. Both instantiations of `T` have the same value, and both have the same type, but their differing universe instantiations make them incompatible: +::: + +これは次の例で見ることができます。 `T` は不要な宇宙多相定義で、常にユニット型のコンストラクタを返します。`T` のインスタンスはどれも同じ値を持ち、また同じ型を持ちますが、宇宙のインスタンス化が異なるため互換性がありません： + ```lean (error := true) (name := uniIncomp) (keep := false) abbrev T.{u} : Unit := (fun (α : Sort u) => ()) PUnit.{u} @@ -359,20 +629,38 @@ abbrev T : Unit := (fun (α : Type) => ()) Unit def test : T = T := rfl ``` -::: +:::: +:::comment Auto-bound implicit arguments are as universe-polymorphic as possible. Defining the identity function as follows: +::: + +自動的に束縛される暗黙の引数は可能な限り宇宙多相となります。恒等関数を次のように定義します： + ```lean def id' (x : α) := x ``` +:::comment results in the signature: +::: + +これは以下のシグネチャになります： + ```signature id'.{u} {α : Sort u} (x : α) : α ``` -:::Manual.example "Universe monomorphism in auto-bound implicit" +:::comment +::Manual.example "Universe monomorphism in auto-bound implicit" +::: +::::Manual.example "自動的に束縛された宇宙のモノ射" +:::comment On the other hand, because {name}`Nat` is in universe {lean}`Type 0`, this function automatically ends up with a concrete universe level for `α`, because `m` is applied to both {name}`Nat` and `α`, so both must have the same type and thus be in the same universe: +::: + +一方、 {name}`Nat` は {lean}`Type 0` に存在するため、この関数は自動的に `α` の具体的な宇宙レベルを求めます。`m` は {name}`Nat` と `α` の両方に適用されるため、どちらも同じ型を持たなければならず、結果として同じ宇宙となります： + ```lean partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do if p (← act) then @@ -392,16 +680,25 @@ info: count.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → Bool #guard_msgs in #check count ``` -::: +:::: +:::comment #### Level Expressions +::: +#### レベル式（Level Expressions） %%% tag := "level-expressions" %%% +:::comment Levels that occur in a definition are not restricted to just variables and addition of constants. More complex relationships between universes can be defined using level expressions. +::: + +定義に現れるレベルは変数と定数の和だけに限定されません。より複雑な宇宙間の関係もレベルの表現を使って定義できます。 + +:::comment ```` Level ::= 0 | 1 | 2 | ... -- Concrete levels | u, v -- Variables @@ -409,26 +706,62 @@ Level ::= 0 | 1 | 2 | ... -- Concrete levels | max Level Level -- Least upper bound | imax Level Level -- Impredicative LUB ```` +::: +```` +Level ::= 0 | 1 | 2 | ... -- 具体的なレベル + | u, v -- 変数 + | Level + n -- 定数の和 + | max Level Level -- 最小上界 + | imax Level Level -- Impredicative な最小上界 +```` +:::comment Given an assignment of level variables to concrete numbers, evaluating these expressions follows the usual rules of arithmetic. The `imax` operation is defined as follows: +::: + +レベル変数が具体的な数値に割り当てられている場合、これらの式の評価は通常の算術の規則に従います。`imax` 演算は以下のように定義されます： + $$``\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}`` +:::comment `imax` is used to implement {tech}[impredicative] quantification for {lean}`Prop`. In particular, if `A : Sort u` and `B : Sort v`, then `(x : A) → B : Sort (imax u v)`. If `B : Prop`, then the function type is itself a {lean}`Prop`; otherwise, the function type's level is the maximum of `u` and `v`. +::: + +`imax` は {lean}`Prop` の {tech}[impredicative] な量化子を実装するために使用されます。特に、`A : Sort u` かつ `B : Sort v` である場合、`(x : A) → B : Sort (imax u v)` となります。もし `B : Prop` ならば、その関数型は {lean}`Prop` であり、それ以外ではその関数型のレベルは `u` と `v` の最大値になります。 + +:::comment #### Universe Variable Bindings +::: + +### 宇宙変数の束縛（Universe Variable Bindings） + +:::comment Universe-polymorphic definitions bind universe variables. These bindings may be either explicit or implicit. Explicit universe variable binding and instantiation occurs as a suffix to the definition's name. Universe parameters are defined or provided by suffixing the name of a constant with a period (`.`) followed by a comma-separated sequence of universe variables between curly braces. -::::keepEnv -:::Manual.example "Universe-polymorphic `map`" +::: + +宇宙多相定義は宇宙変数を束縛します。これらの束縛は明示的・暗黙的のどちらも可能です。明示的な宇宙変数の束縛とインスタンス化は定義の名前の接尾辞として行われます。宇宙パラメータは定数名にピリオド（`.`）を接尾辞として付け、その後に波括弧の間にカンマで区切られた一連の宇宙変数を付けることで定義・提供されます。 + +:::::keepEnv +:::comment +::Manual.example "Universe-polymorphic `map`" +::: +::::Manual.example "宇宙多相な `map`" +:::comment The following declaration of {lean}`map` declares two universe parameters (`u` and `v`) and instantiates the polymorphic {name}`List` with each in turn: +::: + +以下{lean}`map` の宣言では、2つの宇宙パラメータ（`u` と `v`）を宣言し、多相型の {name}`List` を順番にインスタンス化しています： + ```lean def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : @@ -436,15 +769,28 @@ def map.{u, v} {α : Type u} {β : Type v} | [] => [] | x :: xs => f x :: map f xs ``` -::: :::: +::::: +:::comment Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters. When the {TODO}[describe this option and add xref] `autoImplicit` option is set to {lean}`true` (the default), it is not necessary to explicitly bind universe variables. When it is set to {lean}`false`, then they must be added explicitly or declared using the `universe` command. {TODO}[xref] -:::Manual.example "Auto-implicits and universe polymorphism" +::: + +Lean が暗黙のパラメータを自動的にインスタンス化するように、宇宙パラメータも自動的にインスタンス化されます。`autoImplicit` オプションが {lean}`true` に設定されている場合（これがデフォルトです）、宇宙変数を明示的に束縛する必要はありません。 {lean}`false` に設定すると、明示的に追加するか `universe` コマンドを使って宣言する必要があります。 + +:::comment +::Manual.example "Auto-implicits and universe polymorphism" +::: +::::Manual.example "自動的な暗黙さと宇宙多相" +:::comment When `autoImplicit` is {lean}`true` (which is the default setting), this definition is accepted even though it does not bind its universe parameters: +::: + +`autoImplicit` が {lean}`true` （デフォルト値）の場合、この定義は宇宙パラメータを束縛していなくても許可されます： + ```lean (keep := false) set_option autoImplicit true def map {α : Type u} {β : Type v} (f : α → β) : List α → List β @@ -452,7 +798,12 @@ def map {α : Type u} {β : Type v} (f : α → β) : List α → List β | x :: xs => f x :: map f xs ``` +:::comment When `autoImplicit` is {lean}`false`, the definition is rejected because `u` and `v` are not in scope: +::: + +`autoImplicit` が {lean}`false` の場合、`u` と `v` がスコープにないためこの定義は却下されます： + ```lean (error := true) (name := uv) set_option autoImplicit false def map {α : Type u} {β : Type v} (f : α → β) : List α → List β @@ -465,21 +816,39 @@ unknown universe level 'u' ```leanOutput uv unknown universe level 'v' ``` -::: +:::: +:::comment In addition to using `autoImplicit`, particular identifiers can be declared as universe variables in a particular {tech}[scope] using the `universe` command. -:::syntax Lean.Parser.Command.universe +::: + +`autoImplicit` を使うことに加えて、`universe` コマンドを使って特定の識別子を特定の {tech}[scope] 内の宇宙変数として宣言することができます。 + +::::syntax Lean.Parser.Command.universe ```grammar universe $x:ident $xs:ident* ``` +:::comment Declares one or more universe variables for the extent of the current scope. +::: + +現在のスコープの範囲において1つ以上の宇宙変数を宣言します。 + +:::comment Just as the `variable` command causes a particular identifier to be treated as a parameter with a particular type, the `universe` command causes the subsequent identifiers to be implicitly quantified as as universe parameters in declarations that mention them, even if the option `autoImplicit` is {lean}`false`. ::: -:::Manual.example "The `universe` command when `autoImplicit` is `false`" +`variable` コマンドが特定の識別子を特定の型のパラメータとして扱うように、`universe` コマンドは `autoImplicit` オプションが {lean}`false` であっても、それに続く識別子を宇宙パラメータとして暗黙的に量化します。 + +:::: + +:::comment +::Manual.example "The `universe` command when `autoImplicit` is `false`" +::: +:::Manual.example "`autoImplicit` が `false` の際の `universe` コマンド" ```lean (keep := false) set_option autoImplicit false universe u @@ -487,15 +856,33 @@ def id₃ (α : Type u) (a : α) := a ``` ::: +:::comment Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with `universe` even when `autoImplicit` is `true`. -:::Manual.example "Automatic universe parameters and the `universe` command" +::: + +自動的な暗黙の引数は宣言の {tech}[ヘッダ] で使用されるパラメータのみを挿入するため、定義の右側にのみ現れる宇宙変数は `autoImplicit` が `true` の場合でも `universe` で宣言されていない限り引数として挿入されません。 + +:::comment +::Manual.example "Automatic universe parameters and the `universe` command" +::: +::::Manual.example "自動的な宇宙パラメータと `universe` コマンド" +:::comment This definition with an explicit universe parameter is accepted: +::: + +明示的な宇宙パラメータを伴ったこの定義は許可されます： + ```lean (keep := false) def L.{u} := List (Type u) ``` +:::comment Even with automatic implicits, this definition is rejected, because `u` is not mentioned in the header, which precedes the `:=`: +::: + +`u` が `:=` の前にあるヘッダで言及されていないため、自動的な暗黙でもこの定義は却下されます： + ```lean (error := true) (name := unknownUni) (keep := false) set_option autoImplicit true def L := List (Type u) @@ -503,20 +890,35 @@ def L := List (Type u) ```leanOutput unknownUni unknown universe level 'u' ``` +:::comment With a universe declaration, `u` is accepted as a parameter even on the right-hand side: +::: + +宇宙宣言では、`u` は右辺でもパラメータとして許可されます： + ```lean (keep := false) universe u def L := List (Type u) ``` +:::comment The resulting definition of `L` is universe-polymorphic, with `u` inserted as a universe parameter. +::: + +その結果、`L` の定義は宇宙パラメータとして `u` が挿入された宇宙多相となります。 + +:::comment Declarations in the scope of a `universe` command are not made polymorphic if the universe variables do not occur in them or in other automatically-inserted arguments. +::: + +`universe` コマンドのスコープにある宣言は、その中に宇宙変数が無い場合、または自動的に挿入される他の引数の中に宇宙変数が無い場合、多相にはなりません。 + ```lean universe u def L := List (Type 0) #check L ``` -::: +:::: #### Universe Unification @@ -539,37 +941,72 @@ tag := "quotients" * Show the computation rule ::: +:::comment # Module Contents +::: + +# モジュールの内容（Module Contents） + +:::comment As described {ref "module-structure"}[in the section on the syntax of files], a Lean module consists of a header followed by a sequence of commands. +::: + +{ref "module-structure"}[ファイルの構文に関する節] で説明したように、Lean のモジュールはヘッダとそれに続く一連のコマンドで構成されます。 + +:::comment ## Commands and Declarations +::: + +## コマンドと宣言（Commands and Declaration） + +:::comment After the header, every top-level phrase of a Lean module is a command. Commands may add new types, define new constants, or query Lean for information. Commands may even {ref "language-extension"}[change the syntax used to parse subsequent commands]. +::: + +ヘッダの後にある、Lean モジュールのトップレベルのフレーズはすべてコマンドです。コマンドは新しい型を追加したり、新しい定数を定義したり、Lean に情報を問い合わせたりします。コマンドは {ref "language-extension"}[後続のコマンドをパースするために使用される構文を変更する] ことさえもできます。 + ::: planned 100 * Describe the various families of available commands (definition-like, `#eval`-like, etc). * Refer to specific chapters that describe major commands, such as `inductive`. ::: +:::comment ### Definition-Like Commands +::: + +### 定義に類するコマンド（Definition-Like Commands） + ::: planned 101 * Precise descriptions of these commands and their syntax * Comparison of each kind of definition-like command to the others ::: +:::comment The following commands in Lean are definition-like: {TODO}[Render commands as their name (a la tactic index)] +::: + +以下の Lean のコマンドは定義に類するものです： + * {syntaxKind}`def` * {syntaxKind}`abbrev` * {syntaxKind}`example` * {syntaxKind}`theorem` -All of these commands cause Lean to {tech key:="エラボレータ"}[elaborate]elaborator a term based on a signature. +:::comment +All of these commands cause Lean to {tech key:="elaborator"}[elaborate] a term based on a signature. With the exception of {syntaxKind}`example`, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment. +::: + +これらのコマンドはすべて Lean によってシグネチャに応じた項へ {tech key:="エラボレータ"}[エラボレート] されます。結果を破棄する {syntaxKind}`example` を除き、Lean のコア言語での結果の式は将来の環境で使用するために保存されます。 + :::syntax Lean.Parser.Command.declaration ```grammar $_:declModifiers @@ -663,8 +1100,13 @@ example $_ $_ where ``` ::: +:::comment {deftech}_Opaque constants_ are defined constants that cannot be reduced to their definition. +::: + +{deftech}_不透明な定数_ はそれらの定義へ簡約されない定数を定義します。 + :::syntax Lean.Parser.Command.opaque ```grammar opaque $_ $_ @@ -714,10 +1156,20 @@ Describe signatures, including the following topics: ::: +:::comment ### Headers +::: + +### ヘッダ（Headers） + +:::comment The {deftech}[_header_] of a definition or declaration specifies the signature of the new constant that is defined. +::: + +定義または宣言の {deftech}[_ヘッダ_] （header）は定義される新しい定数のシグネチャを指定します。 + ::: TODO * Precision and examples; list all of them here * Mention interaction with autoimplicits diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean index 24e988d..2ab1895 100644 --- a/Manual/Language/Files.lean +++ b/Manual/Language/Files.lean @@ -13,7 +13,7 @@ open Verso.Genre Manual /- #doc (Manual) "Files" => -/ -#doc (Manual) "ファイル" => +#doc (Manual) "ファイル（Files）" => :::comment The smallest unit of compilation in Lean is a single {deftech}[module]. @@ -27,7 +27,7 @@ Lean におけるコンパイルの最小単位は1つの {deftech}[モジュー # Modules ::: -# モジュール +# モジュール（Modules） :::comment Every Lean file defines a module. @@ -45,7 +45,7 @@ Describe case sensitivity/preservation for filenames here ## Encoding and Representation ::: -## エンコードと表現 +## エンコードと表現（Encoding and Representation） :::comment Lean modules are Unicode text files encoded in UTF-8. {TODO}[Figure out the status of BOM and Lean] @@ -63,7 +63,7 @@ Marginal note: this is to make cached files and `#guard_msgs` and the like work ## Concrete Syntax ::: -## 具体的な構文 +## 具体的な構文（Concrete Syntax） :::comment Lean's concrete syntax is extensible. @@ -77,7 +77,7 @@ Lean の具体的な構文は拡張可能です。Lean のような言語では ### Whitespace ::: -### 空白 +### 空白（Whitespace） :::comment Tokens in Lean may be separated by any number of {deftech}[_whitespace_] character sequences. @@ -91,7 +91,7 @@ Lean における字句は {deftech}[_空白_] （whitespace）文字の列で ### Comments ::: -### コメント +### コメント（Comments） :::comment Comments are stretches of the file that, despite not being whitespace, are treated as such. @@ -124,7 +124,7 @@ Lean has two syntaxes for comments: ### Keywords and Identifiers ::: -### キーワードと識別子 +### キーワードと識別子（Keywords and Identifiers） :::comment An {deftech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier] @@ -231,7 +231,7 @@ Hierarchical identifiers are used to represent both module names and names in a ## Structure ::: -## 構造体 +## 構造体（Structure） %%% tag := "module-structure" %%% @@ -253,7 +253,7 @@ A module consists of a {deftech}_module header_ followed by a sequence of {defte ### Module Headers ::: -### モジュールヘッダ +### モジュールヘッダ（Module Headers） :::comment The module header consists of a sequence of {deftech}[`import` statements]. @@ -323,7 +323,7 @@ Lean searches its include path for the corresponding importable module file. ### Commands ::: -### コマンド +### コマンド（Commands） :::comment {tech}[Commands] are top-level statements in Lean. @@ -342,7 +342,7 @@ Make the index include links to all commands, then xref from here ## Contents ::: -## 内容 +## 内容（Contents） :::comment A module includes an {TODO}[def and xref] environment, which includes both the datatype and constant definitions from an environment and any data stored in {TODO}[xref] its environment extensions. @@ -357,7 +357,7 @@ This means that an imported module can be loaded without re-executing all of its # Packages, Libraries, and Targets ::: -# パッケージ・ライブラリ・ターゲット +# パッケージ・ライブラリ・ターゲット（Packages, Libraries, and Targets） :::comment Lean code is organized into {deftech}_packages_, which are units of code distribution. diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean index 9df9504..68fb905 100644 --- a/Manual/Language/Functions.lean +++ b/Manual/Language/Functions.lean @@ -13,7 +13,7 @@ open Verso.Genre Manual /- #doc (Manual) "Functions" => -/ -#doc (Manual) "関数" => +#doc (Manual) "関数（Functions）" => :::comment Function types are a built-in feature of Lean. @@ -188,7 +188,7 @@ i : Nat ::: -# 関数 +# 関数（Functions） :::comment Terms with function types can be created via abstractions, introduced with the {keywordOf Lean.Parser.Term.fun}`fun` keyword. @@ -238,7 +238,7 @@ However, not all functions originate from abstractions: {tech}[type constructors ::: -# カリー化 +# カリー化（Currying） :::comment In Lean's core type theory, every function maps each element of the domain to a single element of the range. @@ -300,7 +300,7 @@ These are equivalent to writing nested {keywordOf Lean.Parser.Term.fun}`fun` ter ::: -# 暗黙の関数 +# 暗黙の関数（Implicit Functions） :::comment Lean supports implicit parameters to functions. @@ -323,7 +323,7 @@ Lean は関数への暗黙のパラメータをサポートしています。こ : 通常の暗黙のパラメータ - 通常の暗黙のパラメータとは、Lean が単一化によって値を決定すべき関数パラメータのことです。言い換えると、各呼び出し部位は、関数呼び出し全体が適切に型付けされるような潜在的な引数の値を1つだけ持つべきです。Lean のエラボレータは関数の各呼び出しですべての暗黙引数の値を見つけようとします。通常の暗黙の引数は波括弧（`{` と `}`）で囲んで記述します。 + 通常の暗黙のパラメータとは、Lean が単一化によって値を決定すべき関数パラメータのことです。言い換えると、各呼び出し部位は、関数呼び出し全体が well-typed であるような潜在的な引数の値を1つだけ持つべきです。Lean のエラボレータは関数の各呼び出しですべての暗黙引数の値を見つけようとします。通常の暗黙の引数は波括弧（`{` と `}`）で囲んで記述します。 :::comment : Strict implicit parameters @@ -501,7 +501,7 @@ example : (⦃x : Nat⦄ → Nat) = (Nat → Nat) := rfl ::: -# パターンマッチ +# パターンマッチ（Pattern Matching） ::::syntax term :::comment @@ -606,7 +606,7 @@ fun n => ::: -# 外延性 +# 外延性（Extensionality） :::comment Definitional equality of functions in Lean is {deftech}_intensional_. @@ -615,7 +615,7 @@ To a first approximation, this means that two functions are definitionally equal ::: -Lean における関数の定義上の等価性は {deftech}_内包的_ （intensional）です。つまり、この定義上の等価性は、束縛変数のリネームと {tech}[reduction] によって _構文上_ （syntactically）で定義されます。大まかに言えば、これは2つの関数が同じアルゴリズムを実装していれば定義上等しいということを意味し、定義域の等しい要素を値域の等しい要素にマッピングしていれば等しいという通常の数学的な等値性の概念とは異なります。 +Lean における関数の定義上の等価性は {deftech}_内包的_ （intensional）です。つまり、この定義上の等価性は、束縛変数のリネームと {tech}[簡約] によって _構文上_ （syntactically）で定義されます。大まかに言えば、これは2つの関数が同じアルゴリズムを実装していれば定義上等しいということを意味し、定義域の等しい要素を値域の等しい要素にマッピングしていれば等しいという通常の数学的な等値性の概念とは異なります。 :::comment Intensional equality is mechanically decidable; Lean's type checker can decide whether two functions are intensionally equal. @@ -623,7 +623,7 @@ Extensional equality is not decidable, so it is instead made available as reason ::: -Lean の型チェッカは2つの関数が内包的に等しいかどうかを判断できます。外延的な等価性は決定できないため、代わりに2つの関数が等しいという {tech}[proposition] を証明する時に推論原理として利用できるようにします。 +Lean の型チェッカは2つの関数が内包的に等しいかどうかを判断できます。外延的な等価性は決定できないため、代わりに2つの関数が等しいという {tech}[命題] を証明する時に推論原理として利用できるようにします。 ::::keepEnv ```lean (show := false) @@ -658,7 +658,7 @@ When reasoning about functions, the theorem {lean}`funext`{margin}[Unlike some i ::: -# 全域性と停止 +# 全域性と停止（Totality and Termination） :::comment Functions can be defined recursively using {keywordOf Lean.Parser.Command.declaration}`def`. diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index ec9e53a..495804c 100644 --- a/Manual/Language/InductiveTypes.lean +++ b/Manual/Language/InductiveTypes.lean @@ -30,7 +30,7 @@ Inductive types may have any number of constructors; these constructors introduc ::: -{deftech}_帰納型_ （inductive type）は Lean に新しい型を導入する主な手段です。 {tech}[universes] と {tech}[関数] は組み込みのプリミティブでユーザが追加することはできませんが、Lean の他のすべての型は帰納型であるか、宇宙・関数・帰納型によって定義されたものであるかのどちらかです。帰納型は {deftech}_型コンストラクタ_ （type constructor）{index}[type constructor] と {deftech}_コンストラクタ_ （constructor） {index}[constructor] によって指定されます；帰納型の性質はこれらから導かれます。各帰納型は1つの型コンストラクタを持ち、 {tech}[universe parameters] と通常のパラメータの両方を取ることができます。帰納型は任意の数のコンストラクタを持つことができます；これらのコンストラクタは帰納型の型コンストラクタによって型が導かれる新しい値を導入します。 +{deftech}_帰納型_ （inductive type）は Lean に新しい型を導入する主な手段です。 {tech}[宇宙] と {tech}[関数] は組み込みのプリミティブでユーザが追加することはできませんが、Lean の他のすべての型は帰納型であるか、宇宙・関数・帰納型によって定義されたものであるかのどちらかです。帰納型は {deftech}_型コンストラクタ_ （type constructor）{index}[type constructor] と {deftech}_コンストラクタ_ （constructor） {index}[constructor] によって指定されます；帰納型の性質はこれらから導かれます。各帰納型は1つの型コンストラクタを持ち、 {tech}[宇宙パラメータ] と通常のパラメータの両方を取ることができます。帰納型は任意の数のコンストラクタを持つことができます；これらのコンストラクタは帰納型の型コンストラクタによって型が導かれる新しい値を導入します。 :::comment Based on the type constructor and the constructors for an inductive type, Lean derives a {deftech}_recursor_{index}[recursor]{see "recursor"}[eliminator]. @@ -41,7 +41,7 @@ Lean additionally produces a number of helper constructions based on the recurso ::: -帰納型の型コンストラクタとコンストラクタに基づいて、Lean は {deftech}_再帰子_{index}[recursor]{see "recursor"}[eliminator] （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上はプリミティブな再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに、システムの他の場所でも使用される再帰子 {margin}[_再帰子_ という用語は再帰的でないデータ型でも常に使用されます。] に基づいた数多くの補助的な構成を提供しています。 +帰納型の型コンストラクタとコンストラクタに基づいて、Lean は {deftech}_再帰子_{index}[recursor]{see "recursor"}[eliminator] （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上は原始再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに、システムの他の場所でも使用される再帰子 {margin}[_再帰子_ という用語は再帰的でないデータ型でも常に使用されます。] に基づいた数多くの補助的な構成を提供しています。 :::comment _Structures_ are a special case of inductive types that have exactly one constructor. @@ -100,7 +100,7 @@ In some situations, this process may fail to find a minimal universe or fail to ::: -宣言の最初の行にて、 {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`inductive` から {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where` までは新しい {tech}[型コンストラクタ] の名前と型を指定しています。型コンストラクタの型シグネチャが提供されている場合、その結果の型は {tech}[universe] でなければなりませんが、パラメータは型である必要はありません。シグネチャが提供されない場合、Lean は結果の型を含むのに十分な大きさの宇宙を推論しようとします。状況によってはこのプロセスは最小の宇宙を見つけることができなかったり、全く見つけることができなかったりすることがあり、その場合は注釈が必要です。 +宣言の最初の行にて、 {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`inductive` から {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where` までは新しい {tech}[型コンストラクタ] の名前と型を指定しています。型コンストラクタの型シグネチャが提供されている場合、その結果の型は {tech}[宇宙] でなければなりませんが、パラメータは型である必要はありません。シグネチャが提供されない場合、Lean は結果の型を含むのに十分な大きさの宇宙を推論しようとします。状況によってはこのプロセスは最小の宇宙を見つけることができなかったり、全く見つけることができなかったりすることがあり、その場合は注釈が必要です。 :::comment The constructor specifications follow {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`. @@ -199,7 +199,7 @@ Empty datatypes are not useless; they can be used to indicate unreachable code. {lean}`No` is a false {tech}[proposition], equivalent to Lean's {lean}`False`: ::: -{lean}`No` は偽の {tech}[proposition] であり、Lean の {lean}`False` と同値です： +{lean}`No` は偽の {tech}[命題] であり、Lean の {lean}`False` と同値です： ```lean inductive No : Prop where @@ -1219,7 +1219,7 @@ The actual dependency structure between the types is not taken into account; eve ::: -相互帰納型には、非相互に定義された帰納型と同様に、プリミティブな再帰子が用意されています。これらの再帰子は、グループ内の他の型を処理しなければならないことを考慮し、それぞれの帰納型に対して動機を持つことになります。`mutual` グループ内のすべての帰納型は同一のパラメータを持つ必要があるため、再帰子はパラメータを最初に受け取り、動機と再帰子の残りの部分を抽象化します。さらに、再帰子はグループの他の型を処理する必要があるため、グループ内の各型コンストラクタについてのケースが必要になります。型の間の実施あの依存構造は考慮されません；相互依存関係が少ないことで追加の動機またはコンストラクタのケースが実際には必要ない場合でも、生成された再帰子はそれらを必要とします。 +相互帰納型には、非相互に定義された帰納型と同様に、原始再帰子が用意されています。これらの再帰子は、グループ内の他の型を処理しなければならないことを考慮し、それぞれの帰納型に対して動機を持つことになります。`mutual` グループ内のすべての帰納型は同一のパラメータを持つ必要があるため、再帰子はパラメータを最初に受け取り、動機と再帰子の残りの部分を抽象化します。さらに、再帰子はグループの他の型を処理する必要があるため、グループ内の各型コンストラクタについてのケースが必要になります。型の間の実施あの依存構造は考慮されません；相互依存関係が少ないことで追加の動機またはコンストラクタのケースが実際には必要ない場合でも、生成された再帰子はそれらを必要とします。 :::comment :: example "Even and odd" diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean index 074ba0c..da8ebe1 100644 --- a/Manual/Language/InductiveTypes/LogicalModel.lean +++ b/Manual/Language/InductiveTypes/LogicalModel.lean @@ -16,14 +16,14 @@ set_option maxRecDepth 800 /- #doc (Manual) "Logical Model" => -/ -#doc (Manual) "論理 モデル" => +#doc (Manual) "論理モデル（Logical Model）" => :::comment # Recursors ::: -# 再帰子 +# 再帰子（Recursors） :::comment Every inductive type is equipped with a {tech}[recursors]. @@ -39,7 +39,7 @@ Recursors have function types, but they are primitive and are not definable usin ::: -## 再帰子の型 +## 再帰子の型（Recursor Types） :::comment The recursor takes the following parameters: @@ -244,7 +244,7 @@ The cases for non-recursive constructors are the base cases, and the additional ### Subsingleton Elimination ::: -### Subsingleton 除去 +### Subsingleton 除去（Subsingleton Elimination） %%% tag := "subsingleton-elimination" @@ -394,7 +394,7 @@ This means that proofs of equality can be used to rewrite the types of non-propo ::: -## 簡約 +## 簡約（Reduction） :::comment In addition to adding new constants to the logic, inductive datatype declarations also add new reduction rules. @@ -417,7 +417,7 @@ If there are recursive parameters, then these arguments to the case are found by # Well-Formedness Requirements ::: -# 適格要件 +# 適格要件（Well-Formedness Requirements） %%% @@ -438,7 +438,7 @@ They are conservative: there exist potential inductive types that do not undermi ::: -## 宇宙レベル +## 宇宙レベル（Universe Levels） :::comment Type constructors of inductive types must either inhabit a {tech}[universe] or a function type whose return type is a universe. @@ -450,7 +450,7 @@ If the universe is not {lean}`Prop`, then the following must hold for each param ::: -帰納型の型コンストラクタは {tech}[universe] か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が {lean}`Prop` であれば、 {lean}`Prop` は {tech}[impredicative] であるため宇宙にはそれ以上の制限はありません。もし宇宙が {lean}`Prop` でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります： +帰納型の型コンストラクタは {tech}[宇宙] か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が {lean}`Prop` であれば、 {lean}`Prop` は {tech}[impredicative] であるため宇宙にはそれ以上の制限はありません。もし宇宙が {lean}`Prop` でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります： * コンストラクタのパラメータが（パラメータか添字かの意味で）帰納型のパラメータである場合、このパラメータの型は型コンストラクタの宇宙より大きくはできません。 * その他のすべてのコンストラクタのパラメータは型コンストラクタの宇宙より小さくなければなりません。 @@ -630,7 +630,7 @@ invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), # Constructions for Termination Checking ::: -# 停止性チェックのための構成 +# 停止性チェックのための構成（Constructions for Termination Checking） %%% tag := "recursor-elaboration-helpers" @@ -651,8 +651,8 @@ First, the equation compiler (which translates recursive functions with pattern Lean のコア型理論が帰納型に対して規定している型コンストラクタ・コンストラクタ・再帰子に加えて、Lean は多くの補助構成を構築しています。まず、等式のコンパイラ（パターンマッチによる再帰関数を再帰子の適用に変換する）はこれらの追加のコンストラクタを使用します： * `recOn` は各コンストラクタのケースよりもターゲットが優先される再帰子のバージョンです。 - * `casesOn` は再帰子のバージョンであり、ターゲットが各コンストラクタのケースより前にあり、再帰的な引数は帰納法の仮定を生成しません。これはプリミティブな再帰ではなく、ケース分析を表現しています。 - * `below` はある動機に対して、ターゲットの部分木である帰納型の _すべての_ 住人がその動機を満たすことを表現する型を計算します。これは、帰納法やプリミティブな再帰の動機を強再帰や強帰納法の動機に変換します。 + * `casesOn` は再帰子のバージョンであり、ターゲットが各コンストラクタのケースより前にあり、再帰的な引数は帰納法の仮定を生成しません。これは原始再帰ではなく、ケース分析を表現しています。 + * `below` はある動機に対して、ターゲットの部分木である帰納型の _すべての_ 住人がその動機を満たすことを表現する型を計算します。これは、帰納法や原始再帰の動機を強再帰や強帰納法の動機に変換します。 * `brecOn` は `below` を使用して、直前の再帰パラメータだけでなく、すべての部分木へのアクセスを提供する再帰子のバージョンです。これは強帰納法を表現しています。 * `noConfusion` は一般的な文であり、そこからコンストラクタの単射性と不連結性を導き出すことができます。 * `noConfusionType` は `noConfusion` に対して用いられ、2つのコンストラクタが等しい場合どうなるかを決定する動機です。別々のコンストラクタの場合、これは {lean}`False` です；両方のコンストラクタが同じであれば、それぞれのパラメータが等しいという結果になります。 diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean index a3973d1..898beb1 100644 --- a/Manual/Language/InductiveTypes/Structures.lean +++ b/Manual/Language/InductiveTypes/Structures.lean @@ -15,7 +15,7 @@ open Lean.Parser.Command («inductive» «structure» declValEqns computedField) /- #doc (Manual) "Structure Declarations" => -/ -#doc (Manual) "構造体 宣言" => +#doc (Manual) "構造体宣言（Structure Declarations）" => ::::syntax command ```grammar @@ -57,7 +57,7 @@ structure RecStruct where ::: -# 構造体のパラメータ +# 構造体のパラメータ（Structure Parameters） :::comment Just like ordinary inductive type declarations, the header of the structure declaration contains a signature that may specify both parameters and a resulting universe. @@ -72,7 +72,7 @@ Structures may not define {tech}[indexed families]. ::: -# フィールド +# フィールド（Fields） :::comment Each field of a structure declaration corresponds to a parameter of the constructor. @@ -80,7 +80,7 @@ Auto-implicit arguments are inserted in each field separately, even if their nam ::: -構造体宣言の各フィールドは、コンストラクタのパラメータに対応します。自動的な暗黙引数はたとえ名前が一致していても各フィールドに別々に挿入され、フィールドは型を定量化するコンストラクタのパラメータになります。 +構造体宣言の各フィールドは、コンストラクタのパラメータに対応します。自動的な暗黙引数はたとえ名前が一致していても各フィールドに別々に挿入され、フィールドは型を量化するコンストラクタのパラメータになります。 :::comment :: example "Auto-implicit parameters in structure fields" @@ -112,7 +112,7 @@ MyStructure.{u, v} : Type (max u v) The resulting type is in `Type` rather than `Sort` because the constructor fields quantify over types in `Sort`. In particular, both fields in its constructor {name}`MyStructure.mk` take an implicit type parameter: ::: -コンストラクタのフィールドは `Sort` の型に対して定量化されるため、結果の型は `Type` ではなく `Sort` になります。特に、コンストラクタ {name}`MyStructure.mk` の両方のフィールドは暗黙の型パラメータを取ります： +コンストラクタのフィールドは `Sort` の型に対して量化されるため、結果の型は `Type` ではなく `Sort` になります。特に、コンストラクタ {name}`MyStructure.mk` の両方のフィールドは暗黙の型パラメータを取ります： ```signature MyStructure.mk.{u, v} @@ -212,7 +212,7 @@ Fields are numbered beginning with `1`. ::: -# 構造体のコンストラクタ +# 構造体のコンストラクタ（Structure Constructors） :::comment Structure constructors may be explicitly named by providing the constructor name and `::` prior to the fields. @@ -487,7 +487,7 @@ def location : Float × Float where # Structure Inheritance ::: -# 構造体の継承 +# 構造体の継承（Structure Inheritance） %%% tag := "structure-inheritance" diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean index 2e32b26..e3884a5 100644 --- a/Manual/Tactics.lean +++ b/Manual/Tactics.lean @@ -28,7 +28,7 @@ tag := "tactics" %%% The tactic language is a special-purpose programming language for constructing proofs. -In Lean, {tech}[propositions] are represented by types, and proofs are terms that inhabit these types. +In Lean, {tech}[命題]propositions are represented by types, and proofs are terms that inhabit these types. {margin}[The {ref "propositions"}[section on propositions] describes propositions in more detail.] While terms are designed to make it convenient to indicate a specific inhabitant of a type, tactics are designed to make it convenient to demonstrate that a type is inhabited. This distinction exists because it's important that definitions pick out the precise objects of interest and that programs return the intended results, but proof irrelevance means that there's no _technical_ reason to prefer one proof term over another. @@ -340,7 +340,7 @@ Printing very large terms can lead to slowdowns or even stack overflows in tooli ## Metavariables Terms that begin with a question mark are _metavariables_ that correspond to an unknown value. -They may stand for either {tech}[universe] levels or for terms. +They may stand for either {tech}[宇宙]universe levels or for terms. Some metavariables arise as part of Lean's elaboration process, when not enough information is yet available to determine a value. These metavariables' names have a numeric component at the end, such as `?m.392` or `?u.498`. Other metavariables come into existence as a result of tactics or {tech}[named holes].