“模式匹配终点先提交漏例和逐行见证，再交决策树与回溯字节码。诊断不替代执行正确性：后两项还要保留第一个动作及变量绑定，而不只是保持“总有某行能匹配”。”
形式陈述
从模式行生成真实分派结构
输入是若干行模式向量 → 动作ID。每列有固定代数数据类型，构造子签名有限、字段数有限；待匹配值已经求值为有限且不可变的良类型树。模式允许通配、线性变量、构造子及or，两臂绑定同名同类型变量。共同核心没有guard、视图函数、副作用匹配或GADT约束。
源语义从第一行向后找，返回第一个结构匹配行的动作ID和变量环境；所有行都不匹配则返回Fail。or采用左到右优先：两臂都匹配时，使用左臂绑定。比如Cons(_,xs) | xs匹配单元素列表时，xs是空尾部，而不是整个列表。动作ID只标识选中的动作，本页不执行动作体。[1, §§2,4]
编译结果有三类节点：Leaf(a,b)返回动作a，并按绑定表b取得变量；Fail返回匹配失败；Switch(o,cases,default)读取位置o的构造子标签，进入对应分支，或者默认分支。它是一份能交给解释器直接运行的IR，不是只画出一个抽象决策示意图。
位置描述子项，例如根列表是(0)，其头是(0,0)、尾是(0,1)，第二根输入是(1)。下载器把“父位置ID、字段编号”驻留为整数槽ID，IR用固定宽度ID引用槽；长路径只在报告时展开。已知槽存着Cons时，才把两个字段存入其子槽，不能先投影再确认构造子。
要保持的结果比覆盖更强
对每个符合模型的输入v，编译结果必须与源语义同时失败，或返回相同动作及相同变量绑定。只要某一行匹配就返回它是不够的：把较晚的兜底放到较早的特殊分支前，会改变程序选择。
另一个结构保证是：沿任意一次生成树执行，同一位置的标签最多测试一次。 它不保证整棵树中只有一个该位置的节点，也不表示编译所得树最小。相比之下，回溯式模式匹配编译允许在尝试后行时重测同一子项，以共享续块控制代码体积。
直觉
一次观察缩小整张候选表
如果知道第一列输入是Cons，所有第一列写Nil的行都可以丢弃；写Cons的行改查头和尾；写通配符的行仍有机会。这个观察同时服务所有候选行，无需每到下一行都重新问一次“列表是不是Cons”。
生成树把所有可能的观察结果都编译好。运行时只走其中一条路径，别的分支不执行。通配行可能出现在多个分支的编译输入里，因此同一段后续判断可能生成多份静态代码。运行少重复测试与编译输出小，是两个需要分别计量的目标。
列可以换，行不能随意换
值都已经求好，观察标签和读取字段没有副作用，所以可以先检查第二列，再检查第一列。换列时，模式、位置和类型必须一起换；候选行的相对先后保持不变。
如果允许惰性求值或会抛异常的视图模式，改变测试次序可能改变是否终止、是否抛异常，届时这里的证明不适用。本页保留的是纯结构分派的动作、绑定和失败结果，没有把它扩展为任意语言完整观察等价。
例子与边界
列表与标记的可执行树
使用以下已补齐的表：
| 行 | 列表 | 标记 | 动作 |
|---|---|---|---|
| 1 | Nil | _ | empty |
| 2 | Cons(T,xs) | F | take-tail |
| 3 | Cons(,) | T | flagged |
| 4 | Cons(F,_) | F | false-head |
| 5 | Nil | T | shadowed |
先选列表列，Nil分支直接到empty；最后一行不会覆盖第一行。Cons分支产生头、尾两个槽。继续先选头时，T分支根据标记F/T选择take-tail/flagged，F分支根据标记F/T选择false-head/flagged。列表尾不需要检查标签。
对(Cons(T,Nil),F)，标签测试依次为列表、头、标记，返回take-tail以及xs=Nil。xs的绑定来自已投影的尾槽；编译器没有把变量擦成通配符后忘记它。对(Cons(F,Nil),F)也做三次标签测试，返回false-head；对(Nil,T)只做一次测试，返回empty。
这棵无共享树有9个节点，含4个Switch和5个Leaf。另一种每次选最右可检列的策略也生成9个节点，但(Nil,T)要先查标记再查列表，做两次测试。因此节点总数相同，不代表每个输入的执行成本都相同。
换选列能改变静态体积
取三列Bool，四行为(T,_,T)→a、(_,_,F)→b、(F,T,T)→c、(_,_,_)→d。没有任何一行被完全遮蔽。
下载器每次选最左可检列得到11个树节点；每次选最右可检列得到9个。对全部8个Bool向量，前者共做20次标签测试，后者16次。特别地，第三列为F的四个输入在右选策略下一步就返回b；左选策略先花时间检查第一列，部分输入还查第二列。
这只比较两个明确定义的策略，不证明右选总是更好，也不宣称9个节点已最优。实际编译器可以依据首行、必要位置、分支密度或后续共享选列；每个启发式仍须服从同一行序与绑定不变量。[1, §§4,7–8]
简单展开可能造成指数体积
一个n列模式，每列都是F|T，动作都是yes。透明实现先展开成2ⁿ行，再生成无共享二叉分派树：节点数为2ⁿ⁺¹−1。n=4时是31个节点，n=8时是511个；每次运行仍只检查n个位置。
这个例子是本页未做or化简、未做DAG合并的实现结果，不是所有决策树编译器的体积下界。识别F|T已覆盖Bool可以直接化简为通配符；结构共享也可以把相同续树合并。代价报告必须说明是否应用这些优化，不能把原始树计数与共享图计数混为一谈。
推论与应用
编译规则与不变量
先按左到右把or展开为相邻替代行，保存每个替代行的动作与“变量名→位置ID”表。连续or用显式栈访问、共用结果列表，避免逐层拼接已展开的前缀；构造子字段再做笛卡尔积。无guard时，这保持首匹配动作与左偏绑定；一旦加入guard，展开需要另审提交语义，不能直接沿用。[1, §4]
递归状态包含有序候选矩阵、各列位置、各列类型。矩阵无行就生成Fail；首行已经全是通配符就生成其Leaf，包括零列情况。否则选择一个含构造子模式的列，连同位置和类型移到前面。
对该列每个出现的构造子c建立分支：保留c行和通配行，c行展开字段，通配行补相同数量的通配字段，其余行删除；把当前位置换成字段位置后递归。若出现的构造子不构成完整签名，再建默认分支，只保留通配行并移去该列。完整签名没有默认分支，良类型输入保证必选到某个case。
核心不变量是：在路径已经获得的标签事实下，剩余矩阵恰好保留仍可能匹配的源行及其顺序；槽表中的值等于对应原输入子项。特化/默认保持第一项，字段投影保持第二项。到Leaf时首行已没有结构要求，绑定表引用的槽也已可用，故动作和环境与源语义一致。反方向，每个源匹配会沿其标签分支到达对应首行，失败也一致。[1, §5]
每次Switch从待查位置前沿中移除o，只加入o的严格子位置。此前的前沿位置彼此不为祖先；故o不会再回到前沿，同一次执行不可能重测它。若数据表示用共享对象，两个不同输入位置可以指向同一对象；保证针对位置，不是针对物理对象地址。
成本需要算生成代码，也要算字段
令A为良构校验前的模式/行/槽规模，E为or展开后规模。默认Bool/List固定签名下，令B=Σ_j(m_j+1)(n_j+1)，其中每项对应实际编译调用的候选矩阵。重排、特化和分支生成主体需O(A+E+B)期望时间，位置驻留字典按常数期望访问计；类型及变量校验保守O((A+1)²)另计。存下生成树、展开行和所有暂存矩阵的分配量由O(A+E+B)控制，不承诺B为多项式。
运行阶段设t为实际Switch数，p为实际投影字段数，b为最终输出绑定数。用已求值的根引用、固定宽度槽和分支字典，分派、日志与绑定构造需期望O(n+t+p+b+1)工作，n是输入列数。完整路径日志占O(t)，槽表新增O(p)项，绑定输出O(b)。若入口还要遍历整棵外部值做类型验证，另加输入树大小；把共享子值打印成完整字符串也按实际打印量收费。
模式匹配终点提供树IR、槽父表、23条回溯字节码和逐输入对照。覆盖检查还能在编译前给出遗漏值与被遮蔽行；两者的职责不同，诊断全表穷尽并不能证明生成的绑定位置正确。
参考资料
- Luc Maranget，Compiling Pattern Matching to Good Decision Trees，ML2008，pp.35–46，作者含附录稿：§§2–3给模式、位置与树语义，§4列选择和or左到右展开，§5正确性，§§6–8讨论共享与启发式。本文整数槽、两列绑定输出和三列计数为自行实现与复算。
- Fabrice Le Fessant、Luc Maranget，Optimizing Pattern Matching，ICFP2001，pp.26–37，§8.1：决策树不重复测试子项与回溯代码体积之间的取舍。这里的目标树未暗中启用最大共享。