Morgen-Kornblume's Blog

12-13社论 写作缘由 又到一年国家公祭日，我们怀着沉痛的心情，悼念那些在抗日战争中被日本侵略者残忍杀害的同胞们。在这一天，我们要铭记历史，缅怀先烈，更要从历史中汲取教训，这是每年必提的话题。但是，今年的国家公祭日，我们要说的话，不仅仅是这些。 在当前国际形势日渐紧张，中日关系较差的特殊时代背景下，我想和大家讲讲该如何看待日本的侵略历史，这中日关系中的最大痛点。 日本在近代对中国和整个东南亚地区的侵略历史，在本文中就不再赘述。 后来在中日关系改善的过程中，毛主席提出过要把日本人民和主导侵略的当时的日本帝国主义政府区分开来看；这个提法基本是正确的，而不仅仅是为了改善外交关系而设计的说辞。 疑问 但是，这个提法也有一个问题，就是把日本人民和日本帝国主义政府区分开来看，这个提法，对于日本人民来说，是不是太过宽容了呢？日本的人民在侵略的过程中是否也负有一定的责任和罪孽呢？ 先说结论：我认为是的，但是，这些责任和罪孽，与那些主张发动侵略、在侵略中犯下战争罪的位高权重的军国主义分子的罪孽相比，是部分性的、次要的，在一定的程度上，我们需要宽容日本人民的罪孽。而军国主义分子们要负的责任和罪孽，是主要 ...

和我签订契约，成为函数式魔法少女吧！ ——胡振江（伪） in 《函数式魔法少女》 写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。 这篇文章主要介绍了 Agda 的基本语法，以及 Agda 中的布尔代数和相关的定理证明。 Agda，启动！ 参考资料： 《函数式程序设计》课件 《Verified Programming in Agda》 提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法 本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。 类型的声明 在 Agda 中，虽然我们的标准库就会包括 Bool、Natural 等类型，但是我们也可以重新出发，自己定义它们。 我们这次就拿最简单的布尔类型来举例。 布尔类型 我们可以这样定义布尔类型： 12345678910module boolean where-- 如果你想要在后面的代码中使用你所定义的类型，你需要在 ...

论文移植 这篇文章是我为北京大学大学思政实践课程——爱乐传习所写的论文，现在移植到这里，以便于更多人看到。 后续内容将在论文撰写完成后更新。 摘要： 在每个时代、每个国家，音乐都是参与人民文化、民族精神和公民人格培育和塑造的重要因素。本文通过历史文献调研的方法，回顾邻国日本在战后以日本共产党和工会组织为领导的工人阶级歌声运动历程，并揭示其在培育日本战后国民精神和思想、唤醒青年的关键作用，以及说明这种作用是如何发生、如何扩大其影响力的，进而从中借鉴经验，为我们开展以音乐为媒介的思政育人教育提供有益的启示。 关键词： 日本；音乐育人；国外马克思主义；革命运动；现代史；工人阶级 引言 “大家齐声合唱的运动，对人类来说不仅是最基本的音乐行为，在社会共同体的形成与维持，在社会重大变革的局面中也经常发挥着至关重要的作用。特别是在近代社会，从法国大革命开始，歌声有时候被作为维持统治的手段，有时又作为集结民众反抗力量的号角。第二次世界大战后在日本风靡一时的‘歌声运动’的意义，就在于它为从音乐和文化为切入点考察日本近现代的历史提供了绝佳的合适材料。”——[日]渡辺 裕《为战后文化注入新的气息——& ...

在过去的一段时间内，我已经完成了黑白棋小游戏的基本逻辑的实现和文字界面的实现，现在我打算开始进行 Unity3D 的开发，实现一个简单的图形界面，进而基于此尝试更多的高级功能。 开个坑先，后面再慢慢填。

Verified 马猴烧酒 in Agda 第一篇 和我签订契约，成为魔法少女吧！ ——QB in 《魔法少女小圆》 写这个文章的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。 选择学习函数式程序设计，就好像选择成为魔法少女，如果你不能真正喜欢并且理解函数式编程、并且为它付出你学习的努力，那么你就会学废，彻彻底底地变成“函数式魔女”。 我还真是个笨蛋。 ——美树沙耶香 in 《魔法少女小圆》 这是本系列文章的第一篇，主要介绍为什么我们要学习 Agda 和 Verified Programming，以及我们需要学什么。 我参考了胡振江老师的《函数式程序设计》课程的课件，以及《Verified Programming in Agda》这本书。 《函数式程序设计》课件 《Verified Programming in Agda》 提示:阅读本文章可能需要一定的FP基础（例如Haskell）\color{red}提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell）提示:阅读本文章可能需要一定的 ...

