Morgen-Kornblume's Blog

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

三月初天津行旅 序 三月初，开学的第二周，学校里的各种活动还没有彻底办起来，总是待在学校里总归是有点无聊的。当我在群里向高中同学们提出要去天津旅行的倡议时，可谓是一呼百应。顺其自然，我也就成为了这次旅行的筹划和组织者，成为了一个旅行团团长的角色。 一个晚上便做完了整个旅行计划，但在事后看来，这份计划的强度实在是太高了，以至于我们两天的时间里每天都走了两万七千步（另外还骑了不少车），但是我们也获得了一份较为完备的天津旅行体验。 三月初天津行程计划-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 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。 先准备一下我们需要用到的布尔型二元关系

和我签订契约，成为函数式魔法少女吧！ ——胡振江（伪） in 《函数式魔法少女》 写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。 这篇文章主要介绍了在 Agda 中的 Internal Verification （内生证明）的数据结构，以及相关的“内生证明”思想。 这是“内生证明”的第一篇文章，我们将会介绍 Vector 的 Internal Verification ，但是内生证明在 Vector 中还是很浅层的，应用也不是很明显，下一篇将会讲到 BST 和 B-Tree 的 Internal Verification ，这时我们就会看到 Internal Verification 的一些更加深入的应用。 但是，下一节将会更加烧脑，所以这一章就权当过渡，休息休息脑子罢！ Agda，启动！ 参考资料： 《函数式程序设计》课件 《Verified Programming in Agda》 提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode ...

和我签订契约，成为函数式魔法少女吧！ ——胡振江（伪） in 《函数式魔法少女》 写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。 这篇文章主要介绍了在 Agda 中定义列表 List 的方法，以及一些和 List 相关的函数和定理证明。 Agda，启动！ 参考资料： 《函数式程序设计》课件 《Verified Programming in Agda》 提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法 本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。 List 及其定义 12345module list wheredata List {l} (A : Set l) : Set l where [] : List A _::_ : (x : A) -> (xs : List A) -> List A 这个 Li ...

讲稿：第五次思修Pre-中国道德与中国理想——以电影《流浪地球》为例（道德部分） 前置介绍 （假如没有主持人，我第一个上去的话就说这些） 今天我组汇报的题目是中国道德与中国理想——以电影《流浪地球》为例。 我组的汇报分为四个部分： 道德，由我来讲 道德与理想的关系，由李嘉豪同学讲 个人理想，李沂桉同学讲 国家理想，方思童、朱冠宇同学讲 接下来我将依次讲三个部分，分别是：道德在《流浪地球》中体现出的几个特征，集体的道德，个人的道德。 请大家先回忆一下流浪地球系列电影的的剧情，我们马上开始吧。 道德在《流浪地球》中体现出的几个特征 道德，是社会意识形态之一，是人们共同生活及其行为的准则和规范。 道德通过社会的或一定阶级的舆论对社会生活起约束作用。 ——百度百科 以上是道德的定义，那么“道德”，作为一种社会规范、一种社会约束力的存在，那么必然有其存在的目的和要维护的对象。 我们暂时将道德存在的目的理解为“维护社会当前秩序的稳定与正常运行”。 那么我们进一步思考，为什么要维护社会当前秩序的稳定与正常运行呢？ 那是因为，社会当前秩序的稳定与正常运行，是社会发展的基础，是社 ...

和我签订契约，成为函数式魔法少女吧！ ——胡振江（伪） in 《函数式魔法少女》 写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。 这篇文章主要介绍了在 Agda 中定义 Peano 自然数、自然数的加法和乘法运算，以及相关的定理证明。 Agda，启动！ 参考资料： 《函数式程序设计》课件 《Verified Programming in Agda》 提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法 本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。 Peano Natural Numbers Peano Natural Numbers 的基本思想是，我们可以用一个类型来表示自然数，这个类型有两个值，一个是 0，另一个是后继函数，它接受一个自然数，返回这个自然数的后继。 在 Agda 中，我们可以这样定义 Peano 自然数： 123data ℕ : Se ...