The Formal Semantics of PVS^{1}

Sam Owre and Natarajan Shankar

owre@csl.sri.com         shankar@csl.sri.com

URL: http://www.csl.sri.com/sri-csl-fm.html

SRI International Computer Science Laboratory Menlo Park CA 94025 USA

Technical Report CSL-97-2R August 1997, Revised March 1999

1Funded by National Aeronautics and Space Administration Contract NAS1-18969, Task 11 and National Science Foundation Grant CCR 9300444.

ii

Abstract

A specification language is a medium for expressing what is computed rather than how it is computed. Specification languages share some features with programming languages but are also different in several important ways. For our purpose, a specification language is a logic within which the behavior of computational systems can be formalized. Although a specification can be used to simulate the behavior of such systems, we mainly use specifications to state and prove system properties with mechanical assistance.

We present the formal semantics of the specification language of SRI’s Prototype Verification System (PVS). This specification language is based on the simply typed lambda calculus. The novelty in PVS is that it contains very expressive language features whose static analysis (e.g., typechecking) requires the assistance of a theorem prover. The formal semantics illuminates several of the design considerations underlying PVS, particularly the interaction between theorem proving and typechecking. iv

Contents

1 Introduction 1 1.1 Real versus Idealized PVS . . . . . . . . . . . . . . . . . . . . 2 1.2 Semantic Preliminaries . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2 The Simple Type Theory 9 2.1 Contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2 Type Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.4 Some Syntactic Operations . . . . . . . . . . . . . . . . . . . . 16 2.5 Type Definitions . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

3 Adding Subtypes 20 3.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

4 Dependent Types 30 4.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

5 Theories and Parametric Theories 41 5.1 Theories without Parameters . . . . . . . . . . . . . . . . . . . 41 5.2 Constant Definitions . . . . . . . . . . . . . . . . . . . . . . . 45 5.3 Parametric Theories . . . . . . . . . . . . . . . . . . . . . . . 45 5.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

6 Conditional Expressions and Logical Connectives 49 6.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 7 Proof Theory of PVS 53

7.1 PVS Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . . 53 7.1.1 Structural Rules . . . . . . . . . . . . . . . . . . . . . . 53 7.1.2 Cut Rule . . . . . . . . . . . . . . . . . . . . . . . . . . 54 7.1.3 Propositional Axioms . . . . . . . . . . . . . . . . . . . 54 7.1.4 Context Rules . . . . . . . . . . . . . . . . . . . . . . . 55 7.1.5 Conditional Rules . . . . . . . . . . . . . . . . . . . . . 55 7.1.6 Equality Rules . . . . . . . . . . . . . . . . . . . . . . 55 7.1.7 Boolean Equality Rules . . . . . . . . . . . . . . . . . . 56 7.1.8 Reduction Rules . . . . . . . . . . . . . . . . . . . . . 56 7.1.9 Extensionality Rules . . . . . . . . . . . . . . . . . . . 56 7.1.10 Type Constraint Rule . . . . . . . . . . . . . . . . . . 57

7.2 Soundness of the Proof Rules . . . . . . . . . . . . . . . . . . 57 7.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

8 Conclusion 61

Bibliography 64

Chapter 1

Introduction

PVS is a system for specifying and verifying properties of digital hardware and software systems. The specification language of PVS is designed to admit succinct, readable, and logically meaningful specifications. The PVS specification language is designed for effective proof construction rather than efficient execution. The design considerations underlying the language are therefore somewhat different from those of a corresponding programming language. For example, the language contains constructs that can be statically typechecked only with the assistance of a theorem prover. This is acceptable because the PVS specification language is intended for use in conjunction with powerful support for automated theorem proving. The logic of PVS is based on a simply typed higher-order logic with function, record, and product types, and recursive type definitions. This type system is extended with subtypes that are analogous to subsets, and with dependently typed functions, records, and products. The resulting type system has several advantages. It is possible, for instance, to statically ensure that all array references are within their respective array bounds. PVS specifications are organized into theories that can be parametric in types as well as individuals. While the semantics of the simply typed fragment is straightforward, the extensions such as subtyping, dependent typing, and (theory-level) parametricity do pose significant challenges. This report presents a concise but idealized definition of the PVS specification language and its intended formal set-theoretic semantics. It is neither an overview of the PVS language nor a guide to the Prototype Verification System (see the PVS user manuals [OSRSC98]).

The primary purpose of the formal semantics is as a useful reference for the developers and users of PVS. The idealized core of the specification language as presented here serves as a succinct foundation for studying the expressive power of the language. Pertinent questions about PVS are answered directly by the formal semantics presented here:

1. What is the semantic core of the language, and what is just syntactic sugar?

2. What are the rules for determining whether a given PVS expression is well typed?

3. How is subtyping handled, and in particular, how are proof obligations corresponding to subtypes generated?

4. What is the meaning, in set-theoretic terms, of a PVS expression or assertion?

5. Are the type rules sound with respect to the semantics?

6. Are the proof rules sound with respect to the semantics?

7. What is the form of dependent typing used by PVS, and what kinds of type dependencies are disallowed by the language?

8. What is the meaning of theory-level parametricity, and what, if any, are the semantic limits on such parameterization?

9. What language extensions are incompatible with the reference semantics given here?

Chapter 8 summarizes the answers to these questions.

1.1 Real versus Idealized PVS

The semantic treatment in this report is incomplete in some important ways. It does not treat the nonlogical parts of the language. In particular, it ignores arithmetic and recursive definitions. It also omits abstract datatypes [OS97]. These will be treated in a future expanded version.

The present semantics also makes several idealizations from the real PVS for the purpose of clarity. While the semantic treatment is not comprehensive, the idealization of PVS used here is faithful to the implemented form of PVS.

1. No name resolution. All names must be in fully resolved form with their theory name and actual parameters. We regard name resolution as a convenience provided by the PVS type checker and not an operation with any semantic relevance. A technical description of name resolution in PVS will be given elsewhere.

2. No overloading. As with name resolution, overloading is a syntactic convenience with no semantic import.

3. No IMPORTINGs. The importing of theories is a hint to name resolution. The semantic definition assumes that all instances of theories declared prior to the present one are visible.

4. Variable declarations ignored. All variables must be locally declared. Global variable declarations are regarded as a syntactic convenience.

5. No records. These are ignored in the semantic treatment since product types capture all the semantically essential features of records.

1.2 Semantic Preliminaries

The PVS specification language is based on higher-order logic. This means that variables can range over individuals (such as numbers) as well as functions, functions of functions, and so on. As is well known, some type distinction is needed; otherwise, it is easy to obtain a contradiction by defining the predicate N(P) as ¬(P (P)) so that both N(N) and ¬N(N) hold. In the theory of types [Chu40], the universe is stratified into distinct types so that a predicate can be applied only to a lower type and thus cannot be applied to itself.

Types also serve as a powerful mechanism for detecting syntactic and semantic errors through typechecking. This role of types is best exemplified by their use in various programming languages such as Algol, Ada, and ML, and is also heavily emphasized in the PVS type system.

The desirability for strong typing in a specification logic is not widely accepted. Fraenkel et al [FBHL84] express the opinion that such typing is repugnant in a mathematical logic since it constrains expressiveness by not allowing individuals of differing types to be treated uniformly. Lamport [Lam94] argues that type correctness is like any other program property and should be established by means of a proof rather than by syntactic restraints. Lamport and Paulson [LP97] analyze the tradeoffs between typed and untyped specification languages. We claim that

1. Types impose a useful discipline on the specification.

2. Types lead to easy and early detection of a large class of syntactic and semantic errors.

3. Type information is useful in mechanized reasoning.

The semantics of a higher-order logic is given by mapping the well-formed types of the logic to sets, and the well-formed terms of the logic to elements of the sets representing their type. The set constructions we use can be formalized within Zermelo-Fraenkel set theory with the axiom of choice (ZFC). The intended interpretation of a function type in higher-order logic is that it represents the set of all functions from the set representing the domain type to the set representing the range types.^{1} PVS also has predicate subtypes that are to be interpreted over the subsets of the set representing the parent type.

The semantics of PVS will be given by considering a sequence of increasingly expressive fragments of PVS. The semantics of each fragment of PVS will be presented in three steps. The first step is to define a set-theoretic universe containing enough sets to represent the PVS types. The second step is to define a typechecking operation that determines whether a given PVS expression is well typed. The third step is to define a semantic function that assigns a representation in the semantic universe to each well-typed PVS type and term.

We first lay out the ZFC set constructions needed for defining the semantics of PVS. The base types in PVS consist of the Booleans bool and the real numbers real. The Booleans can be modeled by any two-element set, say 2 consisting of the elements 0 and 1, where 0 is the empty set and the only element of the set 1. The real numbers can be captured by means of Dedekind cuts or Cauchy sequences, and we label this set R.

To define the semantics, we need a universe that contains the sets 2 and R and is closed under Cartesian products (written as X × Y) and power sets (written as ℘(X)). Note that functions are modeled as graphs, that is, sets of ordered pairs, so that a function type [A→B] is represented by a subset of the powerset ℘([[A]] × [[B]]) of the Cartesian product of the sets [[A]] and [[B]] representing A and B, respectively. A set F that is a subset of X × Y is the graph of a function with domain X and range Y if for every x ∈ X there is a y ∈ Y such that ⟨x, y⟩ ∈ F, and whenever ⟨x, y⟩ ∈ F and ⟨x, y′⟩ ∈ F, we have y = y′. For such a set F, Function(F) holds and dom(F) = X. The set of graphs of total functions from a set Y to a set X is represented as X^{Y}.

1It is only in the standard model of higher-order logic that the function type is required to represent the set of all functions from the domain set to the range set. Higher-order logic can be interpreted in general models where the function type can be interpreted in any manner as long as it satisfies the various axioms such as application, abstraction, and extensionality [And86]. Higher-order logic is complete with respect to the general models interpretation so that a statement that is valid in all models is provable. It is, however, incomplete with respect to the standard model.

If F is the graph of a function and t an element in its domain, then F (t) represents the result of applying the function F to t. At the semantic level, a function F will never be applied to an argument t outside dom(F), because in the PVS language, a function application is typechecked so that the argument expression has the same type as the domain type of the function expression.

We can model the entire type universe of the simply typed fragment of PVS by the set U, which is defined cumulatively by starting from the base sets 2 and R, and including the Cartesian products, the function spaces, and subsets of previously included sets, at each stage. Cartesian products are used to model products in PVS, and function spaces model function types. Subsets are needed to model predicate subtypes. It is sufficient to iterate these stages up to the ordinal ω.

Definition 1.1 (type universe)

U_{0} = {2, R}
U_{i+1} = U_{i} ∪ {X × Y | X, Y ∈ U_{i}} ∪ {X^{Y} | X, Y ∈ U_{i}} ∪ ⋃_{X∈U_{i}} ℘(X)
U_{ω} = ⋃_{i∈ω} U_{i}
U = U_{ω}

We refer to U as the basic universe.^{2} The semantic definitions below will assign a set in U to each PVS type and an element in ⋃ U to each well-typed term of PVS. The rank of a set X in U is the least i such that X ∈ U_{i}. The notion of rank plays an important role in the semantics of dependent types and parametric theories.

1.3 Related Work

There is a long history of work in specification languages. Many ideas similar to those underlying the PVS specification language also occur in other specification languages.

The wide-spectrum languages are typically based on set theory or higherorder logic. The language VDM is one of the earliest such specification formalisms [Jon90]. It is based on a first-order logic with partial functions augmented with datatype axioms. The datatype theories in VDM include those for finite sets, maps, sequences, and recursive datatypes such as lists and trees. VDM has a notion of datatype invariants that yields a simple form of predicate subtyping. Operations on state are specified in terms of pre-condition/post-condition pairs. Specifications are structured into parameterized modules. In contrast to VDM, the PVS language is based on strictly typed higher-order logic with a built-in notion of predicate subtyping and dependent typing. The resulting PVS logic is more compact in that many of the datatypes that are presented axiomatically in VDM can be defined within PVS. There is no builtin notion of state in PVS since it is possible to use the higher-order logic of PVS to define a variety of state-based formalisms, including various linear and branching-time temporal logics. VDM uses a 3-valued logic for the logical connectives in order to deal with partial functions, whereas PVS uses a classical 2-valued logic and predicate subtyping to assign a type to a partial function as a total function on its domain of definition. Jones [Jon90] provides only an informal semantics for VDM. The RAISE system is a comprehensive toolset based on the ideas of VDM [RAISE92].

2The inclusion of X^{Y} in U is actually redundant but aids clarity.

The Z specification language [Spi88] is another wide-spectrum language based on a typed first-order set theory. A Z specification is a collection of schemas consisting of declarations of types and constants accompanied with invariants. Z schemas can either specify datatype invariants or precondition/post-condition constraints. A schema calculus is used to combine schemas using logical connectives. Spivey [Spi88] presents a formal semantics for Z without giving a proof system or a soundness proof. Spivey’s treatment of partial functions in the Z semantics employs the commonly used convention that f(a) when a is not in the domain of a is some arbitrarily chosen value. This is fine for most purposes but can be confusing when dealing with recursively defined partial functions. For example, the definition bad(x) = 1 + bad(x) is everywhere undefined but admitting it as an axiom leads to an immediate contradiction. Z also lacks any mechanism for conservative extensions such as definitional principles for constants and datatypes so that the consistency of Z specification has to be demonstrated by exhibiting a model.

Algebraic specification languages like OBJ [FGJM85] and Larch [GH93] provide an equational/rewriting framework for specifying datatypes and operations on datatypes. OBJ has many of the same theory parameterization mechanisms as PVS. The subsort mechanism in OBJ is also similar except that it is handled by introducing retracts or runtime checks rather than proof obligations generated by the type checker. The OBJ logic is quite restricted compared to PVS since it is based on a first-order, equational framework with an initial semantics where two ground terms are distinct unless they can be proved equal. OBJ has very limited support for proof development and is primarily intended as an executable specification language.

The specification languages that are closer to PVS are those that accompany various automated proof checking systems. The closest of these is Ehdm [EHDM93], which employs a similar higher-order logic with subtyping and proof obligation generation. Ehdm lacks many of the features of PVS: subtyping is restricted to type declarations and there is no dependent typing.

Higher-order logic is used by other systems such as HOL [GM93] and TPS [AMCP84]. Both HOL and TPS employ simply typed higher-order logic without features such as subtyping, dependent typing, or parametric theories. Andrews [And86] gives a thorough account of the semantic aspects of higherorder logic. The formal semantics of the HOL logic are carefully outlined (by Pitts) in the book by Gordon and Melham [GM93].

Systems like Coq [DFH^{+}91] and Nuprl [CAB^{+}86] are based on intuitionistic higher-order logics. Coq allows quantification over types, whereas Nuprl has quantification over a hierarchy of type universes. Both logics admit dependent typing. The set-theoretic semantics of dependently typed intuitionistic type theories has been studied by Dybjer [Dyb91] and Howe [How91, How96]. Not surprisingly, their semantic treatment of dependent typing is similar to the one given here but they do not delimit the possible dependencies as is done with the PVS semantics. The PVS semantics presented here clearly specifies the kind of type dependencies that are disallowed in the logic. Dybjer and Howe also do not address subtyping but do describe the semantics of language features missing in PVS (type universes in the case of Howe, and inductive families in the case of Dybjer). Dybjer does not identify the universe over which terms and types are interpreted. Howe requires an infinite sequence of inaccessible cardinals for his universe construction.

