Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters because the interaction between document and program can be subtle and error-prone. In this paper we describe several such problems, then taxonomize and formalize document languages as levels of a document calculus. We employ the calculus as a foundation for implementing complex features such as reactivity, as well as for proving theorems about the boundary of content and computation. We intend for the document calculus to provide a theoretical basis for new document languages, and to assist designers in cleaning up the unsavory corners of existing languages.
翻译:被动文档与活动程序现已广泛融合。文档语言包含图灵完备的编程元素,而编程语言则包含复杂的文档表示法。然而,目前尚无形式化基础对这些语言进行建模。这一问题之所以重要,是因为文档与程序之间的交互可能微妙且易出错。本文描述了若干此类问题,随后将文档语言分类并形式化为文档演算的不同层级。我们利用该演算作为基础,实现响应式等复杂特性,并证明关于内容与计算边界的一些定理。我们期望文档演算能为新型文档语言提供理论基础,并协助设计者清理现有语言中不尽如人意的角落。