InductiveTypes翻訳完了 (#7)

Author: s-taiga

GLOSSARY.md

@@ -4,19 +4,25 @@
 | --- | --- | --- |
 | abbreviation | 省略形 | |
 | abstraction | 抽象 | |
+| angle bracket | 角括弧 | square bracketと同じ訳語にしているが、直後にコード例がある場合も多いため文脈で見分けられる想定 |
 | annotation | 注釈 | |
+| anonymous constructor | 匿名コンストラクタ | |
 | associativity | 結合性 | |
 | assumption | 仮定 | |
 | attribute | 属性 | |
 | backtrack | バックトラック | 後戻りと書かれる場合あり |
 | binder | 束縛子 | |
+| boolean | 真偽値 | |
 | bound variable | 束縛変数 | |
+| box | ボックス化 | |
 | canonical | 標準 | |
 | carriage return | CR | |
 | case distinction | 場合分け | |
 | chapter | 章 | |
+| clause | 節 | |
 | closed term | 閉項 | |
 | combinator | コンビネータ | |
+| comma | カンマ | |
 | command | コマンド | |
 | command elaboration | コマンドエラボレーション | |
 | compilation | コンパイル | |
@@ -40,22 +46,29 @@
 | dependent | 依存的 | 後ろに何も続かない場合 |
 | dependent function | 依存関数 | |
 | dependent type theory | 依存型理論 | |
+| deriving | 導出 | |
 | desugar | 脱糖 | |
 | domain | 定義域 | |
 | double-struck | 重ね打ち体 | |
 | effect | 作用 | |
 | elaborate | エラボレート | |
 | elaboration | エラボレーション | |
 | elaborator | エラボレータ | |
+| elimination rule | 除去則 | |
 | encoding | エンコード | |
 | English letter | 英語アルファベット | |
+| enum inductive | 列挙的帰納 | |
 | environment | 環境 | |
 | environment extensions | 環境拡張 | |
 | equational lemma | 等式の補題 | |
+| equivalent | 同値 | |
 | evaluate | 評価 | |
+| evidence | 根拠 | |
+| exception | 例外 | |
 | exclamation mark | 感嘆符 | |
 | executable | 実行ファイル | |
 | expression | 式 | |
+| fixed-width integer | 固定幅整数 | |
 | formalization | 形式化 | |
 | form feed | 改ページ | |
 | functional programming language | 関数型プログラミング言語 | |
@@ -67,10 +80,12 @@
 | hierarchical identifier | 階層的識別子 | |
 | hierarchy | 階層 | |
 | higher-order function | 高階関数 | |
+| identically | 同一 | |
 | identifier | 識別子 | |
 | identifier component | 識別子要素 | |
 | identifier continuation character | 識別子継続文字 | |
 | implicit parameter | 暗黙のパラメータ | |
+| index, indices | 添字 | |
 | inductively-defined | 帰納的に定義された | |
 | inductive predicate | 帰納的述語 | |
 | inductive type | 帰納型 | |
@@ -95,11 +110,13 @@
 | letterlike | 文字様 | |
 | longest match | 最長一致 | |
 | macro | マクロ | |
+| machine integer | 機械整数 | |
 | machinery | 機構 | |
 | macro Expansion | マクロ展開 | |
 | mapping | マッピング | |
 | memoization | メモ化 | |
 | monad | モナド | |
+| motive | 動機 | |
 | multi-threading | マルチスレッド | |
 | mutually inductive | 相互帰納 | |
 | namespace | 名前空間 | |
@@ -116,6 +133,7 @@
 | parse | パース | |
 | parser | パーサ | |
 | pattern matching | パターンマッチ | |
+| polymorphic | 多相 | |
 | precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
 | pretty printer | プリティプリンタ | |
 | primitive | プリミティブ | |
@@ -136,8 +154,10 @@
 | representation | 表現 | |
 | reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
 | reserved word | 予約語 | |
+| run-length encoding | 連長圧縮 | |
 | run-time | ランタイム | |
 | rule | ランタイム | |
+| saturated application | 完全な適用 | 固定訳は無いように思われ、飽和では意味が分かりづらいため |
 | scope | スコープ | |
 | separator | 区切り文字 | |
 | set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | |
@@ -154,6 +174,7 @@
 | strictness | 正格 | |
 | structure | 構造体 | |
 | subterm | 部分項 | |
+| subtype | 部分型 | |
 | subscript | 下付き文字 | |
 | syntactically | 構文上 | |
 | syntactic sugar | 構文糖衣 | |
@@ -174,14 +195,22 @@
 | transitive | 推移的 | |
 | transitivity | 推移性 | |
 | tree | 木 | |
+| trivial | 自明な | |
 | trust | 信頼 | |
 | type class | 型クラス | |
 | type class instance synthesis | 型クラスインスタンス合成 | |
+| type signature | 型シグネチャ | |
+| unbox | ボックス化解除 | C#の用語を流用 |
 | underscore | アンダースコア | |
 | unification | 単一化 | |
 | union | 合併 | |
+| unit type | ユニット型 | |
+| universe | 宇宙 | |
+| universe level | 宇宙レベル | |
+| well-formed | 適格 | |
 | well-founded | 整礎 | |
 | whitespace | 空白 | |
+| wrapper | ラッパ | |
 
 
 # 英語表現をそのまま用いている単語
@@ -190,6 +219,8 @@
 | --- | --- |
 | choice node | |
 | packed array | System Verilogという言語にこの名前の文法要素がある？ |
+| strict positively, negatively | 自己言及される定義の分類、定訳は無い模様 |
 | prelude | |
+| relevant, irrelevant | 直訳して「関係・無関係」はわかりづらいと判断 |
 | subject reduction | TAPLに出てくる模様 |
 | type ascription | Scala、Rustに同じ用語あり |

Manual/Elaboration.lean

@@ -272,7 +272,7 @@ It does not include a syntactic termination checker, nor does it perform unifica
 Before new inductive types or definitions are added to the environment by the command or term elaborators, they must be checked by the kernel to guard against potential bugs in elaboration.
 :::
 
-Lean が信頼する {deftech}_カーネル_ （kernel）はコア型理論のための型チェッカの小さく堅牢な実装です。カーネルには構文的停止チェッカは含まれず、単一化も行いません；停止性はすべての再帰関数をプリミティブ {tech}[recursors] の使用にエラボレートすることで保証され、単一化はエラボレータによってすでに実行されていることが期待されます。コマンドと項エラボレータによって新しい帰納型や定義が環境に追加される前に、エラボレータによって潜在的なバグを防ぐために、それらはカーネルによってチェックされなければなりません。
+Lean が信頼する {deftech}_カーネル_ （kernel）はコア型理論のための型チェッカの小さく堅牢な実装です。カーネルには構文的停止チェッカは含まれず、単一化も行いません；停止性はすべての再帰関数をプリミティブ {tech}[再帰子] の使用にエラボレートすることで保証され、単一化はエラボレータによってすでに実行されていることが期待されます。コマンドと項エラボレータによって新しい帰納型や定義が環境に追加される前に、エラボレータによって潜在的なバグを防ぐために、それらはカーネルによってチェックされなければなりません。
 
 :::comment
 Lean's kernel is written in C++.
@@ -297,7 +297,7 @@ The language implemented by the kernel is a version of the Calculus of Construct
 カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です：
 + 完全な依存型
 + 相互に帰納的であったり、他の帰納的データ型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型
-+ {tech}[impredicative] ・定義上証明とは無関係な {tech}[propositions] の拡張的 {tech}[universe]
++ {tech}[impredicative] ・定義上証明と irrelevant な {tech}[propositions] の拡張的 {tech}[universe]
 + {tech}[predicative] なデータの宇宙の非蓄積な階層
 * 定義上の計算規則を伴った {ref "quotients"}[商型] （Quotient type）
 + 命題上の関数外延性 {margin}[関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。]
@@ -342,7 +342,7 @@ In practice, apparent non-ermination is indistinguishable from sufficiently slow
 These metatheoretic properties are a result of having impredicativity, quotient types that compute, definitional proof irrelevance, and propositional extensionality; these features are immensely valuable both to support ordinary mathematical practice and to enable automation.
 :::
 
-Lean の型理論には subject reduction の機能はなく、定義上の等価性は必ずしも推移的ではなく、型チェッカが停止しないようにすることも可能です。これらのメタ理論的な特性はいずれも実際には問題になりません。推移性が失敗するのは非常にまれであり、知る限りではそれを行使するために特別にコードを作成した場合を除き非停止は発生していません。最も重要なことは、論理的健全性に影響がないことです。実際には、見かけ上の非停止は十分に遅いプログラムと区別がつきません。これらのメタ理論的特性は、impredicativity・計算する商型・定義上の証明の無関係性・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。
+Lean の型理論には subject reduction の機能はなく、定義上の等価性は必ずしも推移的ではなく、型チェッカが停止しないようにすることも可能です。これらのメタ理論的な特性はいずれも実際には問題になりません。推移性が失敗するのは非常にまれであり、知る限りではそれを行使するために特別にコードを作成した場合を除き非停止は発生していません。最も重要なことは、論理的健全性に影響がないことです。実際には、見かけ上の非停止は十分に遅いプログラムと区別がつきません。これらのメタ理論的特性は、impredicativity・計算する商型・定義上の証明との irrelevance・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。
 
 :::comment
 # Elaboration Results
@@ -357,7 +357,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}[recursors] を提供します。したがって、エラボレータはパターンマッチと再帰を使用する定義から再帰子を使用する定義に変換する必要があります。この変換はさらに、関数がすべての潜在的な引数に対して停止することの証明でもあります。なぜなら再帰子へ翻訳されるすべての関数は停止するからです。
+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.

