lean-ja · s-taiga · Jan 4, 2025 · Jan 4, 2025 · Jan 4, 2025 · Jan 4, 2025
diff --git a/GLOSSARY.md b/GLOSSARY.md
@@ -30,7 +30,7 @@
 | case distinction | 場合分け | |
 | chapter | 章 | |
 | circular argument | 循環論法 | |
-| clause | 節 | |
+| clause | 句 | deriving, where はどちらも後ろに完全な文ではなく項が来るため、ニュアンス的に節よりも句の方が近いと判断 |
 | closed term | 閉項 | |
 | combinator | コンビネータ | |
 | comma | カンマ | |
@@ -126,9 +126,12 @@
 | immediate value | 即値 | |
 | imperative | 命令型 | |
 | implicit parameter | 暗黙のパラメータ | |
+| impredicative | 非可述 | |
+| impredicativity | 非可述性 | |
 | inaccessible | （仮定のアクセス可否の文脈で）アクセス不能 | |
 | incompatible | 互換性 | |
 | index, indices | 添字 | |
+| indexed family | 添字付けられた型の族 | |
 | induction | 帰納法 | |
 | induction hypothese | 帰納法の仮定 | |
 | inductively-defined | 帰納的に定義された | |
@@ -204,6 +207,8 @@
 | polymorphic | 多相 | |
 | precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
 | predicate | 述語 | |
+| predicative | 可述 | |
+| predicativity | 可述性 | |
 | pretty printer | プリティプリンタ | |
 | primitive | プリミティブ | |
 | primitive recursion | 原始再帰 | |
@@ -330,7 +335,6 @@
 | cumulative | |
 | ellipsis | 他言語でも類似概念があるが、そちらでもそのまま英単語で表現されることが多そうだったため |
 | idiom bracket | https://wiki.haskell.org/Idiom_brackets |
-| impredicativity, predicativity | |
 | inhabited | |
 | no confusion | |
 | out, semi-out | |

diff --git a/Manual/Classes.lean b/Manual/Classes.lean
@@ -264,7 +264,7 @@ While {keywordOf Lean.Parser.Command.declaration}`deriving` clauses are allowed
 
 :::
 
-{keywordOf Lean.Parser.Command.declaration}`deriving` 節は、クラスと構造体のエラボレーションの間の並列性を維持するためにクラス定義で許可されていますが、頻繁に使用されるものではなく、高度な機能と見なされるべきです。
+{keywordOf Lean.Parser.Command.declaration}`deriving` 句は、クラスと構造体のエラボレーションの間の並列性を維持するためにクラス定義で許可されていますが、頻繁に使用されるものではなく、高度な機能と見なされるべきです。
 
 :::comment
 ::example "No Instances of Non-Classes"
@@ -653,7 +653,7 @@ Lean は多くのクラスに対して自動的にインスタンスを生成す
 As part of a command that creates a new inductive type, a {keywordOf Lean.Parser.Command.declaration}`deriving` clause specifies a comma-separated list of class names for which instances should be generated:
 :::
 
