回想正規語言的幫浦引理——這次改用樹來做
回到正規語言的世界時，你用幫浦引理證明了 a^n b^n 不是正規語言。那個想法其實是鴿籠原理的偽裝：一台 DFA 只有有限多個狀態，所以在夠長的執行裡，它必定造訪某個狀態兩次，而這兩次造訪之間的迴圈可以被重複——也就是幫浦——生出新的被接受字串。這就逼住了任何字串無法容忍這種迴圈的語言。本階梯前一篇磨利了一個相關事實：上下文無關語言在某些運算下封閉，卻不在交集或補集下封閉，頭號反例正是 a^n b^n c^n。現在我們要打造真正能證明 a^n b^n c^n 不是上下文無關的工具。
對正規語言有效的訣竅——重複一個狀態——無法直接搬過來，因為下推自動機還多了一個無界的堆疊，所以「同一狀態出現兩次」不再代表「同一情境出現兩次」。取而代之，上下文無關語言的幫浦引理改而對著剖析樹推理，也就是文法賦予字串的結構。一個文法只有有限多個變數（非終端符號）。若字串很長，它的剖析樹一定很高；若樹很高，某條從根到葉的路徑一定會重複某個變數。那個重複的變數就是新的鴿籠，而兩份副本之間的那塊樹，正是我們可以幫浦的部分。
引理怎麼說：五段，其中兩段一起幫浦
陳述如下。對每個上下文無關語言 L，存在一個常數 p，稱為幫浦長度，使得 L 中每個長度 |s| 至少為 p 的字串 s 都能切成五段，s = u v x y z，並滿足三個條件。第一，|v y| 至少為 1——兩段可幫浦的部分至少有一段非空，所以我們不是在幫浦空無一物。第二，|v x y| 至多為 p——可幫浦的中段保持有界，這把那幾段釘在彼此附近。第三，也是核心：對每個 i = 0, 1, 2, …，字串 u v^i x y^i z 也在 L 裡。注意 v 與 y 帶著相同的指數 i：它們同步地一起變大變小。
把它和正規語言的引理比一比：後者把字串切成三段 x y z，幫浦單一中段 y。從一段可幫浦片段躍升到兩段，正是上下文無關語言的全部性格。堆疊以巢狀、成對的方式配對東西——進去時推入、出來時彈出——所以當某物重複時，它是以配對的一對在重複，就像多一層巢狀的左右括號。這正是為什麼 a^n b^n 是上下文無關的（一段 a 的 v 和一段 b 的 y 配對），而 a^n b^n c^n 不是：兩段可幫浦片段無法同時讓三個獨立的計數保持相等。
為什麼成立：一棵高的剖析樹一定重複某個變數
證明是對剖析樹做的一個乾淨的鴿籠論證，值得一看，因為這個證明的結構就是引理的意義。把文法化成每個節點至多有固定數目子節點的形式（喬姆斯基正規形就做到這點：每條規則是 A → B C 或 A → a，所以剖析樹是二元的）。一棵高度為 h 的二元樹至多有 2^h 片葉子。所以若字串 s 夠長——比 2^(變數個數) 還長——它的剖析樹高度必定超過變數個數，因而某條從根到葉的路徑長到足以重複某個變數，比方說 A 在同一條路徑上出現兩次。
想像那兩份 A 一個套在另一個裡面。較低的 A 推導出字串的某一塊——叫它 x，是最內層的產出。較高的 A 推導出更大的一塊，包含 x 加上它左右兩側的材料：左邊的材料是 v，右邊的材料是 y。較高的 A 之前的全部是 u，之後的全部是 z。於是 s = u v x y z。因為兩份副本都是同一個變數 A，掛在較高 A 底下的子樹與掛在較低 A 底下的子樹可以互換：A 能推導出 v A y，A 也能推導出 x。我們愛接幾次就接幾次。
Two copies of A on one path:
S
/
A <- upper A: derives v x y
/ | \
v A y <- lower A: derives x
|
x
A => v A y (the loop we can repeat)
A => x (the base, used to stop)
i=0: drop the loop -> u x z (pump down)
i=1: original -> u v x y z
i=2: loop twice -> u v v x y y z (pump up)
general: -> u v^i x y^i z for all i >= 0這就是那些條件的由來，一次全到齊。被幫浦的兩段恰好是 v 與 y，因為它們夾住內層子樹——所以它們總是以配對的形式一起成長。只要我們選的文法沒有無用的 epsilon（空字串）或單位規則的繞路，就保證較高的 A 確實比較低的 A 多產生一些東西，因而其中至少一段非空（|v y| 至少為 1）。而 |v x y| 保持至多為 p，是因為我們在那條路徑上挑的是最低的那個重複變數，使其子樹維持得很小。整個引理就是這一張圖，仔細讀就懂了。
運用它：對手遊戲與 a^n b^n c^n
要運用這個引理，你玩的是和正規語言情形相同的對手遊戲，只是現在有五段。你不能選 p，也不能選切法；這兩件都由對手決定。你只能選字串 s（聰明地，用 p 來表示）以及幫浦指數 i（用來逼出矛盾）。如果無論對手如何在遵守那兩個邊條件下把 s 切成 u v x y z，總有某個 i 的選擇把 u v^i x y^i z 踢出 L，那麼 L 就不可能是上下文無關的。技巧在於選 s，讓每一種合法的切法都注定失敗。
- 為導出矛盾，假設 L = { a^n b^n c^n : n >= 0 } 是上下文無關的，因此它有一個幫浦長度 p。
- 選取見證字串 s = a^p b^p c^p。它的長度是 3p，遠超過 p，所以引理適用於它。
- 讓對手把 s 切成 s = u v x y z，其中 |v y| 至少為 1 且 |v x y| 至多為 p。因為中段 v x y 長度至多為 p，它太短，無法橫跨全部三個字母區段——它至多只能碰到 a、b、c 三個字母中的兩種。
- 向上幫浦到 i = 2，得到 u v^2 x y^2 z。幫浦加入了 v 與 y 的副本，而它們合起來至多落在三個區段中的兩個，因此它至多只提高三個字母裡兩種的計數。
- 第三個字母的計數毫髮無傷，所以三個計數再也無法全部相等。因此新字串不再是 a^n b^n c^n 的形式，與它本應屬於 L 矛盾。（若某種切法混了順序，例如 v 同時含 a 與 b，會給出更糟的字串如 …abab…，照樣不在 L 裡。）故 L 不是上下文無關的。
停下來體會為什麼這對 a^n b^n c^n 有效，對先前的 a^n b^n 卻不行。只有兩個字母時，兩段可幫浦片段就夠了：v 可以待在 a 之間、y 待在 b 之間，讓兩個計數一起提高，所以 a^n b^n 撐過每一次幫浦，是上下文無關的。有三個字母時，兩段至多讓兩個區段同步；第三個就飄走。一個語言必須保持相等的獨立量的數目，對上引理只允許的兩段幫浦，就是那條分界線。這也正是為什麼a^n b^n c^n 標誌著上下文無關語言的邊界。
當兩段幫浦還不夠：奧格登引理
有時基本的幫浦引理太鈍。設想某個語言，它的長字串恰好含有一大塊好對付的區域——比方一長串某個無害的字母——對手可以把整個 v x y 視窗停在裡頭，只幫浦那段無害的字串，永遠不去動到你在意的部分。於是每次幫浦都留在 L 裡，基本引理什麼也揭不出來。字串雖長，但它的長度並沒有逼迫迴圈落在會痛的地方。
奧格登引理正是針對這個情況的更銳利工具。它讓你先把至少 p 個你選的位置標記為「特別」的，然後保證夾在它們之間被幫浦的片段 v 與 y 至少含有一個被標記的位置——迴圈被逼著穿過你標記的那個點，而不是溜進某個方便的填充區。基本幫浦引理就是把每個位置都標記起來的奧格登引理。有了標記，你還能證明某些語言是本質歧義的，這是樸素的引理辦不到的事。