类型检查算法：证明检查算法的机械实现
上一篇给出了 STLC 的类型规则。规则本身只描述了"什么样的程序合法"，并没有说"怎样判断合法"。本篇把这个判断过程写成一段可运行的 Python 程序，约 200 行。 读完这段代码之后，"类型检查 = 证明检查"会从概念对位落到一段能跑出真实输出的事实。系列主线问题"为什么编译通过就是定理得证"的第一层——证明可被机械检查——也在这里被实证。 算法策略：从规则到代码 上一篇的规则形如： 123 Γ ⊢ e1 : τ1 → τ2 Γ ⊢ e2 : τ1────────────────────────────────────── (App) Γ ⊢ e1 e2 : τ2 把这条规则直接读成一段 Python 代码： 12345678def synth_app(env, app_expr): fn_ty = synth(env, app_expr.fn) if not isinstance(fn_ty, Arrow): raise TypeE...
简单类型 lambda 演算：最小可证明系统
上一篇打通了命题与类型的对应：命题就是类型，证明就是程序。本篇把这条同构落在最小可证明系统上——简单类型 lambda 演算（Simply Typed Lambda Calculus，STLC）。 STLC 是类型系统的"hello world"。它语法只有三种表达式、五条核心类型规则，却已经能精确对应整个直觉主义命题逻辑。读懂 STLC 之后，依值类型、归纳类型、Lean 4 都只是在它上面加构造，不会改变骨架。 本篇先写出 STLC 的语法和类型规则，再画一棵推导树，最后说清楚 STLC 能证明什么、不能证明什么。下一篇把这些规则用 Python 落地成一个真跑的类型检查器。 三种表达式 + 三种类型 STLC 的核心语法可以用 BNF 写成： 123456e ::= x -- 变量 | λ x : τ . e -- 函数（抽象） | e1 e2 -- 调用（应用）τ ::= A -- 基本类型 | τ1 → τ2 ...
命题即类型：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...
