On Fri, Jun 12, 2015 at 12:16 PM, Keean Schupke <ke...@fry-it.com> wrote:
> On 12 Jun 2015 3:15 pm, "Matt Oliveri" <atma...@gmail.com> wrote:
>
>> > Actually the grammar and parsing are the same thing, its just the parser
>> > has
>> > an additional literal representation attached to leaf terms in the
>> > grammar.
>>
>> I'm sure this is not literally true, so I'm not sure what you're really
>> saying.
>
> Why do you think it is not? If you have
>
> additive-expr ::= multiplicative-expr, ('+' | '-'), {additive-expr}-.
>
> Isn't this both the parsing rules and the grammar?
I don't doubt that there are notations which can be interpreted either
as a grammar or a parser. But still, that just means there's two
different interpretations. It would be misleading, but not impossible,
if those interpretations did not correspond to one another. But in any
case, they are not the same.
But I think this started with EBNF vs. parser combinators. There, I
believe there's a less philosophical difference: EBNF has
nondeterministic alternatives ('|'), your parsers seem to instead have
backtracking alternatives. (Maybe these provably coincide in
well-behaved logic programming languages.)
> We can write the grammar + typing rules in a logic language which checks the
> AST. If the type-system is compositional then the parsers and the types
> combine in the same way as the grammar.
Yes. It's a great trick. But that works because a logic program can be
interpreted both as a spec and as an implementation. But specs and
implementations are not the same thing, and I've already said why an
implementation should usually not be taken as a spec.
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.
> 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.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
