Morgen-Kornblume's Blog

和我签订契约，成为函数式魔法少女吧！ ——胡振江（伪） 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 ...

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打，哥们你咋不回去复读高中呢？