问题
模式是字母表 ξ 上的非空词（变量 x,y,… 取任意 «值» 词）；无限词 w «避开» 模式 p，若 w 的任何因子都不是 p 的 «非恒同代入像»。例如 xx（平方）可被 3 字母表上的无限词避开（Thue），xyx 型 «重叠» 需 3 字母表、平方需 3、立方需 2。可避性判定问题：给定模式 p，判定是否存在有限字母表与无限词避开 p——这是词组合学的头号算法问题。基石定理：Bean–Ehrenfeucht–McNulty 与 Zimin（1979–82）刻画了 «不可避» 的模式——恰是 Zimin 词 Z1 = x1, Zn+1 = Znxn+1Zn（含 xx, xyx, xyxzxyx,…）。一般模式的判定算法不存在：单族结果大量（平方/重叠/幂、Abel 幂、公式），统一判定开放。
主要概念
Zimin 词与不可避性的机制
Zimin 词是 «递归加倍» 的模式：任何足够长的词都包含 Zimin 模式的代入像（«Zimin 增长引理»：长度 ≥ 2n 的词含 Zn 的像）。不可避定理的逆：非 Zimin 的模式皆可避——这把 «可避性» 从 «是否存在» 化为 «是不是 Zimin 型» 的结构判定，是问题中唯一 «完成» 的层。Zimin 词在泛代数侧等价于 «无有限基» 的构造（13 号 Perkins 反例链的语言学核心），在逻辑侧等价于 «一切序的良基性»（Zimin 的原动机），三线交汇。
阈值函数与判定难点的位置
对可避模式 p，定义 μ(p) = 避开 p 所需的最小字母表数。判定 «可避» 之后， «μ(p) 的上界» 是第二层（已知：一般可避模式 μ ≤ 2|p| 型的粗上界；平方的 μ = 3 是经典）。判定算法卡壳处：模式族随 «变量的重复模式» 组合爆炸， «单调性»（把 p 的变量换成新变量是否增加可避性）没有一般定理—— «局部替换的效应» 不可预测是算法化的真正障碍。
主要命题与证明
命题 1（低阶 Zimin 词的不可避免；完整证明） （i）k 字母表上任何长 ≥ k+1 的词含模式 xyx 的代入像（重叠型）；（ii）2 字母表上任何长 ≥ 4 的词含平方模式 xx 的像。故无限词必含 xyx 型与（2 字母表）xx 型。
证明 （i）取词的前 k+1 个字符，由鸽笼原理存在字符 a 出现两次：位置 i < j ≤ k+1，w(i) = w(j) = a。因子 w[i..j] = a·(中间段)·a 是 xyx 的像（x ↦ a，y ↦ 中间段）。（ii）设 2 字母表上的词 w[1..4] 无平方像，则相邻对不等：w(1) ≠ w(2)，w(2) ≠ w(3)，w(3) ≠ w(4)（否则该相邻对本身是 xx 像），故 w 严格交替：abab 或 baba，二者整体即平方 ab·ab（相应 baba = ba·ba），矛盾。□
命题 2（Zimin–BEM 定理，1979–82；文献口径陈述） 模式 p 不可避（不存在任何有限字母表上的无限词避开 p）⟺ p 与某 Zimin 词 Zn «形态等价»（重命名变量后的同构）。证明组合 «不可避 ⟹ Zimin 型»（Zimin 的递归构造）与 «Zimin 词不可避»（任意有限字母表上，足够长的词必含 Zimin 像——该方向的阈值与字母表大小相关，原文给出精确界）。
现状说明 定理完成 «可避 ⟺ 非 Zimin» 的二分，但判定算法需要的是 «给定 p，计算 μ(p) 或至少判定 μ(p) < ∞»——二分已给 «有限性»（非 Zimin ⟹ 有限），算法问题剩下 «计算阈值» 与 «Zimin 型识别»（后者显然可判定）；真正的开放层是 «可避模式下阈值的可计算性» 及统一算法。□
命题 3（经典阈值：Thue 的平方避开；完整证明骨架） 3 字母表 {0,1,2} 上存在无限词避开平方模式 xx（Thue 1912；现代证明用 «均匀形态» 或 «重写系统» 的不变子集构造）。
骨架 取 morphism σ : 0 ↦ 012, 1 ↦ 02, 2 ↦ 1 与 «无平方核» 的归纳保持：从核词 ε 出发，逐次应用 σ 并验证 «σ 保持无平方性»（对无平方词 w，σ(w) 无平方的验证归约到 «σ 的像对之间的短重叠检查»——有限情形表）。无限词 = 核链的极限。2 字母表上 xx 不可避（任何 2 元长 ≥ 4 的词含平方——4 个 «奇偶位置» 的鸽笼论证：长 4 的 2 元词中位置 {1,3} 与 {2,4} 的对必有相同对 ⟹ xx 像）。⟹ 阈值 μ(xx) = 3 精确。□
进展与文献
Thue（1912，平方与立方）；Bean–Ehrenfeucht–McNulty（1979）与 Zimin（1982）的不可避定理；Lothaire《Combinatorics on Words》相应章节；Shur 的可避模式与阈值计算（2000 年代–2010 年代）。开放核心：一般可避模式的阈值可计算性； «公式»（多模式联合避让）的判定；与 Abel 幂（16 号）、符号动力学（低复杂度系统避开能力）的接口。