1.4 Outline

In Chapter 2, we define the syntax and semantics of the simply typed fragment of PVS. Type definitions are also introduced in this chapter along with the definition of definitional equivalence on types. Chapter 3 adds subtyping to the simply typed fragment and specifies the additional type rules and semantic definitions that are needed. Chapter 4 extends the language with dependent function and product types. Theories and parametric theories are introduced into the language in Chapter 5. The type rules and semantics for conditional expressions and the logical connectives defined using conditional expressions 8 Chapter 1. Introduction are introduced in Chapter 6. Chapter 7 specifies the axioms and inference rules of PVS.

The Simple Type Theory

PVS is a strongly typed specification language. The simply typed fragment includes types constructed from the base types by the function and product type constructions, and expressions constructed from the constants and variables by means of application, abstraction, and tupling. Expressions are checked to be well typed under a context, which is a partial function that assigns a kind (one of TYPE, CONSTANT, or VARIABLE) to each symbol, and a type to the constant and variable symbols. We use the metavariables Γ, Δ, and Θ to range over contexts. The metavariables A, B, and T range over PVS type expressions, the metavariables r and s range over symbols (identifiers), the metavariables x and y range over PVS variables, and the metavariables a, b, f, and g range over PVS terms. Given a context Γ and a symbol s, we say that Γ(s) is undefined if s is not declared in Γ.

The pretypes of the simple type theory include the base types such as bool and real. A function pretype from domain pretype A to range pretype B is constructed as [A→B]. A product pretype of A_{1}, A_{2} is constructed as [A_{1}, A_{2}]. A type is a pretype that has been typechecked in a given context. Types in the simple type theory are simple enough that the only distinction between pretypes and types is that the symbols in a type must be appropriately declared in the given context.

Example 2.1 (pretypes) bool, real, [bool, real], [[real, bool]→bool].

The preterms of the language consist of the constants, variables, pairs, projections, applications, and abstractions. The metavariables c and d range over constants. Pairs are of the form (a_{1}, a_{2}) where each a_{i} is a preterm. Applications have the form f a where f and a are preterms. A pair projection is an expression of the form p_{i} a, where i ∈ {1, 2}. Lambda abstractions have the form λ(x: T): a, where T is a pretype and a is a preterm. Parentheses are used for disambiguation. A term is a preterm that has been typechecked in a given context.

Example 2.2 (preterms) TRUE, ¬ TRUE, λ (x : bool): ¬(x), p_{2} (TRUE, FALSE), (TRUE, λ (x : bool) : ¬ (¬ x)).

2.1 Contexts

A context is a sequence of declarations, where each declaration is either a type declaration s : TYPE, a constant declaration c : T where T is a type, or a variable declaration x : VAR T. Preterms and pretypes are typechecked with respect to a given context. The empty context is represented as {}. The well-formedness rules for contexts are presented below. A context can also be applied as a partial function so that for a symbol s with declaration D, (Γ, s: D)(s) = D and (Γ, s: D)(r) = Γ(r) for r ≠ s. If s is not declared in Γ, then Γ(s) is undefined. If Γ is a context, then for any symbol s, the kind of the symbol s in Γ is given by kind(Γ(s)). If the kind of s in Γ is CONSTANT or VARIABLE, then the type(Γ(s)) is the type assigned to s in Γ.

Example 2.3 (context)

bool : TYPE, TRUE : bool, FALSE : bool, x : VAR [[bool, bool]→bool]

2.2 Type Rules

The type rules for the simple type theory are given by a recursively defined partial function τ that assigns

1. A type τ(Γ)(a) to a preterm a that is well typed with respect to a context Γ.

2. The keyword TYPE as the result of τ(Γ)(A) when A is a well-formed type under context Γ.

3. The keyword CONTEXT as the result of τ(Γ)(Δ) when Δ is a well-formed context under context Γ. The context Γ is empty for the simply typed fragment so that typechecking is always invoked as τ()(Γ).

Otherwise, τ is undefined in the case of an ill-typed preterm or an ill-formed type or context.

The type rules are given by the recursive definition for τ. Typechecking in PVS assigns a “canonical” type to a preterm. Customarily, type rules are presented as inference rules, but a functional presentation is more appropriate for PVS since

1. The type assignment is deterministic. A term can, in general, though not in the simply typed fragment, be assigned a number of types but it always has at most one canonical type.

2. The soundness proof need only show that the meaning of the term is an element of the meaning of its canonical type. Thus, only the canonical type derivation for a term has to be shown sound and not every valid type derivation.

3. The meaning of a term is therefore given by recursion on the term itself and not on its typing derivation. There is no need to show separately that this meaning is coherent, that is, independent of the typing derivation.

A functional presentation of the type rules also leads to natural and straightforward soundness arguments. Note that the well-formedness rules for contexts and types are trivial in the simply typed situation but become more meaningful when the type theory is extended. Note also that in the type rules for expressions and types, the well-formedness of the relevant context is not explicitly checked. These rules do preserve the well-formedness of the context in each recursive call so that if the initial context is well formed, then so is every intermediate one.

Definition 2.4 (type rules)

τ()({}) = CONTEXT
τ()(Γ, s : TYPE) = CONTEXT, if Γ(s) is undefined

and τ()(Γ) = CONTEXT

τ()(Γ, c: T) = CONTEXT, if Γ(c) is undefined,

τ(Γ)(T) = TYPE,

and τ()(Γ) = CONTEXT

τ()(Γ, x: VAR T) = CONTEXT, if Γ(x) is undefined,

τ(Γ)(T) = TYPE,

and τ()(Γ) = CONTEXT

τ(Γ)(s) = TYPE, if kind(Γ(s)) = TYPE
τ(Γ)([A→B]) = TYPE, if τ(Γ)(A) = τ(Γ)(B) = TYPE

τ(Γ)([A_{1}, A_{2}]) = TYPE, if τ(Γ)(A_{i}) = TYPE for 1 ≤ i ≤ 2
τ(Γ)(s) = type(Γ(s)),

                    if kind(Γ(s)) ∈ {CONSTANT, VARIABLE}

τ(Γ)(f a) = B, if τ(Γ)(f) = [A→B] and τ(Γ)(a) = A
τ(Γ)(λ(x: T): a) = [T →τ(Γ, x: VAR T)(a)], if Γ(x) is undefined

and τ(Γ)(T) = TYPE

τ(Γ)((a_{1}, a_{2})) = [τ(Γ)(a_{1}), τ(Γ)(a_{2}))]
τ(Γ)(p_{i} a) = T_{i}, where

τ(Γ)(a) = [T_{1}, T_{2}]

In the type rule for lambda abstraction, the constraint that Γ(x) must be undefined can be satisfied by suitably renaming the bound variable since we treat terms as equivalent modulo the renaming of bound variables.

Example 2.5 (type rules) Let Ω label the context bool : TYPE, TRUE : bool,

FALSE : bool

τ()({}) = CONTEXT

                   τ()(Ω) = CONTEXT
  τ(Ω)([[bool, bool]→bool]) = TYPE
        τ(Ω)((TRUE, FALSE)) = [bool, bool]
      τ(Ω)(p_{2}(TRUE, FALSE)) = bool
     τ(Ω)(λ(x : bool): TRUE) = [bool→bool]

2.3 Semantics

Recall that a preterm a with a type assigned by τ under context Γ is said to be a term of type τ(Γ)(a) in the context Γ. If γ is an assignment for the symbols declared in context Γ, the semantics of the simple type theory of PVS is given by mapping a type T to a (possibly empty) set M(Γ | γ)(T), and a term a with assigned type T to an element of the set M(Γ | γ)(T) in the basic universe U. The assignment γ is a list of bindings of the form {s_{1} ← t_{1}} … {s_{n} ← t_{n}}. The application of an assignment γ to a symbol s is such that γ{s ← t}(s) is t, whereas γ{r ← t}(s) is γ(s) when r ≢ s.

The meaning function M returns the meaning of a well-formed type A and a well-formed expression a in the context Γ under an assignment γ as M(Γ | γ)(A) and M(Γ | γ)(a),respectively. The meanings of type names, constants, and variables declared in Γ are obtained from the assignment γ. A function type is mapped to the corresponding function space. A product type is mapped to the corresponding Cartesian product. An application term is interpreted by means of set-theoretic function application. A lambda abstraction yields the graph of the corresponding function. A pair expression is mapped to the corresponding set-theoretic ordered pair.

Definition 2.6 (meaning function)

M(Γ | γ)(s) = γ(s),

                        if kind(Γ(s)) ∈ {TYPE, CONSTANT, VARIABLE}

M(Γ | γ)([A→B]) = M(Γ | γ)(B)^{M(Γ | γ)(A)}
M(Γ | γ)([T_{1}, T_{2}]) = M(Γ | γ)(T_{1}) × M(Γ | γ)(T_{2})
M(Γ | γ)(f a) = (M(Γ | γ)(f))(M(Γ | γ)(a))
M(Γ | γ)(λ(x: T): a) = \{⟨y, z⟩ | \begin{matrix}y ∈ M(Γ | γ)(T), \\ z = M(Γ, x: VAR T | γ\{x ← y\})(a)\} \end{matrix}
M(Γ | γ)((a_{1}, a_{2})) = ⟨M(Γ | γ)(a_{1}), M(Γ | γ)(a_{2})⟩
M(Γ | γ)(p_{i} a) = t_{i}, where M(Γ | γ)(a) = ⟨t_{1}, t_{2}⟩

Example 2.7 (meaning function) Let ω be an assignment for the context Ω in Example 2.5, of the form

                {bool ← 2}{TRUE ← 1}{FALSE ← 0}

then

M(Ω | ω)([bool, bool]) = 2 × 2
M(Ω | ω)((TRUE, FALSE)) = ⟨1, 0⟩
M(Ω | ω)(λ(x: bool): TRUE) = {⟨0, 1⟩, ⟨1, 1⟩}

Definition 2.8 (satisfaction) A context assignment γ is said to satisfy a context Γ (in symbols γ ⊧ Γ) iff

1. γ(bool) = 2, 2. γ(TRUE) = 1,

3. γ(FALSE) = 0,

4. γ(s) ∈ U whenever kind(Γ(s)) = TYPE, and

5. γ(s) ∈ M(Γ | γ)(type(Γ(s)))

whenever kind(Γ(s)) ∈ {CONSTANT, VARIABLE}.

Example 2.9 (satisfaction)

1. The assignment ω satisfies context Ω.

2. The assignment ω{one ← 1}{zero ← 0} satisfies the context

     Ω, one : TYPE, zero : one.

We need one useful proposition that asserts that typing judgements are not invalidated when the context is extended.

Proposition 2.10 If τ()(Γ) = τ()(Γ′) = CONTEXT and Γ is a prefix of Γ′, then for all pretypes A, τ(Γ)(A) = TYPE implies τ(Γ′)(A) = TYPE, and for all preterms a, τ(Γ)(a) = A implies τ(Γ′)(a) = A.

The following theorems follow from the induction suggested by the definitions of τ and M. The first of these is straightforward and is given without proof.

Theorem 2.11 (type construction) If τ()(Γ) = CONTEXT and τ(Γ)(a) = A, then τ(Γ)(A) = TYPE.

Theorem 2.12 (type soundness) If τ()(Γ) = CONTEXT, γ satisfies Γ, and τ(Γ)(A) = TYPE, then M(Γ | γ)(A) ∈ U.

Proof. The proof is by induction on the structure of the pretype A. Recall that if X ∈ U, then for some i, X ∈ U_{i}. This yields three cases:

1. A ≡ s: By Definition 2.4, Γ(s) is defined and kind(Γ(s)) is TYPE. Then by Definition 2.6, M(Γ | γ)(s) is γ(s), and by Definition 2.8, γ(s) ∈ U.

2. A ≡ [B→C]: We then have that τ(Γ)(B) = τ(Γ)(C) = TYPE. Letting X label M(Γ | γ)(B), and Y label M(Γ | γ)(C), we have by the induction hypothesis that X ∈ U and Y ∈ U. Let j be the least rank such that M(Γ | γ)(B) ∈ U_{j} and M(Γ | γ)(C) ∈ U_{j}. By Definition 2.6, M(Γ | γ)(A) = Y^{X}, and hence M(Γ | γ)(A) ∈ U_{j+1} by Definition 1.1.

3. A ≡ [A_{1}, A_{2}]: Again by Definition 2.4 and the induction hypothesis, we have for each i ∈ {1, 2}, that M(Γ | γ)(A_{i}) ∈ U. Let j be the least rank such that for i ∈ {1, 2}, M(Γ | γ)(A_{i}) ∈ U_{j}. Then, it is easy to verify from Definition 1.1 that M(Γ | γ)(A) ∈ U_{j+1}.

Theorem 2.13 (term soundness) If τ()(Γ) = CONTEXT, γ satisfies Γ, and τ(Γ)(a) is defined and equal to A, then M(Γ | γ)(a) ∈ M(Γ | γ)(A).

Proof. The proof is by induction on the structure of preterms.

1. a ≡ s: By Definition 2.4, we have that type(Γ(s)) = A. By Definitions 2.6 and 2.8, we have that M(Γ | γ)(a) = γ(s) and γ(s) ∈ M(Γ | γ)(A).

2. a ≡ (f b): By Definition 2.4, τ(Γ)(f) = [B→A], and τ(Γ)(b) = B, for some B such that τ(Γ)(B) = TYPE. Let M(Γ | γ)(A) be X and M(Γ | γ)(B) be Y, then by Definitions 2.4 and 2.6, and the induction hypothesis, we have M(Γ | γ)(f) ∈ X^{Y} and M(Γ | γ)(b) ∈ Y. It therefore follows by Definition 2.6 that M(Γ | γ)((f b)) = (M(Γ | γ)(f))(M(Γ | γ)(b)), and hence M(Γ | γ)((f b)) ∈ X.

3. a ≡ (λ(x: C): b): By Definition 2.4, we have that τ(Γ)(a) is [C→B], where τ(Γ, x: VAR C)(b) is B. Let X be M(Γ | γ)(C), and Y be M(Γ, x: VAR C | γ{x ← u}))(B). By the induction hypothesis, we have that for any u ∈ Y, M(Γ, x: VAR C | γ{x ← u})(b) ∈ X. Since M(Γ | γ)(a) is {⟨u, v⟩ | u ∈ X, v = M(Γ, x: VAR C | γ{x ← u})(b)}, we have that M(Γ | γ)(a) ∈ X^{Y}.

