LP, the Larch Prover -- Overloaded identifiers

LP allows users to overload identifiers for variables and operators. For example, LP allows the simple identifier s to be used both as a function s:Nat->Nat and as a variable s:Set, and it allows the operator identifier - to be used both as a prefix operator and as an infix operator. LP automatically overloads the predefined equality and conditional operators (=, ~=, and if__then__else__), once for each declared sort. There are only two restrictions on overloading:

The same identifier cannot be used to name a variable and a constant (i.e., a nullary operator) of the same sort.
The logical, equality, and conditional operators (except for ~) cannot be overloaded with user-defined signatures.

LP disambiguates user input by using context to associate each identifier with a previous declaration. When context permits more than one association, users must supply additional annotations to resolve the ambiguity.

Disambiguating terms

Users can resolve potential ambiguities in terms by qualifying selected subterms with their sorts. For example, given the declarations

declare variables x, y, z: Bool, x, y, w: Nat

the terms x = z and x = w are unambiguous, but the term x = y is ambiguous. It can be disambiguated in several ways, for example, as x:Nat = y or as x = y:Bool. Given the additional declarations

declare operators f:Nat->Nat, f:Nat->Bool, f:Bool->Bool

the term f(z) is unambiguous, but the term f(w) needs to be disambiguated as either f(w):Nat or f(w):Bool, and the term f(x) needs to be disambiguated as one of f(x:Bool), f(x:Nat):Nat, or f(x:Nat):Bool.

Another potential ambiguity in terms arises from the treatment LP accords to the period symbol (.). For example, given the declarations

declare operators
  1, min:                       -> Nat
  a:                            -> Array
  __.__:             Array, Nat -> Nat
  __ .size, __ .min: Array      -> Nat
  ..

the terms a.size and a.1 are unambiguous, but a.min could represent an application of either the infix operator . or the postfix operator .min. In such cases, LP disambiguates a.min as containing a postfix operator; users who want . to refer to the infix operator can write a.(min).

Disambiguating operators outside of terms

Users can resolve an ambiguous operator identifier by qualifying it with its signature or by decorating it with one or two markers (__) to indicate whether it is an infix, postfix, or prefix operator.

LP, the Larch Prover -- Overloaded identifiers

Disambiguating terms

Disambiguating operators outside of terms

See also