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 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. 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. Keean.
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