4. a ≡ (a_{1}, a_{2}): By Definition 2.4, τ(Γ)(a) = [A_{1}, A_{2}], where τ(Γ)(a_{i}) = A_{i} for i ∈ {1, 2}. By the induction hypothesis, M(Γ | γ)(a_{i}) ∈ M(Γ | γ)(A_{i}) for i ∈ {1, 2}. By Definition 2.6, M(Γ | γ)(a) = ⟨M(Γ | γ)(a_{1}), M(Γ | γ)(a_{2})⟩ and hence M(Γ | γ)(a) is an element of M(Γ | γ)(A) which is M(Γ | γ)(A) × M(Γ | γ)(A_{n}).

5. a ≡ p_{i} b: In this case, we know by Definition 2.4 that τ(Γ)(b) = [A_{1}, A_{2}] with i ∈ {1, 2}, and τ(Γ)(a) = A_{i}. By the induction hypothesis, M(Γ | γ)(b) = ⟨t_{1}, t_{2}⟩, and by Definition 2.6, M(Γ | γ)(a) = t_{i} and M(Γ | γ)(τ(Γ)(b)) = M(Γ | γ)(A_{1})×M(Γ | γ)(A_{2}), hence M(Γ | γ)(a) ∈ M(Γ | γ)(A_{i}).

These three theorems (2.11, 2.12, and 2.13) are the key invariants that must be satisfied by the semantics when the language is extended below with type definitions, subtypes, dependent types, and parametric theories.

2.4 Some Syntactic Operations

We first define the operation of collecting the free variables of a term a in a given context Γ as F V (Γ)(a), and then define the operation of substitution.

Definition 2.14 (free variables)

