Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 11 May 1994 18:24:52 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA19505; Wed, 11 May 1994 11:11:12 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA19501; Wed, 11 May 1994 11:11:07 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA12109; Wed, 11 May 1994 10:11:48 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 11 May 1994 18:10:50 +0100 To: info-hol@cs.uidaho.edu (info-hol mailing list) Subject: Re: does there exists a hol-lex? In-Reply-To: Your message of "Wed, 11 May 94 16:43:35 BST." <4457.9405111543@frogland.inmos.co.uk> Date: Wed, 11 May 94 18:10:28 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:053840:940511171055"@cl.cam.ac.uk> Ralf Reetz proposes formalizing parsing inside the HOL logic. This is a very interesting idea, but as David remarks, it would be a lot of work. One thought is as follows. Embed the grammar of the language inside the logic. Proving that a given parse tree flattens down to a certain token list or string is easy (basically just rewriting). Consequently the hard work of actually parsing can be done in ML, and the result checked inside the logic. This would give a very easy proof that the nominated parse tree is a *possible* parse. If you want to prove that it's the only one (which you might not), you should also prove some sort of determinacy theorem inside the logic. This is certainly likely to be a lot easier than verifying that a HOL term operates correctly as a parser. John.