一句话：将 Datalog 的半朴素求值扩展到 Datafun 的高阶函数式语言，支持一等关系与高阶函数递归。
自底向上 Datalog 引擎常用半朴素求值来优化递归谓词：朴素迭代每轮会重算旧值，而半朴素通过计算相邻迭代差值的安全近似来避免重复，从而渐近提升查询性能。传统半朴素求值既包含程序变换，也包含改进的迭代策略，并依赖 Datalog 的一阶性质。本文将其推广到 Datafun——一种在 Datalog 基础上加入一等关系、高阶函数以及和类型等数据类型的高阶函数式语言，给出适用于高阶程序的半朴素变换与求值策略，使递归定义可在更高阶特性下继续利用半朴素优化的增量计算优势。
One of the workhorse techniques for implementing bottom-up Datalog engines is seminaïve evaluation. This optimization improves the performance of Datalog's most distinctive feature: recursively defined predicates. These are computed iteratively, and under a naïve evaluation strategy, each iteration recomputes all previous values. Seminaïve evaluation computes a safe approximation of the difference between iterations. This can asymptotically improve the performance of Datalog queries. Seminaïve evaluation is defined partly as a program transformation and partly as a modified iteration strategy, and takes advantage of the first-order nature of Datalog code. This paper extends the seminaïve transformation to higher-order programs written in the Datafun language, which extends Datalog with features like first-class relations, higher-order functions, and datatypes like sum types.
@article{paperbot565,
title = {Seminaïve evaluation for a higher-order functional language},
author = {Michael Arntzenius and Neel Krishnaswami},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371090}
}