F V (Γ)(s) = \{ \begin{matrix}\{s\}, if kind(Γ(s)) = VARIABLE \\ ∅, otherwise \end{matrix}
F V (Γ)(f a) = F V (Γ)(f) ∪ F V (Γ)(a)
F V (Γ)(λ(x: T): a) = F V (Γ, x: VAR T)(a) − {x}
F V (Γ)((a_{1}, a_{2})) = F V (Γ)(a_{1}) ∪ F V (Γ)(a_{2})
F V (Γ)(p_{i} a) = F V (Γ)(a)

Definition 2.15 (substitution)

s[a_{1}/x_{1}, …, a_{n}/x_{n}] = \{ \begin{matrix}a_{i}, if for some minimal i, s ≡ x_{i} \\ s, otherwise \end{matrix}
(f a)[a_{1}/x_{1}, …, a_{n}/x_{n}] = (f[a_{1}/x_{1}, …, a_{n}/x_{n}]
a[a_{1}/x_{1}, …, a_{n}/x_{n}])
(λ(y: T): a)[a_{1}/x_{1}, …, a_{n}/x_{n}] = (λ(y′: T): a[y′/y, a_{1}/x_{1}, …, a_{n}/x_{n}]),

where y′ is a fresh variable

(b_{1}, b_{2})[a_{1}/x_{1}, …, a_{n}/x_{n}] = (b_{1}[a_{1}/x_{1}, …, a_{n}/x_{n}],

b_{2}[a_{1}/x_{1}, …, a_{n}/x_{n}])

(p_{i} a)[a_{1}/x_{1}, …, a_{n}/x_{n}] = (p_{i} a[a_{1}/x_{1}, …, a_{n}/x_{n}])

Recall that terms are treated as syntactically equivalent modulo alpha conversion. The above definitions must be extended as more features are added to the language.

2.5 Type Definitions

Here we enrich contexts so that type symbols may have definitions. PVS does not allow recursive type definitions^{1} so a type declaration/definition in a context may use only the symbols declared in the prior part of the context. The main difference in the extended language is that type names can have definitions. In such cases, the definitions rather than the type names are used to determine the actual type of an expression. In other words, two type expressions are treated as the same if they are definitionally equivalent. Most other specification languages tend to employ the weaker notion of name equivalence where syntactically different types are treated as distinct even when their definitions coincide.

To accommodate type definitions, a context can contain type declarations of the form s : TYPE = T, where T is a type. If context Γ contains such a declaration for s, then definition(Γ(s)) is T. To extend τ to handle type definitions under definitional equivalence, we must ensure that τ returns the canonical form of a type where all defined types have been replaced by their definitions. The operation δ(Γ)(T) returns the expanded form of a type relative to the context Γ.

Definition 2.16 (expanded type)

δ(Γ)(s) = s, if definition(Γ(s)) is empty
δ(Γ)(s) = δ(Γ)(definition(Γ(s))), if definition(Γ(s)) is nonempty
δ(Γ)([A→B]) = [δ(Γ)(A)→δ(Γ)(B)]
δ(Γ)([T_{1}, T_{2}]) = [δ(Γ)(T_{1}), δ(Γ)(T_{2})]

The typing rules are augmented to return the type in expanded form. The main issue here is to determine that the definition part of a type declaration in a context is well formed relative to the preceding context. We also need to ensure that τ returns the expanded form of the type corresponding to a preterm.

1For the moment, we are not considering the PVS DATATYPE mechanism, which is a form of recursive type definition [OS97]. Recursive datatypes in the context of the HOL proof checking system are described by Melham [Mel89].

Definition 2.17 (type rules with type definitions)

τ()(Γ, s : TYPE = T) = CONTEXT, if Γ(s) is undefined,

τ()(Γ) = CONTEXT, and τ(Γ)(T) = TYPE

τ(Γ)(s) = δ(Γ)(type(Γ(s))),

                        if kind(Γ(s)) ∈ {CONSTANT, VARIABLE}

Note that the δ operator is idempotent, and τ(Γ)(a) for a term a always returns an expanded type, that is, δ(τ(Γ)(a)) = τ(Γ)(a).

We do not need to update the definition of M from Definition 2.6 since the syntax for terms is unchanged, but we do need to revise the notion of a satisfying context assignment (from Definition 2.8) to respect the type definitions.

Definition 2.18 (satisfaction with type definitions) An assignment γ satisfies a context Γ if in addition to the conditions in Definition 2.8, whenever kind(Γ(s)) = TYPE and definition(Γ(s)) (abbreviated as T) is nonempty, then γ(s) = M(Γ | γ)(T).

Theorems 2.11 and 2.12 and 2.13 continue to hold under these extensions, and the proofs are easily adapted to the modified definitions.

Example 2.19 (type definition) Let Ω′ be the context

Ω, boolop: TYPE = [[bool, bool]→bool], ∨: boolop. Then

τ()(Ω′) = CONTEXT

  δ(Ω′)(boolop) = [[bool, bool]→bool],

τ(Ω′)(∨) = [[bool, bool]→bool]

2.6 Summary

We have defined the simply typed fragment of PVS by introducing the syntax for pretypes and preterms, the type rules and semantics for well-formed contexts, types, and terms. The type rules are presented in a novel functional style where each well-formed context is assigned the label CONTEXT, each wellformed type is assigned the label TYPE, and each well-formed term is assigned a canonical type. The semantics takes a satisfying assignment for a context and maps a well-formed type to a set and a well-formed term to an element of the set corresponding to its canonical type. We then defined the syntactic operations of collecting the free variables in an expression and for substituting terms for variables in an expression.

The simple type theory is then extended with type definitions. With this extension, two type expressions are treated as equivalent if they are identical after all type definitions have been expanded. The operation δ returns the expanded form of a given type expression.

Adding Subtypes

Subtyping is one of the main features of the PVS specification language.^{1} Subtyping in PVS corresponds to the set-theoretic notion of a subset. It raises several delicate issues that were absent in the language presented thus far. In the simply typed fragment, each type corresponds to a set of values that is somehow structurally different from the set of values for another type so that a term has at most one type. Subtyping makes it possible to introduce the natural numbers as a subtype of the reals, and to treat the primes, the even numbers, and the odd numbers as subtypes of the natural numbers. With subtyping, a term can obviously have several possible types, but the typechecking function τ may return only a single type. We constrain τ to return a natural canonical type of an expression that is given by the declarations of the symbols in the expression. If the expression is used in a context where the expected type is a supertype of its canonical type, then the type correctness is straightforward. If the expected type is a subtype that is compatible with the canonical type of the expression, then typechecking generates proof obligations asserting that the expression satisfies the predicate constraints imposed by the expected type. Two types are compatible if they have equivalent maximal supertypes. Type equivalence in the presence of subtypes is not a simple notion. Subtyping also introduces the possibility of types being empty. Typed lambda calculi with possibly empty types have been studied by Meyer, Mitchell, Moggi, and Statman [MMMS90]. This chapter introduces predicate subtypes and defines the notions of compatibility and type equivalence prior to presenting the type rules and semantics.

We restrict our attention to contexts Γ that extend the declarations:

 bool : TYPE,

1The form of subtyping used in PVS is derived from a suggestion of Friedrich von Henke.

 TRUE : bool,
 FALSE : bool,
 boolop : [[bool, bool]→bool],
 ¬ : [bool→bool],
 ∨ : boolop,
 ∧ : boolop,
 ⊃ : boolop

We will abuse PVS notation to employ the customary infix forms of operations like ∨, ∧, and ⊃. The pretype corresponding to a predicate subtype has the form {x: T | a} where x is a symbol, T is a pretype, and a is a preterm. A predicate type in PVS is a function type where the range is the primitive type bool. A predicate is a term that has a predicate type. If a is a term of type bool, then we can define the subtype {x: T | a} consisting of those elements e of T satisfying a[e/x] (e substituted for x in a). Since the elements of the subtype {x: T | a} satisfy the predicate λ(x: T): a, we call this type a predicate subtype to distinguish it from other forms of subtyping. Universal quantification ∀(x: T): a is just an abbreviation for the term (λ(x: T): a) = (λ(x: T): TRUE). Although we use the equality predicate in the definition of universal quantification and in the definitions below, the actual introduction of equality is deferred to a later section following the introduction of parametric theories. The equality between PVS terms of function type is to be interpreted as extensional equality. Note that the ‘=’ symbol is used both for the formal equality symbol in the language and for metatheoretic equality.

Our first step will be to define the notion of a maximal supertype of a given type as μ(T). A maximal type T is one such that μ(T) = T. In a given context, we will apply μ only to the expanded form (given by δ) of a type expression.

Definition 3.1 (maximal supertype)

μ(s) = s
μ({x: T | a}) = μ(T)
μ([A→B]) = [A→μ(B)]
μ([A_{1}, A_{2}]) = [μ(A_{1}), μ(A_{2})]

Note that since subtypes correspond to subsets, in taking the maximal supertype of a function type, the domain type is held fixed. In most type theories with subtypes, the rule for subtyping between function types [A→B] and [A′→B′] requires showing that A′ is a subtype of A, and B is a subtype of B′.

Subtyping between function types is therefore said to be contravariant in the domain type and covariant in the range type. Subtyping on function types in PVS is covariant in the range type but is neither covariant nor contravariant in the domain type. This means that the function type [nat→nat] is not a supertype of the function type [int→nat]. Such a subtyping relation would violate extensionality. Two functions on nat are extensionally equal when they return equal values when applied to equal arguments in nat. Consider two functions in [nat→nat]: abs which returns the absolute value, and idnat which behaves as an identity function on natural numbers and returns 0 otherwise. These two functions will be erroneously identified if they can be viewed as being of type [nat→nat], and the subset interpretation of subtypes would be lost.

We will also employ a weaker supertype μ_{0}(T) or the direct supertype, that only considers supertypes of explicitly given subtypes of the form {x: T | a}.

Definition 3.2 (direct supertype)

μ_{0}({x: T | a}) = μ_{0}(T)
μ_{0}(T) = T, otherwise

Example 3.3 (maximal supertype) Given a context containing the declarations

  int: TYPE,
  0: int,
  ≤: [[int, int]→bool],
  nat: TYPE = {i: int | 0 ≤ i}

natinjection: TYPE = {f: [nat→nat] | ∀(i, j: nat): f(i) = f(j) ⊃ i = j}

we have

   μ(natinjection) = μ([nat→nat])

= [nat→μ(nat)]

                   = [nat→int]
  μ_{0}(natinjection) = [nat→nat]

Note that μ(μ(A)) = μ(A). Note also that a maximal supertype is never a subtype. We can in fact collect the predicates that constrain a type A relative to its maximal supertype μ(A) as π(A).

Definition 3.4 (subtype constraints)

π(s) = λ(x: s): TRUE
π({y: T | a}) = λ(x: μ(T)): (π(T)(x) ∧ a[x/y])
π([A→B]) = λ(x: [A→μ(B)]): (∀(y: A): π(B)(x(y)))
π([A_{1}, A_{2}]) = λ(x: [μ(A_{1}), μ(A_{2})]): (π(A_{1})(p_{1} x) ∧ π(A_{2})(p_{2} x))

Observe that in Definition 3.4, if τ(Γ)(A) = TYPE, then τ(Γ)(π(A)) = [μ(A)→bool].^{2}

Example 3.5 (subtype constraints)

  π(nat)

= λ(j: int): 0 ≤ j

  π([nat→nat])

= λ(g: [nat→int]): ∀(i: nat): (λ(j: int): 0 ≤ j)(g(i))

  π(natinjection)

= λ(f: [nat→int]): π([nat→nat])(f) ∧ (∀(i, j: nat): f(i) = f(j) ⊃ i = j)
= λ(f: [nat→int]):

(λ(g: [nat→int]): ∀(i: nat): (λ(j: int): 0 ≤ j)(g(i)))(f)

∧ (∀(i, j: nat): f(i) = f(j) ⊃ i = j)

Observe that π(μ(A)) is essentially equivalent to λ(x: μ(A)): TRUE.

Since the subtype {x: T | p(x) ∧ q(x)} can also be written as {x: T | q(x) ∧ p(x)}, we need a notion of equivalence between types. One way to do this is to make types “first-class” and to allow explicit theorems to be proved about type equivalence and subtyping. Since this would be a fairly drastic extension to the specification language, we have designed the PVS type system so as to avoid any first-class treatment of types. It turns out that all the needed properties about types (such as equality and subtyping) can be obtained by generating ordinary proof obligations rather than by explicitly proving theorems about types.

2This is somewhat tricky in the case of π({y: T | a}) since in a[x/y], x has type μ(T), whereas y has type T. As shown in Chapter 6, the type rules for conjunction are such that τ(Γ, x: VAR μ(T))(π(T)(x) ∧ a) reduces to τ(Γ, x: VAR μ(T))(π(T)(x))

and τ(Γ, x: VAR μ(T), π(T)(x))(a[x/y]) where the first conjunct is added to the context as a contextual assumption. One can then show by induction that τ(Γ, x: VAR μ(T), π(T)(x))(a[x/y]) = τ(Γ, y: VAR T)(a).

We introduce below a metatheoretic operation that generates the proof obligations needed to establish that two (maximal) types are equivalent. This equivalence is denoted by ≃ and is applied only to maximal types and returns a list of the proof obligations that must be proved. Note the invariant in the definition below that the arguments to ≃ are always maximal. The definition of ≃ makes use of the PVS equality predicate that will be introduced later. A list of formulas is represented as a_{1}, …, a_{n}. Given two such lists a_{1}, …, a_{m} and b_{1}, …, b_{n}, the concatenation of these two lists is written as a_{1}, …, a_{m} ; b_{1}, …, b_{n}.

Definition 3.6 (type equivalence proof obligations)

(s ≃ s) = TRUE
([A→B] ≃ [A′→B′]) = ((μ(A) ≃ μ(A′)); (π(A) = π(A′)); (B ≃ B′))^{3}
([A_{1}, A_{2}] ≃ [B_{1}, B_{2}]) = ((A_{1} ≃ B_{1}); (A_{2} ≃ B_{2}))
(A ≃ B) = FALSE, otherwise

Example 3.7 (type equivalence) Building on the context given in Example 3.3, if we have the following variants of nat and natinjection:

NAT: TYPE = {i: int | i ≤ 0 ⊃ i = 0}

NATinjection: TYPE = {f: [NAT→NAT] | ∀(i, j: NAT): f(i) = f(j) ⊃ i = j}

we get

  μ([natinjection→natinjection]) = [natinjection→[nat→int]]
  μ([NATinjection→NATinjection]) = [NATinjection→[NAT→int]]
  μ([natinjection→natinjection]) ≃ μ([NATinjection→NATinjection])

=

        (μ(natinjection) ≃ μ(NATinjection));
        (π(natinjection) = π(NATinjection));
        ([nat→int] ≃ [NAT→int])

3The type correctness of the proof obligation (π(A) = π(A′)) depends on the prior proof obligations μ(A) ≃ μ(A′).

  (π(natinjection) = π(NATinjection))

=

( λ(f: [nat→int]): (λ(g: [nat→int]): ∀(i: nat): 0 ≤ g(i))(f) ∧ (∀(i, j: nat): f(i) = f(j) ⊃ i = j)

=

λ(f: [NAT→int]):

\begin{matrix}& (λ(g: [NAT→int]): ∀(i: NAT): g(i) ≤ 0 ⊃ g(i) = 0)(f) \\ ∧ & (∀(i, j: NAT): f(i) = f(j) ⊃ i = j) \end{matrix} )

  ([nat→int] ≃ [NAT→int])

    = (int ≃ int);

(λ(i: int): 0 ≤ i) = (λ(i: int): i ≤ 0 ⊃ i = 0); (int ≃ int)

A basic question during typechecking is whether two types are compatible, that is, have the same maximal supertype. Two types are said to be compatible if the type equivalence proof obligations on their respective maximal supertypes are provable. The provability of a formula a under context Γ is represented as ⊢_{Γ} a.

Definition 3.8 (compatible) Two types A and B are said to be compatible in context Γ (in notation, (A ∼ B)_{Γ}) if ⊢_{Γ} a, for each a in (μ(A) ≃ μ(B)).^{4}

We now extend the definition of δ to the case of subtypes so that it leaves the predicate unchanged but expands the definition of the supertype.

Definition 3.9 (expanded type with subtypes)

δ(Γ)({x: T | a}) = {x: δ(Γ)(T) | a}

We now extend the definition τ to the case of subtypes. Here we could force τ to always return a maximal supertype but this is not done in Definition 3.10 since it would weaken the soundness theorem without significantly simplifying the definition of the type rules. The typechecking of contexts has to be modified to generate a nonemptiness proof obligation for the type of any constant declaration. A constant of an empty type would lead to an inconsistent context, and this would mean that constant declarations are not conservative extensions. This modification to Definition 2.4 is not needed for soundness since an inconsistent context makes soundness trivial. It is needed to show that constant declarations and definitions are conservative extensions. Note that with subtypes, the type rule for an application is modified to check that the domain type of the function is compatible with the type of its argument, and that the argument satisfies any constraints imposed by the domain type of the function. The case of projection expressions is also not straightforward since the argument type can be a subtype of a tuple type. In this case, we use the direct supertype (see Definition 3.2) which must be a tuple type.

4The PVS proof rules are described in Chapter 7.

Definition 3.10 (type rules with subtypes)

τ()(Γ, c: T) = CONTEXT, if Γ(c) is undefined,

τ(Γ)(T) = TYPE,

τ()(Γ) = CONTEXT, and ⊢_{Γ} (∃(x: T): TRUE)

τ(Γ)({x: T | a}) = TYPE, if Γ(x) is undefined,

τ(Γ)(T) = TYPE, and τ(Γ, x: VAR T)(a) = bool

τ(Γ)(f a) = B, where μ_{0}(τ(Γ)(f)) = [A→B],

τ(Γ)(a) = A′, (A ∼ A′)_{Γ}, ⊢_{Γ} π(A)(a)

τ(Γ)(p_{i} a) = A_{i}, where μ_{0}(τ(Γ)(a)) = [A_{1}, A_{2}]

Example 3.11 (typechecking subtypes) Let Γ contain the above declara-

tions of int, nat, 0, ≤, and natinjection.

τ(Γ)({i: int | 0 ≤ i})

    = TYPE

τ(Γ)((λ(f: natinjection): f(0))(λ(i: nat): i))

= δ(Γ)(nat), if

       (natinjection ∼ [nat→nat])_{Γ},

⊢_{Γ} ∀(j, k: nat): (λ(i: nat): i)(j) = (λ(i: nat): i)(k) ⊃ j = k, (int ∼ nat)_{Γ}, and ⊢_{Γ} 0 ≤ 0

Only one additional clause to Definition 2.6 is needed to capture the semantics of predicate subtypes.

Definition 3.12 (meaning function with subtypes)

M(Γ | γ)({x: T | a})

= {y ∈ M(Γ | γ)(T) | M(Γ, x: VAR T | γ{x ← y})(a) = 1}

Example 3.13 (semantics of predicate subtypes) If we assign the usual truth table interpretation to the Boolean function ⊃:

M(Γ | γ)({f: [bool→bool] | ∀(x: bool): x ⊃ f(x)})

= {{⟨0, 0⟩, ⟨1, 1⟩}, {⟨0, 1⟩, ⟨1, 1⟩}}.

The following useful propositions are easily proved from the definitions given above. Proposition 3.14 asserts that the maximal supertype of a type is well typed. Proposition 3.15 asserts that the denotation of a type is a subset of the denotation of its maximal supertype. Proposition 3.16 asserts that if all the proof obligations in (A ≃ A′) are valid relative to a given assignment γ for context Γ, then the denotations of A and A′ under γ are equal.

Proposition 3.14 If τ()(Γ) = CONTEXT and τ(Γ)(A) = TYPE, then τ(Γ)(μ(A)) = TYPE.

Proposition 3.15 If τ()(Γ) = CONTEXT, τ(Γ)(A) = TYPE, and γ satisfies Γ, then

1. M(Γ | γ)(A) ⊆ M(Γ | γ)(μ(A)) and

2. M(Γ | γ)(A) ⊆ M(Γ | γ)(μ_{0}(A)).

Proposition 3.16 If A and A′ are maximal types in context Γ, i.e.,

1. τ()(Γ) = CONTEXT,

2. τ(Γ)(A) = τ(Γ)(A′) = TYPE,

3. μ(A) = A and μ(A′) = A′

and for each a in (A ≃ A′), 1. a ≡ TRUE, or

2. a ≡ (a_{1} = a_{2}) and M(Γ | γ)(a_{1}) = M(Γ | γ)(a_{2}) holds,

then M(Γ | γ)(A) = M(Γ | γ)(A′).^{5}

Proposition 3.17 If τ()(Γ) = CONTEXT and τ(Γ)(T) = TYPE, then M(Γ | γ)(T) = M(Γ | γ)({x: μ(T) | π(T)(x)}).

We can now examine the updated forms of the invariants given by Theorems 2.11, 2.12, and 2.13. The proof of Theorem 2.11 remains straightforward. The statement of Theorem 2.13 must now be strengthened to include soundness, that is, if ⊢_{Γ} a and γ satisfies Γ, then M(Γ | γ)(a) = 1. For now, we assume soundness (Theorem 7.2) since we have not yet presented the proof rules.

Theorem 3.18 (type soundness) If τ()(Γ) = CONTEXT, γ satisfies Γ, and τ(Γ)(A) = TYPE then M(Γ | γ)(A) ∈ U.

Proof. There is only one new case to add to the induction proof of Theorem 2.12, namely, when A ≡ {x: T | a}. In this case, by Definition 3.10, τ(Γ)(T) = TYPE, so by the induction hypothesis, M(Γ | γ)(T) ∈ U. Since, by Definition 3.12, M(Γ | γ)(A) ⊆ M(Γ | γ)(T), we have M(Γ | γ)(A) ∈ U by Definition 1.1.

Theorem 3.19 (term soundness) If τ()(Γ) = CONTEXT, γ satisfies Γ, and τ(Γ)(a) = A then M(Γ | γ)(a) ∈ M(Γ | γ)(A).

Proof. There are two affected cases in the proof from that of Theorem 2.13, namely, those of application and projection. The case of projection expressions is straightforward given Proposition 3.15.

When a ≡ (f b), by Definition 3.10, we have that τ(Γ)(f) = [B→A] and τ(Γ)(b) = B′. Let X be M(Γ | γ)(B), X′ be M(Γ | γ)(B′), and Y be M(Γ | γ)(A). Then by Definition 2.6, M(Γ | γ)([B→A]) = Y^{X}. By the induction hypotheses, M(Γ | γ)(f) ∈ Y^{X} and M(Γ | γ)(b) ∈ X′. By Definition 3.10, soundness of the proof rules (Theorem 7.2), and Propositions 3.15 and 3.16, there is a maximal supertype μ(B) of both B and B′ such that X and X′ are both subsets of M(Γ | γ)(μ(B)). Since, by Definition 3.10, ⊢_{Γ} π(B)(b), and by Proposition 3.17, M(Γ | γ)(B) = M(Γ | γ)({x: μ(B) | π(B)(x)}), we have M(Γ | γ)(b) ∈ M(Γ | γ)(B), and hence by Definition 2.6, M(Γ | γ)((f b)) ∈ M(Γ | γ)(A).

5We remind the reader that the formulas a in (A ≃ A′) are equalities, but we have not yet formally introduced equality into the language.

3.1 Summary

PVS features a form of subtyping where it is possible to form the subtype of a type satisfying a given predicate on the type. This kind of subtyping introduces several delicate semantic issues into PVS. A term can now have several types since, for example, the term corresponding to the number 2 can be a prime number, an even number, a natural number, an integer, a rational number, or a real number. When the expected type is a subtype, the canonical type of the actual term must be compatible with the expected type, that is, the two maximal supertypes must be equivalent and the actual term must satisfy any subtype constraints imposed by the expected type. We have defined the notions of maximal supertype, subtype constraints, type equivalence, and compatibility. These notions are used to define the type rules and semantics of the simply typed fragment of PVS extended with subtypes. Note that both type equivalence (and hence, compatibility) and type correctness are undecidable. Proof obligations generated during typechecking are the only source of such undecidability. The modularization of the type system into a decidable part consisting of the simply typed fragment, and the proof obligations generated by subtyping, is perhaps the most significant design consideration in the PVS language.

Dependent Types

The PVS language fragment described thus far is already quite expressive. It employs definitional equivalence between types and contains predicate subtypes. It is undecidable whether an expression in this fragment is type-correct because of the proof obligations that arise with respect to predicate subtypes and type equivalence. The next step is the addition of type dependencies between the components of a type. This extension considerably enhances the utility of this type system. It is also a natural extension given predicate subtyping which already allows types that depend on free variables in the predicates. With dependent typing, we can make the type of one component of a product depend on the value of another component, or the type of the range of a function vary according to its argument value.

A dependent product type is written as [x: A, B]. A dependent function type is written as [x: A→B]. Any product or function type can be transformed into a dependent type by inserting dummy type bindings. Conversely, any dummy type bindings that do not actually bind any variable occurrences can be removed. The type rules and semantics below will assume that all product and function types are presented as dependent types.

Example 4.1 (dependent types)

[i: nat, {j: nat | j ≤ i}],
[i: nat, [{j: nat | j ≤ i}→bool]],
[i: int→{j: int | i ≤ j}].

Before we treat dependent types, we update the definitions of the set of free variables and substitution to account for the fact that with subtyping and dependent typing, both free and bound variables can occur in terms and types. This is needed for the next step where we try to remove type dependencies by substituting a term into a dependent type.

Definition 4.2 (free variables for types)

F V (Γ)([x: A→B]) = F V (Γ)(A) ∪ (F V (Γ, x: VAR A)(B) − {x})
F V (Γ)([x: A, B]) = F V (Γ)(A) ∪ (F V (Γ, x: VAR A)(B) − {x})
F V (Γ)({x: A | a}) = F V (Γ)(A) ∪ (F V (Γ, x: VAR A)(a) − {x})

Definition 4.3 (substitution for types)

[x: A→B][a_{1}/x_{1}, …, a_{n}/x_{n}]

= [y: A[a_{1}/x_{1}, …, a_{n}/x_{n}]→B[y/x, a_{1}/x_{n}, …, a_{n}/x_{n}]]

[x: A, B][a_{1}/x_{1}, …, a_{n}/x_{n}]

= [y: A[a_{1}/x_{1}, …, a_{n}/x_{n}], B[y/x, a_{1}/x_{1}, …, a_{n}/x_{n}]]

{x: A | a}[a_{1}/x_{n}, …, a_{n}/x_{n}]

= {y: A[a_{1}/x_{1}, …, a_{n}/x_{n}] | a[y/x, a_{1}/x_{n}, …, a_{n}/x_{n}]}

where y is a fresh variable.

The definition of μ has to be modified slightly for dependent types. The definition is first extended to type bindings, μ(x: T) = x: μ(T). The definition for the case of dependent function types is unchanged so that μ([x: A→B]) = [x: A→μ(B)]. The definition for the product case is more delicate since the definition μ([x: A, B]) = [x: μ(A), μ(B)] results in a loss of type information regarding the occurrences of x in B.^{1} To ensure that type information regarding x is retained, we define a new operation T \a which constrains the subtype assertions in type T with an additional assertion a.

Definition 4.4 (Adding subtype constraints)

s\a = s
{x: T |b}\a = {x: T |a ∧ b}
[A→B]\a = [A\a→B\a]
[A, B]\a = [A\a, B\a]

1Doug Howe brought this problem to our attention.

We can now define the maximal supertype operation for dependent tuple types.

Definition 4.5 (Maximal supertype for dependent product types)

μ([x: A, B]) = [x: μ(A), B\π(A)(x)]

The definition of π for a dependent function type [y: A→B] is slightly different from that of an ordinary function type since π(B) can contain free occurrences of the variable y. For example, π([i: int→{j: int | i ≤ j}]) must be λ(f: [i: int→int]): (∀(i: int): i ≤ f(i)). The definition for dependent tuples remains essentially unchanged from that of ordinary products.

Definition 4.6 (constraint predicates for dependent types)

π([y: A→B]) = (λ(x: [y: A→μ(B)]): (∀(y: A): π(B)(x(y))))
π([y: A, B]) = (λ(x: [y: μ(A), μ(B)\π(A)(y)]):
π(A)(p_{1} x) ∧ π(B)(p_{2} x)[(p_{1} x)/y])

Example 4.7 (dependent type predicates)

μ([i: int→{j: int | i ≤ j}]) = [i: int→int]
π([i: int→{j: int | i ≤ j}]) = λ(f: [i: int→int]):
∀(i: int): (λ(j: int): i ≤ j)(f(i))

The definition of ≃ must also be massaged slightly for dependent types. Recall that ≃ checks whether two maximal types are equivalent by generating proof obligations as needed. This is the basic operation for checking whether the expected type of an expression is compatible with its actual type. The subtlety now is that the expected type might be a dependent type where the actual type is not. Consider the case of the pair ⟨5, (λ(x: {j: nat | j ≤ 5}): x)⟩ whose type would be computed by τ as [i: nat, [{j: nat | j ≤ 5}→{j: nat | j ≤ 5}]] where the expected type might be [i: nat, [{j: nat | j ≤ i}→{j: nat | j ≤ i}]]. To cope with this, we will allow the option of two maximal types, say A and B, to be compared using ≃ in the context of an expression a. This is indicated by the notation (A ≃ B)/a. Note that (A ≃ B)/a is sensible only when A and B are maximal types. The missing cases in Definition 3.6 are included in Definition 4.8. For a list of formulas a_{1}, …, a_{n}, let (∀(x: T): a_{1}, …, a_{n}) represent the list (∀(x: T): a_{1}), …, (∀(x: T): a_{n}).^{2}

Definition 4.8 (type equivalence for dependent types)

(s ≃ s)/a = TRUE
([x: A→B] ≃ [x′: A′→B′]) = (μ(A) ≃ μ(A′));
(π(A) = π(A′));
(∀(x: A): (B ≃ B′[x/x′]))
([x: A→B] ≃ [x′: A′→B′])/a = (μ(A) ≃ μ(A′));
(π(A) = π(A′));
(∀(x: A): (B ≃ B′[x/x′])/a(x))
([x: A_{1}, A_{2}] ≃ [y: B_{1}, B_{2}]) = (A_{1} ≃ B_{1});
(∀(x: A_{1}): (A_{2} ≃ B_{2}[x/y]))
([x: A_{1}, A_{2}] ≃ [y: B_{1}, B_{2}])/a = (A_{1} ≃ B_{1})/(p_{1} a);
(A_{2}[(p_{1} a)/x] ≃ B_{2}[(p_{1} a)/y])/(p_{2} a)
(A ≃ B)/a = FALSE, otherwise.

As with (A ∼ B)_{Γ}, the notation (A ∼^{a} B)_{Γ} indicates that all the proof obligations a′ in (μ(A) ≃ μ(B))/a are provable, that is, ⊢_{Γ} a′.

With dependent types, the type rules must be modified so as to augment the context suitably to account for any dependencies. We will give the definitions only for dependent type constructions.

Definition 4.9 (type rules with dependent types)

τ(Γ)([x: A, B]) = TYPE, if Γ(x) is undefined,

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

τ(Γ)([x: A→B]) = TYPE, if Γ(x) is undefined,

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

2Note that the type-correctness of the proof obligation (π(A) = π(A′)) in Definition 4.8 depends on the prior proof obligations μ(A) ≃ μ(A′).

τ(Γ)(f a) = B′, where μ_{0}(τ(Γ)(f)) = [x: A→B],

τ(Γ)(a) = A′,

(A ∼^{a} A′)_{Γ},

B′ is B[a/x], ⊢_{Γ} π(A)(a)

τ(Γ)(λ(x: A): a) = [x: A→B], where

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

τ(Γ)(p_{1} a) = A_{1}, where μ_{0}(τ(Γ)(a)) = [x: A_{1}, A_{2}]
τ(Γ)(p_{2} a) = A_{2}[(p_{1} a)/x], where μ_{0}(τ(Γ)(a)) = [x: A_{1}, A_{2}]

Example 4.10 (dependent typing)

τ(Γ)([x: bool, {y: bool | x ⊃ y}]) = TYPE
τ(Γ)([x: bool→{y: bool | x ⊃ y}]) = TYPE

Before we can assign meanings to dependent types, we must augment our definition of the universe U to contain sets corresponding to these constructions. If F is a function with domain set X and a range Y, which is a set of sets, we can define ΣF to be the set {⟨x, y⟩ | x ∈ dom(F), y ∈ F (x)} and ΠF to be the set {f | (∀x ∈ dom(F): f(x) ∈ F (x))}. Note that ΠF ⊆ ⋃_{X∈ΣF} ℘(X) but we include ΠF in the universe U defined below for simplicity. We can drop X ×Y and X^{Y} from the universe definition since X × Y can be obtained from ΣF by defining an F with domain X that always returns Y, and similarly, X^{Y} can be obtained by ΠF where F is defined to with domain Y to always return X. The universe U can then be redefined as below.

Definition 4.11 (type universe with dependent types)

U_{0} = {2, R}
U_{i+1} = U_{i}

∪ ⋃_{X∈U_{i}} ℘(X)

∪ {ΣF | F ∈ W_{i}}

∪ {ΠF | F ∈ W_{i}}
W_{i} = ⋃_{X∈U_{i}} U_{i}^{X}
U_{ω} = ⋃_{i∈ω} U_{i}
U = U_{ω}

One very important consequence of the above extension of the universe is that all type dependencies must be bounded in the sense that if B is a type expression with a single free variable x of type A, then it must be the case that for any set [[A]] representing A, there is a bound n such that for any z in [[A]], the meaning of B under {x ← z} must be in U_{n}. This property is easily proved by induction on the structure of a PVS type since the parameter x can appear only in the predicate part of a subtype where the rank of the meaning of the resulting type cannot vary with the value of x. In particular, there is no way to define a type constructor T^{n} in PVS that returns the n-tuple [\underbrace{T, […, T]}_{n}]

for a given n since this would entail an unbounded dependency. If unbounded type dependencies were allowed in PVS, one can construct a dependent type such as [n: nat→T^{n}] whose representation is not in U as defined above.

The meaning function for dependent types is obtained by adding the cases corresponding to dependent product and function types. All the other cases are unchanged from Definition 3.12. Note that the semantic definition for dependent types is equivalent to the nondependent one when there are no dependencies.

Definition 4.12 (meaning function with dependent types)

M(Γ | γ)([x: A, B]) = ΣF, where
F maps z ∈ M(Γ | γ)(A) to
M(Γ, x: VAR A | γ{x ← z})(B)
M(Γ | γ)([x: A→B]) = ΠF, where
F maps z ∈ M(Γ | γ)(A) to
M(Γ, x: VAR A | γ{x ← z})(B)

Example 4.13 (meaning function with dependent types)

M(Γ | γ)([x: bool, {y: bool | x ⊃ y}]) = {⟨0, 0⟩, ⟨0, 1⟩, ⟨1, 1⟩}
M(Γ | γ)([x: bool→{y: bool | x ⊃ y}]) = {{⟨0, 0⟩, ⟨1, 1⟩},
{⟨0, 1⟩, ⟨1, 1⟩}}

We now need to show that the extensions corresponding to dependent types preserve the properties in Theorems 3.18 and 3.19, namely, M(Γ | γ)(T) ∈ U and M(Γ | γ)(a) ∈ M(Γ | γ)(τ(Γ)(a)). For the former, we prove a stronger theorem that incorporates the rank-boundedness of dependent types.

Theorem 4.14 (rank bounded type semantics) If B is a pretype, x_{1}, …, x_{n} is a list of symbols, A_{1}, …, A_{n} is a list of pretypes such that

1. τ()(Γ, x_{1}: VAR A_{1}, …, x_{n}: VAR A_{n}) = CONTEXT,

2. τ(Γ, x_{1}: VAR A_{1}, …, x_{n}: VAR A_{n})(B) = TYPE, and

3. γ is an assignment satisfying Γ,

then there is an i such that for any list of values z_{1}, …, z_{n} where γ{x_{1} ← z_{1}} … {x_{n} ← z_{n}} is a satisfying assignment for Γ, x_{1}: VAR A_{1}, …, x_{n}: VAR A_{n}, we have

M(Γ, x_{1}: VAR A_{1}, …, x_{n}: VAR A_{n} | γ{x_{1} ← z_{1}} … {x_{n} ← z_{n}})(B) ∈ U_{i}.

Proof. The proof is by structural induction on the pretype B. Let Γ′ denote Γ, x_{1}: VAR A_{1}, …, x_{n}: VAR A_{n}, γ′ denote γ{x_{1} ← z_{1}} … {x_{n} ← z_{n}}, and [[C]] denote M(Γ′ | γ′)(C).

1. B ≡ s: Since [[B]] is just γ(B) by Definition 2.6, we have that there is an i such that [[B]] ∈ U_{i} regardless of the choice of values z_{1}, …, z_{n}.

2. B ≡ {y: T | a}: By the induction hypothesis, we know that for some j, it is always the case that [[T]] ∈ U_{j}. By Definition 3.12, we have that [[B]] ⊆ [[T]] so if we let i = j + 1, then by Definition 4.11, it is always the case that [[B]] ∈ U_{i}.

3. B ≡ [y: C→D]: By Definition 4.9, Γ′(y) is undefined, τ(Γ′)(C) = TYPE, τ()(Γ′, y: VAR C) = CONTEXT, and τ(Γ′, y: VAR C)(D) = TYPE. By the induction hypothesis, for some j, it is always the case that M(Γ′ | γ′)(C) ∈ U_{j}, and for some k, it is always the case that for any satisfying assignment γ′{y ← w} for Γ′, y: VAR C, we have M(Γ′, y: VAR C | γ′{y ← w})(D) ∈ U_{k}. Then the function F mapping w in M(Γ′)(C) to M(Γ′, y: VAR C | γ′{y ← w})(D) is an element of W_{j+k}. Letting i be j + k + 1, we have by Definition 4.12 that M(Γ′ | γ′)(B) is ΠF and is hence an element of U_{i} by Definition 4.11.

4. B ≡ [y: C, D]: Similar to the previous case.

By choosing n to be 0, the previous theorem yields the result that when τ(Γ)(B) = TYPE, M(Γ | γ)(B) ∈ U.

We next need to establish that for any preterm a, if τ(Γ)(a) = A, then M(Γ | γ)(a) ∈ M(Γ | γ)(A). The first step in this direction is the proof of the substitution lemma below.

Proposition 4.15 If τ()(Γ) = τ()(Γ′) = CONTEXT where for each s, Γ(s) is defined if and only if Γ′(s) is defined, and γ is an assignment satisfying both Γ and Γ′, then

1. If Γ(s) = Γ′(s) (i.e., they are equal when either Γ(s) or Γ′(s) is defined), then

(a) τ(Γ)(a) = τ(Γ′)(a), for any preterm a.

(b) τ(Γ)(A) = τ(Γ′)(A), for any pretype A.

2. M(Γ | γ)(A) = M(Γ′ | γ)(A), when τ(Γ)(A) = TYPE.

3. M(Γ | γ)(a) = M(Γ′ | γ)(a), for any preterm a such that τ(Γ)(a) is defined.

Lemma 4.16 (substitution lemma) If τ()(Γ, x: VAR A) = CONTEXT, τ(Γ)(a) = A, then

1. If τ(Γ, x: VAR A)(b) = B, then M(Γ | γ)(b[a/x]) = M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a)})(b).

