User loginNavigation 
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 "nonlogical" operations, such as deletion. So, what does it mean for an operation to be "nonlogical", and why is it a bad thing? Roughly speaking, you can think of the analogy: nonlogical 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 CurryHoward 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 proof search  you get a success when execution finds a proof of the goal. 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 monotonic: deduction from premises can only learn new facts, it can never disprove things you already knew to be true. Since deletion removes facts from the set of things you know, it can't have a logical interpretation in classical/intuitionistic logic. 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 linear logic, then all of the operations that Ganzinger and McAllester use actually do have a nice logical interpretation. 
Browse archivesActive forum topics

Recent comments
4 hours 43 min ago
2 days 7 hours ago
2 days 7 hours ago
3 days 17 hours ago
3 days 23 hours ago
4 days 9 hours ago
4 days 20 hours ago
4 days 23 hours ago
5 days 5 hours ago
5 days 5 hours ago