命题即类型：Curry-Howard 同构
上一篇用 BHK 解释把"证明"重新定义成"构造一个见证物"，并提到那份翻译表"看起来就是一组类型"。本篇正式给出这个直觉的精确版本：Curry-Howard 同构——命题就是类型，证明就是程序，证明检查就是类型检查。 这条同构是形式化方法的基石。理解了它，"为什么形式化编译器编译通过就是定理得证"这条主线问题第一层翻译就被打通：检查证明这件事被压成了机械的类型检查。 本篇不假设读者会 Coq 或 Agda，但要求理解上一篇的 BHK 表，并能读简单的 Python 类型注解。中段会用 Lean 4 写两段简短代码做对照。 同构的对照表 把上一篇 BHK 表整理成"逻辑端 ↔ 类型端"的并列形式： 逻辑端 类型端 程序端的项构造 程序端的项消费 原子命题 A 基本类型 A 公理/假设变量 当作变量使用 ⊥ 空类型 Void / Empty 没有构造子 absurd : Void → C ⊤ 单位类型 Unit () 无信息可消费 P ∧ Q 积类型 P ...
直觉主义逻辑与 BHK 解释：什么算一个证明
形式化方法导引系列的主线问题是：“为什么编译通过就是定理得证”。要把这条等式撑起来，第一步是回答一个看似更基本的问题：什么算一个证明。 中学数学里"证明"通常意味着一段以"证："开头、以"证毕"结束的自然语言论证。这种证明里允许使用反证法、双否定消去、排中律，论证的合法性靠人类同行评议把关。这条路线下，"证明"是一份可被阅读和判断的文档。 形式化系统走另一条路。证明被要求成为一个可以被机械构造、机械检查的对象。这条要求一旦贯彻到底，传统数学里的"反证"和"排中"会被部分剥离，剩下一种叫直觉主义逻辑或构造主义逻辑的子系统。BHK 解释（Brouwer-Heyting-Kolmogorov）正是把"证明"在这个子系统里重新定义成"构造一个见证物"的规范。 本篇展开 BHK 翻译表，解释为什么它天然导向 Curry-Howard 同构，并用 Python 把表里的每一条编码成一个数据类。 古典逻辑与直觉主义逻辑的分歧 考虑一条...
编译通过为什么就是定理得证：形式化方法系列导引
形式化方法课程开学第一周通常会出现一个让 CS 背景的学生愣住的演示：教师在 Lean 4、Coq 或 Agda 里敲完几行代码，按下保存键，编辑器右侧弹出 No goals 或者编译进程打印 Build completed successfully，然后教师宣布：定理已被证明。 让人愣住的不是命题本身，而是这条等式：编译通过 = 定理得证。命令式语言里编译通过只意味着语法和类型对得上，离"这段程序做的事是对的"还远；可在形式化系统里，编译通过却被当成数学意义上的"得证"。 这条等式要怎样才能成立？需要类型系统强到什么程度？类型检查器到底替人类干了哪些活、又留下哪些活没干？这个系列从这个具体问题展开，写给硕士一年级、刚开形式化方法课、有 CS 背景但还没真正用过证明助手的读者。 一个具体场景 Lean 4 里写一条命题以及它的证明可以是这样： 123-- 命题：∧ 满足交换律theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := fun h => ⟨h.right, h.left⟩ 把这段...
U型思考法：从表象到本质的深度思维模型
大多数人解决问题的方式是一条直线：遇到问题 → 凭经验找答案。这种"直线式思考"在处理简单、常规事务时够用，但面对真正重要的决策——选择职业方向、制定企业战略、判断投资标的——往往导致"低水平重复"：解决了表象，问题换个马甲再来。 U型思考法提出了一种不同的路径：遇到问题时不急于在现象层面求解，而是先向下挖掘本质，在本质层面找到根本性解法，再回到现实落地执行。思维轨迹画出来，恰好是一个"U"字。 两个"U"：一字之差，两套体系 在深度思维方法论领域，有两套以"U"命名的理论体系，经常被混淆。先厘清边界： 维度 U型思考（沈拓） Theory U / U型理论（夏莫） 提出者 沈拓，混沌学园创新领教，清华 x-lab 课程教授 Otto Scharmer，MIT 斯隆管理学院资深讲师 发表时间 2022 年（人民邮电出版社） 2007 年（英文初版），2013 年（中译本） 核心问题 如何挖掘问题本质并基于本质做决策 如何从"正在生成的未来"...
情绪提示词：用心理学手段提升 LLM 性能的研究综述
在提示工程领域，有一类反直觉的发现：“对模型说好话"或者"给模型施压”，真的能让它表现更好。这不是段子，而是有严肃学术论文支撑的结论。更进一步的问题是：能不能用 gaslighting（煤气灯操控）式的心理操纵手段，系统性地提升模型性能？ 本文梳理了 2023-2026 年间关于情绪提示词的学术研究，试图回答三个问题：效果有多大、机制是什么、边界在哪里。 关键发现一览 先摆结论，后面逐一展开： 研究 核心发现 提升幅度 EmotionPrompt (Li et al., 2023) 在提示词后追加情绪刺激句，多个 benchmark 显著提升 8%-115% OPRO (Google DeepMind, 2023) LLM 自动优化出"深呼吸"提示词，数学推理大幅提升 GSM8K 上从约 34% 到 80% Anthropic 可解释性研究 (2025-2026) Claude 内部存在 171 个功能性情绪表征，且因果性地影响输出 定性发现 Usman (2026) 8 种情绪框架测试，压力彻底消除诚实行为，但...
回到工程：Linux VM 如何改变性能诊断
前面 16 篇从地址空间到 OOM，逐层拆解了 Linux 虚拟内存子系统的结构和机制。这些知识的价值不只在于读源码——更在于它提供了一种分层诊断习惯：遇到内存相关的性能问题时，先定位层次，再找对象，再看状态转移，最后用指标验证。 核心问题可以压成一句话： Linux VM 的价值不只在源码知识，而在一种分层诊断习惯：先定位层次，再找对象，再看状态转移，最后用指标验证。 系列概念地图 整个系列覆盖的层次和对象： 1234567891011121314151617181920212223用户空间视角 内核视角───────────── ──────────malloc / mmap VMA (vm_area_struct) ↓ 虚拟地址 ↓page fault 页表 (PGD→P4D→PUD→PMD→PTE) ↓ 物理页分配 ↓RSS 增长 ...
OOM Killer：内核什么时候决定杀进程
上一篇讲了 memcg 如何把全局内存资源划分成层级预算。当预算用尽且回收无力时，最后一道防线是 OOM killer——通过终止进程来释放内存。这不是内存管理的常规路径，而是所有正常手段都失败后的兜底。 核心问题可以压成一句话： OOM killer 是多轮分配、回收、压缩、写回、swap 都无法满足请求后的兜底路径，不是内存管理的常规目标。 问题从哪里来 内存分配失败的处理有一个基本问题：内核不能简单地对调用者返回"分配失败"。很多内核代码路径不检查分配失败（GFP_KERNEL 分配假设不会失败），即使返回错误，用户空间进程通常也没有合理的 fallback 逻辑。 所以内核的策略是：在返回失败之前，尽可能通过各种手段释放内存。如果所有手段都用尽仍然无法满足分配请求，最后才走 OOM kill——选择一个进程杀掉以释放它占用的内存。 到达 OOM kill 之前的完整路径： 1234567891011121314__alloc_pages() 分配请求 → 检查 zone 水位线：有空闲页? → 成功返回 → 唤醒 kswapd 后台回收 →...
cgroup memory：内存从全局资源变成局部预算
上一篇讲了 SLUB 如何在页之上管理小对象的分配。到此为止，所有讨论都假设一个全局的内存资源池——进程共享同一组物理页，回收和 OOM 是全局决策。容器化环境打破了这个假设：一个容器不应该消耗完整机器的内存，它的 OOM 不应该波及其他容器。 核心问题可以压成一句话： memcg 把全局 VM 策略投影到层级资源边界里，使回收、统计和 OOM 都带上 cgroup 语义。 问题从哪里来 传统 Linux 内存管理是全局视角：所有进程共享物理内存，kswapd 按全局水位线回收，OOM killer 从全局选 victim。这在单租户系统上没问题，但在多租户场景（容器、虚拟化、共享主机）上不够： 第一，隔离性缺失。一个行为异常的容器可以消耗所有可用内存，触发全局 OOM，导致无关容器的进程被杀。 第二，资源可预测性缺失。一个容器无法知道自己"还能用多少内存"——这取决于其他容器当前的使用情况。 第三，统计粒度缺失。管理员无法回答"这个服务用了多少内存"——/proc/meminfo 只有全局数据。 cgroup memory cont...
SLUB：小对象为什么不直接按页分配
上一篇讲了 buddy allocator 如何按阶管理物理页的分配与释放。但 buddy 的最小粒度是一页（4KB）。内核中绝大多数对象远小于 4KB——一个 struct dentry 是 192 字节，一个 struct inode 是 600 字节左右。如果每个小对象都分配一整页，内部碎片率将高达 95% 以上。 核心问题可以压成一句话： 内核对象通常比一页小得多，SLUB 用 slab cache 把页切成同类型对象池，减少碎片和初始化成本。 问题从哪里来 内核不断创建和销毁各种数据结构：每次 open() 分配一个 struct file，每次路径查找分配一个 struct dentry，每次网络包到达分配一个 struct sk_buff。这些对象有两个共同特点： 第一，大小远小于 4KB。如果用 buddy allocator 直接分配，一个 192 字节的 dentry 占用 4096 字节物理页，利用率不到 5%。 第二，同类型对象的分配/释放极为频繁。dentry 在路径解析密集的工作负载中每秒创建/销毁数十万次。每次都调用 buddy allocat...
Buddy system：物理页如何按阶分配
上一篇讲了 huge page 如何通过增大映射粒度降低 TLB 和页表开销。但分配 2MB 连续物理内存本身就不是简单的事——物理页分配器必须能快速找到指定大小的连续空闲块。Buddy system 就是 Linux 用来解决这个问题的核心机制。 核心问题可以压成一句话： buddy allocator 用按阶（order）拆分和合并管理连续物理页，解决的是页级分配与碎片控制问题。 问题从哪里来 内核需要分配连续物理页的场景很多：DMA buffer 要求物理连续、huge page 需要 order-9（2MB）的连续块（1GB 页通常在启动时通过 HugeTLB 机制预留，不走常规 buddy 路径）、设备驱动需要特定对齐的物理内存。 最简单的方案是维护一个空闲页链表。但这有两个问题：第一，找"连续 N 页"需要遍历链表检查物理地址连续性，时间复杂度不可控；第二，反复分配释放后内存碎片化，即使总空闲页足够也可能凑不出连续块。 Buddy system 用 power-of-two 分块解决这两个问题：只管理 2^n 大小的块（称为 order-n ...