-新しい帰納型を作成するコマンドの一部としての {keywordOf Lean.Parser.Command.declaration}`deriving` 節には、その型からインスタンスが生成されるべきクラス名のカンマ区切りのリストを指定します：
+新しい帰納型を作成するコマンドの一部としての {keywordOf Lean.Parser.Command.declaration}`deriving` 句には、その型からインスタンスが生成されるべきクラス名のカンマ区切りのリストを指定します：
 
 ```grammar
 $[deriving $[$_],*]?

diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
@@ -297,8 +297,8 @@ The language implemented by the kernel is a version of the Calculus of Construct
 カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です：
 + 完全な依存型
 + 相互に帰納的であったり、他の帰納型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型
-+ {tech}[impredicative] ・定義上証明と irrelevant な {tech}[命題] の拡張的 {tech}[宇宙]
-+ {tech}[predicative] なデータの宇宙の非蓄積な階層
++ {tech}[非可述] ・定義上証明と irrelevant な {tech}[命題] の拡張的 {tech}[宇宙]
++ {tech}[可述] なデータの宇宙の非蓄積な階層
 * 定義上の計算規則を伴った {ref "quotients"}[商型] （Quotient type）
 + 命題上の関数外延性 {margin}[関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。]
 + 関数と積についての定義上のη等価性
@@ -342,7 +342,7 @@ In practice, apparent non-termination is indistinguishable from sufficiently slo
 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・計算する商型・定義上の証明の irrelevance・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。
+Lean の型理論には subject reduction の機能はなく、定義上の等価性は必ずしも推移的ではなく、型チェッカが停止しないようにすることも可能です。これらのメタ理論的な特性はいずれも実際には問題になりません。推移性が失敗するのは非常にまれであり、知る限りではそれを行使するために特別にコードを作成した場合を除き非停止は発生していません。最も重要なことは、論理的健全性に影響がないことです。実際には、見かけ上の非停止は十分に遅いプログラムと区別がつきません。これらのメタ理論的特性は、非可述性・計算する商型・定義上の証明の irrelevance・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。
 
 :::comment
 # Elaboration Results

diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
@@ -169,7 +169,7 @@ Type constructors with indices are said to specify {deftech}_indexed families_ {
 
 :::
 
-添字は型の _族_ （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字を持つ型のコンストラクタは {deftech}_添字族_ {index subterm:="of types"}[indexed family] （indexed family）の型を指定すると言われます。
+添字は型の _族_ （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字を持つ型のコンストラクタは {deftech}_添字付けられた型の族_ {index subterm:="of types"}[indexed family] （indexed family）の型を指定すると言われます。
 
 :::comment
 ## Example Inductive Types
@@ -555,7 +555,7 @@ Please refer to {ref "deriving-instances"}[the section on instance deriving] for
 
 :::
 
-帰納的宣言のオプションとして、 {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`deriving` 節は、型クラスのインスタンスを導出するために使用することができます。詳細は {ref "deriving-instances"}[インスタンス導出についての節] を参照してください。
+帰納的宣言のオプションとして、 {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`deriving` 句は、型クラスのインスタンスを導出するために使用することができます。詳細は {ref "deriving-instances"}[インスタンス導出についての節] を参照してください。
 
 {include 0 Manual.Language.InductiveTypes.Structures}
 

diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean
@@ -464,7 +464,7 @@ If the universe is not {lean}`Prop`, then the following must hold for each param
 
 :::
 
-帰納型の型コンストラクタは {tech}[宇宙] か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が {lean}`Prop` であれば、 {lean}`Prop` は {tech}[impredicative] であるため宇宙にはそれ以上の制限はありません。もし宇宙が {lean}`Prop` でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります：
+帰納型の型コンストラクタは {tech}[宇宙] か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が {lean}`Prop` であれば、 {lean}`Prop` は {tech}[非可述] であるため宇宙にはそれ以上の制限はありません。もし宇宙が {lean}`Prop` でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります：
  * コンストラクタのパラメータが（パラメータか添字かの意味で）帰納型のパラメータである場合、このパラメータの型は型コンストラクタの宇宙より大きくはできません。
  * その他のすべてのコンストラクタのパラメータは型コンストラクタの宇宙より小さくなければなりません。
 

diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean
@@ -46,7 +46,7 @@ Structures do not add any expressive power to Lean; all of their features are im
 
 :::
 
-{deftech}[構造体] （structure）は単一のコンストラクタを持ち、添字を持たない帰納型です。これらの制限と引き換えに、Lean は構造体のための数々の便利なコードを生成します：アクセサ関数が各フィールドに対して生成される・位置引数ではなくフィールド名に基づく追加のコンストラクタ構文が利用できる・同様の構文を使用して特定の名前付きフィールドの値を書き換えることができる・構造体は他の構造体を拡張することができる。他の帰納型と同様に、構造体も再帰的です；また strict positivity に関しても同じ制約を受けます。構造体は Lean の表現力を増すものではありません；すべての機能はコード生成の観点から実装されます。
+{deftech}[構造体] （structure）は単一のコンストラクタを持ち、添字を持たない帰納型です。これらの制限と引き換えに、Lean は構造体のための数々の便利なコードを生成します：アクセサ関数が各フィールドに対して生成される・位置引数ではなくフィールド名に基づく追加のコンストラクタ構文が利用できる・同様の構文を使用して特定の名前付きフィールドの値を書き換えることができる・構造体は他の構造体を拡張することができる。他の帰納型と同様に、構造体も再帰的にすることができます；また strict positivity に関しても同じ制約を受けます。構造体は Lean の表現力を増すものではありません；すべての機能はコード生成の観点から実装されます。
 
 ```lean (show := false)
 -- Test claim about recursive above
@@ -76,7 +76,7 @@ Structures may not define {tech}[indexed families].
 
 :::
 
-通常の帰納型宣言と同様に、構造体宣言のヘッダにはパラメータと結果の宇宙の両方を指定できるシグネチャが含まれます。構造体は {tech}[添字族] を定義することはできません。
+通常の帰納型宣言と同様に、構造体宣言のヘッダにはパラメータと結果の宇宙の両方を指定できるシグネチャが含まれます。構造体は {tech}[添字付けられた型の族] を定義することはできません。
 
 :::comment
 # Fields
@@ -438,7 +438,7 @@ When updating a structure, array values may also be replaced by including the in
 This updating does not require that the index expression be in bounds for the array, and out-of-bounds updates are discarded.
 :::
 
