From lojban-out@lojban.org Sat Apr 10 21:24:22 2004 Return-Path: X-Sender: lojban-out@lojban.org X-Apparently-To: lojban@yahoogroups.com Received: (qmail 72363 invoked from network); 11 Apr 2004 04:24:22 -0000 Received: from unknown (66.218.66.167) by m25.grp.scd.yahoo.com with QMQP; 11 Apr 2004 04:24:22 -0000 Received: from unknown (HELO chain.digitalkingdom.org) (64.81.49.134) by mta6.grp.scd.yahoo.com with SMTP; 11 Apr 2004 04:24:22 -0000 Received: from lojban-out by chain.digitalkingdom.org with local (Exim 4.30) id 1BCWW5-0001xl-Gh for lojban@yahoogroups.com; Sat, 10 Apr 2004 21:24:21 -0700 Received: from dsl081-049-134.sfo1.dsl.speakeasy.net ([64.81.49.134] helo=chain.digitalkingdom.org) by chain.digitalkingdom.org with esmtp (Exim 4.30) id 1BCWVX-0001xC-Dq; Sat, 10 Apr 2004 21:23:47 -0700 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 ; 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 ; 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 ; 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 ; Sun, 11 Apr 2004 00:23:42 -0400 Date: Sun, 11 Apr 2004 00:23:42 -0400 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 X-list: lojban-list To: lojban@yahoogroups.com X-eGroups-Remote-IP: 64.81.49.134 X-eGroups-From: Rob Speer From: Rob Speer Reply-To: rspeer@MIT.EDU Subject: [lojban] Re: Official parser and "lo ni'a zu crino" X-Yahoo-Group-Post: member; u=116389790 X-Yahoo-Profile: lojban_out X-Yahoo-Message-Num: 22003 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