On Sat, Jun 13, 2015 at 3:49 AM, Keean Schupke <ke...@fry-it.com> wrote: > On 13 Jun 2015 12:50 am, "Matt Oliveri" <atma...@gmail.com> 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 think this subthread got sidetracked, and it's probably my fault for using "proof assistant" too narrowly. What I was trying to say, and you apparently agree, is that logic programming languages are not necessarily able to carry out general reasoning about programs. >> >> 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). That may appear so, but it's different, since the grammar refers to surface syntax, whereas a separate set of typing rules would refer to ASTs, and not involve surface syntax. The cases of the AST type(s) do not exactly match the cases in the grammar, so a separate grammar is not redundant. For example, only a grammar would have a case to wrap an expression in parentheses. Conventional typing rules do not need that case. >> 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. I think I misunderstood you. You said: On Fri, Jun 12, 2015 at 7:09 PM, Keean Schupke <ke...@fry-it.com> wrote: > 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. I thought you were saying you'd have a constrained search algorithm in the system for proving logic programs equivalent, so a programmer could use this to verify an efficient parser. But now I'm thinking you're proposing something less magical. But I still don't understand how it constitutes a proof of equivalence for two logic programs (the efficient parser and the grammar). It may not be worth explaining it yet. There are still simpler things, like HasTwo, and even10, that I'm waiting for you to address. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