2. If τ(Γ, x: VAR A)(C) = TYPE, then M(Γ | γ)(C[a/x]) = M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a)})(C).

Proof. The proof is by simultaneous structural induction on the preterm b and the pretype C. The following cases deal with the preterm b.

1. b ≡ s: If s ≡ x, then by Definition 4.12, the left-hand side M(Γ | γ)(b[a/x]) is M(Γ | γ)(a), and the right-hand side M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a)})(b) is also M(Γ | γ)(a).

If s ≢ x, then by Definition 4.12, the left-hand side and the right-hand side are both equal to γ(s).

2. b ≡ (λ(y: C): d): Since C can contain free occurrences of x, we have by the induction hypothesis that M(Γ | γ)(C[a/x]) = M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a)})(C). Also, M(Γ | γ)((λ(y: C): d)[a/x]) is equal to the set of ordered pairs ⟨v, z⟩ such that v ∈ M(Γ | γ)(C[a/x]) and z = M(Γ, y: VAR C[a/x] | γ{y ← v})(d[a/x]).

By the induction hypothesis, M(Γ, y: VAR C[a/x] | γ{y ← v})(d[a/x]) = M(Γ, y: VAR C[a/x], x: VAR A | γ{y ← v}{x ← M(Γ | γ)(a)})(d). Since x does not occur free in C[a/x], by Proposition 4.15 we can exchange the occurrences of y and x so that M(Γ, y: VAR C[a/x], x: VAR A | γ{y ← v}{x ← M(Γ | γ)(a)})(d) = M(Γ, x: VAR A, y: VAR C[a/x] | γ{x ← M(Γ | γ)(a)}{y ← v})(d).

By Definition 4.12, the right-hand side is the set of ordered pairs of the form ⟨v, z⟩ such that v ∈ M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a)})(C) and z = M(Γ, x: VAR A, y: VAR C | γ{x ← M(Γ | γ)(a)}{y ← v})(d). By Proposition 4.15 and the induction hypothesis, we know that M(Γ, x: VAR A, y: VAR C | γ{x ← M(Γ | γ)(a)}{y ← v})(d) = M(Γ, x: VAR A, y: VAR C[a/x] | γ{x ← M(Γ | γ)(a)}{y ← v})(d), and hence it follows that the two sets of ordered pairs are equal.

3. b ≡ (f c): In this case, b[a/x] ≡ (f[a/x] c[a/x]) and the conclusion follows easily from the induction hypothesis and Definition 4.12.

4. b ≡ (b_{1}, b_{2}): The conclusion follows easily from Definitions 2.15, 4.12, and the induction hypotheses.

5. b ≡ (p_{i} c): This case is also straightforward since b[a/x] ≡ (p_{i} c[a/x]), and by the induction hypothesis, M(Γ, x: VAR a | γ{x ← M(Γ | γ)(a)})(c) = M(Γ | γ)(c[a/x]).

The remaining cases deal with the pretype C.

1. C ≡ s: This case is trivial since by Definition 2.15, C[a/x] ≡ C and the left-hand and right-hand sides both reduce to γ(C).

2. C ≡ {y: T | d}: The argument here follows along the lines of the b ≡ (λ(x: C): D) case above. By the induction hypotheses, we know that

M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a)})(T)

= M(Γ | γ)(T [a/x])

M(Γ, y: VAR T [a/x], x: VAR A | γ{y ← z}{x ← M(Γ | γ)(a)})(d)

= M(Γ, y: VAR T [a/x] | γ{y ← z})(d[a/x]),
for any z ∈ M(Γ | γ)(T [a/x])

The conclusion follows from Proposition 4.15 and Definition 4.12.

