PVS‎ > ‎Theory‎ > ‎

### Type inference

 NotationsT, 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 U]: TYPE    allowing dependence of Tj on xi, with i U]: TYPE   a simple form of above Functional type, when there is no dependency(Predicate subtyping):    p: [T -> bool]    |-    (p): TYPE    so that (p) ≤ TType inference rulesYou 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 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: UWe shall see that this type inference system, yet only semi-formal, can nevertheless be substantially simplified.CaveatThe 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 revisitedWith 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