在 形式语言的理论中，正则语言的泵引理 是一个 引理， 它描述了所有正则语言的基本属性。非正式地说，这个引理描述的是，在一种常规语言中，所有足够长的单词都可以通过 泵 ——即让单词的某非零部分重复任意次数——产生依然位于同一语言中的新单词。
具体来说，泵引理描述的是，对于任一常规语言 ，总存在一个常数 ，使得任何长度至少为 的单词 在 中可以分成三个子串， ，其中中间部分 一定不能是空的，这样的话 通过重复构建 零次或更多次得到的结果仍然在 。这种重复过程被称为“泵”。此外，泵引理限制了 可能的拆分方式，保证 的长度最长为 。有限语言 显然地 满足泵引理： 等于 中的最大字符串长度加一。
泵引理对于证伪特定语言的正则性是有用的。它最先在1959年被 迈克尔·拉宾 和 达纳·斯科特 证明，[1] 不久后在1961年被 Yehoshua Bar-Hillel, Micha A. Perles和 Eli Shamir再次发掘，提出了简化版本：上下文无关语言的泵引理。[2][3]
是一种正则语言，那么存在一个仅取决于 的整数 ，使得每一个在 中，长度至少为 的字符串 （ 被称为“泵长度”[4])可以写成 (即， 可分为三个子串)，并满足以下条件:
是可以被抽取或泵入的子字符串(移除或重复任意次，结果字符串总是在 中)。(1)指 的长度至少为一；(2)表示泵送 产生的循环必须在前 个字符中。|x|必须小于 (结论(1)和(2))，但除此之外，对 和 没有其他限制。
简而言之，对于任何正则语言 ，任何足够长的单词 (在 中)可以被分成3部分，即 ，使得所有满足 的字符串都在 中。
下面是泵引理的一个形式表达式。
泵引理经常被用来证明一种特定的语言是非正则的：用反证法 (对于语言的正则性)，举出一个在语言中(符合要求长度的)单词，该单词缺少泵引理中概述的属性。
例如，语言 在字母表上 可以证明是非正则的，如下所示:
设 ，和 为上面泵引理的形式化描述中使用的符号。我们假设存在常数 ，在 中的 由 给出， 它是一个长度大于 的字符串。由泵引理，一定存在某种分解 满足 和 ，同时使得所有的 ， 都在 中 。因为有 ，我们知道 仅由 的实例组成 。 此外，因为 ，它至少包含字母 的一个实例 。我们现在泵入 : 中 的实例 的要多，因为我们增加了 的实例，而没有增加 的实例。因此， 不在 中。结果与假设矛盾。因此， 是正则的(即存在这样一个 )这个假设一定是不正确。因此 是非正则的。
证明匹配(即合适嵌套)括号语言为非正则遵循同样的想法。给定一个长度 ，那一定存在一串左右匹配的括号，开头全为超过 长度的左括号，这样 将完全由左括号组成。 通过重复 ，我们可以生成一个不包含相同数量左括号和右括号的字符串，因此它们不能平衡。
每种正则语言都存在一个 有限状态自动机 (FSA)与其对应。这种FSA中的状态数是有限的，这个状态数就是 泵长度 。对于一长度至少为 的字符串， 为开始状态， 是当字符串传入FSA之后到达的 个状态组成的序列，。 因为FSA只有 个状态，在这个序列中 被访问的状态中至少有一个状态是重复的。用 来表示这个状态。状态机从第一次跳到状态 到第二次跳变到 之间的转移过程中会匹配一个字符串， 在引理中，这个字符串叫做 ，因为不管去除 还是令字符串 重复任何次数，状态机都能匹配到这些字符，泵引理的所有条件都得到满足。
例如，下图显示了一个FSA。
FSA接受字符串: abcd。由于该字符串的长度至少与状态的数量一样大，也就是4，由鸽笼原理可知在开始状态和接下来的四个访问状态中必须至少有一个重复状态。在本例中，只有 是重复状态。因为对于子字符串bc，状态机从状态 开始，又结束于状态 ，这部分的状态转移可以重复进行，给出字符串abcbcd，FSA仍然会接受。 或者也可以删除 bc 部分，FSA仍将接受给出的字符串 ad。就泵引理而言，字符串 abcd 可以被分解为三部分： 部分包含字符串a， 部分包含bc 和 部分包含 d。
虽然泵引理声明所有的正则语言都满足上述条件，但这种说法的逆命题是不正确的：满足这些条件的语言可能仍然是非正则的。换句话说，泵引理的原始版本和一般版本都给出了一个正则语言的必要不充分条件。
例如，考虑以下语言:
。
换句话说， 包含字母表 中包含所有长度为3的子字符串中有一个重复字符的字符串，以及该字母表上的所有符合1/7的字符是‘3’的字符串。这种语言是非正则的，但在 情况下仍然可以被“泵入”或“抽取”。假设字符串 s 长度至少为5。然后，因为字母表只有四个字符，所以字符串前五个字符中至少有两个是重复的。它们最多可以被三个字符分隔（有三个字符夹在两个重复字符之间）。
麦卡勒定理 提供了一个精确表征正则语言的测试。 证明语言是正则的典型方法是为语言构造一个 有限状态机 或者 正则表达式。
^Rabin, Michael; Scott, Dana (Apr 1959). "Finite Automata and Their Decision Problems" (PDF). IBM Journal of Research and Development. 3 (2): 114–125. doi:10.1147/rd.32.0114. Archived from the original on December 14, 2010.CS1 maint: Unfit url (link) Here: Lemma 8, p.119.
^Bar-Hillel, Y.; Perles, M.; Shamir, E. (1961), "On formal properties of simple phrase structure grammars", Zeitschrift für Phonetik, Sprachwissenschaft und Kommunikationsforschung, 14 (2): 143–172.
^John E. Hopcroft; Rajeev Motwani; Jeffrey D. Ullman (2003). Introduction to Automata Theory, Languages, and Computation. Addison Wesley. Here: Sect.4.6, p.166.
^Berstel, Jean; Lauve, Aaron; Reutenauer, Christophe; Saliola, Franco V. (2009). Combinatorics on words. Christoffel words and repetitions in words. CRM Monograph Series. 27. Providence, RI: American Mathematical Society. p. 86. ISBN 978-0-8218-4480-9. Zbl 1161.68043..
^Savitch, Walter (1982). Abstract Machines and Grammars. p. 49. ISBN 978-0-316-77161-0..
^John E. Hopcroft & Jeffrey D. Ullman (1979). Introduction to Automata Theory, Languages, and Computation. Reading/MA: Addison-Wesley. ISBN 978-0-201-02988-8. Here: p. 72, Exercise 3.2 (which give a slightly less general version, requiring |w|=p) and 3.3.
暂无