PVS‎ > ‎Theory‎ > ‎

Type inference

  • T, U, T1, …, TN denote types;
  • T ≤ U denotes the fact that T is a subtype of U;
  • x, x1, …, xN denote distinct variables;
  • e, f, t, t1, …, tN denote expressions;
  • T[x1/t1; …; xk/tk] is the result of the parallel substitution of t1 for x1, …, tk for xk, in T.
Type construction
  • (Bool) :   |-  bool: TYPE
  • (Real):   |-  real: TYPE
  • (Rational):    |-   rational ≤ real
  • (Int):    |-    int ≤ real
  • (Nat):    |-    nat ≤ int
  • (Product):   |-    [x1: T1, …, xN: TN]: TYPE    allowing dependence of Tj on xi, with i<j (sometimes called Dependent Product)
  • (Product'):   |-    [T1, …, TN]: TYPE     a simple form of above Product, when there is no dependency
  • (Functional):    |-    [x1: T1, …, xN: TN -> U]: TYPE    allowing dependence of Tj on xi, with i<j, and U on all xi
  • (Functional'):    |-    [T1, …, TN -> U]: TYPE   a simple form of above Functional type, when there is no dependency
  • (Predicate subtyping):    p: [T -> bool]    |-    (p): TYPE    so that (p) ≤ T
Type inference rules
You can skip this section, and directly go to Type inference rules revisited, if you prefer to directly see a trimmed and simplified version of the type inference system, with 6 rules only.
  • (Application):    t1: T1', …, tN: TN', f: [x1: T1, …, xN: TN -> U]    |-    f(t1, …, tN): U'
    • with Tj' = Tj[x1/t1; …; xj-1/tj-1] and U' = U[x1/t1; …; xN/tN]
  • (Application'):     t1: T1, …, tN: TN, f: [T1, …, TN -> U]    |-    f(t1, …, tN): U
  • (Abstraction):    e: U    |-     (LAMBDA (x1: T1, …, xN: TN): e): [x1: T1, …, xN: TN, -> U]
    • allowing dependence of Tj on xi, with i<j, and U on all xi
  • (Abstraction'):    e: U    |-     (LAMBDA (x1: T1, …, xN: TN): e): [T1, …, TN -> U]
    • provided [x1: T1, …, xN: TN -> U] is not dependent and thus equivalent to [T1, …, TN -> U]
  • (Product):  t1: T1', …, tN: TN   |-    (t1, …, tN): [x1: T1, …, xN: TN]
    • with Tj' = Tj[x1/t1; …; xj-1/tj-1]
  • (Product'):     t1: T1, …, tN: TN    |-    (t1, …, tN): [T1, …, TN]
    • a simplified form of Product, when there is no dependency
  • (Universal):   e: bool  |-   (FORALL (x1: T1, …, xN: TN): e): bool
  • (Existential):   e: bool  |-   (EXISTS (x1: T1, …, xN: TN): e): bool
  • (Subtyping):     t: T, T≤U    |-    t: U
We shall see that this type inference system, yet only semi-formal, can nevertheless be substantially simplified.


The above presentation of PVS types and type inference rules should be considered as semi-formal rather than formal. A more formal presentation would require the explicit introduction of contexts of variables, in the inference rules. This would probably render the type inference rules harder to understand, at least in a first approach.

On the other hand, the whole system can be simplified:
  • Rules with primed names (Rule') can be removed, as they are just a special case of (Rule), slightly simplified owing to the lack of dependency;
  • Some rules can be simplified, by considering just one variable x instead of N variables x1, …, xN, on the grounds that a function of N variables is identified with a function of one variable, in other words:
    • [x1: T1, …, xN: TN -> U] = [[x1: T1, …, xN: TN] -> U]
  • For instance, (Application) and (Abstraction) can be simplified into:
    • (Application):    t: T, f: [x: T -> U]    |-    f(t): U[x/t]
    • (Abstraction):    e: U    |-     (LAMBDA (x: T): e): [x: T -> U]
Type inference rules revisited

With the observations of the previous Caveat section, we obtained a fairly trimmed and simplified type inference system:
  • (Reduction):   f: [x1: T1, …, xN: TN -> U]    |-    f: [[x1: T1, …, xN: TN] -> U]
  • (Application):    t: T, f: [x: T -> U]    |-    f(t): U[x/t]
  • (Abstraction):    e: U    |-     (LAMBDA (x: T): e): [x: T -> U]
  • (Product):  t1: T1', …, tN: TN   |-    (t1, …, tN): [x1: T1, …, xN: TN]
    • with Tj' = Tj[x1/t1; …; xj-1/tj-1]
  • (Universal):   e: bool  |-   (FORALL (x: T): e): bool
  • (Existential):   e: bool  |-   (EXISTS (x: T): e): bool