强调非确定性的声明式语言的高效程序设计：应用与形式推理
Effectful Programming in Declarative Languages with an Emphasis on Non-Determinism: Applications and Formal Reasoning
摘要：
本文研究了有效的声明式编程，强调非确定性作为一种效果。一方面，我们对使用非确定性作为底层实现思想来开发应用程序感兴趣。我们讨论两个应用程序使用功能逻辑程序设计语言咖喱。这些实现的关键思想是利用Curry所采用的非确定性和非严格性的相互作用。第一个应用程序调查排序算法参数化的比较功能。通过对这些排序函数应用一个非确定性谓词，我们得到一个置换枚举函数。我们将Curry中的实现与Haskell中的实现进行比较，后者使用一元接口来建模非确定性。我们在这项工作中讨论的另一个应用程序是概率编程库。我们不是将分布建模为事件和概率对的列表，而是使用Curry内置的非确定性来建模分布。在这两种情况下，我们观察到非确定性和非严格性的组合比使用列表来建模非确定性的实现更有优势。另一方面，我们提出了一个想法，有效的声明式程序设计语言的形式推理。为了从简单的效果开始，我们首先专注于对功能子集进行建模。也就是说，利息的效果是总体性的和非总体性的。然后，我们观察到，这两种效果的一般方案模型可以概括为捕捉广泛的影响。显然，下一步是将这一思想应用于模型非确定性。更准确地说，我们实现了Curry的非确定性模型：具有调用时间选择的非严格非确定性。因此，我们最后讨论了为什么目前的表示模型调用的名称，而不是库里的调用的需要语义，并给出了一个展望的想法来解决这个问题。
英文摘要：
This thesis investigates effectful declarative programming with an emphasis on non-determinism as an effect. On the one hand, we are interested in developing applications using non-determinism as underlying implementation idea. We discuss two applications using the functional logic programming language Curry. The key idea of these implementations is to exploit the interplay of non-determinism and non-strictness that Curry employs. The first application investigates sorting algorithms parametrised over a comparison function. By applying a non-deterministic predicate to these sorting functions, we gain a permutation enumeration function. We compare the implementation in Curry with an implementation in Haskell that uses a monadic interface to model non-determinism. The other application that we discuss in this work is a library for probabilistic programming. Instead of modelling distributions as list of event and probability pairs, we model distributions using Curry's built-in non-determinism. In both cases we observe that the combination of non-determinism and non-strictness has advantages over an implementation using lists to model non-determinism. On the other hand, we present an idea to apply formal reasoning on effectful declarative programming languages. In order to start with simple effects, we focus on modelling a functional subset first. That is, the effects of interest are totality and partiality. We then observe that the general scheme to model these two effects can be generalised to capture a wide range of effects. Obviously, the next step is to apply the idea to model non-determinism. More precisely, we implement a model for the non-determinism of Curry: non-strict non-determinism with call-time choice. Therefore, we finally discuss why the current representation models call-by-name rather than Curry's call-by-need semantics and give an outlook on ideas to tackle this problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
