Notations- 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.
Caveat
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
|