EagleBear2002 的博客

\[ \def\A{\mathfrak{A}} \]

本节知识点

表达式是符号的任意有限序列。大多数表达式没有意义，项和合式公式是具有特定意义的表达式。

项定义为在常数符号和变量之前加上函数符号构成的表达式。

原子公式的做工相当于命题逻辑中的命题符号，原子公式是具有如下形式的表达式： \[ Pt_1t_2\dots t_n \] 合式公式（或公式）是指由原子公式通过使用 0 次或多次连接符号和量词符号构成的表达式。

摘要

本文汇总了南京大学技术科学实验班部分专业的学分组成，以供大学生涯规划参考。

本文对《技术科学实验班主修培养方案》中的所有课程学分进行如下统计：

• 大一通修：包括大一思政、数学、英语、体育等课程；
• 大类必修：大一上阶段的专业必修课，包括《C 语言程序设计基础》《信息科学中的物理学（上）》《微观经济学》；
• 课程组必修：大一下阶段进入课程组后的专业必修课；
• 大一必修：包括以上三部分，是大一阶段所有的必修课总学分。

摘要

ANSI SQL-92 [MS，ANSI] 根据以下现象定义隔离级别：脏读、不可重复读和幻像。本文表明，这些现象和 ANSI SQL 定义无法描述几种流行的隔离级别，包括这些级别的标准锁定实现。调查现象的模糊性可以得到更清晰的定义；此外，还引入了更好地描述隔离类型的新现象。定义了一种重要的多版本隔离类型，即快照隔离。

作者：

• Hal Berenson, Microsoft Corp., haroldb@microsoft.com
• Phil Bernstein, Microsoft Corp., philbe@microsoft.com
• Jim Gray, Microsoft Corp., gray@microsoft.com
• Jim Melton, Sybase Corp., jim.melton@sybase.com
• Elizabeth O’Neil, UMass/Boston, eoneil@cs.umb.edu
• Patrick O'Neil, UMass/Boston, poneil@cs.umb.edu

