Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <3815.9404051001@frogland.inmos.co.uk>
Subject: recursives defs over sets.
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Tue, 5 Apr 1994 11:01:35 +0100 (BST)
Content-Type: text
Content-Length: 1408

Otmane Ait Mohamed has said:
> Let f,g:string->* and 
>   
>      FN:(string)set and
> 
>      R:*->*->bool.
> 
> I want to define a recursive function over set  by:
> 
> 
>   "AND f g  {}      = ?x.~(x IN FN) /\ R (f x) (g x)    
> 
>   !S.FINITE S ==>
> 
>   AND f g (y INSERT S) = (y IN S) => AND f g S | (R (f y) (g y) /\ AND f g S)"
> 
> 
> Has anyone defined such function? I'd appreciate any help or pointers.

1) In general, the thing you want to do isn't what you expect since

	y INSERT S = y INSERT (y INSERT S)

and

	x INSERT (y INSERT S) = y INSERT (s INSERT S)

i.e. a definition by cases of

	G {} = C
	G (x INSERT S) = H x (G S)

doesn't work.

2) In your case I think you can make it work by taking a set image.


AND f g S = ~(F IN (IMAGE (\y. R (f y) (g y)) S)) /\
             (?x.~(x IN FN) /\ R (f x) (g x))

BTW, I assume that FN is a constant.

The first conjunct maps the relation over all elements of the set. If F is
an element of the resultant set then the conjucntion of all the relations
is false.

Actually ... a simpler version is:

AND f g S = (?x.~(x IN (S UNION FN)) /\ R (f x) (g x))

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."