课程概述¶
亲切和蔼的卜磊老师来上课，主要讲一些形式语言和一点初步的计算理论。课程前期可能会与编译原理有较多重合。
课程内容¶
- 正则语言和有限状态自动机
- 上下文无关语言和下推自动机
- 递归语言、递归可枚举语言和图灵机
- 一点点可判定性、计算复杂性的科普
教材¶
课程PPT写得比较完备，不看课本也足够 survive。教材的中文译版也可以在 box 里找到。
需要说明的是，最后几节课会科普一些建模的形式化方法。这部分内容比较晦涩，关于 CTL LTL Petri-Net 的讲解也比较少，需要仔细听课。
课程考核与给分¶
分数占比如下：
- 50% 期末
- 20% 实验
- 30% 作业
- 1~5 分的bonus
总评均分没有上80。
作业¶
共三次，分别对应 正则语言、上下文无关语言、图灵机 三部分内容。
个人认为三次作业中第二次作业的难度会稍大。助教会批阅并给出讲解，体验还是不错的。
作业的重点在于套路的掌握。
实验¶
用 C++ 实现简单的图灵机模拟器，需要解析特定格式的图灵机程序、输出中间步骤、输出结果。
Corner case 会比较多，需要细心读实验手册，充分测试。
Bonus¶
似乎是20级特供。
利用 SpaceEX 和 Scenario 两个软件分别对无人机阵列进行建模。实际的操作类似数电里的 logisim，需要拖拽很多图形并填写触发条件，并且很难验证正确性。
Bonus 加分仅针对 50 分平时分，不作溢出处理。
考试¶
期末题量稍大，试题分布大概如下：
- 考察设计 DFA
- 考察设计 CFG 和对应的 PDA
- 图灵机编程
- 几个泵引理的运用
- 一道判断语言类型的选择题
- 可判定性和规约方法的运用
- 迁移系统建模
- 操作封闭性的证明
其中建模题似乎是必考的，压轴证明题难度与作业最难题相当，前几题都比较繁琐需要写很多，要注意把握时间。
总结¶
属于内容比较有意思、老师助教也都很 nice 的课程。难度就见仁见智了。