algorithm - Racket 定义的渐进类型 lambda 演算的“重复”语法？

Question

我不明白repeat (j l h)下面关于渐进类型lambda演算的论文中的代码片段是什么意思，算法是快速排序，也许知道算法的人可以猜到语法定义：

---

编辑：根据我目前的理解，算法有错误，应该是：[i: (Ref Int) (box (- l 1))]，即h应该是l。

---

论文链接：https ://dl.acm.org/doi/10.1145/3314221.3314627#sec-supp

他们的 Grift 编译器的源代码是用编写的，.rkt所以我希望如果有人知道 Racket 可以提供帮助，这里定义了重复语法：https ://github.com/Gradual-Typing/Grift/blob/95c56d94b38e9b33adf7a662c6d7768430d977da/src/language/语法.rkt#L126

我是函数式编程/Racket/GTLC+ 的新手，抱歉，我已尽力描述我的问题...

Answer 1

1. 的意思repeat(j l h)是for j in a[l]...a[h]（包括）。
2. [i: Int (box (- h 1))]用 value初始化一个Int名为icreate at heap的变量的含义operator-(h, 1)。
3. 该算法有错误就行了：[i: (Ref Int) (box (- h 1))]，我认为应该是[i: (Ref Int) (box (- l 1))]，原因：我认为h是高端的，当满足条件时repeat循环会增加i，这可能导致i > h这是荒谬的。