Expressive Typing and Abstract Theories in Nuprl and PVS

Paul Jackson U. of Edinburgh

NOTES:

TPHOLs 26th August ’96 • Assume some familiarity with HOL-like sys-

tem, but not necessarily PVS or Nuprl.

• Issues orthogonal to constructivity. No need to know about constructive type theory or propositions-as-types encoding of logic.

• will try to include references to other systems where appropriate (e.g. Coq, IMPS, Mizar).

0-1

I: Expressive Typing

• Examples of types in Nuprl and PVS, but not in e.g. HOL.

• Description and evaluation of type-checking procedures in

– Nuprl

– PVS Subtypes and Parametric Types

• Examples:

ℕ = {i:ℤ | i ≥ 0}
{j..k} = {i:ℤ | j ≤ i ≤ k}
Inj(A, B) = {f:(A → B)|
∀x, y : A. fx = fy ⇒ x = y}

• Use for function domain types:

Array (T, n) = {i:ℕ | i < n} → T

• Provide information on function ranges (examples to come)

• subtyping for quantifiers is a notational convenience. For function domains is significant advance in expressiveness.

2-1

Dependent-Product Types

x:A × B_{x} (Σx:A. B_{x})

⟨a, b⟩ ∈ x:A × B_{x}

if a ∈ A and b ∈ B_{a}. Type of subtraction function on ℕ:

(i:ℕ × {j:ℕ | j ≤ i}) → ℕ Dependent-Function Types

x:A → B_{x} (Πx:A. B_{x})

f ∈ x:A → B_{x}

if for all a ∈ A we have (f a) ∈ B_{a}. Type of mod function:

ℕ → m:{i:ℕ | i ≠ 0 } → {i:ℕ | i < m} Types for Full Specifications Type of square root function:

x:{z:ℝ | z ≥ 0} → {y:ℝ | y ≥ 0 ∧ y^{2} = x } Type Universes as Types

• Permit definition of functions that take types as arguments and return types as results.

• Consider function τ for programming language semantics that maps elements of:

   Datatype Typ = Int | Bool

                     | Fun of Typ × Typ
                     | Prod of Typ × Typ

to corresponding types in theorem prover. τ needs universe type as range.

• Consider typing the C printf function.

• Very useful for defining classes algebraic of algebraic structures … NOTES:

• Up till now all types feature in both PVS and Nuprl.

• Only Nuprl has universe types.

6-1

Conditional Well-formedness

• Total types for usually-partial datatype de-

structors:

hd ∈ {x:T List | x ≠ nil } → T
tl ∈ {x:T List | x ≠ nil } → T List

• Problem Expression:

x ≠ nil ∧ hd x = k Similar issue with

– P ⇒ Q,

– P ∨ Q

– if P then t else f

Conditional Well-formedness • If-then-else Example:

      fib(n : nat) = if n < 2 then 1 else

fib(n − 1) + fib(n − 2)

• Redundant predicates?

      int?(x) = israt(x) ∧ isint(x)

• Pathological Liberalness? False ∧ (λx.x)

Type checking with expressive types

• Non-parameterized Subtypes: ℕ, ℤ ⊆ ℝ (IMPS, Mizar, Isabelle)

• Integer parameters:

Consider n-element array f of type

Array (T, n) = {i:ℕ | i < n} → T

and lookup f e with e linear? e non-linear?

• Non-uniqueness of Maximal Supertypes

⟨5, λi : {0..5}.i ⟩ has maximal supertypes

ℕ × ({0..5} → {0..5}) and

i : ℕ × ({0..i} → {0..i})

Type checking In Nuprl

• All by refinement-style proof.

•  H_{1}, …, H_{n} ⊢ C

means

“if hypotheses H_{1}, …, H_{n} are both well-formed and true, then conclusion C is also well-formed and true.”

• Emphasize that no type-checking done outside of proof.

• Type-checking proofs are spread throughout the course of any proof; they aren’t all done at start.

10-1

Nuprl rules generating type-checking subgoals

• Rules with a well-formedness premise:

\frac{Γ, A ⊢ B Γ ⊢ A ∈ ℙ}{Γ ⊢ A ⇒ B}

\frac{Γ, x:T ⊢ B Γ ⊢ T ∈ 𝕌}{Γ ⊢ ∀x:T. B}

• Checking newly-introduced terms:

