一句话：在Martin–Löf类型论中构造性地实现有理序列，证明两种有限性概念可互换，并引入带回溯指针的列表。
有理序列是可能无限、但只有有限多个不同后缀的序列。本文在Martin–Löf类型论中给出其多种构造性实现。首先，作者把有理序列的定义直接翻译为类型论语言，构造表达后缀集合有限性的谓词；由于类型论中存在多种不等价的有限性概念，他们考察listability与Noetherianness，并证明在有理序列的实现中二者可以互换。随后，他们引入带回溯指针的列表，作为有理序列的归纳实现，并建立双向转换：带回溯指针的列表可展开为有理序列，有理序列可截断为带回溯指针的列表。最后，以有理数的分数表示与十进制表示相互转换为例说明该实现。
Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.