Language翻訳 (#10)

* 翻訳開始

* 翻訳完了

Author: s-taiga

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,18 +202,21 @@
 | side effect | 副作用 | |
 | signature | シグネチャ | |
 | single quote | シングルクォート | |
+| singleton | 単集合 | |
 | soundness | 健全性 | |
 | square bracket | 角括弧 | |
 | specialization | 特殊化 | |
 | statement | 文 | |
 | strict implicit parameter | 厳格な暗黙のパラメータ | |
+| strictly | （順序の意味で）狭義 | |
 | strictness | 正格 | |
 | strong induction | 強帰納法 | |
 | structure | 構造体 | |
 | subfield | サブフィールド | |
 | 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に同じ用語あり |
+| type ascription | Scala、Rustに同じ用語あり |
+| well-typed | |

Manual/Elaboration.lean

@@ -19,7 +19,7 @@ open Lean (Syntax SourceInfo)
 /-
 #doc (Manual) "Elaboration and Compilation" =>
 -/
-#doc (Manual) "エラボレーションとコンパイル" =>
+#doc (Manual) "エラボレーションとコンパイル（Elaboration and Compilation）" =>
 %%%
 htmlSplit := .never
 %%%
@@ -112,7 +112,7 @@ The next command is parsed and elaborated in this updated state, and itself upda
 # Parsing
 :::
 
-# パース
+# パース（Parsing）
 %%%
 tag := "parser"
 %%%
@@ -174,7 +174,7 @@ Syntax extensions are described in more detail in {ref "language-extension"}[a d
 # Macro Expansion and Elaboration
 :::
 
-# マクロ展開とエラボレーション
+# マクロ展開とエラボレーション（Macro Expansion and Elaboration）
 %%%
 tag := "macro-and-elab"
 %%%
@@ -234,7 +234,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.
@@ -264,7 +264,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.
@@ -297,7 +297,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}[関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。]
@@ -348,7 +348,7 @@ Lean の型理論には subject reduction の機能はなく、定義上の等
 # Elaboration Results
 :::
 
-# エラボレーションの結果
+# エラボレーションの結果（Elaboration Results）
 %%%
 tag := "elaboration-results"
 %%%
@@ -360,7 +360,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 {deftech}_auxiliary matching functions_ that implement the particular case distinction that occurs in the code.
@@ -664,7 +664,7 @@ The most important topics related to Lean's reference-counting-based allocator:
 # Initialization
 :::
 
-# 初期化コード
+# 初期化（Initialization）
 
 :::comment
 Before starting up, the elaborator must be correctly initialized.

Manual/Language.lean

@@ -24,43 +24,81 @@ set_option maxRecDepth 3000
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Source Files" =>
+-/
+#doc (Manual) "ソースファイル（Source Files）" =>
 
 {include 0 Manual.Language.Files}
 
 
+:::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.
 The {keywordOf Lean.Parser.Command.declaration}`instance` command is described in the {ref "instance-declarations"}[section on instance declarations].
 
+:::
+
+これらのコマンドはすべて Lean によってシグネチャに応じた項へ {tech key:="エラボレータ"}[エラボレート] されます。結果を破棄する {syntaxKind}`example` を除き、Lean のコア言語での結果の式は将来の環境で使用するために保存されます。
+
 :::syntax Lean.Parser.Command.declaration
 ```grammar
 $_:declModifiers
@@ -134,8 +172,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 $_ $_
@@ -186,10 +229,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