不动点组合算子和钟Boehm树的模构造
Modular Construction of Fixed Point Combinators and Clocked Boehm Trees
摘要：
不动点组合子（及其推广：循环组合子）是属于微积分和逻辑核心的经典概念。我们从探索不动点组合子（fpc）的结构开始，极大地推广了众所周知的事实，即如果Y是fpc，Y（SI）再次是fpc，生成Boehm序列的fpc。使用无穷大演算，我们设计无穷多个其他的生成方案的fpc的。通过这种方式，我们找到了以模块化方式构建新的柔性印刷电路板的方案和构建块。在创造了大量新的不动点组合子之后，我们的任务是证明它们确实是新的。也就是说，我们必须证明它们的β-不可转换性。通过Boehm树的已知技术不适用，因为所有fpc具有相同的Boehm树（BT）。因此，我们采用“时钟BT的”，与注释，传达信息的节奏，在BT中的数据产生。BT的，从而丰富了一个内在的时钟行为，从而导致一个精致的歧视方法，为DVDA条款。相应的等式严格地介于β-可转换性和BT-等式之间，BT-等式是经典微积分模型中的等式。类似的方法适用于Levy-Longo Berarducci树。最后，我们通过我们称之为“原子钟”的时钟概念的精度来增加辨别能力。
英文摘要：
Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of lambda-calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc's), vastly generalizing the well-known fact that if Y is an fpc, Y(SI) is again an fpc, generating the Boehm sequence of fpc's. Using the infinitary lambda-calculus we devise infinitely many other generation schemes for fpc's. In this way we find schemes and building blocks to construct new fpc's in a modular way. Having created a plethora of new fixed point combinators, the task is to prove that they are indeed new. That is, we have to prove their beta-inconvertibility. Known techniques via Boehm Trees do not apply, because all fpc's have the same Boehm Tree (BT). Therefore, we employ `clocked BT's', with annotations that convey information of the tempo in which the data in the BT are produced. BT's are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda-terms. The corresponding equality is strictly intermediate between beta-convertibility and BT-equality, the equality in the classical models of lambda-calculus. An analogous approach pertains to Levy-Longo Berarducci trees. Finally, we increase the discrimination power by a precision of the clock notion that we call `atomic clock'.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
