APIO 2023 游记(大雾)

缘起

我一个已经退役的 OIer,怎么又去参加 APIO 了呢?

咳咳,事情的起因是这样的:CCF 在 2021 年创办了青少年计算机教育研讨会(Workshop on Computing Education for Teenagers,WCET),在每次线下 OI 活动时会组织面向教师的论坛。由于本次 WCET 活动和 APIO 一块在华山饭店进行,一方面刚好能借此接触到参与 APIO 的选手们,另外一方面也能了解一些算法竞赛与信息技术课程教学动态。对于我这样一位旅游型和社交型选手而言,怎么可能会错失这一面基与交流机会呢?

本来 小花 也想来的,但因为赶大作业推掉了这次行程,于是这次就是我独自一个人去了。

继续阅读APIO 2023 游记(大雾)

京原线非空列车 6437/8 次告别之旅

十二月初突然传来消息,行走于京原线上的非空列车 6437/8 次将要更换空调车底。对于从来没乘坐过非空调列车的我来说,虽然能理解新事物终将取代旧事物的道理,但不可避免地为非空列车的远去而惋惜,也为即将失去的体验机会而遗憾。而 6437/8 次作为离我最近的一趟非空列车,抢救性运转体验也是最容易的。

10 号那天,在丰台机务段参加“毛泽东号”机车研学活动之后,我便来到了北京西站,乘坐了 6437 次列车的北京西-燕山区间。当天是周末,已经有不少学生车迷赶来送别,能看到不少长枪短炮和手机不断地进行拍摄。这一趟坐下来一个多小时,感觉非空列车确实带给了我不少独特的体验,但总感觉体验上还差点意思。

想着 19 号那天来送别的人应该会比较多,也有机会遇到认识的朋友,我就又订了一张 19 号北京-燕山的 6437 次列车的车票(由于想要送别的人和单纯留下车票纪念的人非常多,订票的时候已经只能买到无座车票了,而之后几天再看的时候,就连无座也都不剩了)。在出发的前一夜,越想越觉得该彻底体验下非空列车的我,决定将目的地从燕山延长到涞源,赶着 12306 系统维护的时间到来之前买好了延长段和返程的车票,并订好了涞源过夜的旅馆,这一系列动作进行的非常流畅,完全没有一丝犹豫。

于是这场漫长的送别之旅,就这样开始了。

继续阅读京原线非空列车 6437/8 次告别之旅

2023 春 京广路旅行

序言

算下来,距离上一次真正意义上的长途旅行,已经是三年半的时间了。

2018 年的 NOIp,因为种种机缘巧合,拿了个还不算差的成绩,得以前往广州冬眠参加冬令营(WC 2019 游记),运气很好拿了块铜牌。

后来因为种种原因,原来不在省队线内的我意外进了队,于是就有了 CTS 2019 & APIO 2019 的旅行,当然还有更重要的 NOI 2019 啦。遗憾的是这三次比赛都没能拿到奖项,特别是最重要的 NOI 2019,比赛结束之后我的心态也进入了一个低谷期。

2020 年疫情突然降临,首先推掉的就是当年的冬令营。原本大家都认为这一次和 2003 年那样,并不会持续太久时间,到了暑假一切活动都会恢复正常,没想到一晃就是三年。当年的 WC 和 APIO 都在暑假迁移到了线上,而 NOI 2020 最终未能成行,成为我 OI 时光最大的遗憾。

(非常抱歉先用流水帐记了这么多之前提过的往事,有点偏题了 qwq)

转眼间过完了高中三年,大学也已经过去了一年半,长途旅行终于再次成为一个可选项。也因此在春节之后,我开始为这次旅行策划立项,做起规划。

首先估摸了下旅行的时间。因为今年极早的春节+比较晚的开学时间,整个寒假的时长达到了 50 日,如果选择在元宵节后出发,算下来差不多有 10 天的旅行时间,这样充裕的时间,恐怕之后都很难再找到了。

