强需求调用演算
摘要：一种需要时调用的λ演算，可实现强约减（即在抽象体内约减），并确保只在需要时进行参数求值操作并且最多只求值一次。该演算使用显式替换并包含了现有的强需求策略，但允许更多的约减序列，而且通常更短，同时保持了所需的性质。该演算在强范畴意义上被证明是正规化的：当λ项t在λ演算中存在一个正规形式n时，那么从t出发的任何约减序列最终都会到达正规形式n的一个代表。我们还展示了该演算的一种限制形式具有菱形属性，并且只执行长度最小的约减序列，这使其比现有策略更好。我们使用Abella证明助手对该演算的一部分进行了形式化，并讨论了这个实验对其设计的影响。特别是，这使我们得出了一个基于归纳规则的一种新的关于需要时调用约减的描述。
作者：Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
论文ID：2111.01485
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22