#计算机
从反向传播到多层感知机
记 MarkItDown 工具试用
很早听说微软的 MarkItDown 工具，简单尝试。由于本地空间有限，我在学校提供的云计算实验平台 PKU CLab 上配置了一个 Ubuntu 环境，在我的 Windows 中远程连接。…
天使与方格吞噬者问题的策略模拟
天使问题发生在一张无限大的整数网格棋盘上，天使初始在原点 $(0, 0)$ 处。每回合，先由魔鬼禁用掉任意一个格子，然后天使尝试移动到一个未被禁用的格子。天使的移动受力量值 $K$ 约束：若当前在 $(x, y)$ 则下一步位置需满足 $|x' - x|, |y' - y| \leq K$. 天使的胜利条件是总是有方法移动下去。…
推荐一个 Markdown 转 PDF 的流程
有时我们想要排版出一份数学/物理试卷或者 cheatsheet, 可能涉及到数学公式、代码块，并以 PDF 形式给出，但是不希望使用麻烦的 PDF 编辑器或者 Word, 也不希望使用一整套 pdftex. 此时可用此流程，只需用到 VSCode 与一个浏览器。
或者在 AI 时代也可使用基于 VSCode 开发的 Cursor, 下文提及的样式可以交给 AI 定制（建议在提示词中指明使用的 Markdown 插件）。…
基于有限域上数论的密码系统
主要参考的是 An Introduction to Mathematical Cryptography 第二章离散对数、第三章整数分解及第四章数字签名。…
关于高性能计算的混乱感想
此文主要为吐槽，缺乏实质性内容。大致是发现有一个第三届 PKU HPCGame 的活动可以参加，在其中读题所见的浮光掠影与感想。请忽略其中的错误。…
记 Rust 编译至 WebAssembly 流程
一个完整的极度简化和减少下载量的 Rust 编译至 WebAssembly 的流程。
Bird Meertens 形式与高效程序导出
主要包含使用 Bird Meertens Formalism 导出高效程序与进行自动并行化。
这是本课程的最后一个部分，同时可能是在上半学期和下半学期前部的铺垫下真正想讲的东西。其中函数式编程的想法提供了无副作用的函数和高阶函数的例子，从而能够被我们讨论；定理证明器则允许我们验证推导的正确性。…
Hash 与基于哈希的 table 实现
阅读一下 Rust 标准库的 Hash 与 RawTable 相关代码。本文参考的 Rust 版本是 1.90.0-nightly…
量子信息的基本原理与基本结论
量子信息的一些系统学习。从量子状态定义到量子密集编码、量子隐形传态、纠缠的量化。
Agda 语言与基本的形式化证明
下半学期使用 Agda 来讲授函数式程序推理与演算，也展示了 Internal Verification 思想。…
异或密码的实现与 AES
本文实现 The Cryptopals Crypto Challenges 的基础练习集 Set 1. 曾经我使用 Julia 写过类似的内容，但没有良好的解耦。因此改用 Haskell 进行更清晰的实现，读者可在 Haskell Playground 运行，也可使用自己熟悉的语言实现。…
着色器中的随机与噪声
基于 GLSL 的噪声实现及应用。
基于 GLSL 的色彩与数学绘制
基于 GLSL 的 HSV 操作与经典数学对象的绘制。
GLSL 的基础用法与 Raymarching
基于 GLSL 的着色器基础内容：2D 绚丽图像及 Raymarching.
Haskell 的单子与副作用
函数式语言如何引入副作用：函子、应用函子、单子。
Haskell 的基础概念与语法
函数式语言的基础特性概览：列表、类型与高阶函数。
基于 Lua 的模拟环境
封面图为《末日时在做什么？有没有空？可以来拯救吗？》的角色珂朵莉持有的圣剑「瑟尼欧里斯」，在设定中由 41 个形如“感冒发烧时睡觉不会做噩梦”、“在喝茶时不会被茶烫到舌头”的护符组成，异稟是“将对手化为死者”。本文的想法也类似于此。…
LISP 模式：图灵完备及元编程
在 1960 年，John McCarthy 中一篇论文中定义了一个名为 Lisp（意为 list processing）的编程语言。Paul Graham 认为，“目前为止只有两种真正干净利落，始终如一的编程模式：C 语言模式和 Lisp 语言模式。此二者就像两座高地……随着计算机变得越来越强大，新开发的语言一直在坚定地趋向于 Lisp 模式。”
Lisp 似乎受到了 Lambda 演算与 Kleene 的递归论的影响，但不完全来自于它们。…
无类型 λ 演算与重写系统
本文讨论 Alonzo Church 发明的无类型 λ 演算（λ-calculus）。这是一个类型论与计算理论的基础模型。…