Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <09414-0@swan.cl.cam.ac.uk>; Tue, 28 Apr 1992 14:57:00 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01862; Tue, 28 Apr 92 03:27:50 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA01858; Tue, 28 Apr 92 03:27:46 -0700 Received: by grolsch.cs.ubc.ca id AA27392 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Tue, 28 Apr 1992 03:27:47 -0700 Date: 28 Apr 92 3:27 -0700 From: Sreeranga Rajan To: info-hol Message-Id: <322*sree@cs.ubc.ca> Subject: Well-founded induction? I was wondering if there has been effort in HOL to admit recursive definitions by Well-founded induction wherein I could specify a non-decreasing lexicographic relation on the arguments to the recurive function as a measure of its admittance. There is a library on fixpoints by Prof. Gordon that introduces Scott (Computation) induction from which Well-founded induction could be derived in a general setting of a lexicographic ordering, that might need some work. Jeff pointed out to me on how to get around this by using other nice features of higher-order logic, but I still think that a type theoretic variation of (Boyer-Moore style) well-founded induction would be a very useful tool. A simple case in point is a recursive function taking several lists which would be admitted by induction on the length of the lists. Please forgive me if this has been discussed before as I am new to this mailing list. --Sree (sree@cs.ubc.ca)