On Fri, Jun 12, 2015 at 7:09 PM, Keean Schupke <ke...@fry-it.com> wrote: > On 12 Jun 2015 11:45 pm, "Matt Oliveri" <atma...@gmail.com> wrote: >> If your spec and implementation are separate, then in logic >> programming, it just means you have two logic programs. To prove the >> implementation correct, you'd want to show that the logic programs are >> equivalent. Ironically, I don't believe logic programming can do this. >> It's logic, and it's programming, but you can't make logical >> statements about programs. Pretty sad, huh? This is why I tend to draw >> a distinction between logic programming and "real" logic. Logic >> programming is not really about proving things, it's more like a slick >> way to do backtracking search. Yes, sometimes this proves simple >> things, but it's no proof assistant. > > Actually you can prove the two equivalent. There is no difference between > such logic programming and a proof assistant. Look at Twelf for example.
So I'd say Twelf is not just a logic programming language. Could you prove two Prolog programs equivalent in Prolog? If not, then since Prolog is still considered logic programming, I conclude that logic programming is different from program logics, even though there exist systems that are both. (Note that Twelf is not an example. It's both a logic programming language and a logical framework. I am not being pedantic, these things are used very differently.) I am well aware that you can do logic programming in stronger logics. Stronger than Twelf too. But there's a trade-off between expressiveness of the logic and efficiency and completeness of the search procedure. >> > So perhaps I need to revise my statement: the parsing, grammar, and type >> > checking can all be combined into a single specification if the type >> > system >> > is compositional. (As this is what I have been working on for a while I >> > failed to notice it may be a special case). >> >> I agree you can do this. I maintain that it's a bad idea. > > I think you miss the point. I can take the combined grammar and type > checking specification, expressed formally in logic, and write parsers for > the terminal symbols in the grammar, and it is a parser. I have not missed the point. Yes, you can do this. I maintain that it's a bad idea. In case you've forgotten the reason, it's because I don't think you should combine the grammar with the "type checking specification" for a normative language definition. They are conventionally kept separate, and that's a good thing. > It may not be very > efficient, but that is a separate problem. > > You can then write an efficient parser and you just have to prove that it is > equivalent to some part of the complete grammar. This then becomes a problem > of finding a path from one type to the other, which can be found by a > constrained search of some kind. You're in big trouble if you're expecting any search procedure to be able to automatically prove the equivalence of two logic programs, because equivalence of Turing-complete programs is undecidable, and conventional wisdom is that the search space is too intractably huge to get lucky. You'll find that the constraints you need to make this work essentially _are_ the proof, and will generally need to be devised by hand for each pair of programs. Maybe this is what you have in mind. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
