一句话:用 Taylor 展开的资源敏感理论,统一并简化 λ 演算中原本依赖 Scott、Berry 与 Kahn–Plotkin 理论的重要证明。
论文主张用基于 Taylor 展开与微分 λ 演算的资源消耗理论,取代以语法连续性为基础的传统程序近似理论。作者展示该资源敏感框架能证明 λ 演算中若干通常依赖 Scott 连续性、Berry 稳定性或 Kahn–Plotkin 顺序性的重要结果。方法依赖资源近似项的三个性质:强规范化、合流性与线性性,使证明常可简化为归纳。代表性案例是 Böhm 树语义的 Perpendicular Lines Lemma(垂直线引理),其证明因此变得直接。该工作表明 Taylor 展开在理论层面涵摄上述几类语义框架。
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.