From rspeer@MIT.EDU Sat Apr 10 21:23:44 2004
Received: with ECARTIS (v1.0.0; list lojban-list); Sat, 10 Apr 2004 21:23:44 -0700 (PDT)
Received: from fort-point-station.mit.edu ([18.7.7.76])
	by chain.digitalkingdom.org with esmtp (Exim 4.30)
	id 1BCWVO-0001wt-Qh
	for lojban-list@lojban.org; Sat, 10 Apr 2004 21:23:38 -0700
Received: from grand-central-station.mit.edu (GRAND-CENTRAL-STATION.MIT.EDU [18.7.21.82])
	by fort-point-station.mit.edu (8.12.4/8.9.2) with ESMTP id i3B4Naon016261
	for <lojban-list@lojban.org>; Sun, 11 Apr 2004 00:23:37 -0400 (EDT)
Received: from melbourne-city-street.mit.edu (MELBOURNE-CITY-STREET.MIT.EDU [18.7.21.86])
	by grand-central-station.mit.edu (8.12.4/8.9.2) with ESMTP id i3B4NaI9006778
	for <lojban-list@lojban.org>; Sun, 11 Apr 2004 00:23:36 -0400 (EDT)
Received: from torg.mit.edu (TORG.MIT.EDU [18.208.0.57])
	)
	by melbourne-city-street.mit.edu (8.12.4/8.12.4) with ESMTP id i3B4NZUa003911
	for <lojban-list@lojban.org>; Sun, 11 Apr 2004 00:23:35 -0400 (EDT)
Received: from rob by torg.mit.edu with local (Exim 3.36 #1 (Debian))
	id 1BCWVS-0001sk-00
	for <lojban-list@lojban.org>; Sun, 11 Apr 2004 00:23:42 -0400
Date: Sun, 11 Apr 2004 00:23:42 -0400
From: Rob Speer <rspeer@MIT.EDU>
To: lojban-list@lojban.org
Subject: [lojban] Re: Official parser and "lo ni'a zu crino"
Message-ID: <20040411042342.GB7189@mit.edu>
Mail-Followup-To: lojban-list@lojban.org
References: <20040407124110.46977.qmail@web41903.mail.yahoo.com> <5.2.0.9.0.20040407062416.03375890@pop.east.cox.net> <20040407124110.46977.qmail@web41903.mail.yahoo.com> <5.2.0.9.0.20040408203833.037595d0@pop.east.cox.net> <20040409201538.GS14789@digitalkingdom.org>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20040409201538.GS14789@digitalkingdom.org>
X-Is-It-Not-Nifty: www.sluggy.com
User-Agent: Mutt/1.5.5.1+cvs20040105i
X-archive-position: 7529
X-ecartis-version: Ecartis v1.0.0
Sender: lojban-list-bounce@lojban.org
Errors-to: lojban-list-bounce@lojban.org
X-original-sender: rspeer@MIT.EDU
Precedence: bulk
Reply-to: lojban-list@lojban.org
X-list: lojban-list

On Fri, Apr 09, 2004 at 01:15:38PM -0700, Robin Lee Powell wrote:
> That's impossible.  For one thing, I'm fairly certain that proving
> equivalence of two CFGs is equivalent to the halting problem.  For
> another, the current 'grammar' isn't formalized at all in many major
> respects (the pre-processing and elidable terminators), so there's
> nothing to write a proof against.

It is equivalent to the halting problem: that is, doable in the vast
majority of cases. Just not all.

Here's two equivalent CFGs:

Start -> e

Start -> foo
foo -> e

Nevertheless, it is a bit overdemanding for Bob to require you to prove
complete equivalence.
-- 
Rob Speer