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，该方法通过高级别的证明承载分布式算法设计方法简化了算法设计，同时统一了其他方法，如递归逻辑 / 函数算法，命令式算法等，并将 Horn 子句定义细化为两种类型，即盲目普遍量化（BUQ）和并行普遍量化（PUQ），PUQ 定义下，知识库是扩展性的，其证明过程导致前向链接和自动备忘。