We present a novel definition of an algorithm and its corresponding algorithm language called CoLweb. The merit of CoLweb [1] is that it makes algorithm design so versatile. That is, it forces us to a high-level, proof-carrying, distributed-style approach to algorithm design for both non-distributed computing and distributed one. We argue that this approach simplifies algorithm design. In addition, it unifies other approaches including recursive logical/functional algorithms, imperative algorithms, object-oriented imperative algorithms, neural-nets, interaction nets, proof-carrying code, etc. As an application, we refine Horn clause definitions into two kinds: blind-univerally-quantified (BUQ) ones and parallel-universally-quantified (PUQ) ones. BUQ definitions corresponds to the traditional ones such as those in Prolog where knowledgebase is $not$ expanding and its proof procedure is based on the backward chaining. On the other hand, in PUQ definitions, knowledgebase is $expanding$ and its proof procedure leads to forward chaining and {\it automatic memoization}.
翻译:我们提出了一种称为CoLweb的算法和对应的算法语言的新定义。CoLweb [1] 的优点在于它使得算法设计非常灵活。这种方法迫使我们采用高层次、证明携带的、分布式风格的算法设计方法,适用于非分布式计算和分布式计算。我们认为这种方法简化了算法设计。此外,它还统一了其他方法,包括递归逻辑/函数算法、命令式算法、面向对象的命令式算法、神经网络、交互网络、证明携带代码等。作为一个应用,我们将Horn子句定义分为两种:盲目全量化(BUQ)的和并行全量化(PUQ)的。BUQ定义对应于传统的定义,例如Prolog中的定义,其中的知识库不会扩展,其证明过程基于反向链接。另一方面,在PUQ定义中,知识库是会扩展的,其证明过程导致正向链接和自动备忘。