Vince Jiang

CSCI3130 / 课程伴读 · 本站更新

CSCI3130 L00 Part 2/4 Course Objectives

课程：CSCI3130 Formal Languages and Automata Theory · 2026T1 本讲：L00 Part 2/4 Course Objectives · 原件 L00-课程简介-2026T1.pdf（本地课件） p.13–15 定位：把“学会构造一个程序”和“证明一个模型能做什么”区分开，明确后续学习所需的推理能力。 前后：上一份 L00-P1-课程安排.md · 下一份 L00-P3-计算模型.md

p.13 Outline 分节页。

Course Objectives

为什么学计算理论（p.14–15）【新】

p.14 To strengthen students’ ability to carry out formal and rigorous mathematical arguments

p.14 给出的目标不是某一门编程语言的语法，而是计算机科学的基础、后续课程所需的概念、问题求解能力和严格数学论证。形式化的作用是消除歧义：例如“机器能认出这类字符串”需要说明允许什么输入、机器有什么记忆、怎样运行、何时算接受。缺少任一项，两个看似争论同一问题的人，可能其实使用了不同模型。

补充：构造与证明通常配套出现。先造出自动机只是候选答案；还需证明它接受每个合法串，并拒绝每个不合法串。只试过几个字符串，不能替代对全部字符串的论证。后续反例法、归纳法、泵引理分别服务于不同方向的证明。

p.15 the ability to reason about what the code means, whether it is correct, and whether a computational problem is solvable at all

p.15 把这些目标放到 AI 生成代码的场景：代码更容易产生，并不意味着其意义、正确性、可计算性已经解决。“跑通一个例子”“对所有输入都正确”“存在某种算法能解决这个问题”是三个不同强度的主张。这页还列自动机、文法和形式推理在约束生成、程序验证中的关联；本页没有给出具体 AI 算法，因此不把这些应用名词扩写成课程已教授的技术。

把 p.14 的四项目标逐项落实到本课：计算机科学基础对应“模型有哪些能力”；后续课程准备对应“编译、算法分析可以复用哪些结构”；问题求解对应“怎样构造机器或文法”；严格论证对应“怎样保证构造覆盖全部而且只覆盖合法输入”。这四项一起解释了为什么课程既有图、规则，也有证明。

p.15 明列的应用还有 programming languages、compilers、software verification、cybersecurity，以及 AI 中的 constrained generation 和 verification of AI-generated programs。补充：术语速解：约束生成是让产生的内容服从指定规则；程序验证是检查程序是否满足给定性质。这些词解释应用动机，不表示已经学完对应技术。该页注明文本来自 2026 年 9 月 7 日的 ChatGPT 对话，也示范了前一部分要求的 AI 使用说明。

考试角度：（C 级 通识）这类知识点常见考法是辨别“举例验证”和“普遍证明”，尤其检查构造答案是否证明了两个包含方向。

把“我会了”变成可以检查的能力（补充）

以“认出偶数长度的二进制串”为自取例子。第一层是举例：空串和 01 应接受，0 和 101 应拒绝。第二层是构造：设置“已读长度为偶数”和“已读长度为奇数”两个状态，每读一个符号就切换；初态及接受态是偶数状态。第三层才是证明：读入零个字符时状态正确；假设读完前 k 个时状态记录正确，再读一个字符会同时改变长度奇偶性与机器状态，因此读完 k+1 个时仍正确。输入读尽时，接受恰好等价于长度为偶数。

这个不变量——“状态准确记录已读前缀的奇偶性”——把构造和证明接起来。如果只记住两圈交替的图，换成“三的倍数长度”可能又不会；若懂不变量，就知道需要记录三个余数，并逐次加一取模。能解释状态为什么够用，比背图更可迁移。

自检：测试了前一万个串都正确，是否已经证明正确？

要证明的是哪一个量词：有限个已测试输入，还是所有有限输入？

展开推理与答案

没有。测试只能说明这些输入通过；机器可能在更长的串上出错。归纳证明给出基础情况以及对任意长度的保持关系，才覆盖无限多个输入。测试仍有价值：一个失败样例就足以推翻候选构造。

本讲核心考点

  • 构造模型后还需要严格论证其行为（p.14；C 级）。
  • 可运行、正确和问题可解是不同主张（p.15；C 级）。

附录

本部分没有需要另列的推导；定义与算例在相应页段内。

来源与证据

历史版本考试证据（本次未重新读取全部试卷）：读了 HW01-2025T1-题目.pdf、HW01-2026T1-题目.pdf、HW02-2025T1-题目-更新.pdf、HW03-2025T1-题目.pdf、HW04-2025T1-题目.pdf、HW05-2025T1-题目.pdf、期中练习-含解答-学期待核.pdf、期末-2022T1-资料包.pdf、Final-Exam-2023T1-题目.pdf、Final-Exam-2024T1-题目.pdf、Final-Exam-2025T1-题目.pdf、期末-2023T1-资料包.pdf、期末-2024未核-资料包.pdf；未识别用途的 PDF：无

  • 原件：L00-课程简介-2026T1.pdf（本地课件），PDF p.13–15。
  • 本次复核：2026-10-13；逐页读取上述原件文字，视觉核对结构图、课表、路线图及历史图页，补全具体内容。静态 PDF 外的视频未读取。