\frac{Γ, B_{a} ⊢ C Γ ⊢ a ∈ T}{Γ, ∀x:T. B_{x} ⊢ C}

No checking necessary for cut:

\frac{Γ ⊢ A Γ, A ⊢ C}{Γ ⊢ C}

Nuprl rules for doing type-checking

• Type Well-formedness:

\frac{Γ ⊢ A ∈ 𝕌 Γ, x:A ⊢ B ∈ 𝕌}{Γ ⊢ (x:A → B) ∈ 𝕌}

• Expression Well-formedness:

\frac{Γ ⊢ a ∈ A Γ ⊢ b ∈ B}{Γ ⊢ ⟨a, b⟩ ∈ A × B}

\frac{Γ, x:A ⊢ a ∈ B_{x} Γ, y:A ⊢ B_{y} ∈ 𝕌}{Γ ⊢ (λx. a) ∈ y:A → B_{y}}

Checking function applications in Nuprl

Consider goal Γ ⊢ (f a) ∈ B. Procedure is roughly:

1. Infer a type x:A → B′_{x} for f.

2. Now know that can probably prove

(f a) ∈ B′_{a} Create subgoal

Γ ⊢ B′_{a} ⊆ B

3. Create subgoals Γ ⊢ a ∈ A Γ ⊢ f ∈ x:A → B′_{x} Notes on Nuprl procedure for proving applications

• Proof of B′_{a} ⊆ B can involve reasoning about subtype predicates

• Alternate actions possible if B′_{a} ⊆ B unprovable:

– Alternative typings of f can be tried

– B might be arithmetic subtype. If so, linear arithmetic decision procedure attempts proof of (f a) ∈ B.

Comments on automation of type-checking in Nuprl

• Linear arithmetic decision procedure essential when using arithmetic subtypes.

• Found it very useful to infer arithmetic properties of integer-valued functions. E.g. list length function.

• Performance often very poor. Caching and subsumption checking helpful.

Type checking in PVS

— based around type inference function τ

• On type, returns TYPE if type well-formed.

• On term, returns its type if term well-formed.

• τ also returns list of Type Correctness Conditions (TCCs) which need to be proven.

• TCCs appear as extra lemmas in PVS theories and as extra subgoals in proofs.

• Checking done whenever type, expressions and formulas are introduced, so all formulas in sequents are guaranteed well-formed.

Auxiliary functions on PVS types • μ: finds maximal types

• π: finds predicate part of a type For any type T:

T ≡ {x:μ(T) | π(T)(x) }

An example:

T ≐ ℕ → (i : ℕ × {j:ℤ | j ≤ i})

then

μ(T) = ℕ → (ℤ × ℤ)
π(T) = λf:(ℕ → (ℤ × ℤ)). ∀x:ℕ.
π_{1}(f x) ≥ 0 ∧
π_{2}(f x) ≤ π_{1}(f x)

Definition of PVS type inference function τ

τ(Γ)(⟨a_{1}, a_{2}⟩) = τ(Γ)(a_{1}) × τ(Γ)(a_{2})
τ(Γ)(λx:A. a) = x:A → B where

τ(Γ)(A) = TYPE ∧ B = τ(Γ, x : VAR A)(a)

τ(Γ)(f a) = B_{a}, where

τ(Γ)(f) = x:A → B_{x}, τ(Γ)(a) = A′, μ(A), μ(A′)

Compatible at a Γ ⊢ π(A)(a)

Compatibility testing also creates proof obligations.

Comments on type-checking in PVS

• Maintains seperation of type system and expression language.

• Higher performance than Nuprl, especially when not dealing with theories that generate many TCCs.

• Better, faster decision procedures to help out with solving TCCs. E.g. Shostak’s integrated congruence-closure, linear arithmetic procedure. This also handles some basic non-linear arithmetic.

Property lemmas (judgements) in PVS Given

0 : real
expt : [real,nat->real]
max : [m:real,n:real->
        {p: real | p >= m AND p >= n}]

the user supplies property lemmas such as:

0 HAS_TYPE nat
expt HAS_TYPE [rational, nat -> rational]
expt HAS_TYPE [posint, nat -> posint]
max HAS_TYPE [i:int,j:int ->
                {k: int | i<=k AND j<=k}]
max HAS_TYPE [i:nat,j:nat ->
                {k: nat | i<=k AND j<=k}]
posrat SUBTYPE_OF nzrat

