PVS symbols used in theories or proofs to name functions or lemmas may become ambiguous, for different reasons. PVS is usually very good at disambiguating things from the context, but sometimes fails to do so. In addition, there are some automatic conversions that may result in a different interpretation than the intended one: this can become tricky, especially when it is not easy to understand PVS interpretation from the printed representation. When this happens during type checking, it is useful to look at the theory messages (Meta-x show-theory-messages) and theory warning messages (Meta-x show-theory-warnings), to understand what happens.
There are two essential causes of ambiguity:
It is therefore important to understand that each symbol used to refer to a function, type or lemma has an internal representation, which comprises the symbol itself, but also the name of the theory in which it is defined, and the actuals (corresponding to the theory parameters in the instantiation). Here is the form of the internal representation:
Here are some intermediate representations, from the shortest one, to the longest one:
In case of ambiguity, you may have to specify the actuals, or the theory name, or both.
In some cases, even the longest form is not enough to disambiguate: this happens when there is too much overloading, even in the same theory, and there are not enough arguments to decide, using type information to discriminate. Suppose, for instance, that we have two declarations of foo:
PVS type checker can guess that foo(5)(2) refers to the first foo declaration, and that foo(5)(2, 3) refers to the second foo declaration.
On the other hand, foo alone is ambiguous; foo(5) is also ambiguous. Type coercion may be used to disambiguate:
It is not advisable to use type coercion, as PVS code becomes really clumsy, hard to read. Overloading is a very useful and convenient feature, but one should not exaggerate and should stick to a reasonable use of it!
Note that, in the above example, switching the parameter lists would yield less ambiguity:
With this formulation, PVS can easily disambiguate foo(2) or foo(2, 3); of course, foo alone remains ambiguous, but this is the price to pay for any kind of overloading.