Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: David Shepherd <des@uk.co.inmos>
Message-Id: <10065.9207151716@frogland.inmos.co.uk>
Subject: Re: Recursive definition over sets
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Wed, 15 Jul 92 18:16:25 BST

Phil Weiss has said:
> > (I apologize for the previous empty message; I hit the wrong key.)
> > 
> > Let f : * -> num be a mapping from "indices" to numbers
> > and s : * -> bool be a set of indices.  One can consider the
> > summation, SUM f s, of f(x)'s with x ranging over s, such that
> > 
> >     SUM f {} = 0
> >     SUM f (x INSERT s) = (x IN s) => (SUM f s) | (f x + SUM f s)
> > 
> > Similarly, one can consider maximum, minimum, product, etc. over sets;
> > in fact, for any operation that is independent of the order in which 
> > the operation is done.
> > 
> > My question is: Has anyone written the necessary code for performing
> > this kind of "recursive definitions" over sets?  I'd appreciate anything
> > that can save me the trouble of hacking it myself.
> > 
> 
> I was wondering about this just yesterday.  I could not think of a
> way.  The only idea I had was to examine the way CARD was defined
> in 'mk_sets.ml'.  I got another idea on how I could perform the
> same operation without recursion, but instead using the @ operator.
> 
> I do not know how this will turn out.  I may have to go back and
> define the operation using some form of recursion if it turns
> out proofs using this definition are too difficult.

don't think that this is possible (assuming your using the infinite
set theory) as consider

SUM I {x | T}

(not sure i've got the set syntax correct)

then the result of this is the sum of all numbers which you can prove to
be greater than any number. but since its of type :num its 0 or SUC n for
some n and hence you'd get a contradiction.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"i speak latin to god,   spanish to men,   french to women 
		 and german to my horse."             - charles v of spain