用語の暫定対応

Author: s-taiga

Manual/Elaboration.lean

@@ -431,7 +431,7 @@ To provide a uniform interface to functions defined via structural and well-foun
 In the function's namespace, `eq_unfold` relates the function directly to its definition, `eq_def` relates it to the definition after instantiating implicit parameters, and $`N` lemmas `eq_N` relate each case of its pattern-matching to the corresponding right-hand side, including sufficient assumptions to indicate that earlier branches were not taken.
 :::
 
-構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は {deftech}[整礎再帰] （well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの基準が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。
+構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は {deftech}[整礎再帰] （well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの {deftech}_測度_ （measure）が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。
 
 :::::keepEnv
 :::comment

Manual/IO.lean

@@ -32,7 +32,7 @@ tag := "io"
 
 
 Lean is a pure functional programming language.
-While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking {tech}[definitional equality], is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change.
+While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking {tech}[定義上の等価性]definitional equality, is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change.
 This means that simply adding operations that perform side effects (such as file I/O, exceptions, or mutable references) would lead to programs in which the order of effects is unspecified.
 During type checking, even terms with free variables are reduced; this would make side effects even more difficult to predict.
 Finally, a basic principle of Lean's logic is that functions are _functions_ that map each element of the domain to a unique element of the range.
@@ -129,7 +129,7 @@ example : BaseIO = EIO Empty := rfl
 ## Errors and Error Handling
 
 Error handling in the {lean}`IO` monad uses the same facilities as any other {tech}[exception monad].
-In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[type class].
+In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[型クラス]type class.
 The exceptions thrown in {lean}`IO` have the type {lean}`IO.Error`.
 The constructors of this type represent the low-level errors that occur on most operating systems, such as files not existing.
 The most-used constructor is {name IO.Error.userError}`userError`, which covers all other cases and includes a string that describes the problem.

Manual/Language/RecursiveDefs.lean

@@ -21,10 +21,10 @@ tag := "recursive-definitions"
 %%%
 
 Allowing arbitrary recursive function definitions would make Lean's logic inconsistent.
-General recursion makes it possible to write circular proofs: "{tech}[proposition] $`P` is true because proposition $`P` is true".
+General recursion makes it possible to write circular proofs: "{tech}[命題]proposition $`P` is true because proposition $`P` is true".
 Outside of proofs, an infinite loop could be assigned the type {name}`Empty`, which can be used with {keywordOf Lean.Parser.Term.nomatch}`nomatch` or {name Empty.rec}`Empty.rec` to prove any theorem.
 
