[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [lojban] Re: parsing with error detection and recovery

On 8/17/06, Robin Lee Powell <rlpowell@digitalkingdom.org> wrote:

On Tue, Aug 15, 2006 at 04:34:57PM -0500, Chris Capel wrote:
> So, my question is this: is there an easy way to prove the
> equivalence of PEG parser A with the parts of parser B that apply
> only to valid input?

I'm not aware of any way to prove equivalence of any two PEGs, ever.


Surely that's too strong. Given:

PEG1

text <- 'a' / 'b'

PEG2

text <- a / b
a <- 'a'
b <- 'b'

they can be proven to be equivalent?

Maybe what you mean is that there is no known method that will
prove the equivalence or not of any arbitrary pair of PEGs. But Chris
might not need such a strong method anyway.


I'm not even aware of a way to do that with CFGs.

Furthermore, what you just said sounds like:

   I have these two PEGs with known-different behaviour.  How do I
   prove they are the same?

To which I'd answer, "Umm, you don't, because they aren't".


No, he wants to prove that all the strings parsed by PEG A will be all and
only the strings parsed by parser B which do not use any rule tagged
as ERR.


In other words, I don't think your question is solvable, or even
makes any sense.


I don't know if it's solvable, but the question does make sense to me.


Having said that, I think the original idea is a great one, and I'm
looking forward to the results.


Me too.

mu'o mi'e xorxes