论文标题
ACL2中的迭代
Iteration in ACL2
论文作者
论文摘要
传统上使用递归在ACL2中表达迭代算法。 另一方面，Common Lisp提供了一个构造循环，与大多数编程语言一样，它可以直接支持迭代。 我们描述了一个循环的ACL2模拟循环$，该环路支持有效的ACL2编程和迭代推理。
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- provides direct support for iteration. We describe an ACL2 analogue loop$ of loop that supports efficient ACL2 programming and reasoning with iteration.