-コンストラクタの型の値を更新します。 {keywordOf Lean.Parser.Term.structInst}`with` 節の前にある項は構造体型を持つことが期待されます；これが更新される値です。構造体の新しいインスタンスが作成され、指定されていないすべてのフィールドが更新される値からコピーされ、指定されたフィールドは新しい値に置き換えられます。構造体を更新する時、更新するインデックスを角括弧で囲むことで配列の値を置き換えることもできます。この更新では、院デック氏の式が配列の範囲内にある必要はなく、範囲外の更新は破棄されます。
+コンストラクタの型の値を更新します。 {keywordOf Lean.Parser.Term.structInst}`with` 句の前にある項は構造体型を持つことが期待されます；これが更新される値です。構造体の新しいインスタンスが作成され、指定されていないすべてのフィールドが更新される値からコピーされ、指定されたフィールドは新しい値に置き換えられます。構造体を更新する時、更新するインデックスを角括弧で囲むことで配列の値を置き換えることもできます。この更新では、インデックスの式が配列の範囲内にある必要はなく、範囲外の更新は破棄されます。
 
 ::::
 
@@ -523,7 +523,7 @@ New default values in the child structure take precedence over default values fr
 
 :::
 
-構造体はオプションの {keywordOf Lean.Parser.Command.declaration (parser:=«structure»)}`extends` 節を使用することで他の構造体を拡張することを宣言できます。結果として得られる構造体型は、すべての親構造体型のすべてのフィールドを持ちます。親構造体型が重複するフィールド名を持つ場合、重複するフィールド名はすべて同じ型を持たなければなりません。重複するフィールド名が異なるデフォルト値を持つ場合、そのフィールドを含む最後の親構造体のデフォルト値が使用されます。子構造体の新しいデフォルト値は、親構造体のデフォルト値よりも優先されます。
+構造体はオプションの {keywordOf Lean.Parser.Command.declaration (parser:=«structure»)}`extends` 句を使用することで他の構造体を拡張することを宣言できます。結果として得られる構造体型は、すべての親構造体型のすべてのフィールドを持ちます。親構造体型が重複するフィールド名を持つ場合、重複するフィールド名はすべて同じ型を持たなければなりません。重複するフィールド名が異なるデフォルト値を持つ場合、そのフィールドを含む最後の親構造体のデフォルト値が使用されます。子構造体の新しいデフォルト値は、親構造体のデフォルト値よりも優先されます。
 
 ```lean (show := false) (keep := false)
 -- If the overlapping fields have different default values, then the default value from the last parent structure that includes the field is used.

diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean
@@ -61,7 +61,7 @@ There are four main kinds of recursive functions that can be defined:
 
 : 構造的再帰関数
 
-  構造的再帰関数は、関数が当該引数の厳密な部分コンポーネントに対してのみ再帰呼び出しを行うように引数を取ります。 {margin}[厳密に言えば、型が {tech}[添字族] である引数は、それらの添字と共にグループ化され、コレクション全体が1つの単位とみなされます。] エラボレータは再帰を引数の {tech}[再帰子] の使用に変換します。型が正しい再帰子の使用は、すべての無限後退を回避することが保証されているため、この変換は関数が停止する根拠となります。再帰子を介して定義された関数の適用は定義上は再帰の結果と等しく、カーネル内部において通常は比較的効率的です。
+  構造的再帰関数は、関数が当該引数の厳密な部分コンポーネントに対してのみ再帰呼び出しを行うように引数を取ります。 {margin}[厳密に言えば、型が {tech}[添字付けられた型の族] である引数は、それらの添字と共にグループ化され、コレクション全体が1つの単位とみなされます。] エラボレータは再帰を引数の {tech}[再帰子] の使用に変換します。型が正しい再帰子の使用は、すべての無限後退を回避することが保証されているため、この変換は関数が停止する根拠となります。再帰子を介して定義された関数の適用は定義上は再帰の結果と等しく、カーネル内部において通常は比較的効率的です。
 
 :::comment
 : Recursion over well-founded relations
@@ -135,7 +135,7 @@ As described in the {ref "elaboration-results"}[overview of the elaborator's out
 
 :::
 
- 2. 停止性の分析では、4つの技法を使って Lean のカーネルに関数を正当化しようとします。定義が {keywordOf Lean.Parser.Command.declaration}`unsafe` または {keywordOf Lean.Parser.Command.declaration}`partial` とマークされている場合、この技法が使用されます。明示的な {keywordOf Lean.Parser.Command.declaration}`termination_by` 節が存在する場合、指定された技法のみが試みられます。この節がない場合、エラボレータは探索を実行し、構造的再帰の候補として関数への各パラメータをテストし、各再帰呼び出しで減少する整礎関係を持つ測度を見つけようとします。
+ 2. 停止性の分析では、4つの技法を使って Lean のカーネルに関数を正当化しようとします。定義が {keywordOf Lean.Parser.Command.declaration}`unsafe` または {keywordOf Lean.Parser.Command.declaration}`partial` とマークされている場合、この技法が使用されます。明示的な {keywordOf Lean.Parser.Command.declaration}`termination_by` 句が存在する場合、指定された技法のみが試みられます。この句がない場合、エラボレータは探索を実行し、構造的再帰の候補として関数への各パラメータをテストし、各再帰呼び出しで減少する整礎関係を持つ測度を見つけようとします。
 
 :::comment
 This section describes the four techniques in detail.