一句话：在 sequent calculus 中为带效应的 call-by-name 惰性外延函数给出合流规约系统，并揭示其边界。
本文研究带效应的 call-by-name 语言中函数外延性与重写系统合流性的冲突。作者指出，若简单地把 η 等外延律当作规约规则，合流性很容易被破坏。论文在 sequent calculus 中考察该问题，并借鉴 call-by-name 函数语言理论中的若干洞见，包括两个独立 control calculi 的合流重写以及可靠的 continuation-passing style（CPS）变换。基于这些思想，作者为惰性外延函数给出了一个合流的规约系统，从而在支持外延性的同时保持重写的一致性。最后，论文讨论了该方法在严格求值以及函数之外类型上的局限性。
Abstract Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like η as reduction rules easily breaks confluence. We explore these issues in the setting of a sequent calculus. Building on an insight that appears in different aspects of the theory of call-by-name functional languages—confluent rewriting for two independent control calculi and sound continuation-passing style transformations—we give a confluent reduction system for lazy extensional functions. Finally, we consider limitations to this approach when used for strict evaluation and types beyond functions.
@article{Johnson-FreydDA17,
title = {Call-by-name extensionality and confluence},
author = {PHILIP JOHNSON-FREYD and PAUL DOWNEN and ZENA M. ARIOLA},
journal = {Journal of Functional Programming},
volume = {27},
year = {2017},
doi = {10.1017/s095679681700003x}
}