[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Determinism of choose

On Wed, May 14, 2008 at 3:47 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> How deterministic is the "choose" function? For example, in the else
>  clause of finite_sets sum:
>
>   sum(S,f) : RECURSIVE R =
>     IF (empty?(S)) THEN zero
>     ELSE f(choose(S)) + sum(rest(S),f)
>     ENDIF MEASURE (LAMBDA S,f: card(S))
>
>  how can we be sure that the element removed by 'rest' is the same
>  element returned from the earlier (explicit) 'choose'?
>
>  jerome

The choose function represents a fixed, but arbitrary, choice.  Any
two invocations of choose with the same set passed as parameter
evaluate to the same element of that set.  However, the chosen element
can be *any* member of the set, because the choice is arbitrary.  The
choose function's existence is asserted by the Axiom of Choice [1].

References:
[1] http://en.wikipedia.org/wiki/Axiom_of_choice
-- 
Jerry James
http://loganjerry.googlepages.com/