## User login## Navigation |
## Linear Logical AlgorithmsLinear Logical Algorithms, Robert J. Simmons and Frank Pfenning, 2008.
In my last post, I linked to a paper by Ganzinger and McAllester about specifying algorithms as logic programs, and a) admired how concise and natural the programs were, and b) was sad that the logic programs used some "non-logical" operations, such as deletion. So, what does it mean for an operation to be "non-logical", and why is it a bad thing? Roughly speaking, you can think of the analogy: non-logical operations are to logic programs what impure operations are to functional programs -- they are features which break some parts of the equational theory of the language. Now, the Curry-Howard correspondence for functional programs says that types are propositions, and programs are proofs. It turns out that a different version of this correspondence holds for logic programs: in logic programming, a set of propositions is a program, and the execution of a program corresponds to a process of When you have nonlogical operations in your logic programming language, you've introduced operators that don't correspond to valid rules of inference, so even if your logic program succeeds, the success might not correspond to a real proof. Deletion of facts from a database is a good example of a nonlogical operation. Regular intuitionistic and classical logic is However, it turns out that not all logics are monotonic, and in this paper Simmons and Pfenning show that if you take the language of propositions to be a fragment of |
## Browse archives## Active forum topics |

## Recent comments

2 days 1 hour ago

2 days 15 hours ago

2 days 18 hours ago

4 days 16 hours ago

4 days 17 hours ago

4 days 19 hours ago

5 days 2 hours ago

5 days 6 hours ago

5 days 9 hours ago

5 days 10 hours ago