序列类型与无穷语义
Sequence Types and Infinitary Semantics
摘要：
我们引入了一个新的表示非幂等交集类型，使用\textbf{sequences}（家庭索引的自然数），而不是列表或多集。这允许将\textbf{intersection type}理论扩展到无限$λ$ -演算。因此，我们的特点是遗传头部正常化，这给出了一个积极的答案，被称为\textbf{Klop's Problem}的问题。在我们的方法中，我们使用\textbf{non-idempotent intersection}检索一些著名的结果无穷项。
英文摘要：
We introduce a new representation of non-idempotent intersection types, using \textbf{sequences} (families indexed with natural numbers) instead of lists or multisets. This allows scaling up \textbf{intersection type} theory to the infinitary $λ$-calculus. We thus characterize hereditary head normalization, which gives a positive answer to a question known as \textbf{Klop's Problem}. On our way, we use \textbf{non-idempotent intersection} to retrieve some well-known results on infinitary terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
