[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'?
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 .