Morgen-Kornblume's Blog

邯郸——出师不利的小倒霉蛋之旅 坐不住了 从紧张的招生任务中脱身出来以后，一刻也没有为自己能够闲下来松一口气，迎面而来的是长达四周的小学期。回来后和窦窦子互通了一下日程，发现第一周他上五天课，我上四天课，于是便约好了周六在北京市内玩一玩。 但是我周四早八上完就没课了，这实在是令人感到有些坐不住，会想起 B站UP主 “极客火车迷游中国” 去响堂山石窟的那一期视频，于是便决定效仿他去邯郸度过周四周五，周六再回来和窦窦子玩。 顺便还私信问这个 Up 要了一份通勤车的时刻表。 出发 暑运的客流实在是全方位的火爆，从北京出发的车票很多都被早早抢光，甚至许多加开的临时旅客列车也是一票难求。最后我选了从北京西站出发的 T49 次列车，我上完课收拾一下宿舍，吃完饭再睡半个小时出发，刚好能够赶上，计划通。而且这趟车的硬座也足够便宜，只要 64.5 元便可跨越六七百公里的路程。在邯郸待上一晚上，早晨坐最快的邯长线小票车去磁山，看完磁山遗址坐公交去响堂山石窟，最后在石窟附近的四等小站搭上回邯郸的通勤车；可惜美中不足的是，通勤车回来后没有晚上出发回北京的普通列车；而且，如果不在 22：30 之前回来的话， ...

通辽——独自一人说走就走的旅行 说走就走 18 号是我在 PKU 考试的最后一天，我们工院基本上大一生都是这一天下午四点考完数算，就算是放假和解放了；进入数算的考场前，考试周多日以来的疲惫和压力郁结在胸中；“考完这场就去什么地方旅行吧”，我这样想着，考前三十分钟，我还在手机上检索着 12306 的车票信息，最终，我选择了去通辽，考完试当天的晚上 8 点 49 就出发，睡一晚上，第二天早上十一点到达通辽（京通线单线+部分燕山困难区间小曲线半径+客货混跑造就了这趟平均旅速仅有 60km/h 左右的大慢车）。 数算考试提前半个小时交了卷子，回宿舍简单整备了一下行李，检点了一下就背上背包直奔北京站了，这是我第一次全程独自一人踏上一场长途旅行。 通辽 第二天早上五点半，被列车进某个中途会让站时巨大的闸瓦刹车声吵醒，此时车刚刚进了内蒙古地界，透过拉开的窗帘，我看到了内蒙古清晨的第一缕阳光，远处的山川和近处的农田与村庄徐徐展现在我的眼前，又是一种与我在华北平原和东北三省以及新疆的所见截然不同的风景。 内蒙古这边的车站建筑都非常有特色，普遍都会在主体建筑上顶一个蒙古包式的穹顶（但是有的可能是天花板上加 ...

承德——思考人生之旅 没有什么原因，只是因为期末之前有了时间，想要去看看，去体验生活，体验京承九个半小时的最慢传说，所以就选择了去承德。 这么近，那么美，周末到河北。 4471 启程 如何从北京大学奔赴遥远的昌平北站坐上 4471 呢？ 首先自行车出东门，沿成府路疾驰而下，闪击五道口。 然后搭上 13 号线，速通清河站，赶上 9:10 始发的市郊铁路怀密线列车。 （小粉车可爱捏） 这样你在 9:37 就可以准时抵达昌平北站，然后就可以在天桥下看到 4471 了。 小蘑菇通风口，DF4C 内燃机车，可惜没有抓到传说中的那节 YZ22B 车底，值班员也不让到前面去拍本务机车。 必须吐槽昌平北站的出站换乘，不过那么小一个站，似乎也不是特别需要便捷换乘通道…… 上车的人很少，大家都比较有距离感，除了熟人以外不会坐在一起，硬座和卧代坐的旅客上车后直接原地升舱，列车员也不管。 各色人等 有和我一样掏出电脑的“京城知识分子”， 有一个带了六罐啤酒和花生瓜子下酒菜的失意青年，在这趟车上自我放逐，不知道在哪一站下， 但是更多的还是沿线村镇的居民，他们大多带着一些菜，还有一些在城里买的商品 ...

