在Agda中证明非确定性计算
Proving Non-Deterministic Computations in Agda
摘要：
我们研究证明使用Agda的Curry程序的性质。首先，我们解决的功能正确性的咖喱功能，除了一些句法和语义的差异，是在两种语言的交集。其次，我们使用Agda模型的非确定性功能，两个不同的和有竞争力的方法，将非确定性。第一种方法通过考虑应用程序产生的所有非确定性值的集合来消除非确定性。第二种方法对应用程序可以执行的每个非确定性选择进行编码。我们认为我们的初步试验是成功的。虽然证明程序的性质是一个非常困难的任务，但函数逻辑范式似乎并没有给这个任务增加任何显著的难度或复杂性。
英文摘要：
We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. The first approach eliminates non-determinism by considering the set of all non-deterministic values produced by an application. The second approach encodes every non-deterministic choice that the application could perform. We consider our initial experiment a success. Although proving properties of programs is a notoriously difficult task, the functional logic paradigm does not seem to add any significant layer of difficulty or complexity to the task.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
