澄清不同miniKanren实现版本的搜索算法差异（基于TRS1、TRS2、TRS1*实验）

所有实验结果的核心差异，都来自conde对多分支结果流的合并策略不同，不存在实现bug，只是设计上的权衡区别，结合实验结果可以一一对应：

三种实现的核心策略对比 #

• TRS1（2005年第一版原配套实现）
  采用纯深度优先的顺序追加（append）流合并，无任何公平性设计：执行时会先把第一个分支的所有可能解全部遍历完成，才会开始遍历第二个分支的解；如果第一个分支存在无限递归，会永远卡在第一个分支的遍历上，无法产出其他分支的解。
• TRS1（Racket官方收录的第一版衍生实现）*
  采用全分支公平交错（interleave）流合并：不管分支是有限解还是无限递归，都会按步交错推进每个分支的计算，每次只让每个分支推进一步计算，不会因为单个分支的无限递归完全阻塞其他分支的解产出。
• TRS2（2018年第二版配套实现）
  采用深度优先优先+递归分支挂起的队列式交错：对没有递归调用的纯直接约束（比如等式==），沿用纯深度优先的顺序遍历，快速产出直接解；对调用了自定义递归关系的分支，会把计算状态挂起加入队列，按队列顺序轮流推进，避免无限递归阻塞。

逐组实验的现象溯源 #

第一组实验（无递归的有限分支） #

• TRS1、TRS2的所有分支都是纯等式约束，没有递归调用：TRS1走深度优先顺序，TRS2也对纯等式分支走深度优先，因此顺序都是先产出x=a分支的两个解(a c) (a d)，再产出x=b分支的两个解(b e) (b f)，结果一致。
• TRS1*不管什么分支都做全交错，因此每次推进一个分支的一步：先出a分支的c解，再出b分支的e解，再出a分支的d解，最后出b分支的f解，得到((a c) (b e) (a d) (b f))，和实验结果一致。

第二组实验（有递归的无限解集） #

• TRS1是纯深度优先：遍历lolo关系时，会一直优先走“元素为空列表”的递归路径，不断生成长度递增、所有元素为空的列表，永远不会切到“元素为非空列表”的分支，因此输出全是(() (()) (() ()) ...)这类解，完全不会出现带未绑定变量的非空元素列表。
• TRS1*和TRS2都对递归分支做了交错/挂起队列处理：不会一直卡在全空元素的递归路径，会交替推进“非空元素”的分支，因此会产出((_0)) ((_0 _1))这类包含未绑定变量的非空列表解，结果一致。

第三组实验（存在无限递归分支） #

• TRS1是纯深度优先：外层第一个分支x=a的计算里，包含tmp-rel-2的无限递归流，因此取完第一个解(a c)后，就会永远卡在无限递归的遍历上，永远切不到x=b的分支，所以run 2就会进入循环；只有换成真正交错的condi，才能部分拿到其他分支的解。
• TRS1*是全分支交错：每次推进一步计算，第一轮先出a分支的c解，再推一步b分支得到e解，下一轮切回a分支的时候，就会进入tmp-rel-2的无限递归流，后续的b f、a d等解永远无法被取到，因此run 2能返回((a c) (b e))，run 3就会进入循环。
• TRS2是纯等式优先+递归分支挂起：外层两个分支里，x=b分支全是纯等式约束，没有递归，会被优先深度执行，先产出b e、b f两个解；而x=a分支里调用了递归的tmp-rel关系，会被挂起到队列最后，等前面的纯等式分支跑完，才会被唤醒执行，产出a c的解，因此run 3能正常返回((b e) (b f) (a c))，不会因为a分支的无限递归卡死。

内容的提问来源于stack exchange，提问作者chansey