东北七日零七夜 写这篇文章的时候，已经是我踏上下一场旅行，坐在列车上无所事事之时。对于旅行的记忆和体验早已不如当时就写那么鲜活清晰，而是加入了不少之后的沉淀与思维再加工，但是好在我可以更全面地回顾这次旅行，并记述我在这个时间节点上的所思所想。 写作的勉励 本来其实我有点想偷懒不写这篇文章，但是每每我冒出这等念头之时，我总要想起那位在旅顺二〇三高地偶遇的老人家。我和他是同道中人，他说他常年把他的所思所想和研究成果写在自己的空间里，不为给别人看以求名、求流量，而是给子孙后代留一些精神资源；当然我还年轻，还没有子孙后代那么长远的追求和考量，我写下自己所思所想的目的无非是留下一点自己年轻时思想的足迹，以备将来某一天的察看和回味。 所以，我确乎是要写一点东西。 写这篇文章时是在漫长的旅途中，这篇文章所写的也是一场漫长的旅途，就让我们娓娓道来吧。 旅行之念，动机之肇始 众所周知，北大有着“北京放假大学”的美誉，五四校庆，五一大假，加上周末不调休，使得北大在五一期间足足有了九天假期（4.27~5.5），这么长的假期，总要规划一场跨越祖国千里山河的长途旅行才是。 我是一个不爱凑热闹，喜欢错峰出行的 ...

旅行者系列 - 往返秦皇岛的一日半 缘起 似乎是在上次我邀请群友们去天津游玩后，打开了一位清华帅哥心里面的某种开关似的，他那种读万卷书、行万里路的雄心壮志犹如开闸放水般喷涌而出，于是他在群里发起了一场往返秦皇岛的游玩活动。 尝到少年壮游的美好后，我自然也是不甘落后，但是吸取了上次游玩过久导致学业落下的教训，这次我决定只去一日半，周天在校好好学习。 不过在清华和北大每个人都有自己的事情要忙，群里其他几个人对此兴味寥寥，最后惟我和他双人成行。 本着“谁发起，谁策划”的原则，这回倒是省去了我不少脑力，只需按照这位素有“英伦绅士”之称的帅哥的计划行事即可。 他的行程计划出于著作权考虑我就不放在这里了，但是应该可以从我接下来写的游记中看出一二。 北京站 这还是我第一回来北京站。 之前参观正阳门的铁道博物馆时，我只知道是建国以后，把北京火车站从正阳门迁到了现在的位置。 这次见到北京站，我对那个年代的建筑风格有了更进一步的了解。 苏体中用 它的这种建筑形制总体而言是“苏体中用”：整个建筑结构是苏联或者说欧洲那种高耸宽阔、大顶棚、侧窗采光的结构，但是内部的细节和装潢使用的是新中式的风格，外饰也 ...

三月初天津行旅 序 三月初，开学的第二周，学校里的各种活动还没有彻底办起来，总是待在学校里总归是有点无聊的。当我在群里向高中同学们提出要去天津旅行的倡议时，可谓是一呼百应。顺其自然，我也就成为了这次旅行的筹划和组织者，成为了一个旅行团团长的角色。 一个晚上便做完了整个旅行计划，但在事后看来，这份计划的强度实在是太高了，以至于我们两天的时间里每天都走了两万七千步（另外还骑了不少车），但是我们也获得了一份较为完备的天津旅行体验。 三月初天津行程计划-ver1-修正 如果说上次我去阿克苏的时候主要关注的是南疆作为特殊地区的民族问题等政治和经济议题，那么这次天津之旅我的注意力便不在于此了。我想要关注的是天津这座城市的人文和城市生活，看一看这里的人们是如何生活的，这座城市到底是不是宜居的。 答案马上揭晓。 Day 1 高铁记 乘坐京津城际高铁（复兴号），三十分钟就可以抵达天津站，甚至比从北京大学抵达北京南站还要快；一位同学也为此深深震撼——过去他认为从北京到天津是一段很长的旅程，没想到这么快就能到；我想，这就是高铁时代的魅力吧——使人们免于旅途的舟车劳顿，让 200-300 公里内的城市圈真 ...