3. C ≡ [y: C_{1}→C_{2}]: The argument here is similar to that of the previous case. Essentially, by the induction hypothesis and Proposition 4.15, the function mapping z ∈ M(Γ, x: VAR A | γ{x ← M(Γ | γ)(a))(C_{1}) to M(Γ, y: VAR C_{1}[a/x], x: VAR A | γ{y ← z}{x ← M(Γ | γ)(a)})(C_{2}) is the same as the function mapping z ∈ M(Γ | γ)(C_{1}[a/x]) to M(Γ, y: VAR C_{1}[a/x] | γ{y ← z})(C_{2}[a/x]).

4. C ≡ [y: C_{1}, C_{2}]: Similar to the previous case.

Proposition 4.17 is stated below without proof. It asserts the semantic equivalence with respect to term a of types A and B when (A ∼^{a} B)_{Γ} holds. Note that its correctness depends on the soundness of the proof rules.

Proposition 4.17 If τ()(Γ) = CONTEXT, a is a preterm such that τ(Γ)(a) = B, and (A ∼^{a} B)_{Γ}, then M(Γ | γ)(a) ∈ M(Γ | γ)(A) iff M(Γ | γ)(a) ∈ M(Γ | γ)(B).

Theorem 4.18 If τ()(Γ) = CONTEXT, γ is an assignment satisfying Γ, and a is a preterm such that τ(Γ)(a) = A, then M(Γ | γ)(a) ∈ M(Γ | γ)(A).

Proof. The proof is by induction on the structure of the preterm a.

1. a ≡ s: Then by Definition 4.12, M(Γ | γ)(a) = γ(a), and by Definition 2.8, we have that γ(a) ∈ M(Γ | γ)(A).

2. a ≡ (λ(x: C): b): By Definition 4.9, we have τ(Γ)(a) = A = [x: C→τ(Γ, x: VAR C)(b)]. Let B label τ(Γ, x: VAR C)(b). We know that M(Γ | γ)(A) is of the form ΠF where F maps z ∈ M(Γ | γ)(C) to M(Γ, x: VAR C | γ{x ← z})(B).

By the induction hypothesis on b, we know that for any z ∈ M(Γ | γ)(C), M(Γ, x: VAR C | γ{x ← z})(b) ∈ M(Γ, x: VAR C | γ{x ← z})(B). Since by Definition 4.12, M(Γ | γ)(a) is a function mapping z ∈ M(Γ | γ)(C) to M(Γ, x: VAR C | γ{x ← z})(b), we have M(Γ | γ)(a) ∈ ΠF by the definition of Π.

3. a ≡ (f b): By Definition 4.9, we have that τ(Γ)(f) = [x: B→A′], τ(Γ)(b) = B′, (B ∼^{a} B′)_{Γ}, A ≡ A′[a/x], and ⊢_{Γ} π(B)(b). We know by the induction hypothesis that M(Γ | γ)(f) ∈ M(Γ | γ)([x: B→A′]) and M(Γ | γ)(b) ∈ M(Γ | γ)(B′). By Propositions 4.17 and 3.17, M(Γ | γ)(b) ∈ M(Γ | γ)(μ(B)). We therefore have by Proposition 3.17 that M(Γ | γ)(b) ∈ M(Γ | γ)(B). By Definition 4.12, M(Γ | γ)(a) ∈ M(Γ, x: VAR B | γ{x ← M(Γ | γ)(b)})(A′), and hence by Lemma 4.16 it follows that M(Γ | γ)(a) ∈ M(Γ | γ)(A′[b/x]).

4. a ≡ (a_{1}, a_{2}): The conclusion follows easily from the induction hypothesis and Definition 4.9.

5. a ≡ (p_{i} b): The conclusion follows easily from Proposition 3.17, the induction hypothesis, and Definition 4.9. The (p_{2} b) case also employs Lemma 4.16.

4.1 Summary

Dependent typing is a significant enhancement to PVS since it adds an important degree of flexibility and precision to the type system. Notions such as subtype constraints and type equivalence that were introduced for subtyping can be extended for the case of dependent types. The semantic universe must be extended to include additional sets to accommodate the semantics of dependent types. The rank-boundedness of type dependencies is crucial in demonstrating that dependent types can be interpreted in this extended semantic universe.

Theories and Parametric Theories

The next extension of the PVS language introduces theories and parametric theories. The theory construct of PVS provides a way of packaging together a related collection of declarations. Theories can be parametric in individual or type parameters. Thus, PVS permits polymorphism or type parametricity only at the theory level rather than at the declaration level as in HOL [GM93]. We first consider PVS theories without parameters. The main change now is that contexts are no longer simple and can contain theory declarations as well. A theory declaration has the form m: THEORY = Δ, where Δ is a simple context with no variable or theory declarations. If Γ(m) is the declaration m: THEORY = Δ, then kind(Γ(m)) = THEORY, and definition(Γ(m)) = Δ. Correspondingly, constants and type names are no longer just symbols but can be compound names of the form m.s where m is a symbol naming a theory and s is a symbol corresponding to the constant or type name.

5.1 Theories without Parameters

To define the type rules for theories, we first modify the definition of τ for simple contexts so that the context argument is not always empty. Here Δ; Γ represents the concatenation of contexts.

Definition 5.1 (type rules for contexts)

τ(Θ)({}) = CONTEXT
τ(Θ)(Γ, s : TYPE = T) = CONTEXT, if Γ(s) and Θ(s) are undefined,

τ(Θ)(Γ) = CONTEXT, and

τ(Θ; Γ)(T) = TYPE

τ(Θ)(Γ, c: T) = CONTEXT, if Γ(c) and Θ(c) are undefined,

τ(Θ)(Γ) = CONTEXT, and τ(Θ; Γ)(T) = TYPE

τ(Θ)(Γ, x: VAR T) = CONTEXT, if Γ(x) and Θ(x) are undefined,

τ(Θ)(Γ) = CONTEXT, and τ(Θ; Γ)(T) = TYPE

Example 5.2 (type rules for contexts)

  τ(Ω)(real: TYPE, 0: real, ≤: [[real, real]→bool]) = CONTEXT

The following rule handles theory declarations.

Definition 5.3 (type rule for contexts with theory declarations)

τ(Θ)(Γ, m: THEORY = Δ) = CONTEXT if Θ(m), Γ(m) are undefined

Δ only has constant and type declarations, τ(Θ; Γ)(Δ) = CONTEXT, τ(Θ)(Γ) = CONTEXT

Example 5.4 (contexts with theory declarations)

  τ(Ω)(reals: THEORY = (real: TYPE, 0: real, ≤: [[real, real]→bool]))

    = CONTEXT

Any reference to a type name or a constant s declared in a theory m outside of this theory must be prefixed by the theory name, as in m.s. Note that references to a type name or constant that is declared in the same theory should not be given a theory prefix. Before we can give the type rules, we must update the definition of the type expansion operation δ to prefix symbols with their theory names. Let Γ(m)(s) abbreviate definition(Γ(m))(s), which is the declaration of the symbol s in the definition of the theory m. Let η(Γ, m)(a) be the result of prefixing every unprefixed type or constant symbol in a by m, where a is either an individual or type expression. We omit the definition of η since it is straightforward.

We modify the definition of δ in Definition 2.16 with the following clauses.

Definition 5.5 (expanded type for prefixed symbols)

δ(Γ)(m.s) = δ(Γ)(η(Γ, m)(definition(Γ(m)(s)))), if

definition(Γ(m)(s)) is nonempty.

δ(Γ)(m.s) = m.s if definition(Γ(m)(s)) is empty.

Example 5.6 (expanded type for prefixed symbols) Let Ω′′ be the context

     Ω, reals: THEORY = (real: TYPE, 0: real, ≤: [[real, real]→bool], nonneg real: TYPE = {x: real | ≤ (0, x)}, 1: nonneg real)

   δ(Ω′′)(reals.nonneg real) = {x: reals.real | reals.≤ (reals.0, x)}

The type rules for prefixed symbols are given below.

Definition 5.7 (type rules for prefixed symbols)

τ(Γ)(m.s) = TYPE, if kind(Γ(m)) = THEORY and

kind(Γ(m)(s)) = TYPE

τ(Γ)(m.s) = δ(Γ)(η(Γ, m)(type(Γ(m)(s)))),

if kind(Γ(m)) = THEORY and kind(Γ(m)(s)) = CONSTANT Example 5.8 (type rules for prefixed symbols)

  τ(Ω′′)(reals.nonneg real) = TYPE
            τ(Ω′′)(reals.1) = {x: reals.real | reals.≤ (reals.0, x)}

The operations π, and μ remain unchanged. An assignment γ now maps a theory name m to an assignment γ(m).

Definition 5.9 (meaning function for prefixed symbols)

M(Γ | γ)(m.s) = γ(m)(s)

Example 5.10 (meaning function for prefixed symbols) Let ω′′ be a satisfying assignment for Ω′′ of the form

… {reals ← {real ← R}{0 ← 0} …} ….

M(Ω′′ | ω′′)(reals.real) = R
M(Ω′′ | ω′′)(reals.0) = 0

Definition 5.11 (satisfaction for contexts with theories) An assignment γ satisfies a context Γ if in addition to the constraints stated in Definition 2.18, γ maps every theory m declared in Γ to a satisfying assignment for the body of the theory given by definition(Γ(m)), that is for each declared symbol s in m:

1. If kind(Γ(m)(s)) = TYPE, then γ(m)(s) ∈ U.

2. If kind(Γ(m)(s)) = CONSTANT, then γ(m)(s) ∈ M(Γ | γ)(τ(Γ)(m.s)).

3. If definition(Γ(m)(s)) is nonempty, then

γ(m)(s) = M(Γ|γ)(η(Γ, m)(definition(Γ(m)(s)))).

5.2 Constant Definitions

We first extend the subset of PVS described so far to include constant definitions in a manner similar to type definitions. This extension is used in formalizing the semantics of parametric theories. The syntax for a constant definition is c: T = a where definition(Γ(c)) is a. These definitions are explicit, that is, not recursive. With this extension, the type rule for constant declarations in contexts changes from that of Definition 3.10.

Definition 5.12 (type rule with constant definitions)

τ(Θ)(Γ, c: T = a) = T, if Γ(c) is undefined,

Θ(c) is undefined, τ(Θ)(Γ) = CONTEXT, τ(Θ; Γ)(a) = T′, (T ∼ T′)_{Γ}, ⊢_{Γ} π(T)(a)

The notion of satisfaction must be extended from that of Definition 5.11 to ensure that an assignment for a defined constant satisfies the definition.

Definition 5.13 (satisfaction with constant definitions) An assignment γ satisfies a context Γ if in addition to the conditions in Definition 5.11, whenever kind(Γ(s)) = CONSTANT and definition(Γ(s)) is nonempty, then γ(s) = M(Γ | γ)(definition(Γ(s))).

5.3 Parametric Theories

The extension to parametric theories is obtained by permitting theories to be declared as m[Π]: THEORY = Δ, where Π is a context listing the parameters and Δ is the body of the theory. If the above declaration of m occurs in context Γ, then Π is formals(Γ(m)), and Δ is definition(Γ(m)). For nonparametric theories, formals(Γ(m)) is empty. Types or constants declared in a parametric theory are referenced outside the theory as m[σ].s, where σ is a list of actual parameters consisting of types and terms. The type rule from the nonparametric case must be modified to check the parameters.

Definition 5.14 (type rule for contexts with parametric theories)

τ(Θ)(Γ, m[Π]: THEORY = Δ)

= CONTEXT if Γ(m), Θ(m), Π(m) are undefined

τ(Θ)(Γ) = CONTEXT τ(Θ; Γ)(Π) = CONTEXT, Π has only constant and type declarations without definitions, τ(Θ; Γ; Π)(Δ) = CONTEXT Δ only has type and constant declarations

The type rules for prefixed symbols are given below. The notation Π = σ, where Π is of the form s_{1}: α_{1}, …, s_{n}: α_{n}, and σ is of the form σ_{1}, …, σ_{n}, is short for the context s_{1}: α_{1} = σ_{1}, …, s_{n}: α_{n} = σ_{n}. The definition of η is now extended to substitute actual theory parameters for formals, so that η(Γ, m[σ])(a) prefixes every unprefixed symbol s in a that is declared in definition(Γ(m)) by m[σ], and replaces any s_{i} in a that is declared in formals(Γ(m)) by the corresponding σ_{i} in σ. Definition 5.15 (type rules for prefixed names with actuals) Let Π be formals(Γ(m)).

τ(Γ)(m[σ].s) = TYPE, if

kind(Γ(m)) = THEORY kind(Γ(m))(s) = TYPE and τ(Γ)(Π = σ) = CONTEXT

τ(Γ)(m[σ].s) = δ(Γ)((η(Γ, m[σ])(type(Γ(m)(s)))),

if kind(Γ(m)) = THEORY kind(Γ(m)(s)) = CONSTANT and τ(Γ)(Π = σ) = CONTEXT

Definition 5.16 (type expansion with parametric theories)

δ(Γ)(m[σ].s) = δ(Γ)((η(Γ, m[σ])(definition(Γ(m)(s))))), if

definition(Γ(m)(s)) is nonempty.

δ(Γ)(m[σ].s) = m[σ].s, if definition(Γ(m)(s)) is empty.

The definition of an assignment for a context with parametric theories is a bit complicated. In the nonparametric case, γ(m) simply returns an assignment of values for the types and constants declared in the theory m. For the case of parametric theories m, γ(m) returns a function that maps the meaning of the given actuals σ to an assignment γ(m)(M(Γ | γ)(σ)) for the types and constants declared in the theory m. There is an important restriction that γ(m) must be rank-preserving, that is, if ϖ and ϖ′ are assignments for Π so that for each i where Π_{i} is a type parameter, the rank of ϖ(Π_{i}) equals the rank of ϖ′(Π_{i}), then the ranks of γ(m)(ϖ)(s) and γ(m)(ϖ′)(s) must be the same for each type symbol s declared in m.

It is also important to observe that the semantics of parametric theories makes use of the axiom of choice since the assignment corresponding to a theory m of the form m[t: TYPE]: THEORY = {c: t} is essentially a choice function.

Let γ{Π ← ϖ} represent the assignment such that γ{Π ← ϖ}(s) = ϖ(s) for s in the domain of the context Π, and γ(s), otherwise. The meaning of symbols of the form m[σ].s can then be defined as below.

Definition 5.17 (meaning function for prefixed symbols with actuals)

M(Γ | γ)(m[σ].s)

= M(Γ; Π; Δ | γ{Π ← ϖ}{Δ ← γ(m)(ϖ)})(s), where

Π = formals(Γ(m)) Δ = definition(Γ(m)) ϖ(r) = M(Γ | γ)((Π = σ)(r)), for r ∈ Π

The definition of a satisfying assignment given in Definition 5.11 also must be strengthened. Let Π be the formal parameters to theory m in context Γ; then, an assignment ϖ is said to be satisfying parameter assignment for Π under the assignment γ to Γ iff γ{Π ← ϖ} is a satisfying assignment for Π.

Definition 5.18 (satisfaction for contexts with parametric theories) An assignment γ satisfies a context Γ if in addition to the constraints stated in Definition 5.11, γ maps every parametric theory m declared in Γ with parameters Π and definition Δ, to a function that maps any satisfying parameter assignment ϖ for the theory parameters Π (namely, formals(Γ(m))) to a satisfying assignment γ{Π ← ϖ}{Δ ← γ(m)(ϖ)} for Δ (given by definition(Γ(m))).

5.4 Summary

Theories are used to package related declarations together. Parametric theories can be used to package together declarations that are generic in type and individual parameters. The type rules for contexts must be extended to accommodate the theories. The type rules for simple (nonparametric) theories are straightforward given this extension. The operation of expanding a type using type definitions must be enhanced so that symbols declared in a theory are prefixed with their theory name when referenced outside the theory. Assignments now have the same nested structure as contexts, and the semantic definition is easily extended to handle prefixed symbols. Parametric theories are more complex. The theory prefixes now contain actual parameters that have to be typechecked relative to the expected formal parameters. The assignments corresponding to parametric theories are functions that map given assignments for the formals to assignments for the declarations within a theory. Such a mapping must be constrained to be rank-preserving. Parametric theories can have subtype parameters, and assumptions on the parameters. The rules for subtype parameters and assumptions are omitted for now but will be included in an expanded version of this report.

Conditional Expressions and Logical Connectives

We have, so far, introduced the core of PVS containing types, type definitions, constant and variable declarations, subtypes, dependent types, and theories. In extending the language with both explicit and recursive constant definitions and formulas, a crucial difference is that the logical context under which a type-correctness condition is generated provides additional assumptions that can be used in proving any proof obligations. Examples of expressions where an extended context is needed to establish type correctness by discharging proof obligations include

1. x ≠ y ⊃ (x+y)/(x−y) ≤ 0. The type of the division operator constrains the denominator to be nonzero, that is, {x: real | x ≠ 0}. In the given expression, the denominator can be shown to be nonzero only in the context of the antecedent x ≠ y.

2. IF(i > 0, i, −i) has type nat given integer i provided the then and else parts are typechecked with the assumptions i > 0 and ¬(i > 0), respectively.

PVS has a polymorphic primitive equality predicate:

equality[T : TYPE] : THEORY = { =: [[T, T] -> bool] }

Note that an equality of the form equality[T].=(a, b) is informally written as a = b. When it is relevant to indicate the type parameter, we write the equality as a =_{T} b. It can be deduced from the meaning of equality that if S is a subtype of T, then for a and b in S, it must be the case that a =_{S} b iff a =_{T} b. Thus, we can assume that equality is always parameterized by a maximal type. We assume that any relevant context Γ contains the above declaration of the theory equality. Furthermore, any satisfying assignment γ for such a Γ must satisfy

γ(equality)(X)(=) = {⟨x, x⟩ | x ∈ X}.

The negation operation can be defined in terms of equality as shown below. We assume that the context contains a declaration of the form

   ¬ : [bool→bool] = (λ (x : bool): x = FALSE)

As is clear, a satisfying assignment γ for a context Γ containing the above declaration must be such that γ(¬) yields the usual truth-table semantics, that is, {⟨0, 1⟩, ⟨1, 0⟩}.

We can then introduce the polymorphic IF-THEN-ELSE operation as follows:

if_def [T: TYPE]: THEORY = { IF:[bool,T,T -> T] }

In typechecking conditional expressions, the notion of context has to be extended to include formulas so that the typechecking of the subterm b in IF(a, b, c) is done in the context of a, and the typechecking of c is done in the context of ¬a. There is one new typechecking rule for contexts with formulas.

τ()(Γ, a) = CONTEXT, if

τ()(Γ) = CONTEXT, and (τ(Γ)(a) ∼ bool)_{Γ}

Note that the type rule checks that the type of a is compatible with bool rather than equivalent to it since it is possible that the type of a might be a subtype of bool.

Definition 6.1 (satisfaction for contexts with formulas) An assignment γ satisfies context Γ when in addition to the conditions in Definition 5.18, for each prefix Γ′, a of Γ, M(Γ′ | γ)(a) = 1.

The typechecking of conditional expressions is different from that of other application expressions since the test part of the conditional expression is introduced into the context as a contextual assumption.

Definition 6.2 (type rule for conditional expressions)

τ(Γ)(if def[T ].IF(a, b, c)) = T, if (τ(Γ)(a) ∼ bool)_{Γ},
τ(Γ, a)(b) = B,
(B ∼ T)_{Γ,a},
⊢_{Γ,a} π(T)(b)
τ(Γ, ¬a)(c) = C,
(C ∼ T)_{Γ,¬a},
⊢_{Γ,¬a} π(T)(c)

The meaning of conditional expressions must be treated in a special way since the else part need not denote when the test part is true and, correspondingly, the then part need not denote if the test part is false. We assume that any relevant contexts Γ contain the above declaration of the if def theory. Conditional expressions can be regarded as a new construct in the language rather than a form of application. However, it is conservative to regard conditional expressions as applications since the latter introduce the additional constraint that all the arguments must already denote, that is, applications are strict.

Definition 6.3 (meaning function for conditional expressions)

M(Γ | γ)(if def[T].IF(a, b, c)) = \{ \begin{matrix}M(Γ | γ)(b), & if M(Γ | γ)(a) = 1 \\ M(Γ | γ)(c), & otherwise \end{matrix}

The semantics for conditional expressions raises an important issue. The equality

       if def[bool].IF(x, y, FALSE) = if def[bool].IF(y, x, FALSE)

is semantically valid for variables x and y of type bool. An expression like if def[bool].IF(i ≠ 0, 1/i > 0, FALSE) can be typechecked to have the type bool since it generates a valid proof obligation i ≠ 0 ⊃ i ≠ 0, but the seemingly equivalent expression if def[bool].IF(1/i > 0, i ≠ 0, FALSE) generates an unverifiable proof obligation i ≠ 0. This may seem contradictory since the equality suggests a transformation of a type correct conditional expression to a type incorrect expression. The resolution here is that equality cannot be instantiated with i ≠ 0 for x and 1/i > 0 for y since the expression 1/i > 0 typechecks as having type bool only when i ≠ 0 is known from the context. The same applies in the case of the other propositional connectives, thus ensuring that each expression is type correct in the context in which it occurs.

We can then define the propositional connectives in terms of conditional expressions.

   ∧: [[bool, bool]→bool] = λ(x: bool, y: bool): if def[bool].IF(x, y, FALSE)
   ∨: [[bool, bool]→bool] = λ(x: bool, y: bool): if def[bool].IF(x, TRUE, y)
  ⊃: [[bool, bool]→bool] = λ(x: bool, y: bool): if def[bool].IF(x, y, TRUE)

In the typechecking of terms of the form a ∧ b, we follow the corresponding rule for the definition so that the term a is assumed in the context when typechecking term b. Similarly, for a ∨ b, the formula ¬a is assumed in the context when typechecking b, and for a ⊃ b, the formula a is assumed in the context when typechecking b. The Boolean equivalence operator IFF has no special rules for adding formulas to contexts during typechecking.

6.1 Summary

The use of assumption formulas enables expressions to be typechecked within the narrow context of their use so that the governing assumptions can be used in discharging any proof obligations. The type rules for conditional expressions and the Boolean connectives ∧, ∨, and ⊃ make use of contextual assumptions.

Proof Theory of PVS

The final step in the presentation of the semantics is the presentation of the proof rules for the idealized subset of PVS described thus far. As already indicated, the proof theory is an integral part of the semantics since typechecking and proof checking are closely intertwined. Fortunately, the proof rules turn out to be much less complicated than the type rules.

The PVS proof theory is presented in terms of a sequent calculus. A sequent is of the form Σ ⊢_{Γ} Λ, where Γ is the context, Σ is a set of antecedent formulas, and Λ is a set of consequent formulas. Such a sequent should be read as stating that the conjunction of the formulas in Σ implies the disjunction of formulas in Λ.

Inference rules are presented in the form

\frac{premise(s)}{conclusion} name  side condition

7.1 PVS Proof Rules

7.1.1 Structural Rules

The structural rules permit the sequent to be rearranged or weakened via the introduction of new sequent formulas into the conclusion. All the structural rules can be expressed in terms of the single powerful weakening rule shown below. It allows a weaker statement to be derived from a stronger one by adding either antecedent formulas or consequent formulas. The relation Σ_{1} ⊆ Σ_{2} holds between two lists when all the formulas in Σ_{1} occur in the list Σ_{2}.

\frac{Σ_{1} ⊢_{Γ} Λ_{1}}{Σ_{2} ⊢_{Γ} Λ_{2}} W if Σ_{1} ⊆ Σ_{2} and Λ_{1} ⊆ Λ_{2}

Both the Contraction and Exchange rules shown below are absorbed by the above weakening rule W. The Contraction rules C ⊢ and ⊢ C allow multiple occurrences of the same sequent formula to be replaced by a single occurrence.

\frac{a, a, Σ ⊢_{Γ} Λ}{a, Σ ⊢_{Γ} Λ} C ⊢  \frac{Σ ⊢_{Γ} a, a, Λ}{Σ ⊢_{Γ} a, Λ} ⊢ C

The Exchange rule asserts that the order of the formulas in the antecedent and the consequent parts of the sequent is immaterial. It can be stated as

\frac{Σ_{1}, b, a, Σ_{2} ⊢_{Γ} Λ}{Σ_{1}, a, b, Σ_{2} ⊢_{Γ} Λ} X ⊢  \frac{Σ ⊢_{Γ} Λ_{1}, b, a, Λ_{2}}{Σ ⊢_{Γ} Λ_{1}, a, b, Λ_{2}} ⊢ X

As seen above, inference rules have the general form

\frac{Σ_{1} ⊢ Λ_{1} ⋯ Σ_{n} ⊢ Λ_{n}}{Σ ⊢ Λ} R .

This says that if we are given a leaf of a proof tree of the form Σ ⊢ Λ, then by applying the rule named R, we may obtain a tree with n new leaves.

7.1.2 Cut Rule

The cut rule Cut can be used to introduce a case split on a formula a into a proof of a sequent Σ ⊢_{Γ} Λ so as to yield the subgoals Σ, a ⊢_{Γ} Λ and Σ ⊢_{Γ} a, Λ, which can be seen as assuming a along one branch and ¬a along the other.

\frac{(τ(Γ)(a) ∼ bool)_{Γ} Σ, a ⊢_{Γ} Λ Σ ⊢_{Γ} a, Λ}{Σ ⊢_{Γ} Λ} Cut

7.1.3 Propositional Axioms

The axioms rule Ax simply asserts that a follows from a.

\overline{Σ, a ⊢_{Γ} a, Λ} Ax

The next two rules assert that any sequent with either an antecedent occurrence of FALSE or a consequent occurrence of TRUE is an axiom.

              \overline{Σ, FALSE ⊢_{Γ} Λ} FALSE ⊢  \overline{Σ ⊢_{Γ} TRUE, Λ} ⊢ TRUE

7.1.4 Context Rules

Certain formulas hold in a context simply because they are already asserted in the context either as a formula or a constant definition.

\overline{⊢_{Γ} a} ContextFormula if a is a formula in Γ
\overline{⊢_{Γ} s = a} ContextDefinition if s: T = a is a constant definition in Γ

The context Γ can be extended with antecedent formulas or negations of consequent formulas using the following two rules.

\frac{Σ, a ⊢_{Γ,a} Λ}{Σ, a ⊢_{Γ} Λ} Context ⊢ \frac{Σ ⊢_{Γ,¬a} a, Λ}{Σ ⊢_{Γ} a, Λ} ⊢ Context

The following context-weakening rule is useful since it shows that provability is monotonic with respect to the context.

\frac{Σ ⊢_{Γ} Λ}{Σ ⊢_{Γ′} Λ} ContextW if Γ is a prefix of Γ′

7.1.5 Conditional Rules

The rules governing the elimination of IF-THEN-ELSE in a proof are unusual since they augment the context with the test part or its negation, as in the corresponding type rules.

\frac{Σ, a, b ⊢_{Γ,a} Λ  Σ, c ⊢_{Γ,¬a} a, Δ}{Σ, IF(a, b, c) ⊢_{Γ} Λ} IF ⊢

\frac{Σ, a ⊢_{Γ,a} b, Λ  Σ ⊢_{Γ,¬a} a, c, Λ}{Σ ⊢_{Γ} IF(a, b, c), Λ} ⊢ IF

7.1.6 Equality Rules

The rules for equality can be stated as below. The rules of transitivity and symmetry for equality can be derived from these rules. The notation a[e] is used to highlight one or more occurrences of e in the formula a such that there are no free variable occurrences in e.^{1} The notation Λ[e] similarly highlights occurrences of e in Λ.

1We enforce an invariant on a sequent that it must not contain any free variables. This invariant is preserved by each of the proof rules.

\overline{Σ ⊢_{Γ} a = a, Λ} Refl  \frac{a = b, Σ[b] ⊢_{Γ} Λ[b]}{a = b, Σ[a] ⊢_{Γ} Λ[a]} Repl

7.1.7 Boolean Equality Rules

The rule Repl TRUE asserts that an antecedent formula a can be treated as an antecedent equality of the form a = TRUE, and correspondingly, a consequent formula a can be treated as an antecedent equality of the form a = FALSE.

\frac{Σ[TRUE], a ⊢_{Γ} Λ[TRUE]}{Σ[a], a ⊢_{Γ} Λ[a]} Repl TRUE   \frac{Σ[FALSE], a ⊢_{Γ} Λ[FALSE]}{Σ[a] ⊢_{Γ} a, Λ[a]} Repl FALSE

The rule TRUE-FALSE asserts that TRUE and FALSE are distinct Boolean constants.

                      Σ, TRUE = FALSE ⊢_{Γ} Λ

                                         TRUE-FALSE

7.1.8 Reduction Rules

The reduction rules are equality rules (axioms) that provide the obvious simplifications for applications involving lambda abstractions and product projections.

\begin{matrix}\overline{⊢_{Γ} (λ(x: T): a)(b) = a[b/x]} & β \\ \overline{⊢_{Γ} p_{i}(a_{1}, a_{2}) = a_{i}} & π \end{matrix}

7.1.9 Extensionality Rules

The extensionality rules are also equality rules for establishing equality between two expressions of function or product type. The extensionality rule for functions, FunExt, introduces a Skolem constant s to determine that two functions f and g are equal when the results of applying them to an arbitrary argument s are equal.

\frac{Σ ⊢_{Γ,s:A} (f s) =_{B[s/x]} (g s), Λ}{Σ ⊢_{Γ} f =_{[x:A→B]} g, Λ} FunExt Γ(s) undefined

The extensionality rule for products asserts that two products are equal if their corresponding projections are equal.

\frac{Σ ⊢_{Γ} p_{1}(a) =_{T_{1}} p_{1}(b), Λ Σ ⊢_{Γ} p_{2}(a) =_{T_{2}[(p_{1} a)/x]} p_{2}(b), Λ}{Σ ⊢_{Γ} a =_{[x:T_{1}T_{2}]} b, Λ} TupExt

Recall that the quantifiers can be defined in terms of lambda abstraction and equality so that (∀(x: T): a) is just (λ(x: T): a) = (λ(x: T): TRUE). Existential quantification (∃(x: T): a) can easily be defined as ¬(∀(x: T): ¬a). The proof rules for quantifiers can then be derived from the rules β, TupExt, and the equality rules.

7.1.10 Type Constraint Rule

We need a rule to introduce the type constraint on a term as an antecedent formula of the given goal sequent.

\frac{τ(Γ)(a) = A π(A)(a), Σ ⊢_{Γ} Λ}{Σ ⊢_{Γ} Λ} Typepred

7.2 Soundness of the Proof Rules

Proposition 7.1 If Γ is a prefix of Γ′, τ()(Γ) = τ()(Γ′) = CONTEXT, γ′ is a satisfying assignment for Γ′, and γ = γ′ ↾ Γ then for any a such that τ(Γ)(a) = τ(Γ′)(a), it is the case that M(Γ | γ)(a) = M(Γ′ | γ′)(a).

Theorem 7.2 (soundness) If τ()(Γ) = CONTEXT such that for every formula a in Σ; Λ, (τ(Γ)(a) ∼ bool)_{Γ}, and Σ ⊢_{Γ} Λ is provable, then for any satisfying assignment γ for Γ, either there is a formula b in Σ, such that M(Γ | γ)(b) = 0 or a formula c in Λ, such that M(Γ | γ)(c) = 1.

Proof. The proof is by induction on the structure of the proof of Σ ⊢_{Γ} Λ. Recall that this proof is actually part of a simultaneous induction that includes the soundness of the type rules relative to the semantic function, that is, Theorems 4.14 and 4.18. Specific invocations of the soundness theorem occur in the proofs of Theorem 3.19 and Proposition 4.17.

1. Structural Rules: Since the subset of formulas in the premise and the conclusion of these rules are the same, the conclusion follows easily from the induction hypothesis.

2. Cut: By the semantic soundness of the type rules, we have M(Γ | γ)(a) ∈ 2. If M(Γ | γ)(a) = 0, then by the induction hypothesis on the second subgoal of the proof rule, there must be some b in Σ such that M(Γ | γ)(b) = 0 or a c in Λ such that M(Γ | γ)(c) = 1. The case when M(Γ | γ)(a) = 1 is symmetrical.

3. Propositional Axioms: Obvious.

4. Context Rules:

ContextFormula: If γ satisfies Γ and a ∈ Γ, then M(Γ | γ)(a) = 1.

ContextDefinition: If γ satisfies Γ and s: T = a is a declaration in Γ, then by the definition of satisfaction, M(Γ | γ)(s) = M(Γ | γ)(a).

Context ⊢: The argument is trivial when M(Γ | γ)(a) = 0. Otherwise, γ satisfies the extended context Γ, a, and the conclusion follows from the induction hypothesis.

⊢ Context: Similar to Context ⊢ above.

ContextW: If γ satisfies Γ′, then it also satisfies Γ, and hence the proof.

5. Conditional Rules: We only consider IF ⊢ since the ⊢ IF proof is similar. If M(Γ | γ)(IF(a, b, c)) = 0, the conclusion follows trivially. Otherwise, If γ satisfies Γ, then M(Γ | γ)(a) ∈ 2. If M(Γ | γ)(a) = 1, then M(Γ | γ)(b) = 1. The induction hypothesis on the subgoal Σ, a, b ⊢_{Γ,a} Λ yields the desired conclusion. Similarly, if M(Γ | γ)(a) = 0, we have M(Γ | γ)(c) = 1 and the induction hypothesis on the second subgoal yields the desired conclusion.

6. Equality Rules: The Refl rule is obvious. For the Repl rule, if M(Γ | γ)(a = b) = 0, the conclusion follows trivially. Otherwise, M(Γ | γ)(a) = M(Γ | γ)(b). Hence, γ satisfies the extended context Γ, a = b. Then for each c[a] in Σ[a] or Λ[a], M(Γ | γ)(c[a]) = M(Γ | γ)(c[b]).

7. Boolean Equality Rules: The Repl TRUE and Repl FALSE rules follow easily since when M(Γ | γ)(a) = 1, we have M(Γ | γ)(c[a]) = M(Γ | γ)(c[TRUE]). A similar argument applies to Repl FALSE.

The soundness of TRUE-FALSE is easy since M(Γ | γ)(TRUE = FALSE) = 0.

8. Reduction Rules: The β-reduction rule follows because M(Γ | γ)((λ(x: T): a)(b)) is M(Γ, x: VAR T | γ{x ← M(Γ | γ)(b)})(a) which by the Substitution Lemma 4.16 is equal to M(Γ | γ)(a[b/x]).

The soundness π-reduction rule is a direct consequent of Definition 2.6.

9. Extensionality Rules:

FunExt: First consider the case when the domain type M(Γ | γ)(A) is empty. Then by Definition 4.12, M(Γ | γ)(f) = M(Γ | γ)(g) = ∅. Therefore M(Γ | γ)(f = g) = 1 and hence the conclusion.^{2} The case when M(Γ | γ)(A) is nonempty, we have for any γ satisfying Γ and s ∈ M(Γ | γ)(A), that γ′ given by γ{s ← z} is a satisfying assignment for Γ, s: A. By the induction hypothesis, there is either an a in Σ such that M(Γ, s: A | γ′)(b) = 0 or a c in (f s) = (g s), Λ such that M(Γ, s: A | γ′)(c) = 1. If we have such a b in Σ, by Proposition 7.1, we also have that M(Γ | γ)(b) = 0. A similar argument can be used if we have such a c in Λ. If c is (f s) = (g s), then M(Γ | γ)(f)(z) = M(Γ | γ)(g)(z) for every z in M(Γ | γ)(A). By set-theoretic extensionality, this means that M(Γ | γ)(f) and M(Γ | γ)(g) are identical elements of ΠF where F maps z in M(Γ | γ)(A) to an element of M(Γ, x: VAR A | γ{x ← z})(B). Therefore M(Γ | γ)(f = g) = 1 as desired.

TupExt: If there is some d in Σ such that by applying the induction hypothesis to any of the subgoals M(Γ | γ)(d) = 0, then the same holds for the conclusion sequent. Similarly, if the induction hypothesis on some subgoal yields a c in Λ such that M(Γ | γ)(c) = 1, then the same holds for the conclusion sequent. So the remaining case is when, by the induction hypothesis, M(Γ | γ)(p_{i}(a)) = M(Γ | γ)(p_{i}(b)) for each i ∈ {1, 2}. It is therefore easy to conclude by set-theoretic extensionality that M(Γ | γ)(a) and M(Γ | γ)(b) are identical elements of M(Γ | γ)(a/[T_{1}, T_{2}]). We can then use Proposition 4.17 to conclude that M(Γ | γ)(a) and M(Γ | γ)(b) are identical elements of M(Γ | γ)([T_{1}, T_{2}]).

10. Type Constraint Rule: Recall from Proposition 3.17 that when τ(Γ)(a) = A, then M(Γ | γ)(π(A)(a)) = 1. Given this and the induction hypothesis, it must either be the case that we have a b in Σ such that M(Γ | γ)(b) = 0 or a c in Λ such that M(Γ | γ)(c) = 1.

2Since the subgoal sequent Σ ⊢_{Γ,s:A} (f s) = (g s), Λ is valid when M(Γ | γ)(A) = ∅ for all assignments γ, it is natural to ask how it is actually proved. The only way a type A can be empty under any assignment γ is if M(Γ | γ)(π(A)(a) = 0). The Typepred rule can therefore be used on the Skolem constant s to complete the proof.

To tie the development so far into a single simultaneous induction as promised, we state the key theorem whose subproofs have been given by the theorems presented thus far, namely, Theorems 4.14, 4.18, and 7.2.

Theorem 7.3 If τ()(Γ) = CONTEXT, then

1. If Σ, Λ is a list of preterms such that for every a in Σ; Λ, (τ(Γ)(a) ∼ bool)_{Γ}, and Σ ⊢_{Γ} Λ is provable, then for any satisfying assignment γ for Γ, either there is a b in Σ, such that M(Γ | γ)(b) = 0 or a c in Λ, such that M(Γ | γ)(c) = 1.

2. If A is a pretype such that τ(Γ)(A) = TYPE, then for any assignment γ satisfying Γ, M(Γ | γ)(A) ∈ U.

3. If a is a preterm such that τ(Γ)(a) = A, then for any assignment γ satisfying Γ, M(Γ | γ)(a) ∈ M(Γ | γ)(A).

7.3 Summary

The logical inference rules for the PVS logic have been presented in a sequent calculus format. The formal semantics presented in the earlier chapters is used to establish the soundness of these proof rules.

Conclusion

We have presented the syntax and semantics of idealized PVS in several stages. In the first stage we introduced the simply typed fragment, which was then extended with type definitions. The third such fragment included subtyping; the fourth fragment introduced dependent typing. Finally, we introduced constant definitions and parametric and nonparametric theories.

The semantic definition was given in a novel, functional style where a canonical type was assigned to each type correct term. The interplay between types and proofs in PVS introduced subtleties and complexities into the semantic definition. We can now answer some of the questions raised in Chapter 1:

• What is the semantic core of the language, and what is just syntactic sugar? The semantic core of the language is a typed lambda calculus with simple function and tuple types, predicate subtypes, dependent types, parametric theories, and conditional expressions. Many of the other features of the PVS language such as records and update expressions can be explained in terms of the core language.

• What are the rules for determining whether a given PVS expression is well typed? The typechecking rules have been presented in terms of the definition of the τ operator in Chapters 2, 3, 4, 5, and 6.

• How is subtyping handled, and in particular, how are proof obligations corresponding to subtypes generated? Typechecking an expression a with respect to predicate subtype constraint {x: T |p(x)} is done by generating the proof obligation p(a) under the logical context in which a is being typechecked. This is made precise in Definitions 3.10 and 6.2. Proof obligations are generated when typechecking contexts (for nonemptiness), typechecking expressions with respect to expected subtypes, and comparing two types containing subtype expressions for compatibility.

• What is the meaning, in set-theoretic terms, of a PVS expression or assertion?

The set-theoretic meaning of well-formed PVS types and expressions is given by a meaning function M that assigns a set M(Γ | γ)(T) from the universe U to each type T, and an element M(Γ | γ)(a) of M(Γ | γ)(T) to a given term a of type T.

• Are the type rules sound with respect to the semantics?

The typechecking function τ is defined to check contexts, preterms, and pretypes for type correctness. The type rules are shown to be sound with respect to the given semantics in Theorem 7.3.

• Are the proof rules sound with respect to the semantics?

The proof rules are given in Chapter 7 in a sequent calculus format and proved to be sound with respect to the semantics in Theorem 7.3.

• What is the form of dependent typing used by PVS, and what kinds of type dependencies are disallowed by the language?

The semantic analysis of dependent typing in Chapter 4 revealed that type dependencies were constrained to be rank-bounded. This is true because the dependencies in dependent typing only constrain the predicate part of predicate subtypes. Thus, when there is a dependent type T (n) that depends on a parameter n, the meaning of T (n) has a fixed rank regardless of the meaning assigned to n. The PVS language features used to define dependent types all preserve the rank-boundedness. Language extensions violating rank-boundedness such as a type dependency of the form [n: nat→T^{n}] are disallowed. One can extend the language with such dependent types, but the semantics would then be considerably more complicated.

• What is the meaning of theory-level parametricity, and what, if any, are the semantic limits on such parameterization?

The semantics of parametric theories is described in Chapter 5. In particular, the semantics for parametric theories is given in terms of rankpreserving maps between the meanings of the parameters and the meanings of the identifiers declared in the theory. These maps must be such that the rank of an assignment to a type in a theory depends only on the ranks of the (meanings of the) type parameters.

• What language extensions are incompatible with the reference semantics given here?

We have already indicated that any language extension, such as an ntuple type T^{n}, that violates rank-boundedness would be incompatible with the semantics presented here.

This report presents only the core language of PVS. A more complete semantic treatment would include arithmetic, recursive constant definitions, inductive definitions, recursive datatypes, assumptions on theory parameters, and type judgements.

Acknowledgments. The advice and encouragement of John Rushby, Rick Butler, Paul Miner, Pat Lincoln, and Mandayam Srivas are greatly appreciated, as are the useful expert comments of Peter Dybjer, Mike Gordon, Doug Howe, and Paul Jackson. Bruno Dutertre, Paul Miner, and Harald Rueß suggested numerous improvements to earlier drafts.

Bibliography

[AMCP84] P. B. Andrews, D. A. Miller, E. L. Cohen, and F. Pfenning. Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 169–192. American Mathematical Society, Providence, R.I., 1984.

[And86] Peter B. Andrews. An Introduction to Logic and Type Theory: To Truth through Proof. Academic Press, New York, NY, 1986.

[CAB^{+}86] R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.

[Chu40] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[DFH^{+}91] Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Christine Paulin-Mohring, and Benjamin Werner. The COQ proof assistant user’s guide: Version 5.6. Rapports Techniques 134, INRIA, Rocquencourt, France, December 1991.

[Dyb91] Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Logical Frameworks, pages 280–306. Cambridge University Press, 1991.

[EHDM93] User Guide for the Ehdm Specification Language and Verification System, Version 6.1. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. Three volumes.

[FBHL84] A. A. Fraenkel, Y. Bar-Hillel, and A. Levy. Foundations of Set Theory, volume 67 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, The Netherlands, second printing, second edition, 1984.

[FGJM85] Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and José Meseguer. Principles of OBJ2. In Brian K. Reid, editor, 12th ACM Symposium on Principles of Programming Languages, pages 52–66. Association for Computing Machinery, 1985.

[GH93] John V. Guttag and James J. Horning with S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993.

[GM93] M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK, 1993.

[How91] Douglas J. Howe. On computational open-endedness in Martin-Löf’s type theory. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 162–172, Amsterdam, The Netherlands, 15–18 July 1991. IEEE Computer Society Press.

[How96] Douglas J. Howe. Semantic foundations for embedding HOL in Nuprl. In Martin Wirsing and Maurice Nivat, editors, Algebraic Methodology and Software Technology, 5th International Conference, AMAST’96, pages 85–101. Number 1101 in Lecture Notes in Computer Science, Springer Verlag, 1996.

[Jon90] Cliff B. Jones. Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, second edition, 1990.

[Lam94] Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872–923, May 1994.

[LP97] Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed? SRC Research Report 147, Digital Systems Research Center, Palo Alto, CA, May 1997. Available at

http://www.research.digital.com/SRC.

[Mel89] Thomas F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Theorem Proving, pages 341–386, New York, NY, 1989. Springer-Verlag.

[MMMS90] Albert R. Meyer, John C. Mitchell, Eugenio Moggi, and Richard Statman. Empty types in polymorphic lambda calculus. In Gerard Huet, editor, Logical Foundations of Functional Programming, University of Texas at Austin Year of Programming, pages 273– 284. Addison-Wesley, 1990.

[OS97] S. Owre and N. Shankar. Abstract datatypes in PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1997. Revised version of SRI-CSL-93-9. To appear as a NASA Contractor Report.

[OSRSC98] S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. User Guide for the PVS Specification and Verification System. Computer Science Laboratory, SRI International, Menlo Park, CA, September 1998. Three volumes: Language, System, and Prover Reference Manuals.

[RAISE92] The RAISE Language Group. The RAISE Specification Language. BCS Practitioner Series. Prentice-Hall International, Hemel Hempstead, UK, 1992.

[Spi88] J. M. Spivey. Understanding Z: A Specification Language and its Formal Semantics. Cambridge Tracts in Theoretical Computer Science 3. Cambridge University Press, Cambridge, UK, 1988.