\[ \def\K{\mathsf{K}} \def\V{\mathsf{V}} \def\H{\mathcal{H}} \def\R{\mathsf{R}} \def\W{\mathsf{W}} \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\WT{\mathsf{WT}} \def\RT{\mathsf{RT}} \def\Serialization{\mathsf{Serialization}} \def\po{\mathsf{\textcolor{red}{po}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\CM{\mathsf{\textcolor{brown}{CM}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\CMto{\overset{\CM}{\longrightarrow}} \def\COto{\overset{\CO}{\longrightarrow}} \def\WRto{\overset{\WR}{\longrightarrow}} \def\WRxto{\overset{\WR(x)}{\longrightarrow}} \def\wrxto{\overset{\wr(x)}{\longrightarrow}} \def\potto{\overset{\po_t}{\longrightarrow}} \]

摘要

现代数据库采用弱隔离级别来满足高可用性事务。然而，最近许多生产数据库中都出现了弱隔离错误。这引发了人们对数据库实现是否在实践中真正实现其承诺的隔离保证的担忧。在本文中，我们介绍了 Plume，这是第一个高效、完整的弱隔离级别黑盒检查器。Plume 建立在模块化、细粒度、事务异常模式的基础上，我们利用这些模式建立了代表性弱隔离级别的合理和完整特征，包括读取提交、读取原子性和事务因果一致性。Plume 利用两种技术（向量和树时钟）的新颖组合来加速隔离检查。我们广泛的评估表明，Plume 可以在大量异常数据库执行历史中重现所有已知违规行为，在三个生产数据库中检测新的隔离错误以及信息反例，比最先进的检查器发现更多的弱隔离异常，并在各种工作负载下有效地验证隔离保证。

作者：

• SI LIU, ETH Zurich, Switzerland
• LONG GU, State Key Laboratory for Novel Software Technology, Nanjing University, China
• HENGFENG WEI*, State Key Laboratory for Novel Software Technology, Nanjing University, China
• DAVID BASIN, ETH Zurich, Switzerland

\[ \def\v{\overline{v}} \]

教材 1.7 紧致性和能行性

习题 1：设 \(\Sigma\) 的每个有限子集都是可满足的，证明 \(\Sigma ; \alpha\) 和 \(\Sigma ; \neg \alpha\) 中至少有一个也是如此。(这是紧致性定理证明的一部分)

提示：如果不是这样，那么对于有限子集 \(\Sigma_1 \subseteq \Sigma\) 和 \(\Sigma_2 \subseteq \Sigma\)，\(\Sigma_1 ; \alpha\) 和 \(\Sigma_2 ; \neg \alpha\) 都是不可满足的。再考虑 \(\Sigma_1 \cup \Sigma_2\)。

不使用紧致性定理的证明：使用反证法。如果不是这样，则对于有限子集 \(\Sigma_1 \subseteq \Sigma\) 和 \(\Sigma_2 \subseteq \Sigma\)，\(\Sigma_1 ; \alpha\) 和 \(\Sigma_2 ; \neg \alpha\) 都是不可满足的。因此 \(\Sigma_1 \cup \Sigma_2\) 也是不可满足的。这与“\(\Sigma\) 的每个有限子集都是可满足的”相矛盾。

\(Q.E.D.\)

摘要

本文整理了南京大学本科生学号和研究生学号组成规则，并整理了院系专业代码、本科招生专业代码和新生学院各书院之间的对应关系。依照本文的规则，可根据学号判断学生信息。

本科生学号组成

本科生学号由 9 位阿拉伯数字组成。其中：

1. 第 1-2 位表示入学年份，例如 24 表示 2024 年入学；
2. 第 3 位是录取类型代码，其中 1 表示统招，2 表示第二学位，5 表示留学生；
3. 第 4-6 位是招生专业（或大类）代码，其中第 4-5 位是院系代码；
4. 第 7-9 位是流水号，不同书院不同年份可能参考性别、生源地、高考分数、出生日期、录取时间等因素进行排序。

\[ \def\size{\mathsf{size}} \def\F{\mathcal{F}} \]

教材 1.3 解析算法

习题 3：证明引理 13B 中关于运算 \(\varepsilon_\lnot\) 的情形。

证明：对具有该性质的合适公式的集合 \(S\)，使用归纳法。

只包括一个命题的合适公式，没有符合条件的真初始段，原命题显然成立。

下面验证 \(S\) 在 \(\varepsilon_\lnot\) 下是封闭的。考虑 \(S\) 中的 \(\alpha\)，\((\lnot \alpha)\) 的真初始段如下：

1. \((\)
2. \((\lnot\)
3. \((\lnot \alpha_0\)，其中 \(\alpha_0\) 是 \(\alpha\) 的真初始段
4. \((\lnot \alpha\)

显然，\(\alpha_0 \in S\)。原命题显然正确。

\(Q.E.D.\)

习题 4：假定将合式公式的定义修改为去掉其中所有的右括号。对于

摘要

课程资源概览

• 课程视频资源：https://space.bilibili.com/479141149/channel/collectiondetail?sid=1720732
• 课程幻灯片：https://github.com/courses-at-nju-by-hfwei/cpl-lectures/tree/main
• 教材：《C 语言程序设计：现代方法（第 2 版·修订版）》（ISBN: 9787115565198）
• 课程 oj：校内访问：https://oj.cpl.icu/、校外访问：https://public.oj.cpl.icu/
• 课程讲义：https://ymv59wdgrr.feishu.cn/wiki/A1HzwviAgiFnQwkfRUWcVjqunLf

课程资源结构

\[ \def\P{\mathcal{P}} \def\T{\mathbb{T}} \def\V{\mathbb{V}} \def\D{\mathbb{D}} \def\Tr{\mathbb{Tr}} \def\Ev{\mathbb{Ev}} \def\X{\mathsf{X}} \def\begin{\mathsf{begin}} \def\ld{\mathsf{ld}} \def\isu{\mathsf{isu}} \def\del{\mathsf{del}} \def\end{\mathsf{end}} \def\HB{\mathsf{HB}} \def\PO{\mathsf{\textcolor{black}{PO}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{red}{WW}}} \def\RW{\mathsf{\textcolor{blue}{RW}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\ARB{\mathsf{\textcolor{orange}{ARB}}} \def\CC{\mathtt{CC}} \def\CM{\mathtt{CM}} \def\CCv{\mathtt{CCv}} \def\PC{\mathtt{PC}} \def\SI{\mathtt{SI}} \def\SER{\mathtt{SER}} \]

摘要

分布式存储系统和数据库被各种类型的应用程序广泛使用。对这些存储系统的事务访问是一种重要的抽象，它允许应用程序程序员将操作块（即事务）视为原子执行。出于性能原因，现代数据库实现的一致性模型比标准可序列化模型弱，后者对应于在顺序一致内存上执行的事务的原子性抽象。例如，因果一致性就是在实践中广泛使用的此类模型之一。

在本文中，我们研究了因果一致性的几种变体之间的特定于应用程序的关系，并解决了自动验证给定事务程序是否对因果一致性具有鲁棒性的问题，即在任意因果一致数据库上执行时，其所有行为都是可序列化的。我们表明，没有 ww 竞争的程序在所有这些变化下都具有相同的行为集，并且我们表明，检查鲁棒性是多项式时间可归结为顺序一致共享内存上事务程序的状态可达性问题。后一个结果的一个令人惊讶的推论是，允许不可比较的行为集的因果一致性变体允许可比较的稳健程序集。这种简化还为利用现有的并发程序验证方法和工具（假设顺序一致性）来推理在因果一致的数据库上运行的程序打开了大门。此外，它允许确定当在不同站点执行的程序是有限状态时，检查稳健性的问题是可判定的。

作者：

\[ \def\ran{\text{ran}} \def\FUN{\mathsf{FUN}} \]

讲义 0.2.18 数学归纳法

习题 1：证明设 \(A\) 为传递集合，则 \(A^+\) 也是传递集合。

证明：由 \(A\) 的传递性可知，\(\forall a \in A, a \subseteq A\)。取任意 \(b \in A^+\)，只要证明 \(b \subseteq A^+\)。

\(A^+\) 是 \(A\) 的后继（此处右上角的 \(+\) 并不是传递闭包），即 \(A^+ = A \cup \set{A}\)。

1. 若 \(b \in A\) 则 \(b \subseteq A \subseteq A^+\)；
2. 若 \(b \notin A\) 则 \(b = A\)，此时 \(b \subseteq A^+\) 成立。

\(Q.E.D.\)

习题 2：证明对任意自然数 \(n\)，都有 \(0 = n\) 或 \(0 \in n\)。