On 13 Jun 2015 12:50 am, "Matt Oliveri" <[email protected]> wrote: > 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.)
Sure, but nothing stops my logic language also being a logical framework. > 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. True. In fact I think what makes logic programming is the searchability. So we can have searchability as a requirement for the logic. There are still many logics available, including an interesting fragment of intuitionistic and linear logic. > >> I agree you can do this. I maintain that it's a bad idea. The grammar specification in the type checking will be redundant. The type-inference specification will be the same as the grammar (the same clauses with additional arguments for the types). > They are > conventionally kept separate, and that's a good thing. I am not convinced. > 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. I am not sure if this is true for typed programs. If we constrain the search to well typed programs of the same type, and the values of the logic program represent the types of the value level programs, and we have principal typings then the proof we need is that the parser has a type which is the same as the grammar rule, and type equality is principal(X) = principal(Y), where = is unification. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
