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; Tue, 14 Jun 1994 01:20:50 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26709; Mon, 13 Jun 1994 18:01:13 -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 AA26696; Mon, 13 Jun 1994 17:59:04 -0600 Received: from itd0.dsto.gov.au by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA12944; Mon, 13 Jun 1994 16:57:27 -0700 Received: from tcs22.dsto.gov.au by itd0.dsto.gov.au with SMTP (5.64+1.3.1+0.50/DSTO-1.0) id AA05384; Tue, 14 Jun 1994 09:27:04 +0930 Date: Tue, 14 Jun 1994 09:27:04 +0930 From: Jim Grundy Message-Id: <9406132357.AA05384@itd0.dsto.gov.au> To: info-hol@cs.uidaho.edu Subject: Re: Mutually recursive definitions In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Fri, 10 Jun 94 10:06:29 EDT Cc: indra@cse.iitkgp.ernet.in Hi Although this example can be reworked without mutually recursive functions, there are times when this the best way to go. The solution in HOL88 is to define a tuple of functions recursively. Its not pretty, but it works. Here is the example suggested implemented in HOL88: letrec (evenlist,oddlist) = ( (\l. if null l then true else (hd l) => oddlist (tl l) | evenlist (tl l)) , (\l. if null l then false else (hd l) => evenlist (tl l) | oddlist (tl l)) );; Hope this help Jim Grundy ======================================================================== Information Technology Division | Building 171 Laboratories Area | phone: +61 8 2596162 PO Box 1500 | fax: +61 8 2595980 Salisbury SA 5108 | email: jug@itd.dsto.gov.au AUSTRALIA | telex: AA82799 ========================================================================