Manual/Language.lean

@@ -37,7 +37,7 @@ A term is {deftech}_well-typed_ if it has a type under the rules of Lean's type
 Only well-typed terms have a meaning.
 
 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.
 
 A {deftech}_derivation_ demonstrates the well-typedness of a term by explicitly indicating the precise inference rules that are used.
@@ -131,8 +131,8 @@ but is expected to have 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.
+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.
 
 
 {include Manual.Language.Functions}

Manual/Language/Functions.lean

@@ -239,7 +239,7 @@ However, not all functions originate from abstractions: {tech}[type constructors
 
 :::
 
-{keywordOf Lean.Parser.Command.declaration parser:=Lean.Parser.Command.definition}`def` のようなキーワードで定義された関数定義は {keywordOf Lean.Parser.Term.fun}`fun` に脱糖されます。しかし、すべての関数が抽象されたものではありません： {tech}[type constructors] ・ {tech}[constructors] ・ {tech}[recursors] は関数型を持つ場合がありますが、関数抽象だけでは定義できません。
+{keywordOf Lean.Parser.Command.declaration parser:=Lean.Parser.Command.definition}`def` のようなキーワードで定義された関数定義は {keywordOf Lean.Parser.Term.fun}`fun` に脱糖されます。しかし、すべての関数が抽象されたものではありません： {tech}[型コンストラクタ] ・ {tech}[コンストラクタ] ・ {tech}[再帰子] は関数型を持つ場合がありますが、関数抽象だけでは定義できません。
 
 :::comment
 # Currying
@@ -711,7 +711,7 @@ These operations result in an arbitrarily chosen inhabitant of the type in Lean'
 
 :::
 
-同様に、配列への範囲外アクセスなど、コンパイルされたコードでは実行時に失敗するはずの操作は、結果の型が inhabited であることが分かっている場合にのみ使用することができます。これらの操作の結果、Lean のロジックでは型の住人が任意に選ばれます（具体的には、その型の {name}`Inhabited` インスタンスで指定されたもの）。
+同様に、配列への範囲外アクセスなど、コンパイルされたコードではランタイムに失敗するはずの操作は、結果の型が inhabited であることが分かっている場合にのみ使用することができます。これらの操作の結果、Lean のロジックでは型の住人が任意に選ばれます（具体的には、その型の {name}`Inhabited` インスタンスで指定されたもの）。
 
 :::comment
 ::example "Panic"