用途：把散落在决策日志、工程规范、形式化规范、快速上手里的专门术语收拢成一页纸，供新人按图索骥。每个条目给：定义 → 出处。出处优先给决策编号（D43）或文档章节（工程规范 §2 I-14），不给重复展开。
本文不重复定义通用编程/PL/数学术语（函数、类型、多态、合一、命题等），只定义本项目自己的概念或对通用词的特定用法。
维护：本表随语言演进追加，不删条目；废弃概念标记 [废弃] 保留。
| 术语 |
定义 |
出处 |
| 凝华 |
语言名字的来源：命题不经运行时，直接在编译期"凝结"为静态保证。与物理现象"气→固"同构。 |
语言简介 开篇 |
| 上下文系统 |
本语言的灵魂：命题作为独立存在弥散在作用域 Γ 里，函数的上文/下文描述"调用前空气里必须有什么、调用后空气里会多出什么"。不是参数、不是值。 |
草案思路 D20/54；形式化规范 §3
|
| 命题 / 值 二分 |
值世界（可求值、可 print、可传参）；命题世界（住 Γ，编译期证明，不进 JS）。两个世界不通：x != 0 是值，x ≠ 0 是命题。 |
草案思路 D54；形式化规范 §1.1
|
| 弥散 |
命题像气体一样在作用域里流动。事实来源有三：显式注入（axiom/var）、函数下文、if/when 分支条件。if/when 是值世界 → 命题世界的唯一桥。 |
形式化规范 §3.1 |
| 零成本擦除 |
命题、类型、理论参数全部不落入 JS。例外：类型类字典（D22 加了此例外）。unchecked.axiom[q] 只留 // axiom: q 注释供审计。 |
草案思路 D22 |
| unchecked |
唯一的逃逸口。三种形态：unchecked.axiom[q]（逃证明义务）、unchecked f(x)（逃纯度）、unchecked v = 1（逃可变性）。 |
草案思路 D5；语言语法 §5
|
| 设计原则宪法 |
九条判据（D41 八条 + D63 第九条"风味纲领"）。语法争议一律先问宪法。 |
草案思路 D41/63 |
| 风味纲领 |
语法像 Kotlin；基础概念像 Rust；创新概念像定理证明器与函数式语言（Koka/Lean 圈）。 |
草案思路 D63 |
| 健全但不完备 |
证明器的承诺边界：所有规则保真（健全），但不承诺证明一切（不完备，哥德巴赫免谈）。证不出 ≠ 假，用 axiom 补。 |
草案思路 D40；形式化规范 §4
|
| 术语 |
定义 |
出处 |
| Γ（Gamma） |
作用域内命题事实的多重集。条目：e:τ、e₁=e₂、谓词原子 n{ts}、命题绑定、伴生记录 f<args>。 |
形式化规范 §3 |
| 上文（preps / 前置） |
fun f(...) <p> : T 中的 <p>。调用前必须在 Γ 里找到 p 的证明。缺 → E-PRE-UNPROVEN。 |
形式化规范 §3.1 |
| 下文（posts / 后置） |
fun f(...) : T <q> 中的 <q>。函数体的证明义务：体末尾 Γ 必须蕴含 q。缺 → E-POST-UNPROVEN。 |
形式化规范 §3.1 |
| 函数体是证明义务 |
声明不是可信公理。体结束时 Γ ⊇ 下文；逃生门只有 unchecked.axiom。 |
草案思路 D18 |
$（返回值指代） |
下文/调用注入中指代返回值。体内 $ ≡ 末表达式；调用点 $ ≡ 调用表达式本身。多路 return 时保守取 null（不猜）。 |
草案思路 D17；工程规范 §2 I-19
|
$n（参数引用） |
具名函数的上/下文里指第 n 个形参；声明期由 rewriteDollarN 统一改写为参数名并发提示。函数体内禁用（E-PARAM-REF-IN-BODY）。 |
草案思路 D58/65；工程规范 §2 I-16
|
伴生命题 f<args> |
函数被调用 ⇔ 此命题被证明。配公理 f<args> → ps₂ 可推出下文；也可用于证明"参数被调用过"（如 map 的 size≠0 ⟺ ∃a. f<a>）。 |
草案思路 D38/55 |
| 供给（supply） |
调用点向上文/命题参数提供证据。两种：自动（从 Γ 检索，0 元候选；歧义报 E-PROP-AMBIGUOUS）、显式（f<q>() 尖括号）。 |
草案思路 D4；语言语法 §1 邻接规则
|
unchecked.axiom[q] |
命题逃逸：直接往 Γ 注入 q，不经证明器检验。留 // axiom: q 注释。 |
草案思路 D5 |
by [q] |
辅助策略（语句式/后缀式）：把人给的中间命题注入 Γ。D51 暂缓投入，保留代码等自动证明遇瓶颈时启用。 |
草案思路 D48/51 |
pure<f> 命题 |
单参命题。持有它 → 编译器认为调用 f 是纯的，无需 unchecked 逃逸。未标 @unpure 的函数自动注册 pure<name>。 |
草案思路 D34/54 |
| 上下文驱动行为 |
命题不只是传参用，还能改变编译行为。三个落地实例：e : Nat 智能转换、pure<f> 放行非纯调用、T: Show 类型类约束。 |
草案思路 D54 |
| 术语 |
定义 |
出处 |
Type sealed |
类型是 sealed interface，三个实现：NamedType（名义/参数）、FunType（函数）、TupleType（元组）。 |
草案思路 D57/65；工程规范 §2 I-15
|
| 兼容层 |
Type.name/args 是 interface 上的计算属性。FunType 返回哨兵名 "(fn)"、TupleType 返回 "(tuple)"。旧 ~220 处读取点靠它零改动。 |
工程规范 §2 I-15 |
| 名义类型 |
首字母大写的具名类型（Nat/Optional[Nat]）。函数/元组不是名义类型，判定一律走 isNominal()。 |
工程规范 §2 I-15 |
| 类型类（class） |
Haskell 的 typeclass 换 Rust 的 impl 机制。声明 class Show[T] { fun show() }，实现 impl Show for Int { ... }。 |
草案思路 D6；语言简介 语言立场 |
| 隐式 self |
impl 方法不写接收者参数；体内裸用字段名 name ≡ self.name。形参可遮蔽字段（发 H-FIELD-SHADOW）。 |
草案思路 D68；工程规范 §2 I-17
|
| 字典传递 |
类型类方法调用按实参类型在 impl 表找唯一实例，把字典作为隐藏首参传入（dict_X.m(d, __self, args)）。推翻 D19 的单态化。 |
草案思路 D60 |
dictHits |
语义层的字典解析留痕：IdentityHashMap[CallExpr, String]。键是调用点实例（不是方法名！），否则同名方法多类型实例时分发错误。 |
草案思路 D68；工程规范 §2 I-18
|
| 单态化 |
[废弃]（D60 推翻）类型类按具体类型生成特化函数（show$Int），不做运行时字典。 |
草案思路 D19 已废 |
Any 严苛准入 |
顶类型。声明合法，但禁止直接调用涉 Any 的函数、禁止创建/赋值含 Any 成员的结构体——一律 unchecked。涉 Any 的推导失效须手动标注。 |
草案思路 D52/59 |
Nothing |
空类型。返回 Nothing 的函数后接代码发 W-UNREACHABLE；return 语句返回 Nothing 标记。 |
草案思路 D31 |
Null |
单值类型（Unit 职责），唯一值 null。与 Optional 的 None 严格区分（D45）。 |
草案思路 D45 |
syntheticT |
推导失败时的占位类型 (推导:xxx)。typeLooseEq 放行 synthetic（宽松策略：推导不出时不误报）。 |
Types.kt；草案思路 D31 |
| 数值提升 |
Nat ⊆ Int ⊆ Rat 的 join。在 typeLooseEq 里做（先于 name 相等判定，否则 Nat vs Int 误报）。 |
工程规范 §2 I-10 |
@tuple 形参 |
变长参数=同类型变长元组。只接受元组字面量实参（裸名报 E-TUPLE-VARARG）。取代 @vararg（D61）。 |
草案思路 D61 |
Array[T] / Result[T,E] |
[未实现] v1.0 P2/P5 引入。数组是内建原语；Result 用 Sublimation 自举。 |
v1.0补全计划 §4/§7 |
| 术语 |
定义 |
出处 |
when |
真模式匹配（Kotlin 拼写）。Java 式 switch 全废。支持解构、嵌套、is T [as x]、守卫 if、绑定主题 when(var e=0)、通配 _、else。 |
草案思路 D29/46 |
| 分支命题 |
每个分支注入的命题。构造子/字面量 → subj = pat（∃ 封闭自由变量）；is T → subj : T；else/_ → ⊤。后分支继承前分支的否定。 |
工程规范 §2 I-14 |
| 穷尽性判定 |
判据 = 分支命题的析取在 Γ 里可证恒真（不是合取，D43 澄清）。 |
草案思路 D43 |
| 覆盖律 |
枚举的穷尽析取，按 when 主题的具体类型就地生成（不用全局 ∀——泛型枚举 Optional vs Optional[Nat] 会失配）。 |
草案思路 D49；工程规范 §2 I-3
|
coverShapes |
覆盖律的递归深展开。内层形状若给单等式 v=term 就把 term 代入外层，与分支命题的 ∃ 形态同构。安全阀 COVER_DEPTH=3 / COVER_MAX_SHAPES=64。 |
草案思路 D64 |
| α-等价 |
命题比较时按绑定变量出现序重命名为 #k 再比结构。不能改回字符串比较——覆盖律用 __cov0、分支用模式变量名，名字必然不同。 |
工程规范 §2 I-5 |
| 析取子集规则 |
(A∨B) ⊢ (A∨B∨C) 有效（子集方向），反向无效。方向反了会让缺分支的 when 误判穷尽。 |
工程规范 §2 I-6 |
| 构造子单射 |
C<a> = C<b> → a = b。用于嵌套穷尽性（Some(Some(y)) 推分量等式）。 |
Prop.injective；草案思路 D49 |
| 穷尽性降级 |
D66 拍板：穷尽性是提示不是要求。判不出 → 值类型退化为 unsealedT；有覆盖律但覆盖不全 → W-NON-EXHAUSTIVE；无覆盖律主题 → 静默退化。流向非 Null 报 E-NON-SEALED-MATCH。 |
草案思路 D66 |
| 术语 |
定义 |
出处 |
| 饱和闭包 |
Prover.closure：从 Γ 迭代推出新事实至不动点。含合取分解、双否消去、∀ 单名实例化、MP 前向链接、矛盾检测 p ∧ ¬p → ⊥。≤3 轮。 |
形式化规范 §4 |
| 合一（matchTerm） |
∀ 实例化时做谓词头匹配 + 项的一阶合一（变量单向实例化，不合一算术）。 |
形式化规范 §3.4 |
| modus ponens |
p ∈ Γ 且 p → q ∈ Γ ⇒ 加入 q。用户点名的自动证明核心。 |
草案思路 未决清单；形式化规范 §4
|
| 深度上限 |
maxDepth=6 / maxRounds=3（经验值）。超限报 E-DEEP-SATURATION。需右嵌套 → 链才能触发（左结合会一次下钻就转查原子目标）。 |
工程规范 §2 I-7；草案思路 D72 |
| 目标项作候选 |
closure(gamma, listOf(goal)) 的第二参数只贡献实例化候选，不加入事实（否则目标平凡可证，破坏健全性）。 |
工程规范 §2 I-7 |
| 等式推理 |
[P4 落地] 对称、传递（BFS 等式图）、等量代换（浅层，不递归）、类型事实的等式传播。在目标侧做，不修改 Γ。 |
v1.0补全计划 §6 |
E-DEEP-SATURATION |
饱和超深度上限。健全性保证（宁可不证也不猜）的代价。 |
语言语法 §6 |
| 术语 |
定义 |
出处 |
| struct（结构体） |
圆括号声明：struct Point(x: Nat, y: Nat = 0)。字段可带默认值（函数形参不允许，报 E-DEFAULT-PARAM）。 |
草案思路 D69 |
| 命名字段构造 |
Point(x = 1)——独立 AST 节点 StructCtorExpr。触发条件：大写名 + (IDENT = 前瞻（() 空括号不算，留给 None() 零参构造子）。 |
草案思路 D69 |
| enum（枚举） |
enum Color { Red(), Green() }；带字段构造子即 ADT（Circle(Nat)）。零参构造子作值引用时生成调用（None → None()）。 |
草案思路 D46；工程规范 §2 I-12
|
| impl 完整性 |
impl 成员默认必须实现 class 方法；额外函数必须 @new（反向 override）。 |
草案思路 D7 |
@mut |
变量可变（JS let）。不注入初值等式——可变变量仅保有自反相等 v = v，v = 0 视为不成立。 |
草案思路 D35；工程规范 §2 I-9
|
@unpure |
声明非纯函数。纯作用域调用需 unchecked 或供给 pure<f>。 |
草案思路 D25/54 |
@new |
impl 成员声明"这不是实现类方法集的函数"。 |
草案思路 D7 |
| main 入口 |
具名零参 fun main() 自动作为入口调用（codegen 尾部追加 main();）。带形参报 E-MAIN-PARAMS。 |
草案思路 D70 |
| 显式 return |
return e / 裸 return 仅函数体块顶层语句位合法。值位/lambda/嵌套块报 E-RETURN-OUTSIDE——它们是 IIFE，return 逃不出去。 |
草案思路 D71/75；工程规范 §2 I-19
|
| 术语 |
定义 |
出处 |
| 四段管线 |
词法 → 语法 → 语义 → JS 生成，四段独立可测。全部手写 Kotlin，零第三方依赖。 |
语言简介 编译管线 |
| 邻接规则 |
词法器记录 precededBySpace。紧贴的 < = 实例化（类型实参/供给/命题项）；带空格的 < = 比较中缀。a<b 与 a < b 含义不同。 |
工程规范 §2 I-1 |
| 擦除映射 |
命题层、类型、理论参数全部擦除；值层映射到原生 JS。详见 草案思路 D22-24 映射表。 |
草案思路 D22 |
| mangle |
JS 名字改写：避开保留字、符号名转合法标识符。P0 后加模块前缀（core_math__gcd）。 |
JsCodeGen.mangle；v1.0补全计划 §2.2 |
| prelude |
编译期注入的基础类型和函数（Bool/Null/Optional/print/emptyTuple/singleTuple）。P0 后是否改为隐式挂载的 stdlib 模块：待拍板。 |
草案思路 D45；v1.0补全计划 §4.4 |
| 术语 |
定义 |
出处 |
| 四级诊断 |
错误（无法编译）／警告（能编译但可能有问题）／提示（建议改）／补充（默认不输出，-v 显示）。 |
语言简介 编译器分级 |
| 诊断码 |
E-*（错误）、W-*（警告）、H-*（提示）、D-*（补充）。全表见 语言语法 §6。 |
语言语法 §6 |
E-PRE-UNPROVEN |
调用时上文在 Γ 里证不出。 |
语言语法 §6 |
E-POST-UNPROVEN |
函数体结束时下文不成立。 |
语言语法 §6 |
E-NON-SEALED-MATCH |
非密封 when 的值流向非 Null 上下文。 |
草案思路 D49 |
E-RETURN-OUTSIDE |
return 出现在函数体块顶层语句位以外。 |
草案思路 D71/75 |
E-DEEP-SATURATION |
命题饱和超深度上限（maxDepth=6）。 |
工程规范 §2 I-7 |
| 术语 |
定义 |
出处 |
| 决策日志（D 编号） |
草案思路.md 里的编号条目，每条带"决定 → 理由 → 代价"。代码注释引用编号。已到 D75（P0 后加 D76）。 |
草案思路.md |
| 不变量（I 编号） |
工程规范.md §2 里"血泪换来的"硬约束。违反必引入难查 bug。已到 I-19（P0 后加 I-20~I-24）。 |
工程规范 §2 |
| 轮次 |
项目采用回合制：一轮 = 总结 → 讨论 → 指导文档 → 执行 + 汇报。已到第 5 轮（P0）。 |
工程规范 §0 协作流程 |
| 指导文档（plan/N.*.md） |
每轮一份，由规格作者（Max）写、执行者（Flash/Qwen）读。改动清单、不变量引用、验收标准、禁止事项、上报格式。 |
工程规范 §8 文档地图 |
| Max / Flash / Qwen |
角色：Max = 规格作者（写指导文档、不写码）；Flash = 早期执行者；Qwen Agent = 当前执行者。 |
工程规范 §0 |
| 示例四件套 / 六件套 |
端到端验收的固定 fixture：diffuse/value/optional/when（四件套）+ goal/showcase（六件套）。改 codegen 后产物必须逐字节不变（或重新生成基线）。 |
工程规范 §7 |
| prelude 注入 |
编译期往 Symbols 里塞基础类型和函数（Bool/Null/Optional/print/emptyTuple/singleTuple）。 |
Symbols.collect() |
| P0–P11 |
v1.0 补全计划的 12 个阶段（模块系统 → 字符串 → 集合 → IO → 自动推理 → Result → 泛型约束 → 合一 → 语法糖 → 停机 → 浮点 → 压测）。 |
v1.0补全计划 §1 |
| 术语 |
定义 |
出处 |
| 目录即模块 |
一个目录 = 一个模块，目录名即模块名。同模块内文件共享符号表。根目录（编译入口）是根模块 /。 |
v1.0补全计划 §2.2 |
| 可见性方向 |
父→子可见（传递）；子→父不可见；兄弟默认不可见，靠挂载建立；根 / 看所有后代，后代看不到根。 |
v1.0补全计划 §2.2 |
| 挂载（mount） |
<模块名>.settings 里的 mount core as c——在当前模块的命名空间里加一条指针，不复制代码。可多父，指向同一份符号。 |
v1.0补全计划 §2.2 |
| 显式装配 impl |
impl 也要挂载才可见——d 想用 c 的 impl Show for Point，必须挂载 c。这是"显式装配"不是"隐式发现"。 |
v1.0补全计划 §2.2 |
| 可见路径集合 |
canSee(from, to) 不是查表布尔——它必须计算 from 的完整可见路径集合（后代 + 挂载目标及其后代，递归传递）。P0 的硬约束。 |
工程规范 §2 I-20（P0 起用） |
| 引用路径 |
相对当前模块视角。project/main.subl 和 project/data/stringData.subl 引用 core 都写 core.math.gcd（因 core 通过 project 的挂载传递可见）。 |
v1.0补全计划 §2.2 |
E-CIRCULAR-MOUNT |
挂载链成环。 |
v1.0补全计划 §2.4 |
E-PARSE-SETTINGS |
settings 文件语法错。 |
v1.0补全计划 §2.4 |
通用术语（不重复定义）：类型、函数、多态、合一、模式、绑定、作用域、递归、纯度、lambda、柯里化、求值策略、正则……
项目里出现过但已废弃的概念（保留标记，避免未来再翻到）：单态化（D19 → D60）、uncheck.law（D5 → unchecked.axiom）、@vararg（D26 → D61 @tuple）、switch/case（D29 → when）、大括号 struct 体（D69 改圆括号）。
查不到的术语：把文档通读一遍再回来找；如果确实缺，追加到对应分类里。