我在P大的新学期 早早回校 2 月 15 日，我就回到了 P 大。这是我大学生涯中第一次在寒假结束后提前回校，似乎也是首次独自一人，开启一段前往异乡的长旅，这倒是一种很奇妙的体验，有点孤独和寂寞，但也有一种遗世独立般的莫名的自由感。 我应该是第二个离开宿舍的，有点遗憾，走的时候没能好好收拾一下宿舍；不过回来时的所见还是略让我更感到失望，宿舍虽然走的时候有好好收进来各种衣架之类的外设，关闭了各种各样的电器，但是地面还是一点也没有打扫，还有一些垃圾，这真的令我不太爽。 没办法，只能自己动手，把宿舍打扫了一遍，把自己和舍友摆在外面的东西收拾了一下，然后就开始了新的学期。 大消费 寒假回家过年，收获了一笔不小的压岁钱，钱包一下子充裕起来，然后就禁不住追求美好生活的愿望诱惑，一下子就花了不少钱，买了一些自己想要的东西。 首先是新学期的一系列教材，这个是必须的，花了我几百大元。 然后去超市采购了一系列的生活消费品，也花了一两百元。 败家之眼 接下来是大头，我买了一台新的笔记本电脑，这个是我一直想要的，用来弥补我现在使用的游戏本便携性的不足，和记电子笔记不方便的问题。 想要弥补便携性的不足，还要能够 ...

出乌鲁木齐记 高中三年，大约是出于学业繁忙之故，寒假没有会过一次阿克苏去探望我的爷爷奶奶，上一次去的时候大概还是上初一或初二的时候。 现在上大学，寒假也没有作业，时间毕竟充裕，也确乎是有一定的时间去看看我的爷爷奶奶。 但是为什么不选在过年的时候去呢？ 这里就涉及到我的一点点小小的私心了：我和爷爷奶奶的心理联系并不是很深刻，这也许是他们因为和我们家分居两地，所以在我的成长中陪伴较少的缘故罢；况且今年我们2月19号上课，在家过年的时间就很少了，所以我选择在乌市陪伴我的父母一起过年；心理上和爷爷奶奶的联系很弱，但是生理血缘和社会文化背景所带来的要求依然存在，所以最后就变成了这个样子。 1 月 27 日，深夜，刚刚结束返回高中母校对高一年级的宣讲，陪着他们到了结束晚自习的 23：30，坐在回家的车上，我开始思考起了应该规划一个怎样的行程，使得我能够在阿克苏短程逗留，完成我的探望任务，也顺便做一点游览。 轻装简从 和家人简单商议，一场行程就这样定了下来： 1 月 28 日 23：20 开的 T9536 次列车，次日 9：10 到阿克苏。 1 月 31 日 23：20 开的 T9538 次列车， ...

2023年终总结——写在两年的交会之处 梦是现实的延续，现实是梦的终结。 ——《新世纪福音战士》 你啊，是从什么时候开始做一场梦的呢？ 以前是不会写年终总结的，我总是有意无意地在想要忘记、丢弃，或者说逃避吧，我的历史；更不想让别人看到我的历史。但是上高中时，我们的班主任将写年终总结这件事当作了一项元旦时期必做的“作业”，当然，这是一项很自由的作业，想怎么样写都可以。我现在已然养成了写年终总结的习惯，而且决定每年都挑选这一年中比较重要的事情开诚布公地写下来，讲一讲我的故事和感想。 今年的年终总结，就写我的梦想和我的追梦吧。 小小的梦想 我的当前持有着怎样的梦想呢？说通俗一点，就是“向深空更深处去”——造最大最强的火箭，去太空中更远的地方游目骋怀，满足我那探索一切未知的好奇心。 梦是现实的延续。 在那个燥热的午后，当我从八道湾的旧平房中翻出一本1999年的旧科技杂志，嗅着其中的油墨味趴在床上借着窗外的阳光津津有味地阅读起来时，命运的齿轮开始转动…… 1999年啊，那是上一个太空时代的尾声，亦是下一个太空时代的开始。杂志中，尽管和平号空间站（Mir）的图片看上去已经破旧到不堪入目的程度， ...

和我签订契约，成为函数式魔法少女吧！ ——胡振江（伪） in 《函数式魔法少女》 写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。 这篇文章主要介绍了在 Agda 中的 Internal Verification （内生证明）的数据结构，以及相关的“内生证明”思想。 这是“内生证明”的第二篇文章，我们将会讲到 BST 和 B-Tree 的 Internal Verification ，这时我们就会看到 Internal Verification 的一些更加深入的应用。 烧脑环节开始了！ Agda，启动！ 参考资料： 《函数式程序设计》课件 《Verified Programming in Agda》 提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法 本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。 先准备一下我们需要用到的布尔型二元关系