## 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

12 min 35 sec ago

1 hour 50 min ago

2 hours 31 min ago

2 hours 55 min ago

3 hours 57 min ago

4 hours 9 min ago

9 hours 37 min ago

13 hours 57 sec ago

16 hours 53 min ago

21 hours 11 min ago