Implementing Dynamic Programming in Computability Logic Web
This work addresses the problem of algorithm design complexity and fragmentation for researchers and practitioners in computer science by proposing a unifying framework, though it appears incremental in refining existing logical definitions.
The paper introduces CoLweb, a novel algorithm language that enforces a high-level, proof-carrying, distributed-style approach to simplify and unify algorithm design across various paradigms, including recursive, imperative, and neural networks. As an application, it refines Horn clause definitions into BUQ and PUQ types, with PUQ enabling forward chaining and automatic memoization for expanding knowledgebases.
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}.