序列类型与无穷语义

我们引入非幂等交截类型的一种新表示，使用\textbf{序列}（以自然数索引的族）而非列表或多重集。这使得\textbf{交截类型}理论可扩展至无穷 $\lambda$-演算。由此我们刻画了遗传首部规范化（hereditary head normalization），对被称为\textbf{Klop问题}的疑问给出了肯定回答。在此过程中，我们利用\textbf{非幂等交截}重新获得了关于无穷项的一些已知结果。