Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Mon, 29 Mar 1993 00:53:21 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26282; Sun, 28 Mar 93 14:00:54 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA26277; Sun, 28 Mar 93 14:00:31 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sun, 28 Mar 1993 23:00:05 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Transfinite recursion: opinions sought Date: Sun, 28 Mar 93 22:59:57 +0100 From: John Harrison Message-Id: <"swan.cl.ca.415:28.03.93.22.00.13"@cl.cam.ac.uk> Quite a lot of people seem to want to define functions using non-primitive recursion. Since I was in this situation myself recently, I decided to prove a general theorem to add to the "wellorder" library. Accordingly I have proved what seems to me to be the natural analog of the recursion theorem in ZF set theory: i.e. recursions of the following form are permissible: f(a) = some function of (a and f restricted to {b | b < a}) More precisely, the theorem states that a recursion equation !a. f(a) = h[f,a] is satisfied by a unique |f| provided that there is some "measure" function |ms| into the field (domain + range) of a wellordering, such that for any |f| and |a|, the value of |h[f,a]| is independent of the values |f| takes for |x| with |ms(x) >= ms(a)|. The actual theorem is: |- !l h (ms:*->***). woset l /\ (!x. fl(l)(ms(x))) /\ (!f g x. (!y. (less l)(ms y,ms x) ==> (f(y) = g(y))) ==> (h f x = h g x)) ==> ?!f:*->**. !x. f x = h f x where (less l)(x,y) = l(x,y) /\ ~(x = y) and for the definitions of |woset| and |fl|, see the "wellorder" library. The version for measures into |:num| may be more comprehensible: |- !h ms. (!f g x. (!y. ms y < ms x ==> (f(y) = g(y))) ==> (h f x = h g x)) ==> ?!f:*->**. !x. f x = h f x" I am interested in opinions on whether this theorem is worth adding to the "wellorder" library, and whether there are any special cases which would be worthwhile proving as well. Note that I don't intend to write a user-friendly function for making general recursive definitions -- I'll leave that to others who have already done some work towards this. But I think this theorem could be a useful basis for such work. John.