在这一前提下,接下来需要决定的就是旅行的目的地了。在这一问题上,我一开始就定下了广度优先的路线。在一省之内花掉十天时间,固然可以吃透当地大部分的旅游资源,但在人文风情等方面则显得有些单调了。

最终目的地被选定为湖北、湖南、广东三省的中心城市:武汉、长沙、广州及深圳。而因为这条旅游路线大体沿着京广铁路,这次旅行也有了“京广路旅行”的名字。

继续阅读2023 春 京广路旅行

归纳证明方法论——使用归纳法构建一般性结论的证明

(本文是对 James Wilcox 的 Exercises on Generalizing the Induction Hypothesis 的一点详细解说,也感谢 James Wilcox 在文章中提供的几道颇有练习价值的证明题!)

由于大多数数据类型常见的递归属性,在 Coq 中使用归纳法证明命题是一件颇为常见且基础的操作。

然而,有些具有递归性质的命题并不易于使用归纳法直接进行证明,原因在于,这些命题中的部分变量取了特定的值,而归纳过程中这些变量的值会发生变化,从而导致归纳过程无法继续下去。对此,我们往往需要找到一个更一般性的命题,用归纳法证明这一一般命题,随后使用该一般命题构建对原命题的证明。

下面便是两道实践此类命题证明方法论的绝佳例题。

继续阅读归纳证明方法论——使用归纳法构建一般性结论的证明

2023 上半年总结

充实,还是空耗

其实现在写这篇总结似乎还为时过早,因为上半年的事情还不能说全部处理完毕,还有多达 4 学分,两门课程的作业没有全部完成。这两门课又全是同一个陌生领域,理论计算机科学的硬课,未知性带来的心理负担可想而知。

总觉得每挺过一个 ddl,压力应该会递减,结果这学期的经历直接啪啪打脸。因为每翻过一个 ddl,才发现接下来的水相比更深了一些。虽然早有心理准备,但心理准备和真正面对还是两回事。

继续阅读2023 上半年总结

MIT 18.408 概率可验证证明 学习笔记 序

本系列是 MIT 18.408 Topics in Theoretical Computer Science: Probabilistically Checkable Proofs Fall 2022 的学习笔记。该课程内容也被用于北京理工大学 2023 春季学期的组合数学课程。

该系列全部内容均采用 CC BY-NC-SA 4.0 协议进行许可。

继续阅读MIT 18.408 概率可验证证明 学习笔记 序

ICPC EC Final 2022 游记

Day -1

想着早点到上海,留出点时间随机游走,于是订了足够早出发(十点整)的 G7 次的车票。结果就是不得不八点多出门赶车。

运气不太好,没赶上早高峰房山线跨线进 9 号线的车,换乘次数 +1。

到北京南站的时候离开车差不多半个小时,过了安检上楼之后刚好赶上开始检票,冗余时间感觉不太充足。

上车的人是真的多,怪不得京沪高铁能赚钱()

订的票很不幸地是 01 排,结果就是面前没有座位了,对于我们这样的三人连座来说,由于过道在车厢中间位置,桌板的大小缩了不少,坐在靠过道的我为了用上桌板还得往窗户那边凑过去。

虹桥 2 号航站楼的伪虚拟换乘挺有意思。名义上是虚拟换乘车站,但是可以在中间两个轨道停车的时候通过穿过车厢的方式实现换乘。

在同济的高中好友邀我去看花,然而发现四平路离宝山并不算近,再加上身心颇为疲惫,只得婉拒,颇为遗憾。

晚上我校的几个队(可惜 ddl 不在)找了个上海菜馆恰饭。菜馆是对着 知乎上的一个清单 找的,味道确实不错,很符合我对上海菜的想象!

继续阅读ICPC EC Final 2022 游记

谈谈 Windows 与 Linux 双系统环境下的时间不同步问题

在 Windows 和 Linux 两个操作系统间切换时,会产生时间不同步的问题——从 Windows 系统切换到 Linux 系统时,时间会向后推 8 小时;而当从 Linux 系统切换回 Windows 系统的时候,时间又向前推了 8 小时。

继续阅读谈谈 Windows 与 Linux 双系统环境下的时间不同步问题