From 725c4a5244e145f47d34b57af2f44575e3600867 Mon Sep 17 00:00:00 2001 From: s-taiga <56785231+s-taiga@users.noreply.github.com> Date: Sat, 14 Dec 2024 15:22:41 +0900 Subject: [PATCH] =?UTF-8?q?=E8=AA=A4=E5=AD=97=E4=BF=AE=E6=AD=A3=20(#93)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 目についた誤字修正 * 訳注追記 --- .../src/getting-to-know/functions-and-definitions.md | 6 ++++-- functional-programming-lean/src/next-steps.md | 6 ++++-- .../src/programs-proofs/arrays-termination.md | 2 +- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/functional-programming-lean/src/getting-to-know/functions-and-definitions.md b/functional-programming-lean/src/getting-to-know/functions-and-definitions.md index 8bddefa9..f0fd29bf 100644 --- a/functional-programming-lean/src/getting-to-know/functions-and-definitions.md +++ b/functional-programming-lean/src/getting-to-know/functions-and-definitions.md @@ -184,7 +184,7 @@ When it makes sense to do so, natural number literals can be used for new types, This is part of Lean's mission of making it convenient to represent mathematics, and different branches of mathematics use number notation for very different purposes. The specific feature that allows this overloading does not replace all defined names with their definitions before looking for overloading, which is what leads to the error message above. --> -このエラーは、Lean が数値リテラルのオーバーロード(overload)を許可しているために発生します。自然数リテラルは、あたかもその型がシステムに組み込まれているかのように、新しい型に使用することができます。これは、数学の表現を便利にするという Lean の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。 +このエラーは、Lean が数値リテラルの**オーバーロード**（overload）を許可しているために発生します。ある型に対して数値リテラルのオーバーロードを適切に設定することで、自然数リテラルはあたかもその型がシステムに組み込まれているかのように、新しい型に使用することができます。これは、数学の表現を便利にするという Lean の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。 [^fn1] @@ -224,4 +224,6 @@ Definitions that are to be unfolded are called _reducible_. Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand. Definitions produced with `abbrev` are marked as reducible. --> -舞台裏では、オーバーロードの解決時に、展開可能(unfoldable)であると内部でマークされる定義もあれば、そうでない定義もあります。展開される定義は *reducible* (簡約可能)と呼ばれます。Lean をスケールさせるためには、定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると、型が非常に大きくなり、機械が処理するのに時間がかかりますし、ユーザにとっても理解しづらいものになります。`abbrev` で生成された定義は reducible であるとマークされます。 \ No newline at end of file +舞台裏では、オーバーロードの解決時に、**展開可能**（unfoldable）であると内部でマークされる定義もあれば、そうでない定義もあります。展開される定義は**簡約可能**（reducible）と呼ばれます。Lean をスケールさせるためには、定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると、型が非常に大きくなり、機械が処理するのに時間がかかりますし、ユーザにとっても理解しづらいものになります。`abbrev` で生成された定義は reducible であるとマークされます。 + +[^fn1]: 訳注：この機能は[後の章](https://lean-ja.github.io/fp-lean-ja/type-classes/pos.html#%E6%95%B0%E5%80%A4%E3%83%AA%E3%83%86%E3%83%A9%E3%83%AB)で詳しく解説されます。 diff --git a/functional-programming-lean/src/next-steps.md b/functional-programming-lean/src/next-steps.md index eb138dc5..4d2416de 100644 --- a/functional-programming-lean/src/next-steps.md +++ b/functional-programming-lean/src/next-steps.md @@ -35,7 +35,7 @@ Lean4そのものについては以下のリソースで記述されています * [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/) はLeanで証明を書くためのチュートリアルです。[^fn1] * [The Lean 4 Manual](https://leanprover.github.io/lean4/doc/) はLean言語とその機能のリファレンスを提供しています。本書執筆時点ではまだ不完全ですが、本書よりもLeanの多くの側面が詳細に記述されています。 * [How To Prove It With Lean](https://djvelleman.github.io/HTPIwL/) は [_How To Prove It_](https://www.cambridge.org/highereducation/books/how-to-prove-it/6D2965D625C6836CD4A785A2C843B3DA#overview) という定評のある教科書のLeanベースの付録であり、紙と鉛筆で数学的証明を書くための入門書です。 - * [Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book) は中置演算子や記法などからマクロ・カスタムのタクティク・完全にカスタムな組み込み言語まで、Leanの拡張メカニズムの概要を提供しています。 + * [Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book) は中置演算子や記法などからマクロ・カスタムのタクティク・完全にカスタムな組み込み言語まで、Leanの拡張メカニズムの概要を提供しています。 [^fn4] * [Functional Programming in Lean](https://lean-ja.github.io/fp-lean-ja/) は再帰に関するジョークが好きな読者には面白いかもしれません。 [^fn3] - 1. 配列はパタンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために [証明の義務](../props-proofs-indexing.md) が課せられます。 + 1. 配列はパターンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために [証明の義務](../props-proofs-indexing.md) が課せられます。 2. 配列全体を左から右に処理するループは末尾再帰関数ですが、呼び出すたびに減少する引数を持ちません。