# 术语：induction **URL:** \ **Category:** 翻译\ **Created:** [March 21, 2019, 1:03am UTC](https://discourse.rocq-prover.org/t/induction/240 "2019-03-21T01:03:53Z")\ **Posts on this page:** 16\ **Page:** 1

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [March 21, 2019, 1:03am UTC](https://discourse.rocq-prover.org/t/induction/240/1 "2019-03-21T01:03:53Z")

在 Coq 中，`induction` 策略的理论基础为 [structural induction](https://en.wikipedia.org/wiki/Structural_induction)，中文维基称其为“[结构归纳法](https://zh.wikipedia.org/wiki/%E7%BB%93%E6%9E%84%E5%BD%92%E7%BA%B3%E6%B3%95)”。但“归纳”二字易同“[归纳推理](https://zh.wikipedia.org/wiki/%E5%BD%92%E7%BA%B3%E6%8E%A8%E7%90%86)”混淆。诚然英语亦面临此问题，但汉语能否更通达地表述此概念？已知掣肘因素如：“数学归纳法”是 structural induction 在自然数之特例，此概念在中学已普及。請教台灣同仁：國語中“歸納”是否兼具 inductive reasoning 和 structural induction 含義？ ---

**Author:** ![HuStmpHrrr](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hustmphrrr/32/42_2.png) [@HuStmpHrrr](https://discourse.rocq-prover.org/u/HuStmpHrrr)\ **Post date:** [March 22, 2019, 4:18am UTC](https://discourse.rocq-prover.org/t/induction/240/2 "2019-03-22T04:18:25Z")

我不是认真的：我总觉得中英的逻辑和数学用语陷入一种困境。一方面，如果英语的用了一个用烂的词指代一个特定的概念，那么中文的意思表达就特定得多。比方说群（group），环（ring），格（lattice)，范畴（category），中文都比英文要好太多。但是另一方面，如果术语用到的是组合型的词汇，那英语实在是好太多了。这些词汇的中文翻译简直无法直视，意思也难以表达。比方说morphism, intuitionism, homotopy等。最后点一下题：翻译的话我觉得归纳法就挺好的，毕竟中学也是这么教的。没必要修改译法，免得和大部分人的固有知识不匹配。 ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [March 22, 2019, 5:20am UTC](https://discourse.rocq-prover.org/t/induction/240/3 "2019-03-22T05:20:59Z")

试释之：归纳者，归有限以纳无穷也。演绎者，循式列陈诸言，以竟厥辞也；其中结构归纳者，穷其里，俱现其外也。虽无穷者，皆整础也，故言之凿凿。几经查阅，[日](https://ja.wikipedia.org/wiki/%E6%A7%8B%E9%80%A0%E7%9A%84%E5%B8%B0%E7%B4%8D%E6%B3%95)[韩](https://ko.wikipedia.org/wiki/%EC%88%98%ED%95%99%EC%A0%81_%EA%B7%80%EB%82%A9%EB%B2%95)[越](https://vi.wikipedia.org/wiki/Quy_n%E1%BA%A1p_to%C3%A1n_h%E1%BB%8Dc)均以“归纳”论上述两概念，我也觉得与其逆四国通行之用法，不如将“结构归纳”诠释为：通过演绎，实现严谨的归纳。 ---

**Author:** ![sora](https://avatars.discourse-cdn.com/v4/letter/s/ad7895/32.png) [@sora](https://discourse.rocq-prover.org/u/sora)\ **Post date:** [March 23, 2019, 5:07am UTC](https://discourse.rocq-prover.org/t/induction/240/4 "2019-03-23T05:07:35Z")

无论如何，在我们使用的严格的语境（sf 的翻译中，比如）下，常见的“归纳推理”不出现在任何地方，所以我觉得没有辨析的需要。 ~~所~~~~ 谓 ~~~~数~~~~ 学 ~~~~归~~~~ 纳 ~~~~法~~~~ 的 ~~~~，~~~~ 就 ~~~~已~~~~ 经 ~~~~是~~~~ “ ~~~~通~~~~ 过 ~~~~演~~~~ 绎 ~~~~，~~~~ 实 ~~~~现~~~~ 严 ~~~~谨~~~~ 的 ~~~~归~~~~ 纳 ~~~~”~~~~ 的 ~~~~了~~~~ 。 ~~~~只~~~~ 是 ~~~~此~~~~ 处 ~~~~我~~~~ 们 ~~~~使~~~~ 用 ~~~~CIC~~~~ ， ~~~~才~~~~ 会 ~~~~出~~~~ 现 ~~~~“~~~~ 结 ~~~~构~~~~ ” ~~~~的~~~~ 。 ~~~~数~~~~ 学 ~~~~上~~~~ ， ~~~~还~~~~ 有 ~~~~其~~~~ 他 ~~~~乱~~~~ 七 ~~~~八~~~~ 糟 ~~~~的~~~~ 归 ~~~~纳~~~~ 法 ~~~~，~~~~ 就 ~~~~是~~~~ 大 ~~~~体~~~~ 跟 ~~~~ well ~~~~-~~~~ founded ~~~~对~~~~ 应 ~~~~的~~~~ 那 ~~~~些~~~~ ， ~~~~我~~~~ 们 ~~~~可~~~~ 以 ~~~~在~~~~ 不 ~~~~是~~~~ “ ~~~~序~~~~ 列 ~~~~”~~~~ 而 ~~~~是~~~~ “ ~~~~网~~~~ ” ~~~~或~~~~ 者 ~~~~“~~~~ 滤 ~~~~子~~~~ ” ~~~~上~~~~ 做 ~~~~归~~~~ 纳 ~~~~，~~~~ 毕 ~~~~竟~~~~ 归 ~~~~纳~~~~ 这 ~~~~事~~~~ 情 ~~~~只~~~~ 跟 ~~~~序~~~~ 结 ~~~~构~~~~ 有 ~~~~关~~~~ 系 ~~~~。~~~~ 在 ~~~~这~~~~ 些 ~~~~情~~~~ 况 ~~~~下~~~~ ， ~~~~都~~~~ 没 ~~~~有~~~~ 使 ~~~~用~~~~ “ ~~~~结~~~~ 构 ~~~~归~~~~ 纳 ~~~~法~~~~ ” ~~~~的~~~~ 先 ~~~~例~~~~ ， ~~~~或~~~~ 者 ~~~~说~~~~ ， ~~~~“~~~~ 数 ~~~~学~~~~ 归 ~~~~纳~~~~ 法 ~~~~”~~~~ 的 ~~~~意~~~~ 涵 ~~~~已~~~~ 经 ~~~~足~~~~ 够 ~~~~ general ~~~~了~~~~ 。~~（事实错误） ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [March 23, 2019, 6:58am UTC](https://discourse.rocq-prover.org/t/induction/240/5 "2019-03-23T06:58:20Z")

> [@sora](#): > > 无论如何，在我们使用的严格的语境（sf 的翻译中，比如）下，常见的“归纳推理”不出现在任何地方，所以我觉得没有辨析的需要。此处讨论的翻译事宜不限于特定教材，旨在为整个中文数理科学社区提供参考。 > [@sora](#): > > 数学上，还有其他乱七八糟的归纳法，就是大体跟 well-founded 对应的那些，我们可以在不是“序列”而是“网”或者“滤子”上做归纳，毕竟归纳这事情只跟序结构有关系。在这些情况下，都没有使用“结构归纳法”的先例，或者说，“数学归纳法”的意涵已经足够 general 了。视野内关于数学归纳法的讨论似乎均面向自然数，故建议以“结构归纳法”谓广义狭义之辨。 ---

**Author:** ![sora](https://avatars.discourse-cdn.com/v4/letter/s/ad7895/32.png) [@sora](https://discourse.rocq-prover.org/u/sora)\ **Post date:** [March 23, 2019, 7:01am UTC](https://discourse.rocq-prover.org/t/induction/240/6 "2019-03-23T07:01:23Z")

那是统统用结构归纳法还是用数学归纳法 when possible 呢？ ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [March 23, 2019, 7:34am UTC](https://discourse.rocq-prover.org/t/induction/240/7 "2019-03-23T07:34:03Z")

**“数学归纳法”甚普及，可用作体词。** 例：[加法结合律](https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html#lab54) 定理：对任意自然数 `n`、`m`、`p`，均有：`n + (m + p) = (n + m) + p`。证明： **以数学归纳法对 `n` 分类讨论：** - 对于 `n = 0`：试论：`0 + (m + p) = (0 + m) + p`。由加法之定义，上式显而易见。 - 对于 `n = S n'`，其中 `n'` 满足 `n' + (m + p) = (n' + m) + p`：试论： `(S n') + (m + p) = ((S n') + m) + p`。由加法之定义，上式等价于： `S (n' + (m + p)) = S ((n' + m) + p)`。据归纳假设，上式显而易见。证毕。 **“结构归纳法”可简称“归纳”，用作谓词。** 例：[链表联接结合律](https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html#lab81) 定理：对任意链表 `l1`、`l2`、`l3`，均有：`(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)`。证明： **归纳讨论 `l1` 之构造：** - 对于 `l1 = []`：试论：`([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)`。由链表联接之定义，上式显而易见。 - 对于 `l1 = n::l1'`，其中 `l1'` 满足 `(l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)`：试论：`((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3)`。由链表联接之定义，上式等价于： `n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)`。据归纳假设，上式显而易见。证毕。 ---

**Author:** ![sora](https://avatars.discourse-cdn.com/v4/letter/s/ad7895/32.png) [@sora](https://discourse.rocq-prover.org/u/sora)\ **Post date:** [March 23, 2019, 8:09am UTC](https://discourse.rocq-prover.org/t/induction/240/8 "2019-03-23T08:09:01Z")

那鉴于“数学归纳法”是“结构归纳法”的特例，用法不同恐怕要引发疑惑？另外，我觉得“以数学归纳法对 `n` 分类讨论”中提到 **分类讨论** 实际模糊了重点。中文文献（不光是中译文献，毕竟数学家平时也会说到归纳法）中，常见的用法是 - 对 n 用数学归纳法 - 对 n 用归纳法（保持 m 固定） - 用数学归纳法下面这样的才是可见于教材的论述文字。 - 证明：用归纳法。`n = 0` 时，易得结论成立。现假设 `n = k` 时结论成立，则对于 `n = k + 1` 有… 这不仅是个翻译问题，甚至，完全不是个翻译问题：对数学归纳法一词的使用，在中文语境里早有定式。更武断一点，我认为，没有数学家会用“以数学归纳法对 `n` 分类讨论”这种说法。 ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [March 23, 2019, 1:31pm UTC](https://discourse.rocq-prover.org/t/induction/240/9 "2019-03-23T13:31:18Z")

> [@sora](#): > > - 对 n **用** 数学归纳法 > - 对 n **用** 归纳法（保持 m 固定） > - **用** 数学归纳法你提到的三种用法，谓语均为“用”。该动词虚无缥缈，不表示任何动作。我因此代之以“讨论”，并前置“归纳”为状语。命名定式尚可鉴，修辞糟粕不得取。 ---

**Author:** ![sora](https://avatars.discourse-cdn.com/v4/letter/s/ad7895/32.png) [@sora](https://discourse.rocq-prover.org/u/sora)\ **Post date:** [March 23, 2019, 2:36pm UTC](https://discourse.rocq-prover.org/t/induction/240/10 "2019-03-23T14:36:34Z")

用“用”并没什么问题吧，否则要是开头是别的提示文字，你怎么对应？ - 证明：用归纳法。和 - 证明：用 Zorn’s Lemma。有一样的结构，这样的相似性是我不愿意失去的。把这些文字放在证明的最开头，只是点明构成证明主体的 **主要工具 n.** ，不应该要费心挑一个谓语（因为不是重点）。现在这样恐怕是能找到的最简练最强调重点的说法了。要是“我们用归纳法来证明定理1”这种，你准备如何调整？ ~~另外，称共同体的选择为糟粕可是很严肃的指控啊。~~ 🤪 ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [March 23, 2019, 8:49pm UTC](https://discourse.rocq-prover.org/t/induction/240/11 "2019-03-23T20:49:38Z")

> [@sora](#): > > 用“用”并没什么问题吧 “用”可用于动宾短语作状语，例如你提到的： > [@sora](#): > > 我们用归纳法来 **证明** 定理1 此句谓语“证明”是具体的动作，故可取。 > [@sora](#): > > 另外，称共同体的选择为糟粕可是很严肃的指控啊。所谓共同体，数学水平我惮于指控，但落笔佶屈聱牙，令学生头痛不堪，此吾敢言也。 ---

**Author:** ![luochen1990](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/luochen1990/32/141_2.png) [@luochen1990](https://discourse.rocq-prover.org/u/luochen1990)\ **Post date:** [July 10, 2019, 9:50am UTC](https://discourse.rocq-prover.org/t/induction/240/12 "2019-07-10T09:50:01Z")

“结构归纳法”是个直译的专有名词呀, 并且我觉得这个直译非常的达意, 没有必要在这种地方搞创新. 另外 “数学归纳法” 中的 “数学”, 特指 “算术”, 指对自然数运用归纳法, 这个意思也非常明确, 建议不要混淆两者. ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [July 10, 2019, 5:01pm UTC](https://discourse.rocq-prover.org/t/induction/240/13 "2019-07-10T17:01:49Z")

暂定遣词循惯例，造句略区分，例： > [@术语：induction](https://discourse.rocq-prover.org/t/induction/240/7): > > “数学归纳法”甚普及，可用作体词。例：[加法结合律](https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html#lab54) 定理：对任意自然数 n、m、p，均有：n + (m + p) = (n + m) + p。证明：以数学归纳法对 n 分类讨论：对于 n = 0：试论：0 + (m + p) = (0 + m) + p。由加法之定义，上式显而易见。对于 n = S n'，其中 n' 满足 n' + (m + p) = (n' + m) + p：试论： (S n') + (m + p) = ((S n') + m) + p。由加法之定义，上式等价于： S (n' + (m + p)) = S ((n' + m) + p)。据归纳假设，上式显而易见。证毕。 “结构归纳法”可简称“归纳”，用作谓词。例：[链表联接结合律](https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html#lab81) 定理：对任意链表 l1、l2、l3，均有：(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)。证明：归纳讨论 l1 之构造：对于 l1 = []：试论：([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)。由链表联接之定义，上式显而易见。对于… 请批评指正。 ---

**Author:** ![HuStmpHrrr](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hustmphrrr/32/42_2.png) [@HuStmpHrrr](https://discourse.rocq-prover.org/u/HuStmpHrrr)\ **Post date:** [August 4, 2019, 6:04pm UTC](https://discourse.rocq-prover.org/t/induction/240/14 "2019-08-04T18:04:16Z")

我认为数学归纳法歧义很大，数学归纳法可以是对n的structural induction；也可以是对某个k的k-induction；也可以是strong induction。可以避免的时候应该尽量避免。 ---

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\ **Post date:** [August 5, 2019, 8:57am UTC](https://discourse.rocq-prover.org/t/induction/240/15 "2019-08-05T08:57:26Z")

你的建议是 structural induction 均译为“结构归纳”，而不考虑对象是否为自然数？这样确实更为精准。 ---

**Author:** ![HuStmpHrrr](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hustmphrrr/32/42_2.png) [@HuStmpHrrr](https://discourse.rocq-prover.org/u/HuStmpHrrr)\ **Post date:** [August 5, 2019, 4:07pm UTC](https://discourse.rocq-prover.org/t/induction/240/16 "2019-08-05T16:07:39Z")

对，无须考虑。本质上也就只有structural induction，没必要引入多种术语引起歧义。