PVS‎ > ‎Theory‎ > ‎

symbols

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:
  • overloading: the same function symbol has been defined more than once, in the same theories or different theories, and PVS cannot guess which function is specified from the context;
  • importing: PVS allows polymorphic importing (which is actually implicit for all the prelude), so that sometimes, PVS cannot guess which instance of the theory is to be used, for a given symbol declared or defined in the theory, when the theory has parameters; problems can also occur when several specific instances of the same theory have been imported, or when the same symbol has been declared or defined in different theories that are imported.
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:
  • theory[actual1, ..., actualN].symbol
Here are some intermediate representations, from the shortest one, to the longest one:
  • symbol
  • symbol[actual1, ..., actualN]
  • theory.symbol
  • theory[actual1, ..., actualN].symbol
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:
  1. foo(n: nat)(p: nat): nat
  2. foo(n: nat)(p, q: nat): nat
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:
  • foo::[nat -> [nat -> nat]]             % refers to the first foo declaration;
  • (foo(5))::[nat -> nat]                 % refers to the first foo declaration;
  • (foo(5))::[nat, nat -> nat]            % refers to the second foo declaration;
  • (foo::[nat -> [nat, nat -> nat]])(5)   % refers to the second foo declaration.
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:
  1. foo(p: nat)(n: nat): nat
  2. foo(p, q: nat)(n: nat): nat
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.
Comments