diff --git a/GLOSSARY.md b/GLOSSARY.md index 7261783..bb664e0 100644 --- 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 index 89a8dd3..7c8423b 100644 --- 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 index ead55ff..89ead4f 100644 --- 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 index 494be84..48a1121 100644 --- 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 index 242c15b..4233630 100644 --- 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 index dd714a8..6162378 100644 --- 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 index fe032ec..b11571b 100644 --- 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. diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean index 1d728da..3e2e87f 100644 --- a/Manual/Monads/Syntax.lean +++ b/Manual/Monads/Syntax.lean @@ -447,7 +447,7 @@ The second binds a pattern to the result. The fallback clause, beginning with `|`, specifies the behavior when the pattern does not match the result. ::: -2番目はパターンを結果に束縛します。 `|` で始まるフォールバック節は、パターンが結果にマッチしなかった場合の動作を指定します。 +2番目はパターンを結果に束縛します。 `|` で始まるフォールバック句は、パターンが結果にマッチしなかった場合の動作を指定します。 ```grammar let $x:term ← $e:term @@ -461,7 +461,7 @@ This syntax is also translated to a use of {name}`bind`. This indicates a pure, rather than monadic, definition: ::: -この構文も {name}`bind` の使用に変換されます。 {lean}`do let x ← e1; es` は {lean}`e1 >>= fun x => do es` に変換され、フォールバック節はデフォルトのパターンマッチに変換されます。 {keywordOf Lean.Parser.Term.doLet}`let` は `←` の代わりに標準的な定義構文 `:=` によって使用することもできます。この場合はモナドではなく純粋な定義を示します： +この構文も {name}`bind` の使用に変換されます。 {lean}`do let x ← e1; es` は {lean}`e1 >>= fun x => do es` に変換され、フォールバック句はデフォルトのパターンマッチに変換されます。 {keywordOf Lean.Parser.Term.doLet}`let` は `←` の代わりに標準的な定義構文 `:=` によって使用することもできます。この場合はモナドではなく純粋な定義を示します： :::syntax Lean.Parser.Term.doSeqItem ```grammar @@ -891,7 +891,7 @@ Each collection is iterated over at the same time, and iteration stops when any ::: -{keywordOf Lean.Parser.Term.doFor}`for`​`…`​{keywordOf Lean.Parser.Term.doFor}`in` ループでは、実行する反復処理を指定する節が少なくとも1つ必要です。この節は、コロン（`:`）が続くオプションのメンバシップ証明名・束縛パターン・キーワード {keywordOf Lean.Parser.Term.doFor}`in` ・コレクションの項から構成されます。パターンは {tech}[識別子] であり、コレクションの任意の要素と一致しなければなりません；この位置でのパターンは暗黙のフィルタとして使うことはできません。カンマで区切ることでさらに節を指定することができます。各コレクションは同時に反復され、いずれかのコレクションの要素がなくなると反復処理が停止します。 +{keywordOf Lean.Parser.Term.doFor}`for`​`…`​{keywordOf Lean.Parser.Term.doFor}`in` ループでは、実行する反復処理を指定する句が少なくとも1つ必要です。この節は、コロン（`:`）が続くオプションのメンバシップ証明名・束縛パターン・キーワード {keywordOf Lean.Parser.Term.doFor}`in` ・コレクションの項から構成されます。パターンは {tech}[識別子] であり、コレクションの任意の要素と一致しなければなりません；この位置でのパターンは暗黙のフィルタとして使うことはできません。カンマで区切ることでさらに句を指定することができます。各コレクションは同時に反復され、いずれかのコレクションの要素がなくなると反復処理が停止します。 :::comment ::example "Iteration Over Multiple Collections" diff --git a/Manual/Terms.lean b/Manual/Terms.lean index 5a5b261..f3f883b 100644 --- a/Manual/Terms.lean +++ b/Manual/Terms.lean @@ -2323,10 +2323,10 @@ variable {α : Type u} ::: ::::example "型の絞り込み" :::comment -This {tech}[添字族]indexed family describes mostly-balanced trees, with the depth encoded in the type. +This {tech}[添字付けられた型の族]indexed family describes mostly-balanced trees, with the depth encoded in the type. ::: -この {tech}[添字族] は深さが型にエンコードされた平衡に近い木を記述します。 +この {tech}[添字付けられた型の族] は深さが型にエンコードされた平衡に近い木を記述します。 ```lean inductive BalancedTree (α : Type u) : Nat → Type u where @@ -2440,7 +2440,7 @@ This is useful to bridge the gap between dependent pattern matching on indexed f ::: -判別子の名前が指定されると、 {keywordOf Lean.Parser.Term.match}`match` はパターンと判別子が等しいという証明を生成し、 {tech}[右辺] で指定された名前に束縛します。これは添字族に対する依存パターンマッチと明示的な命題引数を期待する API とのギャップを埋めるにあたって便利であり、仮定を利用するタクティクを成功させるために役立ちます。 +判別子の名前が指定されると、 {keywordOf Lean.Parser.Term.match}`match` はパターンと判別子が等しいという証明を生成し、 {tech}[右辺] で指定された名前に束縛します。これは添字付けられた型の族に対する依存パターンマッチと明示的な命題引数を期待する API とのギャップを埋めるにあたって便利であり、仮定を利用するタクティクを成功させるために役立ちます。 :::comment ::example "Pattern Equality Proofs" @@ -2552,7 +2552,7 @@ However, a process called {deftech}[discriminant refinement] automatically adds ::: -添字族にマッチする場合、添字も判別子でなければなりません。一方で、パターンは正しく型付けされない可能性があります：添字が単なる変数であるにもかかわらず、コンストラクタの型がより具体的な値を必要とする場合は型エラーとなります。しかし、 {deftech}[判別子の絞り込み] （discriminant refinement）と呼ばれる処理によって自動的に添字が追加の判別子として追加されます。 +添字付けられた型の族にマッチする場合、添字も判別子でなければなりません。一方で、パターンは正しく型付けされない可能性があります：添字が単なる変数であるにもかかわらず、コンストラクタの型がより具体的な値を必要とする場合は型エラーとなります。しかし、 {deftech}[判別子の絞り込み] （discriminant refinement）と呼ばれる処理によって自動的に添字が追加の判別子として追加されます。 :::::keepEnv :::comment @@ -2564,7 +2564,7 @@ In the definition of {lean}`f`, the equality proof is the only discriminant. However, equality is an indexed family, and the match is only valid when `n` is an additional discriminant. ::: -{lean}`f` の定義では、等式の証明が唯一の判別子です。しかし、等式は添字族であり、マッチは `n` が追加の判別子である場合にのみ有効です。 +{lean}`f` の定義では、等式の証明が唯一の判別子です。しかし、等式は添字付けられた型の族であり、マッチは `n` が追加の判別子である場合にのみ有効です。 ```lean def f (n : Nat) (p : n = 3) : String := diff --git a/Manual/Types.lean b/Manual/Types.lean index 3d53a0b..005b44c 100644 --- a/Manual/Types.lean +++ b/Manual/Types.lean @@ -274,7 +274,7 @@ Propositions have the following properties: ::: -: impredicativity +: 非可述性 命題はあらゆる宇宙からの型に対して量化することができます。 @@ -382,7 +382,11 @@ Because propositions and data are used differently and are governed by different 命題とデータは異なる使われ方をし、異なる規則に支配されるため、より便利に区別するために {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` の省略形です。 +:::comment ## Predicativity +::: + +## 可述性（Predicativity） :::comment Each universe contains dependent function types, which additionally represent universal quantification and implication. @@ -399,9 +403,12 @@ In other words, propositions feature {deftech}[_impredicative_] {index}[impredic ::: -命題を返す関数である述語（つまり、関数の結果が `Prop` にある型である場合）は引数の型がどのような宇宙に会っても構いませんが、関数の型自体は `Prop` に留まります。言い換えると、命題は {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] な量化子を特徴づけます。というのも、命題はそれ自体、すべての命題（および他のすべての命題）についての文になりうるからです。 +命題を返す関数である述語（つまり、関数の結果が `Prop` にある型である場合）は引数の型がどのような宇宙に会っても構いませんが、関数の型自体は `Prop` に留まります。言い換えると、命題は {deftech}[_非可述_] {index}[impredicative]{index subterm := "impredicative"}[quantification] な量化子を特徴づけます。というのも、命題はそれ自体、すべての命題（および他のすべての命題）についての文になりうるからです。 -::::Manual.example "Impredicativity" +:::comment +::Manual.example "Impredicativity" +::: +::::Manual.example "非可述性" :::comment Proof irrelevance can be written as a proposition that quantifies over all propositions: ::: @@ -430,7 +437,7 @@ For these universes, the universe of a function type is the least upper bound of ::: -{tech key:="universe level"}[レベル] `1` 以上の宇宙（つまり、`Type u` の階層）では、量化子は {deftech}[_predicative_] です。 {index}[predicative]{index subterm := "predicative"}[quantification] これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。 +{tech key:="universe level"}[レベル] `1` 以上の宇宙（つまり、`Type u` の階層）では、量化子は {deftech}[_可述_] です。 {index}[predicative]{index subterm := "predicative"}[quantification] これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。 :::comment ::Manual.example "Universe levels of function types" @@ -703,7 +710,7 @@ Level ::= 0 | 1 | 2 | ... -- 具体的なレベル | u, v -- 変数 | Level + n -- 定数の和 | max Level Level -- 最小上界 - | imax Level Level -- Impredicative な最小上界 + | imax Level Level -- 非可述な最小上界 ```` :::comment @@ -723,7 +730,7 @@ If `B : Prop`, then the function type is itself a {lean}`Prop`; otherwise, the f ::: -`imax` は {lean}`Prop` の {tech}[impredicative] な量化子を実装するために使用されます。特に、`A : Sort u` かつ `B : Sort v` である場合、`(x : A) → B : Sort (imax u v)` となります。もし `B : Prop` ならば、その関数型は {lean}`Prop` であり、それ以外ではその関数型のレベルは `u` と `v` の最大値になります。 +`imax` は {lean}`Prop` の {tech}[非可述] な量化子を実装するために使用されます。特に、`A : Sort u` かつ `B : Sort v` である場合、`(x : A) → B : Sort (imax u v)` となります。もし `B : Prop` ならば、その関数型は {lean}`Prop` であり、それ以外ではその関数型のレベルは `u` と `v` の最大値になります。 :::comment ### Universe Variable Bindings