EagleBear2002 的博客

这里必须根绝一切犹豫,这里任何怯懦都无济于事

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

教材 2.2 真值与模型

习题 13:证明同态定理的 (a)。

\(h\) 是从 \(\A\)\(\B\) 中的同态,\(s\) 将变量的集合映射到 \(|\A|\) 中。

  1. 对每个项 \(t\),我们有 \(h(\overline{s}(t)) = \overline{h \circ s}(t)\),其中 \(\overline{s}(t)\) 是在 \(\A\) 中计算的,而 \(\overline{h \circ s}(t)\) 是在 \(\B\) 中计算的;
阅读全文 »

摘要

全球造船业经历了深刻的变革,其范围、复杂性和贸易影响都呈现出多样化。本研究通过分析日本、韩国和中国造船企业的演变模式来探讨这些转变。我们踏上一段历史之旅,追溯行业领导地位从欧洲向亚洲的转变。作为案例研究,我们详细研究了韩国造船业从国内优势到全球地位的五个转型阶段。为了建立一个涵盖日本、韩国和中国造船业的比较框架,我们引入了两个关键参数:创新价值交付能力和全球市场定位。这些参数阐明了这三个亚洲国家在造船领域采取的独特发展路径。我们的研究结果强调,在竞争加剧和地缘政治动态不断变化的环境中,领先的公司战略性地利用其国家制造优势和物流基础设施,同时巧妙地应对全球政治的复杂性和各自国家所奉行的产业政策。这项研究为未来对后疫情时代全球船舶制造业的研究提供了宝贵的见解和启示。

关键词:Shipbuilding industry · Comparative studies · Competitive landscape · Growth theory · Japan · Korea · China

Introduction

全球造船业曾经以西方为中心,近几十年来踏上了变革之旅。尖端技术的出现和贸易动态的演变推动了深刻的转变,重塑了竞争格局。目前,该行业的中心位于亚太地区,日本、韩国和中国处于领先地位(Yum 2022;Gavalas 等 2022)。这些国家在造船业的崛起与其制造业的增长同步,包括钢铁、化学品、汽车、电子和半导体(Jiang 等 2013;Oh 和 Rhee 2008;Park 等 2022;Park 和 Jeong 2012)。尽管有值得注意的研究贡献侧重于过去二十年的变化(Bruno 和 Tenold 2011;Shin 和 Hassink 2011;Ferreira 等人 2018),但我们对包括 2000-2020 年代在内的亚洲造船业全面转型的理解仍然严重不足(Feng 等人 2023b;Gavalas 等人 2022;Park 等人 2021)。鉴于全球格局瞬息万变,竞争加剧,地缘政治动态不断演变,这一差距尤为紧迫。

阅读全文 »

摘要

经典哲学的危机揭示了人们对提供数学基础的数学和哲学标准的困惑。

题目中提到的三个学派都试图给数学提供一个坚实的基础,三个危机意味着这些学派未能完成其任务。本文“以现代的眼光”审视这些危机,使用今天可用的数学,而不仅仅是创建这些学派的先驱们所用的数学。因此,本文不以严格的历史方式来处理这三个危机,也不讨论目前大量的、技术性的数学,这些数学是由上述三个学派所引入的技术而产生的。原因之一是,这样的讨论需要一本书,而不是一篇短文;原因之二是,所有这些技术性数学与数学哲学关系不大,而在这篇文章中,我想强调逻辑主义、直觉主义和形式主义中那些建立在哲学之上的内容。

本文转载自柳渝科学网博客:科学网—数学中的三个危机 :逻辑主义、直觉主义和形式主义 - 译文(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 两个系统为例,直观展示公理的祖先不是上帝,而是逻辑或形式二者之一

我的导师曾经在软件学院教授《离散数学》,这是我本科阶段最喜欢的课程之一,也是我了解他的研究方向的入口。目前我的研究课题是数据库程序鲁棒性,该问题涉及到形式语言、形式化方法和数理逻辑,该领域的论文往往通篇都是希腊字母、形式逻辑符号和命题充要条件的证明。我在《数理逻辑》开课之前自学了一些集合论与形式化相关的内容,很幸运能够在研究生阶段开始之前管窥整个数学大厦的基石。笔者既不是数学专业的研究人员,也谈不上数学爱好者,仅在此与同好分享一些浅陋观点。挂一漏万,还请读者批评指正。

阅读全文 »

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

教材 2.2 真值与模型

习题 3:证明:\(\set{\forall x(\alpha \to \beta), \forall x\alpha} \models \forall x \beta\)

证明:对每个结构 \(\mathfrak{A}\) 和每个函数 \(s: V \to | \A |\),有 \(\models_\A \forall x(\alpha \to \beta)[s]\)\(\models_\A \forall x \alpha[s]\),即 \(\models_\A \forall x((\alpha \to \beta) \land \alpha)[s]\)。因此 \[ \models_\A \forall x((\alpha \to \beta) \land \alpha)[s] \\ \iff \forall d \in \A. \models_\A((\alpha \to \beta) \land \alpha)[s(x|d)] \\ \iff \forall d \in \A. \models_\A(\beta \land \alpha)[s(x|d)] \\ \iff \models_\A \forall x(\beta \land \alpha)[s] \\ \iff \models_\A \forall x(\beta)[s] \land \models_\A \forall x(\alpha)[s] \\ \] \(Q.E.D.\)

习题 4:证明:如果 \(x\)\(\alpha\) 中不是自由出现的,那么 \(\alpha \models \forall x \alpha\)

阅读全文 »

摘要

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

专业方向 大一通修 大一上专业必修 课程组必修 大一必修 大二、大三通修 大二、大三专业必修 前三年必修 大一必修/前三年必修
智能科学与技术 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%

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

  • 大一通修:包括大一思政、数学、英语、体育等课程;
  • 大类必修:大一上阶段的专业必修课,包括《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 位是流水号,不同书院不同年份可能参考性别、生源地、高考分数、出生日期、录取时间等因素进行排序。
阅读全文 »