论文标题
再回到那里然后返回
Getting There and Back Again
论文作者
论文摘要
“在那里再次返回”（TABA）是一种编程模式，递归调用穿越一个数据结构，然后随后的返回遍历另一个数据结构。本文介绍了新的TABA示例，完善了现有的示例，并使用COQ证明助手将其控制流和数据流形式化。每个形式化都会为笔和纸的证明机械化，从而更容易“获得” TABA。此外，本文识别并说明了塔巴的尾巴回报变体，它来回（tafa）并没有回来，而是随着更多的尾巴调用而出现。
"There and Back Again" (TABA) is a programming pattern where the recursive calls traverse one data structure and the subsequent returns traverse another. This article presents new TABA examples, refines existing ones, and formalizes both their control flow and their data flow using the Coq Proof Assistant. Each formalization mechanizes a pen-and-paper proof, thus making it easier to "get" TABA. In addition, this article identifies and illustrates a tail-recursive variant of TABA, There and Forth Again (TAFA) that does not come back but goes forth instead with more tail calls.
