[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: COND and incomplete information
Robert P. Goldman writes:
> I'm afraid I don't understand this. I understand that I am defining a
> function but, since p is a variable (of type process in this case),
> why is maybe(p) a constant function? Surely if p and q are different,
> maybe(p) need not equal maybe(q). Or have I misunderstood the syntax?
You're right, I misspoke. The function `maybe' may have
different values given different arguments. Its value at
any fixed argument, however, is fixed. That may or may not
make sense in your example; I don't know what p represents.
If the value of p uniquely identifies a single execution of
a process, then it may be reasonable to use your `maybe'
approach. (Or the `choose' equivalent I describe below.)
In this case, you could prove things like
wanted_time(p) = timer_setting(p)
IMPLIES (run_time(p) = 123 OR run_time(p) = 345)
If p's value only specifies the values of certain parameters
of the process, then you probably want run_time to be
nondeterministic, since you want to allow two processes with
the same parameters to choose different paths. If that's
the case, you'll probably want run_time to return a set or
range of possible runtimes.
By the way, an equivalent expression to maybe(p), which
won't require defining extra functions, is
That has the added advantage that you can use it several
times and each occurrence may have a different value.