Ogden 引理（Ogden's lemma）
/ Ogden: OG-den /
有時候原始的上下文無關幫浦引理太弱了：語言確實不是上下文無關，但引理允許 v x y 放在哪裡的自由度，讓你假想的對手總能找到一個留在語言內的「安全」切法。Ogden 引理用「讓你插旗」來修補這點。在切法發生「之前」，你把字串中某些位置標記為「特選的」（distinguished），引理便逼得被抽取的部分必須真的「用到」你標記的位置——奪走對手的逃生路線。
精確地說：對上下文無關語言 L，存在常數 p，使得若 z 屬於 L 且你「標記」了 z 中至少 p 個位置，則 z 切成 u v x y z'，並滿足三個被強化的條件：(1) v 與 y 合起來至少含一個被標記的位置（|v y| 含 >= 1 個標記，所以抽取不能溜進未標記的填料裡）；(2) 窗口 v x y 至多含 p 個被標記的位置（不是至多 p 個符號——界限是針對「標記」）；(3) 對每個 i >= 0，u v^i x y^i z' 屬於 L。普通幫浦引理正是「把所有位置都標記」的 Ogden 引理特例，所以 Ogden 引理「嚴格」更強——原始引理能做的每件事它都能做，還能做更多。
回報是觸及範圍。Ogden 引理能證明原始引理碰不到的語言「不」是上下文無關，也是顯示某些文法「先天歧義」（inherently ambiguous，語言的任何文法都避不開歧義）的標準工具。它能乾淨處理的著名例子是 { a^i b^j c^k d^l : i = 0 或 j = k = l }，你標記 b、c 或 d 來逼抽取進入那個必須保持平衡的部分。和每個幫浦式引理一樣，它是必要而非充分——通不過它就證明了非上下文無關性，但滿足它證明不了任何正面結論。
對 L = { a^i b^j c^k d^l : i = 0 或 j = k = l }，原始引理很吃力，因為 i = 0 這個逃生口總能提供一個安全切法。比如把所有 b 都標記：Ogden 引理逼得 v 與 y 包含被標記的 b，抽取於是破壞 j = k = l 的平衡，揭出原始引理揭不出的矛盾。
標記位置以把抽取逼到你要的地方——一個比原始 CFL 幫浦引理嚴格更強的工具。
條件 (2) 的界限算的是「被標記」的位置、不是所有符號——這是常見的混淆。Ogden 引理推廣了原始幫浦引理（把全部標記起來），但和它一樣是必要而非充分。