Other typing-related issues in both PVS and Nuprl

• Argument synthesis

• Coercions

• Contravariant function subtyping Argument synthesis

• In PVS can write

      map f a

• PVS infers type parameters S and T from

types of f and a

      map[S,T] f a

• Something similar happens in Nuprl and many other systems Coercions and function domain subtyping

• In

b ; ∑ ; i=a f_{i}

ideally have f ∈ {a..b} → T

• But then

b ; ∑ ; i=a f_{i} = c−1 ; ∑ ; i=a f_{i} + b ; ∑ ; i=c f_{i}

requires additional typings f ∈ {a..c − 1} → T, f ∈ {c..b} → T Evaluation of expressive typing

• Specifications significantly more accurate and concise

• Higher level of reasoning

• Performance a concern

• Need fast powerful – linear (+ non-linear?) arithmetic

– congruence reasoning

– property inference

– proof obligation subsumption

• If used with care, large developments very feasible

II: Abstract Theories

• Examples, Uses

• PVS

• Nuprl

• Issues Introduction to abstract theories Informally, an abstract theory consists of

• types T

• operators (possibly nullary) F over the types in T.

• predicates that the operators F can be as-

sumed to satisfy An abstract theory is instantiated when instances are provided for the types and operators that satisfy the predicates Examples of abstract theories A monoid is a tuple ⟨M, ∘ , e⟩ where

• M is a type,

• ∘ is a binary operator of type C^{2} → C and e is a distinguished element of M,

• ∘ is associative and e is a left and right

identity for ∘. Other examples are linear orders and stacks.

Example instances of abstract theories

Semigroup :  ⟨ℝ, min⟩

Monoid :  ⟨T List, append, nil⟩

AbelianMonoid :  ⟨𝔹, ∧, ⊤⟩

⟨ℕ, max , 0⟩ ⟨T Set, ∪, ∅⟩

Group :  ⟨T Bij, ∘, id, inv⟩
Field :  ⟨ℝ, +, −, 0, ×, 1 ⟩

Example theorems over abstract theories Theorems about iteration:

• on semigroup / monoid

⊢ k ; ∑ ; i=j x_{i} = x_{j} + k ; ∑ ; i=j+1 x_{i}

• on abelian monoid

⊢ _{i∈A}^{∑} x_{i} + _{i∈B}^{∑} x_{i} = _{i∈A⊎B}^{∑} x_{i}

• on ring

a × k ; ∑ ; i=j x_{i} = k ; ∑ ; i=j a × x_{i}

Uses of abstract theories

• General theorem-proving support (view as enriched polymorphism)

• Program specification and refinement

• Mathematics (Algebra, Analysis, Topology, Category Theory)

An abstract theory as a PVS theory

monoids1[T : TYPE, o:[T,T->T], e:T] : THEORY
BEGIN
ASSUMING
x,y,z : VAR T
assoc  : ASSUMPTION  (x o y) o z =
                        x o (y o z)
lident : ASSUMPTION  e o x = x
rident : ASSUMPTION  x o e = x
ENDASSUMING
...
END monoids1

A development in PVS monoids theory

i,j : VAR int
f : VAR [int->T]
% f(i) o ... o f(j)
itop(i,j)(f): RECURSIVE T =
  IF i > j THEN e
  ELSE f(i) o itop(i+1,j)(f) ENDIF
   MEASURE  LAMBDA (i,j)(f) : max(1+j-i,0)

itop_unroll_hi : LEMMA
  i <= j IMPLIES
    itop(i,j)(f) = itop(i,j-1)(f) o f(j)

Importing and instantiating PVS theories

monoids2 : THEORY
BEGIN
intplusmon : THEORY = monoids1[int,+,0]
i,j: VAR int
f : VAR int->int
sum(i,j)(f) = intplusmon.itop(i,j)(f)
n: VAR nat
sum_squares : LEMMA
   6 * sum(0,n)(LAMBDA (i): i * i) =
     n * (n+1) * (2 * n + 1)
END monoids2

Abstract theories in Nuprl

All instances of a theory are collected into a type:

MonSig == T:𝕌 x op:(T→T→T) x T
|m| == m.1
*m == m.2.1
em == m.2.2
Assoc(T;op) ==
  ∀x,y,z:T. x op (y op z) = (x op y) op z
Ident(T;op;id) ==
  ∀x:T. x op id = x ∧ id op x = x
