所以我有这个问题，我正在研究关于上下文无关语法的归纳证明。
鉴于这个语法
S-> aSb | 不锈钢 | 抗体
使用归纳法证明文法生成的字符串不以abb开头。
很容易看出这实际上是正确的，但是我对如何对其进行正式证明有一些问题。
我正在考虑对单词的长度使用按值归纳的课程，或者对推导的长度使用按值归纳的课程（在这种情况下，我真的不知道哪个更好）。
让我们对推导的长度使用归纳法。
基本情况：推导的长度是一步，那么唯一的可能性是 S-> ab，这显然成立。
归纳假设：如果 S=>w' 有 n 个推导（n>0），则 w' 不以 abb 开头
感应步：？？？
归纳步骤是我遇到问题的地方，我真的不明白该怎么做。
我想知道是否有人可以解释我应该在那里做什么？
谢谢！
对于 n 的任何归纳，基本情况是 P(0) 或 P(1)，归纳假设是 P(n)，归纳步骤是证明 P(n) 蕴含 P(n+1)。所以你希望你的归纳步骤是：
归纳步骤：假设对于所有 w' 使得 S => w' 具有 n 个推导步骤，w' 不以字符串 abb 开头，证明对于所有 w'' 使得 S => w'' 具有 n+1推导步骤，w'' 不以字符串 abb 开头。
换句话说：如果对于所有长度为 n 的推导，我们具有 w 不以 abb 开头的性质，我们希望证明对于所有长度为 n+1 的推导，相同的性质成立。
每个长度为 n+1 的推导都有 S -> aSb、s -> SS 或 s -> ab 之一。（如果我们要求 n > 0，则最后一个不适用。）所以您需要案例分析。
案例 1：S -> aSb。如果 S 可以扩展为单个 b，或扩展为以 bb 开头的字符串，我们就反驳了结论。如果我们可以证明语言中没有单词以 b 开头，或者等价地每个单词都以 a 开头，我们就可以建立这种情况的结论。
案例 2：S -> SS。初始字符串 abb 必须是
归纳假设排除了其中的第一个和最后一个。那么有多少种方法可以定义第一个 S 和第二个 S 之间的前缀 'abb'？我数了两个：'a' + 'bb' 和 'ab' + 'b'。如果我们能证明这在任何语言中都是不可能的，那么我们就自由了。
所以，如果我的任务是产生这个证明，我会首先证明语言中没有任何单词以“b”开头，然后用它来处理这两种情况。