Logical frameworks are successful in modeling proof systems. Recently, CoLF extended the logical framework LF to support higher-order rational terms that enable adequate encoding of circular objects and derivations. In this paper, we propose CoLF$^\omega$ as an alternative interpretation of CoLF-style signatures where terms are taken to be all possibly infinitary terms that are consistent with a given signature. In particular, we propose the notion of productive B\"ohm trees, a particular kind of typed $\bot$-free B\"ohm trees that are closed under hereditary substitution. We show that the productive B\"ohm trees are capable of meta-encoding their own structure. Overall, we hope to establish CoLF$^\omega$ as a new formal framework for the encoding of infinitary regular and non-regular structures.

翻译：逻辑框架在建模证明系统中取得了成功。最近，CoLF 扩展了逻辑框架 LF，以支持高阶有理项，从而能够充分编码循环对象与推导。本文提出将 CoLF$^\omega$ 作为 CoLF 类型签名的一种替代解释，其中项被视为与给定签名一致的所有可能的无限项。特别地，我们提出了"生成性 Böhm 树"的概念，这是一种特定类型的带类型的无 $\bot$ 的 Böhm 树，且在遗传替换下封闭。我们证明生成性 Böhm 树能够对其自身结构进行元编码。总体而言，我们期望将 CoLF$^\omega$ 建立为一种新的形式化框架，用于编码无限正则与非正则结构。