摘要
经典哲学的危机揭示了人们对提供数学基础的数学和哲学标准的困惑。
题目中提到的三个学派都试图给数学提供一个坚实的基础，三个危机意味着这些学派未能完成其任务。本文“以现代的眼光”审视这些危机，使用今天可用的数学，而不仅仅是创建这些学派的先驱们所用的数学。因此，本文不以严格的历史方式来处理这三个危机，也不讨论目前大量的、技术性的数学，这些数学是由上述三个学派所引入的技术而产生的。原因之一是，这样的讨论需要一本书，而不是一篇短文；原因之二是，所有这些技术性数学与数学哲学关系不大，而在这篇文章中，我想强调逻辑主义、直觉主义和形式主义中那些建立在哲学之上的内容。
本文转载自柳渝科学网博客：科学网—数学中的三个危机 ：逻辑主义、直觉主义和形式主义 - 译文（1）：逻辑主义 - 柳渝的博文
\[ \def\true{\mathrm{true}} \def\false{\mathrm{false}} \def\and{\mathrm{and}} \def\or{\mathrm{or}} \def\not{\mathrm{not}} \def\xor{\mathrm{xor}} \def\if{\mathrm{if}} \]
写在前面
子曰：“朝闻道，夕死可矣。”
——《论语·里仁第四》
Bourbaki 学派认为数学没有先验的公理，我并不完全认同这一观点（其实我甚至不完全理解这一观点）。本文尝试以公理化集合论和 Church Numerals 两个系统为例，直观展示公理的祖先不是上帝，而是逻辑或形式二者之一。
我的导师曾经在软件学院教授《离散数学》，这是我本科阶段最喜欢的课程之一，也是我了解他的研究方向的入口。目前我的研究课题是数据库程序鲁棒性，该问题涉及到形式语言、形式化方法和数理逻辑，该领域的论文往往通篇都是希腊字母、形式逻辑符号和命题充要条件的证明。我在《数理逻辑》开课之前自学了一些集合论与形式化相关的内容，很幸运能够在研究生阶段开始之前管窥整个数学大厦的基石。笔者既不是数学专业的研究人员，也谈不上数学爱好者，仅在此与同好分享一些浅陋观点。挂一漏万，还请读者批评指正。
摘要
本文汇总了南京大学技术科学实验班部分专业的学分组成，以供大学生涯规划参考。
| 专业方向 | 大一通修 | 大一上专业必修 | 课程组必修 | 大一必修 | 大二、大三通修 | 大二、大三专业必修 | 前三年必修 | 大一必修/前三年必修 |
|---|---|---|---|---|---|---|---|---|
| 智能科学与技术 | 34.5 | 9 | 15 | 58.5 | 11 | 32 | 101.5 | 57.6% |
| 软件工程（智能软件方向） | 34.5 | 9 | 13 | 56.5 | 11 | 40 | 107.5 | 52.6% |
| 集成电路与集成系统 | 34.5 | 9 | 8 | 51.5 | 11 | 29 | 101.5 | 50.7% |
| 数字经济 | 34.5 | 9 | 3 | 46.5 | 11 | 39 | 86.5 | 53.8% |
本文对《技术科学实验班主修培养方案》中的所有课程学分进行如下统计：
摘要
ANSI SQL-92 [MS，ANSI] 根据以下现象定义隔离级别：脏读、不可重复读和幻像。本文表明，这些现象和 ANSI SQL 定义无法描述几种流行的隔离级别，包括这些级别的标准锁定实现。调查现象的模糊性可以得到更清晰的定义；此外，还引入了更好地描述隔离类型的新现象。定义了一种重要的多版本隔离类型，即快照隔离。
作者：
\[ \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\WT{\mathsf{WT}} \def\RT{\mathsf{RT}} \def\po{\mathsf{\textcolor{red}{po}}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\CM{\mathsf{\textcolor{orange}{CM}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} \def\CMto{\xrightarrow{\CM}} \def\COto{\xrightarrow{\CO}} \def\WRto{\xrightarrow{\WR}} \def\WRxto{\xrightarrow{\WR(x)}} \def\wrxto{\xrightarrow{\wr(x)}} \def\potto{\xrightarrow{\po_t}} \]
摘要
现代数据库采用弱隔离级别来满足高可用性事务。然而，最近许多生产数据库中都出现了弱隔离错误。这引发了人们对数据库实现是否在实践中真正实现其承诺的隔离保证的担忧。在本文中，我们介绍了 Plume，这是第一个高效、完整的弱隔离级别黑盒检查器。Plume 建立在模块化、细粒度、事务异常模式的基础上，我们利用这些模式建立了代表性弱隔离级别的合理和完整特征，包括读取提交、读取原子性和事务因果一致性。Plume 利用两种技术（向量和树时钟）的新颖组合来加速隔离检查。我们广泛的评估表明，Plume 可以在大量异常数据库执行历史中重现所有已知违规行为，在三个生产数据库中检测新的隔离错误以及信息反例，比最先进的检查器发现更多的弱隔离异常，并在各种工作负载下有效地验证隔离保证。
作者：
摘要
本文整理了南京大学本科生学号和研究生学号组成规则，并整理了院系专业代码、本科招生专业代码和新生学院各书院之间的对应关系。依照本文的规则，可根据学号判断学生信息。
本科生学号由 9 位阿拉伯数字组成。其中：
24 表示 2024 年入学；1 表示统招，2
表示第二学位，5 表示留学生；摘要
| 知识模块 | 知识单元 | 资源 |
|---|---|---|
| 课程介绍 | 0-intro | PPT+视频 |
| 课程介绍 | 李薛成-OJ小贴士 | 视频 |
| 数据类型 | 1-types-io | PPT+视频 |
| 条件分支和循环 | 2-if-for-array | PPT+视频 |
| 条件分支和循环 | 3-for-a-while | PPT+视频 |
| 条件分支和循环 | 4-loops | PPT+视频 |
| 函数和递归 | 5-function | PPT+视频 |
| 函数和递归 | 6-recursion | PPT+视频 |
| 函数和递归 | 7-data-types | PPT+视频 |
| 指针和链表 | 8-pointers-arrays | PPT+视频 |
| 指针和链表 | 9-pointers-cstrings | PPT+视频 |
| 指针和链表 | 10-double-pointers | PPT+视频 |
| 指针和链表 | 11-function-pointers | PPT+视频 |
| 指针和链表 | 12-struct | PPT+视频 |
| 指针和链表 | 13-linked-lists | PPT+视频 |
| 番外篇-实践教程 | 13-epilogue-20221221 | 视频 |
| 番外篇-实践教程 | 共 13 个工具类短视频 | 视频 |
\[ \def\P{\mathcal{P}} \def\V{\mathbb{V}} \def\Tr{\mathbb{Tr}} \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\CC{\mathtt{CC}} \def\CM{\mathtt{CM}} \def\CCv{\mathtt{CCv}} \]
摘要
分布式存储系统和数据库被各种类型的应用程序广泛使用。对这些存储系统的事务访问是一种重要的抽象，它允许应用程序程序员将操作块（即事务）视为原子执行。出于性能原因，现代数据库实现的一致性模型比标准可序列化模型弱，后者对应于在顺序一致内存上执行的事务的原子性抽象。例如，因果一致性就是在实践中广泛使用的此类模型之一。
在本文中，我们研究了因果一致性的几种变体之间的特定于应用程序的关系，并解决了自动验证给定事务程序是否对因果一致性具有鲁棒性的问题，即在任意因果一致数据库上执行时，其所有行为都是可序列化的。我们表明，没有 ww 竞争的程序在所有这些变化下都具有相同的行为集，并且我们表明，检查鲁棒性是多项式时间可归结为顺序一致共享内存上事务程序的状态可达性问题。后一个结果的一个令人惊讶的推论是，允许不可比较的行为集的因果一致性变体允许可比较的稳健程序集。这种简化还为利用现有的并发程序验证方法和工具（假设顺序一致性）来推理在因果一致的数据库上运行的程序打开了大门。此外，它允许确定当在不同站点执行的程序是有限状态时，检查稳健性的问题是可判定的。
作者：
\[ \def\P{\mathcal{P}} \def\Tr{\mathsf{Tr}} \def\PO{\mathsf{\textcolor{black}{PO}}} \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{pink}{ARB}}} \def\CC{\mathtt{CC}} \def\PC{\mathtt{PC}} \def\SI{\mathtt{SI}} \def\SER{\mathtt{SER}} \def\assume{\mathtt{assume}} \def\CountTickets{\mathtt{CountTickets}} \def\Register{\mathtt{Register}} \def\CreateEvent{\mathtt{CreateEvent}} \def\assume{\mathtt{assume}} \def\Password{\mathtt{Password}} \def\AxPrefix{\mathsf{AxPrefix}} \]
摘要
对数据库的并发访问通常封装在事务中，以便与其他并发计算隔离并具有对故障的恢复能力。现代数据库为事务提供了各种语义，这些语义对应于一致性和可用性之间的不同权衡。由于较弱的一致性模型提供了更好的性能，因此一个重要的问题是研究给定程序所需的最弱一致性级别（以满足其规范）。作为处理此问题的一种方法，我们研究了在用较弱的一致性模型替换一致性模型时检查给定程序是否具有相同的行为集的问题。这种称为鲁棒性的属性通常意味着在削弱一致性时程序的任何规范都会得到保留。我们专注于比标准可序列化性更弱的一致性模型的鲁棒性问题，即因果一致性、前缀一致性和快照隔离。我们表明，检查这些模型之间的鲁棒性是多项式时间可归结为可序列化下的状态可达性问题。我们还使用这种归结来推导一种基于 Lipton 归结理论的实用证明技术，该技术可以证明程序是鲁棒的。我们已经将我们的技术应用于分布式系统和数据库文献中的几个具有挑战性的应用。
作者：
\[ \def\prefix{\mathsf{prefix}} \def\postfix{\mathsf{postfix}} \def\T{\mathcal{T}} \def\I{\mathcal{I}} \def\C{\mathsf{C}} \def\W{\mathsf{W}} \def\R{\mathsf{R}} \def\Obj{\mathsf{Obj}} \]
摘要
虽然可串行化始终保证应用程序的正确性，但可以选择较低的隔离级别来提高事务吞吐量，但风险是引入某些异常。如果在指定的隔离级别下，所有可能的事务交错都是可串行化的，则一组事务对给定的隔离级别具有鲁棒性。因此，鲁棒性始终保证应用程序的正确性，同时具有较低隔离级别的性能优势。虽然鲁棒性问题在文献中受到了广泛关注，但只获得了充分条件。最值得注意的例外是 Fekete 的开创性工作，他获得了确定针对 SI 的鲁棒性的特征。在本文中，我们解决了较低 SQL 隔离级别 RU 和 RC 的鲁棒性问题，它们是根据禁止的脏写和脏读模式定义的。本文的第一个主要贡献是，我们根据特定形式（拆分和多拆分调度 ）的反例调度 的缺失以及满足各种属性的干涉图中的环的缺失来表征针对这两个隔离级别的鲁棒性。与 Fekete 的工作的一个关键区别是，本文获得的环属性必须考虑事务内操作的相对顺序，因为 RU 和 RC 不满足原子可见性要求。一个特殊的结果是后者导致了针对 RC coNP-complete 的鲁棒性问题。本文的第二个主要贡献是 coNP-hardness 证明。对于 RU，我们获得了 LOGSPACE-completeness。
作者：