-Banning recursive function definitions outright would render Lean far less useful: {tech}[inductive types] are key to defining both predicates and data, and they have a recursive structure.
+Banning recursive function definitions outright would render Lean far less useful: {tech}[帰納型]inductive types are key to defining both predicates and data, and they have a recursive structure.
 Furthermore, most useful recursive functions do not threaten soundness, and infinite loops usually indicate mistakes in definitions rather than intentional behavior.
 Instead of banning recursive functions, Lean requires that each recursive function is defined safely.
 While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.{margin}[The section on {ref "elaboration-results"}[the elaborator's output] in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.]
@@ -33,15 +33,15 @@ There are four main kinds of recursive functions that can be defined:
 
 : Structurally recursive functions
 
-  Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.{margin}[Strictly speaking, arguments whose types are {tech}[indexed families] are grouped together with their indices, with the whole collection considered as a unit.]
-  The elaborator translates the recursion into uses of the argument's {tech}[recursor].
+  Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.{margin}[Strictly speaking, arguments whose types are {tech}[添字族]indexed families are grouped together with their indices, with the whole collection considered as a unit.]
+  The elaborator translates the recursion into uses of the argument's {tech}[再帰子]recursor.
   Because every type-correct use of a recursor is guaranteed to avoid infinite regress, this translation is evidence that the function terminates.
   Applications of functions defined via recursors are definitionally equal to the result of the recursion, and are typically relatively efficient inside the kernel.
 
 : Recursion over well-founded relations
 
   Many functions are also difficult to convert to structural recursion; for instance, a function may terminate because the difference between an array index and the size of the array decreases as the index increases, but {name}`Nat.rec` isn't applicable because the index that increases is the function's argument.
-  Here, there is a {tech}[measure] of termination that decreases at each recursive call, but the measure is not itself an argument to the function.
+  Here, there is a {tech}[測度]measure of termination that decreases at each recursive call, but the measure is not itself an argument to the function.
   In these cases, {tech}[well-founded recursion] can be used to define the function.
   Well-founded recursion is a technique for systematically transforming recursive functions with a decreasing measure into recursive functions over proofs that every sequence of reductions to the measure eventually terminates at a minimum.
   Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition.

Manual/Language/RecursiveDefs/Structural.lean

@@ -37,7 +37,7 @@ Next, for each group of parameters, a translation using `brecOn` is attempted.
 {spliceContents Manual.Language.RecursiveDefs.Structural.CourseOfValuesExample}
 
 The `below` construction is a mapping from each value of a type to the results of some function call on _all_ smaller values; it can be understood as a memoization table that already contains the results for all smaller values.
-Recursors expect an argument for each of the inductive type's constructors; these arguments are called with the constructor's arguments (and the result of recursion on recursive parameters) during {tech}[ι-reduction].
+Recursors expect an argument for each of the inductive type's constructors; these arguments are called with the constructor's arguments (and the result of recursion on recursive parameters) during {tech}[ι簡約]ι-reduction.
 The course-of-values recursion operator `brecOn`, on the other hand, expects just a single case that covers all constructors at once.
 This case is provided with a value and a `below` table that contains the results of recursion on all values smaller than the given value; it should use the contents of the table to satisfy the motive for the provided value.
 If the function is structurally recursive over a given parameter (or parameter group), then the results of all recursive calls will be present in this table already.

Manual/Language/RecursiveDefs/Structural/CourseOfValuesExample.lean

@@ -30,7 +30,7 @@ theorem List.below_eq_below' : @List.below = @List.below' := by
   congr
 ```
 
-In other words, for a given {tech}[motive], {lean}`List.below'` is a type that contains a realization of the motive for all suffixes of the list.
+In other words, for a given {tech}[動機]motive, {lean}`List.below'` is a type that contains a realization of the motive for all suffixes of the list.
 
 More recursive arguments require further nested iterations of the product type.
 For instance, binary trees have two recursive occurrences.

Manual/Monads/Syntax.lean

@@ -532,7 +532,7 @@ for $[$[$h :]? $x in $y],* do
 :::
 
 A {keywordOf Lean.Parser.Term.doFor}`for`​`…`​{keywordOf Lean.Parser.Term.doFor}`in` loop requires at least one clause that specifies the iteration to be performed, which consists of an optional membership proof name followed by a colon (`:`), a pattern to bind, the keyword {keywordOf Lean.Parser.Term.doFor}`in`, and a collection term.
-The pattern, which may just be an {tech}[identifier], must match any element of the collection; patterns in this position cannot be used as implicit filters.
+The pattern, which may just be an {tech}[識別子]identifier, must match any element of the collection; patterns in this position cannot be used as implicit filters.
 Further clauses may be provided by separating them with commas.
 Each collection is iterated over at the same time, and iteration stops when any of the collections runs out of elements.
 

Manual/Monads/Zoo.lean

@@ -157,8 +157,8 @@ For example, there might be a mutable {lean}`Nat` and a mutable {lean}`String` o
 As long as they have different types, it should be convenient to access both.
 In typical use, some monadic operations that are overloaded in type classes have type information available for {tech key:="synthesis"}[instance synthesis], while others do not.
 For example, the argument passed to {name MonadState.set}`set` determines the type of the state to be used, while {name MonadState.get}`get` takes no such argument.
-The type information present in applications of {name MonadState.set}`set` can be used to pick the correct instance when multiple states are available, which suggests that the type of the mutable state should be an input parameter or {tech}[semi-output parameter] so that it can be used to select instances.
-The lack of type information present in uses of {name MonadState.get}`get`, on the other hand, suggests that the type of the mutable state should be an {tech}[output parameter] in {lean}`MonadState`, so type class synthesis determines the state's type from the monad itself.
+The type information present in applications of {name MonadState.set}`set` can be used to pick the correct instance when multiple states are available, which suggests that the type of the mutable state should be an input parameter or {tech}[半出力パラメータ]semi-output parameter so that it can be used to select instances.
+The lack of type information present in uses of {name MonadState.get}`get`, on the other hand, suggests that the type of the mutable state should be an {tech}[出力パラメータ]output parameter in {lean}`MonadState`, so type class synthesis determines the state's type from the monad itself.
 
 This dichotomy is solved by having two versions of many of the effect type classes.
 The version with a semi-output parameter has the suffix `-Of`, and its operations take types explicitly as needed.
@@ -270,7 +270,7 @@ Providing the state type explicitly using {name}`getThe` from {name}`MonadStateO
 (getThe String, getThe Nat) : M String × M Nat
 ```
 
-Setting a state works for either type, because the state type is a {tech}[semi-output parameter] on {name}`MonadStateOf`.
+Setting a state works for either type, because the state type is a {tech}[半出力パラメータ]semi-output parameter on {name}`MonadStateOf`.
 ```lean (name := setNat)
 #check (set 4 : M Unit)
 ```

Manual/Monads/Zoo/Combined.lean

@@ -60,7 +60,7 @@ In one ordering, state changes are rolled back when exceptions are caught; in th
 The latter option matches the semantics of most imperative programming languages, but the former is very useful for search-based problems.
 Often, some but not all state should be rolled back; this can be achieved by “sandwiching” {name}`ExceptT` between two separate uses of {name}`StateT`.
 
-To avoid yet another layer of indirection via the use of {lean}`StateT σ (EStateM ε σ') α`, {name}`EStateM` offers the {name}`EStateM.Backtrackable` {tech}[type class].
+To avoid yet another layer of indirection via the use of {lean}`StateT σ (EStateM ε σ') α`, {name}`EStateM` offers the {name}`EStateM.Backtrackable` {tech}[型クラス]type class.
 This class specifies some part of the state that can be saved and restored.
 {name}`EStateM` then arranges for the saving and restoring to take place around error handling.