Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 25 May 1993 09:44:19 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08368; Tue, 25 May 93 01:32:55 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA08363; Tue, 25 May 93 01:32:43 -0700 Message-Id: <9305250832.AA08363@ted.cs.uidaho.edu> Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <17479-0@iraun1.ira.uka.de>; Tue, 25 May 1993 10:10:00 +0200 Date: Tue, 25 May 93 10:11:21 MET DST From: schneide To: info-hol@ted.cs.uidaho.edu Subject: letrec-expressions Let-Expressions in HOL are very readable and convenient and moreover they allow a structure sharing which can save exponential costs. However, in these expressions do not allow any form of recursion. One way to circumvent this is to introduce a fixpoint operator which can be used to "unrecursivize" the recursive definition. Has anybody done this before or are there other proposals for simulation letrec expressions? Klaus Schneider