Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Message-Id: <9207151552.AA09392@leopard.cs.uidaho.edu>
Subject: Re: Recursive definition over sets
To: info-hol@edu.uidaho.cs.ted
Date: Wed, 15 Jul 92 8:52:31 PDT
In-Reply-To: <9207150815.AA01480@maui.cs.ucla.edu>; from "chou@cs.ucla.edu" at Jul 15, 92 1:15 am
Mailer: Elm [revision: 66.33]

> 
> (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.

Phil.

--
Philip Weiss	Laboratory for Applied Logic	weiss@leopard.cs.uidaho.edu
(Disclaimer: My views are not their views)	weiss872@snake.cs.uidaho.edu