Mon == { m:MonSig | Assoc(|m|;*m)
                 ∧ Ident(|m|;*m;em) }

Note essential use of type universe 𝕌.

Instances of monoids in Nuprl

<ℤ,+> ==  <ℤ, λx,y.x + y, 0>
⊢ <ℤ,+> ∈ Mon
r↓xmn ==  <|r|, *r, 1r>
⊢ ∀r:Rng. r↓xmn ∈ Mon

Example abstract theorem in Nuprl

⊢ ∀g:Mon. ∀a,b:ℤ.
    a ≤ b

    ⇒ (∀E:{a..b^{−}} → |g|. ∀k:ℤ.

          Πg a ≤ j < b. E[j]
          = Πg a + k ≤ j < b + k. E[j - k])

b−1 ; ∏ ; j=a E_{j} = b+k−1 ; ∏ ; j=a+k E_{j−k}

When should algebraic classes be types? If classes are not types

• Quantification over classes always outermost ∀

• Fixed finite number of class instances If classes are types

• Arbitrary quantification and families of instances OK

• Can define reason about functions and operations on algebraic structures. E.g. free constructions, refinement mappings • Algebraic class ≐ collection of instances of

an abstract theory

• not types approach OK for much theoremproving support

• Type universes complicate type theory. Get non-canonical type expressions

• IMPS, EHDM, OBJ provide special support for refinement mappings without use of classes. However support not as flexible as when have classes

• classes essential for maths

37-1

Algebraic classes in PVS

monoids9[T : TYPE] : THEORY
BEGIN
 MonTy : TYPE =
        [#
          c : set[T],
          op:[(c),(c)->(c)],
          id:(c)
        #]
 Mon?(m : MonTy) : bool =
   associative?(op(m))
   AND left_identity(op(m))(id(m))
   AND right_identity(op(m))(id(m))
 Mon : TYPE = (Mon?)
...
END monoids9

NOTES:

• Similar to approach Elsa Gunter tried in HOL

• However, get function domains right in PVS

38-1

PVS development using monoid class type

m,n,p : VAR Mon
x,y : VAR T
HomTy(m,n) : TYPE = [(c(m)) -> (c(n))]
hom?(m,n)(f : HomTy(m,n)) : bool =
  (FORALL (x,y:(c(m))) : f(op(m)(x,y))
                         = op(n)(f(x),f(y)))
  AND f(id(m)) = id(n)
Hom(m,n) : TYPE = (hom?(m,n))
hom_comp : LEMMA
   FORALL (f:Hom(m,n)),(g:Hom(n,p)) :
     hom?(m,p)(g o f)

Automatically instantiating abstract theories Consider using the abstract theorem:

\begin{matrix}∀m:Mon. ∀x, y, z, w:|m|. \\ (x ∘_{m} y) ∘_{m} (z ∘_{m} w) = x ∘_{m} (y ∘_{m} z) ∘_{m} w \end{matrix}

to rewrite

(1 + 2) + (3 + 4) where + ∈ ℤ → ℤ → ℤ.

A simple matching function could yield bindings

x ↦ 1, y ↦ 2, z ↦ 3, w ↦ 4
∘_{m} ↦ +

Type matching could give |m| ↦ ℤ, yielding the binding

m ↦ ⟨ℤ, +, u ⟩

for unknown u. Knowing m must have type Mon, consultation of a maths database could give the full binding

m ↦ ⟨ℤ, +, 0 ⟩

Issues in automatic instantiation

• database still needed to justify typing for m, even if no unknowns.

• database might only have entry

⟨ℤ, +, 0, − ⟩ ∈ AbGroup Need to know that

      AbGroup ⊆^{∗} Mon

• Automation of inference with ⊆^{∗} important • Defining S ⊆^{∗} T easiest when S, T have

named fields (Mizar, IMPS, Axiom).

⊆^{∗} with named fields (structural subtyping)

AbGroup  Mon
fields  C : 𝕌  C : 𝕌
op : C^{2} → C  op : C^{2} → C
inv : C → C  id : C

id : C

properties Assoc(C , op)  Assoc(C , op)
Ident(C , op, id)  Ident(C , op, id)

Inv(C , op, id, inv) Comm(C , op)

Key issues in abstract theories

• theory interpretations – special support / automation needed – structure subtyping a first step

• Algebraic classes as types or theories? – For mathematics

– For hardware/software verification – For program specification refinement