复出 本来上了大学以后，是不想打算法竞赛的，但是我决定给自己找点事做，找点学术上的兴趣爱好，刚好学院里面有个大佬拉我组队打THUPC，我也就答应了。但是因为自己太菜被甩了，所以很生气，就准备拉上过去的朋友们一起打这个比赛，现在这里占个坑，等比赛结束了再来写题解。 本段文字创建于2023年12月6日。（为了防止某禁赛三年悲剧重演，提醒下次来的时候填写更新日期；当然，我的博文是有创建日期记录的） 题解 你们觉得我会写题解吗？ 当然是不会的，这个比赛里面，我根本没有什么会的。 我太菜了。 菜就多练，不会写就别玩。 OI是OI，校赛是校赛。 哥们你要是把校赛当OI打，哥们你咋不回去复读高中呢？

为什么会突然去读这本书 以前初高中的时候看过，但是那时候这篇小说被发行商串在各种各样的刘慈欣的集子里面，然后被删减和改版的也很多，后来听说这篇小说有完整版本，但是一直没有找到。最近在B站上看视频，看到科幻视界讲这本书的视频，于是又重新发生了兴趣，去Z-Library上找到了这本书的完整版，花了上周天一个早上的时间读完了这四百多页的电子书，深有感触。 完整版目录（供参考） 死星：终结、夜空骄阳 选拔：山谷故事、国家 大学习：世界课堂、总参谋长、味精和盐 交接世界：大量子、新世界试运行、公元钟、超新星纪元 超新星纪元初：超新星纪元初一小时、悬空时代 惯性时代：视察、全国大会、好玩的世界、争论 糖城时代：美梦时期、沉睡时期 美国糖城时代：冰淇淋盛宴、美国糖城时代、世界游戏 超新星战争：南极洲、铁血游戏、一千个太阳、公元地雷、反击、暴风雪 创世纪：新总统、访问、新世界游戏、交换、抉择、大移民、创世纪 附记：蓝星星 读后感和我对前几个月大学生活的反思 关于这本书，我觉得最有意义的部分就在于作者对于人类历史一般规律的探讨，在这里充满了辩证性的思考。我 ...

为什么是函数式程序设计？ 这是一篇有点邪性的文章，主要内容是传 FP 的教，当一个 QB 式的人物，把天真无邪的新人程序员带进 FP 的世界，变成 FP 魔法少女。 如果你不想当函数式魔法少女，那么请你立即退出这篇文章。 引言 函数式程序设计是一种具有悠久历史的程序设计方法。在几十年以来的大多数时间中，函数式程序设计栖身于象牙塔内，慢慢成长，积蓄力量，并没有在软件开发实践中得到广泛使用。然而，世异时移，这种情况正在发生变化。随着软件系统复杂性的不断提高以及软件与现实世界关系的日益紧密，如何严格确保软件系统的正确性和可靠性，逐渐成为一个重要的现实问题。函数式程序设计建立在严格的数学概念的基础上，具有良好的数学性质，为上述问题提供了一种现实可行的解决方案。目前，大多数的主流程序设计语言都在逐渐引入函数式程序设计的各种成分。 学习函数式程序设计的基本思想、核心概念、以及相关的程序设计方法和程序推理方法，能够为学生从事算法设计、程序语言设计、软件开发等领域的研究和实践工作建立坚实的理论基础。 —— 《计算概论A（实验班），函数式程序设计》课程介绍 我曾经是一个 OIer，会写很多的 C++ ...

献给我的19岁生日 一篇随笔，谨以此纪念我度过的十九个春秋。 献诗 月行于中天之上 照耀着摇篮（cradle）中的孩子啊 雪花飘转 风儿呼啸 它们都在为了你的诞生而舞蹈与歌唱 即使今天你不在故乡(heimat)的摇篮中 即使今天你已经长大 不再相信童话 但世界上依然有人为你祝福与歌唱 为了这1365\frac{1}{365}3651​的奇迹 为了你诞生的这一天 所以，也请为了你自己而歌唱吧 歌唱…… 一点随想 这是我的 19 岁生日，也是第一个在大学里，在远离家的地方度过的生日。 在这样一个特殊的日子和特殊的场景，我想，我应该写点什么。 进入大学以来，我的整个生活都发生了翻天覆地的变化。世界以它的方式在我的面前展开，让我探知到了巨大的信息量和多样性。而我又身处北京大学这样一个高智人群聚集的地方，这让我有时感到自己的渺小和无知（卑京大学实锤了）。进了大学后，我还没有来得及享受成年、离开家乡以后自由自在的生活，期中考试以后一天比一天冷的天气，北京冬天刮起来的大风，就将世界夫人的残酷一面展现在了我的眼前。社会中内卷啦，竞争啦，阶级的上升和下降啦……种种的压力顺着无形的利维坦的无数的触手， ...