Interactive Program Derivation

Martin David Coen St. John’s College

A dissertation submitted for the degree of Doctor of Philosophy in the University of Cambridge

March 1992

Declaration

This dissertation is the result of my own work and includes nothing which is the outcome of work done in collaboration. This dissertation is not substantially the same as any I have submitted for a degree, diploma or other qualification at any other university. ii

Acknowledgements

I should like to thank my research supervisor, Dr Lawrence Paulson, for the freedom he allowed me in my research, and the interest he took in my work. His patient consideration of my ideas and the influence of his own research have been of great value throughout the development of this work. Thanks is also due to Tobias Nipkow and Andy Pitts for many valuable discussions about various aspects of the work.

This dissertation has benefitted from comments made on earlier drafts by Gavin Bierman, Marcus Moore, Valeria de Paiva and Clive Tong. Tom Melham also kindly read a draft and made helpful suggestions, both about the content of the dissertation and its layout. Thanks are due to Graham Titmus for his stalwart efforts in keeping the machines in the laboratory running, and to Margaret Levitt for keeping the bureaucratic wheels turning. I should also like to thank the Laboratory for the Foundations of Computer Science for the time I spent in Edinburgh during my second year.

Financial support for this work came from several sources. The main part of the work was supported by a studentship from the Science and Engineering Research Council. I am grateful to the ESPRIT Basic Research Action 3245 ‘Logical Frameworks’ for equipment and funding to attend conferences, as well as support in the final months. St John’s College also helped with funding to attend conferences.

Last, but by no means least, I should like to thank my family and Deborah Lamb for their continued support during the last few years. iv

Summary

As computer programs are increasingly used in safety critical applications, program correctness is becoming more important; as the size and complexity of programs increases, the traditional approach of testing is becoming inadequate. Proving the correctness of programs written in imperative languages is awkward; functional programming languages, however, offer more hope. Their logical structure is cleaner, and it is practical to reason about terminating functional programs in an internal logic.

This dissertation describes the development of a logical theory called CCL for reasoning about the correctness of terminating functional programs, its implementation using the theorem prover Isabelle, and its use in proving formal correctness. The theory draws both from Martin-Löf’s work in type theory and Manna and Waldinger’s work in program synthesis. It is based on classical first-order logic, and it contains terms that represent classes of behaviourally equivalent programs, types that denote sets of terminating programs and well-founded orderings. Well-founded induction is used to reason about general recursion in a natural way and to separate conditions for termination from those for correctness.

The theory is implemented using the generic theorem prover Isabelle, which allows correctness proofs to be checked by machine and partially automated using tactics. In particular, tactics for type checking use the structure of programs to direct proofs. Type checking allows both the verification and derivation of programs, reducing specifications of correctness to sets of correctness conditions. These conditions can be proved in typed first-order logic, using well-known techniques of reasoning by induction and rewriting, and then lifted up to CCL. Examples of program termination are asserted and proved, using simple types. Behavioural specifications are expressed using dependent types, and the correctness of programs asserted and then proved. As a non-trivial example, a unification algorithm is specified and proved correct by machine.

The work in this dissertation clearly shows how a classical theory can be used to reason about program correctness, how general recursion can be reasoned about, and how programs can direct proofs of correctness. vi

Contents

1 Introduction 1 1.1 Formal Program Derivation . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Previous Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Kinds of Computational Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 The Aims of this Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.5 Outline of the Dissertation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 Review of Other Work 7 2.1 Deductive Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 Calculus of Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.4 Comments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3 The Theory CCL 19 3.1 Meta-Theoretic Conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2 An Untyped Functional Language . . . . . . . . . . . . . . . . . . . . . . . . 21

3.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.2.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

3.3 Term Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.3.1 A Pre-Order Over Terms . . . . . . . . . . . . . . . . . . . . . . . . 24 3.3.2 An Equivalence Over Terms . . . . . . . . . . . . . . . . . . . . . . . 26

3.4 Types for L . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3.4.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.4.2 Types and Type-Formers . . . . . . . . . . . . . . . . . . . . . . . . 29 3.4.3 Predicates for Types . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

3.5 Well-Founded Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.6 The Theory CCL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.7 The Strength of CCL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

4 Implementation 41

4.1 Encoding CCL in Isabelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.1.1 Overview of Isabelle . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.1.2 The Encoding of CCL . . . . . . . . . . . . . . . . . . . . . . . . . . 44

4.2 Derived Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 4.2.1 Induction Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4.2.2 Strong Type Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.2.3 Freeness of Constructors . . . . . . . . . . . . . . . . . . . . . . . . . 48

4.3 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 4.3.1 Local Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 4.3.2 Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

4.4 Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.4.1 Type Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.4.2 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.4.3 Introducing Recursive Functions . . . . . . . . . . . . . . . . . . . . 58 4.4.4 Introducing Local Declarations . . . . . . . . . . . . . . . . . . . . . 59 4.4.5 Properties of Recursive Calls . . . . . . . . . . . . . . . . . . . . . . 59 4.4.6 Well-Founded Orderings . . . . . . . . . . . . . . . . . . . . . . . . . 60

4.5 Interpretation of First-Order Theories . . . . . . . . . . . . . . . . . . . . . 61 4.5.1 Simple Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 4.5.2 Sorts of Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 4.5.3 Abstract Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

4.6 Summary of Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . 65

5 Proving Programs Correct 67 5.1 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 5.2 Specifying Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 5.3 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.4 Derivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 5.5 Proving Correctness Conditions . . . . . . . . . . . . . . . . . . . . . . . . . 73 5.6 An Extended Example: Unification . . . . . . . . . . . . . . . . . . . . . . . 73

5.6.1 A Formal Specification of Correctness . . . . . . . . . . . . . . . . . 73 5.6.2 First-Order Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 5.6.3 Derivation of Unification . . . . . . . . . . . . . . . . . . . . . . . . . 81

6 Conclusion 85

6.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 6.1.1 Interleaving Programming with Verification . . . . . . . . . . . . . . 85 6.1.2 Denotational and Operational Approaches . . . . . . . . . . . . . . . 86

6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 6.2.1 Other Target Languages . . . . . . . . . . . . . . . . . . . . . . . . . 86 6.2.2 Improving Type Checking . . . . . . . . . . . . . . . . . . . . . . . . 87 6.2.3 An Environment for Program Correctness . . . . . . . . . . . . . . . 89

A Well-Founded Induction 91 A.1 Well-Founded Relations and Induction . . . . . . . . . . . . . . . . . . . . . 91 A.2 Constructing Well-Founded Relations . . . . . . . . . . . . . . . . . . . . . 93

A.2.1 Irreflexive Transitive Closure . . . . . . . . . . . . . . . . . . . . . . 93 A.2.2 Mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 A.2.3 Lexicographic Ordering . . . . . . . . . . . . . . . . . . . . . . . . . 95

References 97

List of Figures

3.1 Evaluation Rules for L . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.2 Monotonicity Rules for CCL . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3 Type Rules for CCL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.4 Rules for Well-Founded Orderings in CCL . . . . . . . . . . . . . . . . . . 35 3.5 Natural Deduction Rules for First-Order Logic . . . . . . . . . . . . . . . . 36 3.6 General Rules of Equality for CCL . . . . . . . . . . . . . . . . . . . . . . . 37 3.7 Conversion Rules for CCL . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.8 Congruence Rules for CCL . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.9 Gödel’s System T . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

4.1 An Encoding of the Unit Data Type . . . . . . . . . . . . . . . . . . . . . . 51 4.2 An Encoding of the Boolean Data Type . . . . . . . . . . . . . . . . . . . . 52 4.3 An Encoding of the Disjoint Union Data Type . . . . . . . . . . . . . . . . 53 4.4 An Encoding of the Natural Number Data Type . . . . . . . . . . . . . . . . 54 4.5 An Encoding of the List Data Type . . . . . . . . . . . . . . . . . . . . . . 55 4.6 Axioms for Finite Set Theory . . . . . . . . . . . . . . . . . . . . . . . . . . 64

5.1 A Theory of Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 5.2 Facts about Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.3 Facts about Domains and Ranges . . . . . . . . . . . . . . . . . . . . . . . 79 5.4 Isabelle Proofs for Substitutions . . . . . . . . . . . . . . . . . . . . . . . . 80 5.5 Lemmas for Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . 84 x LIST OF FIGURES

Chapter 1

Introduction

As programming has moved from machine code to higher level languages removed from hardware, there has been a change in the understanding of the craft. The creation of high level languages with reasonably clean logical structure has led to some discipline in program development. Dijkstra illustrated this change in attitude by the change in terminology from ‘computer science’ to ‘computing science’ [16, page 210]. With the continuing growth in the size and complexity of programs and their use in safety critical applications, assurance of correctness is becoming increasingly important. The traditional approach of testing is inadequate. Formal reasoning now provides a more viable approach, as the semantics of programming languages has become clearer and theorem proving technology more developed. This dissertation introduces a formal system for reasoning about the correctness of functional programs. More importantly, it describes the implementation of the system and its use in proving some significant examples.

1.1 Formal Program Derivation

A computational logic is a formal system for reasoning about the behaviour of programs in a target programming language. This encompasses both external logics such as those of Floyd and Hoare [2], which provide logical comments external to the program, and internal logics such as Martin-Löf’s Type Theory(MLTT) [40], in which programs are represented as terms in the logic. A specification in a computational logic defines a class of programs satisfying the desired input/output behaviour. Proving the correctness of a program with respect to a specification is by proving membership in the defined class. A computational logic should allow specifications of varying flexibility, from simply requiring that a program terminates to completely defining its behaviour for all allowed inputs.

Before considering computational logics further, it is important to note their limitations. Formal methods are not a panacea. Formal correctness must rely on a formal specification. For large or complex applications, a formal specification is likely to contain discrepancies with the intended behaviour. Proving the correctness of a program with respect to a flawed specification cannot guarantee the intended behaviour. Furthermore, proving correctness in a computational logic assures the specified behaviour only with respect to a particular abstract model of computation in the target language. Correctness of an actual program must rely on the implementation (compiler, hardware, etc.) being faithful to this model.

That said, the exercise of formal reasoning is not futile. By allowing abstract specification of program behaviour, computational logics permit much clearer and more concise specifications than are possible in the target programming language itself, narrowing the gap between a designer’s intentions and the formal description. An abstract model of computation can be chosen to be an idealisation of an implementation (for the logic in Chapter 3, a Natural Semantics [23] is used). Cohn presents a good discussion of these issues in the context of hardware verification [11].

The purpose of formalising program correctness in a computational logic is to exploit machine-based theorem provers. Proof checking by machine has greatly advanced over the past few years. Systems now exist in which it is possible to carry out proofs interactively using tactics to perform some parts automatically (e.g. HOL [20], Isabelle [54] and NuPrl [12]). Using this technology, many areas of mathematics have been formally developed (e.g. ZF set theory and the real numbers). Whether this is a useful exercise in itself is another matter, but proving the correctness of programs is one area of mathematics in which there are clear advantages to a formal approach. Correctness proofs tend to be straightforward but long and full of detail, which makes them tedious and prone to error when done by hand. Machine-based theorem provers can keep track of the tedious detail in proofs and automate the simpler parts.

1.2 Previous Work

Early work on formal program development, as opposed to the informal methodologies proposed by Dijkstra [16] and Gries [22], was done by Burstall and Darlington [7] using program transformation. A clear but inefficient program is used to specify a problem. It is transformed into a less clear but more efficient program by a series of steps, each of which is guaranteed to preserve the program’s behaviour. Using a program as specification defines the class of programs with exactly the same input/output behaviour. Though much can be done within this framework (see Bird [5, 6]), it is too concrete. For example, specifying a compiler by presenting one possible implementation fixes the code generated for each source program, so prohibiting transformation to a compiler that generates better code. Specifications must be more abstract, describing the task required rather than a particular implementation.

Floyd-Hoare techniques have been used to formally verify that imperative programs satisfy their specifications; logics such as LCF have been used for verifying functional programs [51]. More recently, formal methods have been devised for the synthesis of programs in high level languages hand-in-hand with the development of their proofs of correctness. Manna and Waldinger [34] have used tableau-based theorem proving to synthesise general recursive, functional programs from first-order specifications.

Functional programming languages offer a relatively clean logical structure, satisfying Leibniz’s Law (the substitutivity of equals for equals), in contrast to imperative languages in which the simple structure is destroyed by constructions such as assignment and aliasing. Moreover, correctness proofs for functional programs closely follow the structure of the algorithms themselves; an algorithm can be used as a template to direct its proof of correctness. Both verification and synthesis can be directed in this way. In verification, the algorithm fixes the template from the outset; whereas in synthesis, the template (and hence the algorithm) is incrementally instantiated as the proof progresses. The two styles may be freely mixed in one proof, verifying an algorithm where it is given and synthesising it elsewhere. This is a promising approach to program correctness; it is much easier to write programs than to prove their correctness.

In an intuitionistic framework, there is an identification between proofs and programs known as the Curry-Howard isomorphism. The insights that arise from formalising this isomorphism in type theories have led to a plethora of computational logics: including work using MLTT [8], NuPRL [12] and the Calculus of Constructions [45]. In particular, Paulin [50] and Hayashi [24] consider extracting a functional program from an intuitionistic proof that its specification can be met. Dybjer [17] has suggested using Aczel’s theory LTC, an untyped framework, as a computational logic.

1.3 Kinds of Computational Logic

Two possible bases for a computational logic are denotational and operational semantics.

• In a denotational logic, each construction in the target programming language is given meaning by the term it denotes in the logic. Properties of actual programs can be inferred provided there is a good fit between the mathematical meaning of terms and their computational behaviour (at least computational adequacy [43]). Giving meaning to non-terminating programs requires partial functions or the addition of an element representing “undefined” to every type. Domain theory takes the second approach: a domain is a complete partial ordering of a set with a bottom element ⊥. Programs are continuous functions between domains. The computational logic LCF [21, 53, 10] is based on domain theory. Although interesting non-terminating programs do exist, the inclusion of an extra case (⊥) in proofs makes logics such as LCF unnecessarily awkward for reasoning about terminating programs [51]. If only terminating programs are considered, then set theory can be used. Programs denote total functions, but require annotations. For example, λ-abstraction is typed, and the operator for general recursion includes a well-founded relation. In this context, data types can be constructed, and general recursive programs can be denoted using well-founded recursion.

• In an operational logic, programs are represented by abstract syntax trees. An evaluation relation is defined between programs to capture the operational semantics, and this is used to define an equivalence relation. Two programs are equivalent if they behave in the same way in all contexts (observational congruence [43]). Properties of programs (including correctness) are expressed with respect to this equivalence. This is the approach adopted in Chapter 3.

Intuitionistic logics provide an appealing framework for computational reasoning. Proofs have computational content; if a proposition is regarded as a program specification, then its proof contains an algorithm that meets this specification. Complications arise when useful forms of inductive types and recursion are considered. Much work is being done in the development of intuitionistic computational logics [40, 4, 25, 33]. Although intuitionistic logic is not used here, it has had much influence on this work (see §2.2). But the intuitive understanding of logic, at least amongst programmers, is and is likely to remain classical. Unless the chosen model of computation prohibits a classical framework, there is no reason to insist that a computational logic be intuitionistic.

As a computational logic, typed first-order logic^{1} is unsatisfactory, because new types cannot be defined within the logic but require additional axioms, and only simply typed total functions may be considered. But it is still a useful framework for reasoning within particular domains. For example, first-order logic, extended with a type of natural numbers nat together with axioms stating the behaviour of the constructors 0 and S and the primitive recursive operator nrec, is a suitable theory in which to define the arithmetic functions + and ×, and prove facts about them. Several types can be present in one theory, for example booleans and natural numbers; the well-formedness of formulae ensures that each set of axioms applies only to terms of the appropriate type. Types can also be polymorphic, for example the type of List(α) of lists of α, where α is a variable ranging over types. For a given programming problem, data types and simply typed functions over them can be axiomatised in typed first-order logic, and facts derived within this framework (see §4.5).

1This is often called ‘sorted first-order logic’. But the word sort has a specific meaning in the context of the theorem prover Isabelle, so to avoid any confusion it is not used here.

Gordon’s formulation [20] of Church’s higher-order logic [9] allows the construction of new data types [42]. It too uses only simple types, not depending on terms. Simple types work well as partial specifications, not requiring termination; the host of strongly typed functional languages bears witness to this. But for total specifications requiring termination, simple types are insufficient. For example, a function for subtractive division can be defined in ML by

     fun div(n,d) = if (n<d) then 0 else div(n-d,d) + 1;

with the ML type nat*nat -> nat. Termination can be proved for all n ∈ Nat and all d ∈ {x ∈ Nat | x ≠ 0}. But the function cannot be typed as a total function Nat ∗ Nat →Nat, it needs a further condition on the input Nat ∗ {x:Nat, x ≠ 0} →Nat. A simply typed version of this function must include an arbitrary value for div(n,0).

     fun div(n,0) = <dummy>
       | div(n,d) = if (n<d) then 0 else div(n-d,d) + 1;

1.4 The Aims of this Work

This dissertation considers the implementation and use of a computational logic for proving the correctness of terminating functional programs. The target language is a core functional programming language, including general recursion, but excluding non-determinism, concurrency and imperative features.

The logic CCL (Classical Computational Logic) is developed and implemented using the theorem prover Isabelle with a collection of tactics to support reasoning about program correctness. The intention is not that CCL is to be the final word in computational logics— it clearly isn’t—but rather that the development and use of CCL may shed some light on what makes a computational logic effective. It is hoped that this dissertation will convince the reader that

• classical logics are suitable for reasoning about program correctness,

• the economy of considering only total functions need not preclude general recursion, and

• using programs as templates to direct correctness proofs is an effective approach to formal program development.

1.5 Outline of the Dissertation

• Chapter 2 describes the work that has had the greatest influence on this dissertation. In particular, Mana and Waldinger’s use of well-founded induction and deductive tableaux for reasoning about general recursion, the foundational work in Martin-Löf’s type theories on the logical nature of types for functional languages, and Paulin’s work on extracting programs from constructive proofs.

• Chapter 3 introduces the computational logic CCL. From a formulation of the target programming language, the constants of CCL are defined and its rules derived. Properties of CCL are proved that justify its use as a computational logic.

• Chapter 4 describes the implementation of CCL using the generic theorem prover Isabelle. Tactics are developed for type checking, rewriting and other more specific aspects of program correctness. First-order logic, extended with computational types, is used to prove many of the lemmas necessary for correctness. CCL acts as a meta-logic in which to interpret first-order logic.

• Chapter 5 describes how the implementation of CCL is used to prove program correctness. An extended example is considered: an algorithm for unification is introduced, formally specified within CCL and derived using the implementations of CCL and first-order logic.

• Chapter 6 summarises the main contributions of this dissertation and describes some areas of further research suggested by the work.

• Appendix A introduces well-founded induction and constructions for well-founded relations.

6 Chapter 1. Introduction

Review of Other Work

In Chapter 3, a computational logic is developed for a target programming language with a particular notion of evaluation. Although the motivations are quite different, the major inspiration for this comes from Martin-Löf’s type theoretic approach to logic [39, 40], and the subsequent work in Computing Science based on this. But in contrast to type theory, general recursion is considered; Manna and Waldinger’s work on program synthesis clearly shows the merits of this [34].

§2.1 describes Manna and Waldinger’s deductive tableau system, and its use in program synthesis. §2.2 introduces the basic ideas behind Type Theory, and considers how they lead to a computational logic. §2.3 outlines the work of Paulin [50], which has similar aims to mine but takes a somewhat different approach. Finally, §2.4 briefly describes the relevance of this work to the approach taken in the dissertation.

2.1 Deductive Tableaux

For many years, Manna and Waldinger have been proponents of program synthesis as a theorem proving task. They developed a system of deductive tableaux in which proving that a specification can be met synthesises a functional program.

Their deductive system is based on the notion of a tableau, which consists of a collection of rows each with three columns. Each row contains a single sentence of predicate logic, called an assertion if it appears in the first column and a goal if it appears in the second. The third column may sometimes contain an output expression, which records the program fragment that has been constructed at a particular stage of the proof, but has no bearing on the proof itself. Each row in a tableau has either the form

assertions  goals  output
A_{i}(\overline{a}, \overline{x})  t_{i}

or

G_{i}(\overline{a}, \overline{x})  t_{i}

where \overline{a} denotes all the constants and \overline{x} all the free variables in a goal or assertion. As a convention, write a, b, c, f, g … for constants and x, y, z … for variables. The variables in a row are “dummies”, which can be systematically renamed without changing the meaning of the row. The meaning of a tableau with assertions A_{i}(\overline{a}, \overline{x}) and goals G_{i}(\overline{a}, \overline{x}) is given by the following associated sentence of predicate logic.

(⋀_{i} ∀\overline{x}. A_{i}(\overline{a}, \overline{x})) ⊃ (⋁_{i} ∃\overline{x}. G_{i}(\overline{a}, \overline{x}))

A tableau is therefore valid iff under all interpretations at least one of the assertions is false or at least one of the goals is true. Clearly, the distinction between assertions and goals is superfluous; a sentence that appears as an assertion (goal) could instead appear in its negation as a goal (assertion). The distinction is only for clarity in the deductions.

A program is specified by an input/output relation. Given an input a such that P (a) holds, the program should output a value b such that the relation R(a, b) holds. Manna and Waldinger write this as

f(a) ⇐ find z such that R(a, z),
where P (a)

which corresponds to the theorem

∀a. P (a) ⊃ ∃z. R(a, z)

Synthesis begins with a tableau representing this theorem.

assertions  goals  {output \atop f(a)}

P (a)

R(a, z)  z

At each step in the deduction, rows are added to the tableau. Never is there a requirement to delete a row (though it may help proof search to do so). A deduction terminates when a terminal row is reached (i.e. one which makes the tableau trivially valid), either

true  t

or

false  t

The synthesised program is then

f(a) ⇐ t

A deduction step uses a rule from one of the following categories: splitting, transformation, non-clausal resolution and recursive calls. For brevity, only the propositional part of the deduction system is described, though it has been developed for predicate logic [37, Chapter 11].

Splitting rules allow assertions and goals to be decomposed into their logical components. They are simple consequences of the meaning of tableaux. There are rules andsplit, orsplit and ifsplit corresponding to the sequent rules ∧-left, ∨-right and ⊃-right. For example, the rule andsplit is written as

F ∧ G  t ; \begin{matrix}F & t \\ G & t \end{matrix}

meaning that if the rows above the double line are present in the tableau, then those below the double line may be added. There are no rules corresponding to the sequent rules ∧- right, ∨-left and ⊃-left; instead, transformation rules are used in particular instances.

Transformation rules allow one sentence (either an assertion or a goal) to be derived from another. The transformation rule

r ⇒ s if P

means that r is a logically equivalent sentence to s, or that r is a term equal to s, provided P holds. If r can be unified with a subexpression of F, and θ is the most general unifier, then for this rewrite rule the following deduction rules allow substitution in assertions and goals respectively.

F  t ; P θ ⊃ F θ[sθ/rθ]  tθ

F  t ; P θ ∧ F θ[sθ/rθ]  tθ

where tθ denotes the application of the substitution θ to the expression t, and t[y/x] denotes the substitution of y for all free occurrences of x in t. Transformation rules are more than simple rewriting; they allow arbitrary procedures. For example, the rule

f(x) = a ⇒ x = e if P

represents solving the equation f(x) = a for x under a condition P. They can also be used for simple inference. The rewrite rule

f(a) = f(b) ⇒ true if a = b

reduces a goal f(a) = f(b) to the goal a = b. If the side condition of a rule is vacuous (true), then it is omitted.

P ∧ true ⇒ P

reduces any subexpression that matches the left-hand side.

Non-Clausal Resolution allows subsentences of two rows to be unified, and then eliminated by classical case analysis. This generalises the conventional resolution of Robinson [58], allowing greater freedom in how it can be used—a problem for automation. Consider two rows, containing assertions F and G. If θ is the most general unifier of subsentences of F and G (P_{F} and P_{G} respectively), then

\begin{matrix}F & t_{1} \\ G & t_{2} \end{matrix}

F θ[true/P_{F} θ] ∨ Gθ[false/P_{G}θ] if P_{F} then t_{1}θ else t_{2}θ

If neither initial row has an output term, then none is created for the new row; if only one of the initial rows has an output term t, then the output term for the new row is tθ. Other rules can be deduced for the cases when F and G are an assertion and a goal, a goal and an assertion, and two goals. The case for a goal and an assertion is also shown, because of its use with the recursion hypothesis below.

\begin{aligned}& F & t_{1} \\ G & & t_{2} \end{aligned}

F θ[true/P_{F} θ] ∧ ¬Gθ[false/P_{G}θ] if P_{F} then t_{1}θ else t_{2}θ

This should be read with the same proviso on the output expression as above. Recursive Calls are the most interesting feature of this work. The assertion

{(u ≺_{w} a ∧ P (u) ) ⊃ \atop R(u, f(u))}

can always be added to a tableau as a general induction hypothesis. It states that if there exists some u such that u ≺_{w} a holds (where a is the formal parameter in the original specification, and w is an, as yet, undetermined well-founded relation) and P (u) holds (where P is the original input condition), then R(u, f(u)) holds (where f is the name of the function being synthesised, and f(u) is a recursive call). Using resolution (for a goal and an assertion) and some transformations, this assertion can be used with the row

R(s, z)  t(z)

to deduce the new row

s ≺_{w} a ∧ P (s)  t(f(s))

which introduces the recursive call f(s) into the output expression. The first conjunct (s ≺_{w} a) is the termination condition. This is an effective way to handle recursion for two reasons. First, the induction principle is well-founded induction (see §A), which allows the synthesis of any form of recursion that terminates. Second, the choice of well-founded relation w, and hence the form of recursion, need not be fixed at the time the recursive call is considered. It is possible to solve the condition on partial correctness (i.e. the conjunct P (s)) before considering the termination condition. Each recursive call in a synthesised program produces a goal for termination. If these goals are satisfiable, then at the end of the proof a relation can be chosen and the goals proved.

As an example, consider the inductive step used in synthesising a program to find the integer quotient of two numbers from the following specification.

div(n, d) ⇐ find q such that ∃ r. r < d ∧ r ≥ 0 ∧ n = q × d + r,
where n ≥ 0 ∧ d > 0

For simplicity, type conditions are omitted from the specification and from the following tableaux. They would appear in the logic as predicates, for example integer(n). The initial tableau is

assertions goals

output div(n, d)

n ≥ 0 ∧ d > 0

{∃ r. r < d ∧ r ≥ 0 ∧ \atop n = q × d + r}  q

After some arithmetic reasoning, the following row is added by transformation.

{∃ r. r < d ∧ r ≥ 0 ∧ \atop n − d = x × d + r}  x + 1

As this goal is an instance of the initial goal, it is appropriate to add an instance of the induction hypothesis, in which R has the form of the initial assertion and P has the form of the initial goal.

{⟨u, v⟩ ≺_{w} ⟨n, d⟩ ⊃ u ≥ 0 ∧ v > 0 ⊃ \atop ∃ r. r < v ∧ r ≥ 0 ∧ u = div(u, v) × v + r}

Applying resolution between the last two rows followed by some transformations gives

{⟨n − d, d⟩ ≺_{w} ⟨n, d⟩ ∧ \atop n − d ≥ 0 ∧ d > 0}  div(n − d, d) + 1

where the unifying substitution is

θ = {n − d/u, d/v, div(n − d, d)/x}

At this point, the relation w is uninstantiated. It is chosen so that the termination condition can be solved. Here, the less-than relation on the first component of the pairs is sufficient. The derivation is completed by further transformations and some case analysis by resolution, synthesising the program

div(n, d) ⇐ if n < d then 0 else div(n − d, d) + 1

Some guidance is provided by a polarity strategy, which restricts the use of resolution by insisting that a positive occurrence of one subsentence is used only with a negative occurrence of the other; and by a recurrence strategy, which determines when an induction hypothesis should be introduced.

Using this system by hand, programs have been synthesised from specifications for subtractive division [34], various forms of sorting [63], integer square root [36] and unification [35]. Some of the examples, notably unification, use forms of recursion that could not be easily handled by the primitive recursion rules of type theory. More recently, the deductive tableau system has been implemented by machine.

2.2 Type Theory

Many insights into formally reasoning about functional programs come from examining the relationship between programs and proofs in intuitionistic logic. Below, a type theory is introduced that closely resembles some versions of Martin Löf’s Type Theory, and its application to program derivation is considered.

A proposition is intuitionistically valid iff a proof of it can be given. The meanings of the logical connectives are given in terms of proofs. Heyting [26] gave an informal explanation along the following lines.

a proof of  consists of
⊥  –

A ∧ B a proof of A and a proof of B

A ∨ B a proof of A or a proof of B together with an indication of

which it is

A ⊃ B an operation that when applied to a proof of A yields a proof

of B

∀ x. B(x) an operation that when applied to an object a yields a proof

of B(a)

∃ x. B(x) an object a together with a proof of B(a)

Such a concrete notion of proof can be made more explicit by introducing a language of proof terms.

a proof of  has the form of
⊥  –

A ∧ B a pair ⟨a, b⟩, where a is a proof of A and b is a proof of B

A ∨ B either inl(a), where a is a proof of A, or inr(b), where b is a

proof of B

A ⊃ B a function lam x.b(x), where b(a) is a proof of B provided

that a is a proof of A

∀ x. B(x) a function lam x.b(x), where b(a) is a proof of B(a) for an

object a

∃ x. B(x) a pair ⟨a, b⟩, where a is an object and b is a proof of B(a)

As the meaning of a formula is given by its proof, a proposition can be identified with the type of all its proofs. This gives a correspondence between judgements of the form “a inhabits type A”, written a: A, and judgements of the form “a is a proof of A” known as the Curry-Howard isomorphism.

There is a correspondence between simple type theory and propositional logic, shown in the following table.

Proposition Type  Proof Term
canonical non-canonical
⊥  0  –
A ∧ B  A × B  ⟨a, b⟩  split(p, f)
A ∨ B  A + B inl(a),inr(b) when(p, f, g)
A ⊃ B  A → B lam x.b(x)  apply(f, a)

A proof of the proposition A ⊃ A ∨ B inhabits the type A → A + B, for example the term lam x.inl(x). Quantification requires indexed families of types, that is types of the form B(x) indexed by an object x of type A.

Proposition  Type  Proof Term
canonical non-canonical
∀ x∈A. B(x) Πx:A.B(x) lam x.b(x) apply(f, a)
∃ x∈A. B(x) Σx:A.B(x)  ⟨a, b⟩  split(p, f)

The type Πx:A.B(x) is the product of a family of types, each object of which is a function that applied to an object a of type A, yields an object of type B(a). The type Σx:A.B(x) is the sum of a family of types, each object of which is a pair ⟨a, b⟩, where a is an object of type A and b is an object of type B(a).

The non-canonical terms select information from proofs. Their meanings are given by the following implicit operational semantics.

• split is an operation that takes a term p and an operation f. If p yields the canonical term ⟨a, b⟩ then split yields the result of f(a, b), i.e. split(⟨a, b⟩ , f) ⇝ f(a, b).

• when is an operation that takes a term u and two operators f and g. If u yields the canonical term inl(a) then when yields the result of f(a), and if u yields the canonical term inr(b) then when yields the result of g(b), i.e. when(inl(a), f, g) ⇝ f(a) and when(inr(b), f, g) ⇝ g(b).

• apply is an operator that takes terms f and a. If f yields the canonical term lam x.b(x) then apply yields the result of b(a), i.e. apply(lam x.b(x), a) ⇝ b(a).

Under the interpretation of propositions-as-types, the proof rules of natural deduction correspond to rules of type inference. For example, the natural deduction rule ∧I corresponds to the type inference rule for pairing,

\frac{A  B}{A ∧ B}  \frac{a: A  b: B}{⟨a, b⟩: A × B}

and the rule ∧E corresponds to the type inference rule for split.

\frac{A ∧ B  \begin{aligned}[ & A ; B & ] \\ & C \end{aligned}}{C}  \frac{p: A × B  \begin{matrix}[ x: A ; y : B ] & x,y \\ c(x, y) : C \end{matrix}}{split(p, c) : C}

The notation [ ]_{x,y} binds the eigenvariables x and y in the inference x : A ∧ y : B ⟹ c(x, y) : C. It is described more fully in §3.1. There are also equality rules in type theory, reflecting the implicit operational semantics of the non-canonical terms.^{1} For example

a: A  b: B  \begin{matrix}[ x: A ; y : B ] & x,y \\ c(x, y) : C \end{matrix}
split(⟨a, b⟩ , c) = c(a, b) : C

For type theory to provide a useful framework for proof checking, it must be possible to check that a proof a actually proves A; the judgement a:A must be decidable when a is instantiated. Clearly, if a is unknown, then finding a proof of A is in general undecidable for anything beyond propositional reasoning. That a : A is decidable is a consequence of term reduction being Church-Rosser and strongly normalising. Type theory admits an interpretation of logic in which propositions correspond to types, proofs to terms and proof normalisation (cut elimination) to term reduction.

There is also an interpretation of type theory as a programming language. Terms and types represent the usual data structures; term reduction gives an operational semantics for the terms. The essential difference between this and a strongly typed functional language such as ML is that all terms of the type theory represent terminating programs.

It is natural to extend the purely logical type theory with inductive reasoning, either by encoding new inductive schemes into a general well-ordered type [49, Chapters 15 and 16], or by considering the theory as an open system to which axiomatisations of new types may be added [3]. For example, the type of natural numbers Nat has introduction rules for zero (zero) and successor (succ),

zero : Nat  \frac{n: Nat}{succ(n) : Nat}

and an elimination rule, which allows structural induction (in this case just mathematical induction).

n: Nat  b: B(zero)  \begin{matrix}[ x: Nat ; y : B(x) ] & x,y \\ c(x, y) : B(succ(x)) \end{matrix}
nrec(n, b, c) : B(n)

The non-canonical constant has reductions

nrec(zero, b, c) ⇝ b nrec(succ(n), b, c) ⇝ c(n, nrec(n, b, c))

corresponding to primitive recursion over Nat.

1These correspond to the reduction rules of Prawitz for natural deduction proofs [57].

The judgement a: A can be read in three ways

• a inhabits type A,

• a is a proof of proposition A, or

• a is a program satisfying specification A.

An algorithm can be derived as the constructive proof of the proposition

∀ x∈A. ∃ y ∈B. C(x, y)

where C(x, y) specifies the relation between input and output. A term inhabiting the corresponding type has the form

lam x. ⟨b, p⟩ : Πx:A.Σy:B.C(x, y)

which is a function from an object a: A to a pair ⟨b, p⟩ in which b is the desired result and p is a proof that C(a, b) holds.

Type theory is a good approach to formal reasoning about functional programs, as it reveals the similarities between programs and proofs. Branching in a program is reasoned about using case analysis, and recursion using induction. For the type theory described above, the two are combined; primitive recursion in programs corresponds to structural induction in proofs. Moreover, there is a single rule for each program term-former, making it simple to direct a proof with a program template. For the theory presented above, this is a trivial observation since programs are identified with proofs. It becomes more interesting when a distinction is made between proofs and programs.

Dependent types allow the input/output behaviour of programs to be easily expressed in specifications. Assume a subtype type-former. For some program f, a predicate of the form

∀ x. P (x) ⊃ Q(x, f(x))

is expressed as

f : Πx:{x:A, P (x)}.{y:B, Q(x, y)}

Without dependent types, specifications become slightly longer and more clumsy,

f : {u:{x:A, P (x)} →B, ∀ x:A.P (x) ⊃ Q(x, u(x))}

which is awkward when they are used as hypotheses for recursive calls.

But there are complications to this approach. Terms are used on the one hand to represent proofs, and on the other to represent programs. Giving two distinct roles to one object is not ideal; a proof object necessarily contains a complete justification of a proposition, whereas a program need contain only the algorithm for computing the result. For a programming language, reduction should be determinant and terminating under a particular strategy. The stronger conditions of Church-Rosser and strong normalisation, necessary for a term to act as a proof object, are too restrictive. Strong normalisation leads to a restricted form of recursion—primitive recursion. Although primitive recursion allows all feasible computations to be expressed, for example the encoding of Ackermann’s function as a primitive recursive function of higher type (a functional) by Nordström [47], it does not provide a style that is at all practical for programming (see §2.4).

For program derivation, type theory needs to be adapted to

• remove computationally uninteresting information from program terms, and

• provide general forms of recursion.

Computationally uninteresting information can be discarded by extracting programs from completed proofs. This is the basis of the work done in the Calculus of Constructions (see §2.3). Alternatively, subtyping can be used to discard the redundant information as a term is constructed.

A subset type-former can be introduced with the following introduction and elimination rules.

\frac{a: A B(a) true}{a: \{x:A, B(x)\}}

\frac{a: \{x:A, B(x)\}}{a: A}  \frac{a: \{x:A, B(x)\}}{B(a) true}

But this does not easily fit together with the notion of propositions-as-types. For the subset construct to work properly, a distinction must be made between propositions and types [59].

Paulson [52] describes an attempt to handle recursion schemes other than primitive recursion by describing well-founded relations in type theory. Nordström [48] presents a notion of elements of A accessible through a relation ≺, Acc(A, ≺). The relation ≺ is wellfounded with respect to A if Acc(A, ≺) is equal to A. This provides a rule of well-founded induction, with a proof term rec(e, p) in which e is the body of the recursion and p is the initial value.

Despite its limitations and the awkward style of reasoning, Martin Löf’s Type Theory has been used for program derivation. In particular, Chisholm describes a machine checked derivation of a simple parsing algorithm [8].

2.3 Calculus of Constructions

Paulin developed a variant of the Calculus of Constructions [13] in which programs of F_{ω} may be extracted from proofs [50].

F_{ω} is a higher-order extension of the simply typed lambda calculus [19]. As well as terms and types, there is an additional level of orders. Types that inhabit the order Data are called data types. Terms that inhabit data types are called programs. All well-typed terms are strongly normalising. The usual data types are definable, but with iteration in place of primitive recursion. For example, instead of the primitive recursor for natural numbers, nrec, defined such that

nrec 0 t u  ⇝ t
nrec S(n) t u ⇝ u n (nrec n t u)

there is an iterator, nit, defined such that

nit 0 t u  ⇝ t
nit S(n) t u ⇝ u (nit n t u)

Although recursion may be encoded using iteration, this is very inefficient. For example, an iterative predecessor function on the natural numbers would decompose its argument to 0, and then construct a result with one fewer S nodes.

The Calculus of Constructions (CoC) is an impredicative higher-order lambda-calculus with dependent types, which has been used to formalise and check mathematical reasoning. F_{ω} is the part of CoC in which types are not dependent on terms. For reasoning about programs of F_{ω} in CoC, it is convenient to distinguish the program types (Data) from the propositions, and to further distinguish the informative propositions (Spec) from the noninformative ones (Prop). Informative propositions have computational content, and their proofs contain programs; non-informative propositions have only a ‘logical’ content, and their proofs should be discarded. Here too, propositions are separated from types, which allows subsets to be expressed, and additional axioms to be realised without producing an inconsistent environment.

Paulin uses a variant of CoC, the Calculus of Constructions with Realisations. The notion of realisability gives an internalisation of the computational meaning of proofs; it captures the idea of extraction in a precise and systematic way. For each proposition A, there is a realisability predicate λx . R(A, x). If the judgement t : A is derivable, then there is a proof of R(A, t′) where t′ is the program extracted from proof t. The extraction function, t′ = E(t), is inductively defined over the structure of terms. It removes the noninformative parts of the term and all type dependencies to produce a program term of F_{ω}. The relation between extraction and realisability is illustrated by the following picture.

[figure: ⊢ t ∈ M ∈ Spec; E; R; ⊢ E(t) ∈ E(M) ∈ Data; ⊢ u ∈ R(M, E(t))]

Furthermore, if there exists a term u such that R(A, u) is derivable, then u is said to realise A and A is consistent in the theory. If the axiom ax:A is added to the theory, then ax may appear in extracted terms. A reduction strategy is needed for ax, for which it is correct to replace ax by u in a program. This allows an axiom of well-founded induction to be added to the theory with a proof term that provides general recursion.

2.4 Comments

This dissertation is largely influenced by the work described above. But it should be noted that, despite initial appearances, classical logic is not incompatible with a computational logic, even when based on type theory. Taking a type theoretic approach to program correctness leads naturally to a system in which propositions and their proofs are distinguished from program types and their programs. Once this is done, propositional reasoning can be made classical (by adding a suitable axiom and a non-constructive proof term), whilst the program type system remains constructive. Moreover, though insufficient to represent propositions, sets can be used to represent program types, which allows the use of subsets, fixed points, etc. Similarly in CCL, the logical system is classical first-order logic (though not based on type theory), and the program type system is constructive (and types are just sets).

General recursion is essential for a programming language to be practical. Although primitive recursive functionals allow all feasible computations to be expressed, they do not always allow the most natural or efficient algorithm. Hoare’s algorithm for quicksort is a familiar example that illustrates this point. Assume partition functions les x xs and gts x xs that return the elements of xs that are less-than or equal to x and greater than x respectively. Quicksort can be defined in ML by

    fun qsort [] = []
      | qsort (x::xs) = (qsort (les x xs)) @ x::(qsort (gts x xs));

In ML, the primitive recursive encoding is

    fun qsort l =
       let fun qsortx 0 l = []
             | qsortx n [] = []
             | qsortx n (x::xs) = (qsortx (n-1) (les x xs))
                                  @ x::(qsortx (n-1) (gts x xs))
       in qsortx (length l) l end;

Clearly, this is unsatisfactory. Apart from its awkwardness, the encoding is inefficient; executing an application of the primitive recursive version of quicksort evaluates the measure function length l (a completely wasted computation) as well as sorting the list. Similarly, a primitive recursive function to find the next prime after some given integer must calculate an upper bound on the prime before searching for it.

For every terminating program, a well-founded relation can be found that orders the successive recursive calls. Well-founded induction can, therefore, be used as a general scheme for reasoning about recursion. A suitable proof rule is described by Paulson in the context of Martin-Löf’s Type Theory [52]. Furthermore, with a single proof rule, the choice of recursion scheme (i.e. the instantiation of the well-founded relation) can be postponed to a later stage in a proof. For correctness proofs to be directed by algorithms this is essential; the form of recursion is not fixed at the outermost level of a function declaration, but at the points at which recursive calls are made. Manna and Waldinger’s work on program synthesis uses well-founded induction in this way. By delaying the choice of well-founded relation until the end of a proof, partial correctness and termination can be separated—a technique practised since the advent of Floyd-Hoare logic.

The Theory CCL

CCL is a classical logic for reasoning about terminating, general recursive, functional programs. The theory is presented as a natural deduction calculus and given meaning in a meta-language based on set theory, described in §3.1.

CCL contains an untyped, target programming language L, described in §3.2. Programs in L are represented by their abstract syntax trees; and execution is defined by an Evaluation Semantics—a set of rules in the style of Natural Semantics [31, 44], a refinement of Structural Operational Semantics [56]. In §3.3, an observational equivalence is defined between programs (similar to applicative bisimulation [1] and observational congruence [43]). Two programs are equivalent in this sense if they evaluate to normal forms, which have the same outermost constructor and whose components are equivalent. Observational equivalence is proved to be a congruence relation over the term-formers of L. It can, therefore, be used as an equality relation over equivalence classes of programs, and the term-formers can be lifted up to equivalence classes in the obvious way.

In §3.4, types are inductively defined as sets of equivalence classes of terminating programs. There is a universe of types; arbitrary subsets can be considered, and inductive types represented using a fixed point. Well-founded orderings, introduced in §3.5, are used to ensure termination over general schemes of recursion. They are built from a set of defined constructors, so that well-foundedness is just a well-formedness condition.

CCL includes the connectives of first-order logic. §3.6 describes the complete logic, and §3.7 presents a result about the strength of CCL. The theory is constructed from objects of the following syntactic categories.

• ι_{=} are equivalence classes of programs,

• τ are types of programs,

• ω are orderings well-founded over ι_{=}, and

• o are formulae.

Formulae are those of classical first-order logic, with quantification over terms (ι_{=}) and types (τ), together with the following predicates.

• a: A, the membership relation on types,

• a = b, an overloaded equality between terms and between types,

• a ≺_{R} b, the membership relation on well-founded orderings, and

• Mono(f), which holds iff the function f from types to types is monotonic.

3.1 Meta-Theoretic Conventions

The metalanguage, used to specify the syntax of object-level expressions and give meaning to inference rules, is developed within ZF set theory. As in higher-order logic, it includes a simply typed λ-calculus over a given set of ground types G, with terms identified up to αβη-conversion. To avoid confusion with the object-level, types of the metalanguage are called meta-types. In addition to the basic forms, constants may be defined so that the syntax of meta-terms is

e ::= x | c | λx.e | e(e′)

where x is a meta-variable, c is a constant, λx . e denotes meta-abstraction and e(e′) meta-application. Multiple abstractions λx_{1}. λx_{2}…. e are written as λx_{1} x_{2} …. e, and multiple applications e(e_{1})(e_{2}) … as e(e_{1}, e_{2}, …). Meta-types are constructed over the set of ground types G using ⇒ for meta-level function space.

s ::= s_{g} | s⇒s′ where s_{g} ∈ G

Meta-type inhabitation is just set membership, written e ∈ s. There are the usual typing rules for abstraction and application, so that meta-level abstraction provides a uniform notation for variable binding in the syntax of object languages. Meta-types correspond to meta-types in the Isabelle implementation (see §4.1). The explicit use of set theory to give a semantics to CCL (e.g. Definition 3.2) is not required in the Isabelle implementation, which is just an axiomatisation of CCL.

Rules of an object theory are presented in a natural deduction style, including the use of hypothetical hypotheses [61]. As illustration, the following rules are taken from the first-order logic of §3.6.

\frac{P Q}{P ∧ Q}

states that for all P and Q, P ∧ Q holds if the premises P and Q both hold. The following rule is hypothetical.

\frac{∃ x. P (x) \begin{matrix}[ P (x) ] & x \\ Q \end{matrix}}{Q}

It states that if ∃ x. P (x) holds, and P (x) implies Q for all x, then Q holds. The brackets […]_{x} indicate that the eigenvariable x is bound in the inference P (x) implies Q, and cannot occur free in any other assumptions. When no hypothesis is present, eigenvariables annotate an overscore, for example

\frac{P (x)^{x}}{∀ x. P (x)}

The following rule has a hypothetical hypothesis.

\frac{P ↔ Q \begin{aligned}[ & \begin{matrix}[ Q] \\ P \end{matrix} ; \begin{matrix}[ P ] \\ Q \end{matrix} & ] \\ & R \end{aligned}}{R}

It states that R holds if P ↔ Q holds and if Q implies P and P implies Q then R holds. Hypothetical hypotheses can be annotated with eigenvariable conditions in the same way as hypotheses.

Logical equivalence at the meta-level (≡) is used for definitions. For example, the definition of ↔ in first-order logic is

P ↔ Q ≡ (P ⊃ Q) ∧ (Q ⊃ P)

Before the logical connectives of CCL are introduced in §3.6, the symbols ∀, ∃, ∧, ∨, ¬, ⟹ and ↔ are used for the meta-logical connectives.

3.2 An Untyped Functional Language

This section describes the syntax and operational semantics of the untyped functional programming language L. The language L can be regarded as an untyped λ-calculus sugared with constants for finite enumerations, pairs, general recursion and local declarations. The additional syntax allows an evaluation strategy to be defined for L, and the subsequent imposition of a typing regime (see §3.4). Terms of the programming language L are represented by their abstract syntax trees; the meta-type ι is the set of all such terms. Constants of L are meta-functions over terms, and so the well-formedness of terms is ensured by the meta-type system.

First, the syntax of L is introduced, together with an informal description of the possible reductions. Then, an operational semantics is presented that embodies one particular evaluation strategy. Determinacy and termination are defined with respect to this semantics.

3.2.1 Syntax

Following the traditional functional programming parlance of McCarthy [41] and Landin [32], the term-formers of L are introduced in two groups: constructors, which build terms of particular structure; and destructors, which break up terms built by particular constructors.

Finite enumerations are constructed from the base term z ∈ ι and the successor termformer s ∈ ι ⇒ ι, for example z, s(z) and s(s(z)). Functions are constructed using the term-former lam ∈ (ι ⇒ ι) ⇒ ι, and pairs using ⟨⟩ ∈ ι ⇒ ι ⇒ ι. Write lam(λx.b(x)) as lam x.b(x), and ⟨⟩(a, b) as ⟨a, b⟩.

Each destructor reduces particular terms. As an informal motivation, these reductions are described using the relation ⇝. The term vcase ∈ ι does not reduce any term; it corresponds to an abort.^{1} The term-former scase ∈ ι ⇒ ι ⇒ (ι ⇒ ι) ⇒ ι reduces terms formed by z or s.

scase(z, b, c) ⇝ b
scase(s(a), b, c) ⇝ c(a)

The term-former pcase ∈ ι⇒((ι⇒ι)⇒ι)⇒ι reduces terms formed by lam.

pcase(lam x.b(x), c) ⇝ c(b)

1The destructors are named according to their corresponding type-formers, introduced in §3.4.

Reduction of lam, using pcase, follows the pattern of reduction for the other constructors; it is more general than that for function application (cf. the destructor funsplit in Martin-Löf’s Type Theory [49]). In particular, pcase allows an induction rule (η-rule) to be derived (see §4.2.1). The term-former split ∈ ι⇒(ι⇒ι⇒ι)⇒ι reduces terms formed by ⟨⟩.

split(⟨a, b⟩ , c) ⇝ c(a, b)

These four destructors behave similarly to pattern matching in ML; compare the term split(p, λx y.c(x, y)) with the ML code

            case p of <x,y> => c(x,y);

But the destructors of L are cruder than pattern matching in ML; they each match terms of only one data type, and every case must be considered. In addition to destructors for case analysis, two further destructors are introduced for recursion and local declarations. The term-former rec ∈ ι⇒(ι⇒(ι⇒ι)⇒ι)⇒ι reduces any term.

rec(a, h) ⇝ h(a, λx.rec(x, h))

It allows general recursion to be expressed; the term rec(a, λx g.h(x, g)) corresponds to the ML code

            let fun g(x) = h(x,g) in g(a) end;

Finally, the term-former let ∈ ι ⇒ (ι ⇒ ι) ⇒ ι introduces local definitions and forces the immediate evaluation of a term. Write let(a, λx.b(x)) as let x be a in b(x) end.

\frac{a ⇝ a′}{let x be a in b(x) end ⇝ b(a′)}

Write CON for the set of constructors {z, s, lam, ⟨⟩}, and DES for the set of destructors {vcase, scase, pcase, split, rec, let}.

3.2.2 Evaluation

The transition semantics informally described by ⇝ gives an intuition for the destructors. Now, an Evaluation Semantics (Natural Semantics) is formally presented for L. Programs are closed terms^{2} of L. Evaluation is defined as a particular strategy for reducing programs to canonical form.

Definition 3.1 A closed term of L is canonical iff it has one of the following forms

z  s(a)  lam x.b(x)  ⟨a_{1}, a_{2}⟩

for any terms a and meta-functions b.

Definition 3.2 The evaluation relation ▷ ∈ ι ⇒ ι ⇒ o is defined as the least relation satisfying the rules of Figure 3.1.

2As usual, closed terms are those in which no variable occurs free.

z ▷ z  s(a) ▷ s(a)

lam x.b(x) ▷ lam x.b(x)  ⟨a, b⟩ ▷ ⟨a, b⟩

\frac{u ▷ z  v ▷ a}{scase(u, v, w) ▷ a}  \frac{u ▷ s(a)  w(a) ▷ b}{scase(u, v, w) ▷ b}

\frac{u ▷ lam x.b(x)  v(b) ▷ a}{pcase(u, v) ▷ a}  \frac{u ▷ ⟨a, b⟩  v(a, b) ▷ c}{split(u, v) ▷ c}

\frac{v(u, λx.rec(x, v)) ▷ a}{rec(u, v) ▷ a}  \frac{u ▷ a  v(a) ▷ b}{let x be u in v(x) end ▷ b}

Figure 3.1: Evaluation Rules for L

In L, function application is a derived form. Call-by-name ‘ ∈ ι ⇒ ι ⇒ ι and call-by-value application ˆ ∈ ι⇒ι⇒ι are defined by

f ‘ a ≡ pcase(f, λx.x(a))
f ˆ a ≡ let x be a in f ‘ x end

For call-by-value, let forces the immediate evaluation of a. From these definitions, the following evaluation rules are derived.

\frac{u ▷ lam x.b(x)  b(v) ▷ a}{u ‘ v ▷ a} ; \frac{u ▷ lam x.b(x)  v ▷ a  b(a) ▷ c}{u ˆ v ▷ c}

In keeping with a lazy regime, only the call-by-name form (‘) is used.

The definition of ▷ provides a Prolog-style interpreter for L; evaluating a program t to canonical form a corresponds to proving the theorem t ▷ a by depth-first search over the evaluation rules. If a is initially uninstantiated, then it will become instantiated during the proof.

For a fixed evaluation strategy, there is no need of theorems for confluence (Church-Rosser) and strong normalisation. Instead, determinacy and termination are considered. If a program can be evaluated to canonical form, then there is a unique result and a unique derivation.

Theorem 3.1 (Determinacy) For any program t and canonical terms a and a′, if t ▷ a and t ▷ a′ then a and a′ (and their derivations) are identical.

Proof: By rule induction over the evaluation rules of Figure 3.1. Operators for which there is only one rule obviously preserve determinacy. For scase, the induction hypothesis ensures that at most one of the two rules is applicable as the premises u ▷ z and u ▷ s(a) are mutually exclusive.

In L, the evaluation of program t to canonical form a corresponds to the derivation ⊢ t ▷ a. Attempting to evaluate a program that fails to terminate either reaches a noncanonical term that cannot be reduced (e.g. vcase), or leads to a derivation that also fails to terminate. Write t↓ iff program t terminates.

Definition 3.3 (Termination) For any program t, t↓ iff ∃ a∈ι. t ▷ a

Clearly, not all programs terminate. Consider the following terms.

vcase  split(z, λx y.x)  rec(a, λx g.g(x))

and the paradoxical combinator

Ω ≡ lam x.(x ‘ x) ‘ lam x.(x ‘ x)

3.3 Term Equality

To reason about programs conveniently, a type-less equality is required that reflects the operational semantics, capturing our intuitive notion of when programs are the same. For a lazy regime, applicative bisimulation is an appropriate relation [1].

A pre-order ≼ is defined over terms, and term equality = is defined as the free equivalence generated by ≼. Using results from Howe [28], the equivalence relation is shown to be a congruence.

3.3.1 A Pre-Order Over Terms

The arity of a meta-function f, written α(f), is the sequence of meta-types of its arguments (e.g. α(split) is [ι, ι ⇒ ι ⇒ ι]). Write \overline{x} for a possibly empty sequence of arguments. For a relation R over terms, write \overline{x}R\overline{x}′ for sequences of equal length, when the relation R holds pointwise over the arguments in each sequence; and write f Rf′ for meta-functions f and f′ of the same arity, when the relation R holds for all applications (i.e. ∀ \overline{x}∈α(f). f(\overline{x})Rf′(\overline{x})).

Term equality is defined using the pre-order ≼ ∈ ι ⇒ ι ⇒ o. Informally, t ≼ t′ iff t fails to terminate or t and t′ evaluate to terms with the same outermost constructor and components \overline{x} and \overline{x}′ for which \overline{x} ≼ \overline{x}′. Formally, the relation is defined as the greatest fixed point of the function [·], defined over relations as follows.

Definition 3.4 [·] is a mapping over term relations such that for all relations R defined over closed terms and for all terms t and t′

t [R] t′ iff ∀ c∈CON . ∀ \overline{x}∈α(c). t ▷ c(\overline{x}) ⟹ (∃ \overline{x}′ ∈α(c). t′ ▷ c(\overline{x}′) ∧ \overline{x} R \overline{x}′)

The function [·] is monotonic (i.e. ∀ R R′. R ⊆ R′ ⊃ [R] ⊆ [R′]), so that by the Knaster-Tarski Theorem [15] there is a greatest fixed point given by the following definition.

Definition 3.5 ≼ ≡ ⋃{ R over closed terms | R ⊆ [R] } Therefore, for all closed terms t and t′

t ≼ t′ iff ∀ c∈CON . ∀ \overline{x}∈α(c). t ▷ c(\overline{x}) ⟹ (∃ \overline{x}′ ∈α(c). t′ ▷ c(\overline{x}′) ∧ \overline{x} ≼ \overline{x}′)

Theorem 3.2 ≼ is a pre-order.

Proof:

• Reflexivity (t ≼ t): The identity relation (syntactic equality ≡) is contained in ≼, since ≡ ⊆ [≡].

• Transitivity (t ≼ u ∧ u ≼ v ⟹ t ≼ v): Let ∘ represent relational composition. To prove that ≼ is transitive, it suffices to prove [R] ∘ [S] ⊆ [R ∘ S] for all relations R and S, since this implies (≼ ∘ ≼) ⊆ ≼. So, prove t [R ∘ S] v assuming t ([R] ∘ [S]) v, that is there exists u such that

t [R] u  and  u [S] v (1)

By the definition of [·], if t fails to terminate then t[R ∘ S]v trivially holds, otherwise (1) implies that u terminates which in turn implies that v terminates and for some c ∈ CON

t ▷ c(\overline{x})  and  u ▷ c(\overline{x}′)  and  \overline{x} R \overline{x}′ (2)
u ▷ c(\overline{x}′)  and  v ▷ c(\overline{x}′′)  and  \overline{x}′ S \overline{x}′′ (3)

The term c(\overline{x}′) is common to both since evaluation is unique. Therefore,

t ▷ c(\overline{x})  and  v ▷ c(\overline{x}′′)  and  \overline{x} (R ∘ S) \overline{x}′′ (4)

and so t [R ∘ S] v.

Although ≼ is defined by propagating evaluation through the constructors, this is done in a pointwise fashion so that ≼ is stronger than the corresponding definition for an eager evaluation scheme ≼_{e}. For example, consider

⟨Ω, z⟩ ⋠ ⟨Ω, s(z)⟩  but  ⟨Ω, z⟩ ≼_{e} ⟨Ω, s(z)⟩

Moreover, t ≼ t′ does not imply that the terms t and t′ have the same canonical form. Consider the following distinct canonical terms, which satisfy the relation.

⟨lam x.x ‘ z, z⟩ ≼ ⟨z, z⟩

However, if t ≼ t′ holds for a program t that terminates, then t′ also terminates and the two canonical forms have the same outermost constructor.

Theorem 3.3 For all closed terms t and t′, if t ≼ t′ then t↓ implies t′ ↓.

Proof: As t terminates, the definition of ≼ implies that there exists a term a′ such that t′ ▷ a′, that is t′ terminates.

The relation ≼ is shown to be a congruence. Howe [28] proved that if an extensionality condition holds for each of the operators of a lazy computation system, then the equivalence relation is a congruence. This result is directly applicable to all the operators of L except rec. The proofs of extensionality closely follow the examples presented by Howe and so are not given here.

Theorem 3.4 For all closed meta-functions f and closed sequences \overline{x}, \overline{x}′ such that f(\overline{x}) and f(\overline{x}′) are well-formed, closed terms

\overline{x} ≼ \overline{x}′ ⟹ f(\overline{x}) ≼ f(\overline{x}′)

Proof: For the operators

z, s, lam, ⟨⟩, scase, pcase, split, let

the proof of congruence follows the details of Howe [28]. For each, the extensionality condition is proved (in the same way as the examples presented by Howe) and congruence then inferred.

The evaluation rule for rec is not suited to this approach. Instead, congruence for rec is proved directly, that is

a ≼ a′ ∧ h ≼ h′ ⟹ rec(a, h) ≼ rec(a′, h′)

If rec(a, h) fails to terminate this holds immediately. Otherwise

∃ d. rec(a, h) ▷ d in k steps

By induction on the length of the evaluation, assume

rec(x, h) ≼ rec(x, h′)

holds for all rec(x, h) that evaluate in < k steps. From the evaluation rule for rec, rec(a, h) ≼ rec(a′, h′) holds if

(∗) h(a, λx.rec(x, h)) ≼ h′(a′, λx.rec(x, h′))

Either rec(x, h) is not evaluated in the execution of h(a, λx.rec(x, h)) in which case its value is irrelevant and (∗) holds, or rec(x, h) ▷ e in under k steps, rec(x, h) ≼ rec(x, h′) follows from the induction hypothesis and again (∗) holds.

3.3.2 An Equivalence Over Terms

The infix relation = ∈ ι ⇒ ι ⇒ o is defined as the free equivalence generated by the pre-order ≼.

Definition 3.6 For all closed terms t and t′, t = t′ iff t ≼ t′ ∧ t′ ≼ t.

Theorem 3.5 (Equivalence) = is an equivalence relation.

Proof: As ≼ is a pre-order, it immediately follows that = is reflexive, transitive and symmetric.

The meta-type ι_{=} is defined as the set of equivalence classes of terms (ι) under this relation.

Definition 3.7 ι_{=} is the set ι/=

As with ≼, the relation = does not respect canonical forms. The termination and congruence results for ≼ are symmetric and so carry over to =.

Theorem 3.6 (Termination) For all closed terms t and t′, if t = t′, then t↓ iff t′ ↓.

Theorem 3.7 (Congruence) For all closed meta-functions f and closed sequences \overline{x}, \overline{x}′ such that f(\overline{x}) and f(\overline{x}′) are well-formed, closed terms

\overline{x} = \overline{x}′ ⟹ f(\overline{x}) = f(\overline{x}′)

The definition of ≼, and therefore that of =, reflect the evaluation of terms. Conversion rules can be derived that correspond to transitions in the operational semantics. For the destructor let, a conversion rule is derived only for terminating arguments.

Theorem 3.8 (Conversion) For all terms and meta-functions a, b, c, h the following conversions hold for well-formed, closed terms.

• scase(z, b, c) = b

• scase(s(a), b, c) = c(a)

• pcase(lam x.b(x), c) = c(b)

• split(⟨a, b⟩ , c) = c(a, b)

• rec(a, h) = h(a, λx.rec(x, h))

• a↓ ⟹ let x be a in b(x) end = b(a)

Proof: By the definition of equality, the formula a = b holds iff a ≼ b and b ≼ a. In each case, if the left-hand side fails to terminate, then the relation trivially holds; otherwise there exists a unique derivation. Except for the rule for let, evaluation is lazy and the conversions are simple to prove. Three of the twelve cases are illustrated.

• pcase(lam x.b(x), c) ≼ c(b)

There exists a derivation for the evaluation of the left-hand side that concludes with

\frac{lam x.b(x) ▷ lam x.b(x) c(b) ▷ a}{pcase(lam x.b(x), c) ▷ a}

for some a. Therefore,

pcase(lam x.b(x), c) ▷ a  and  c(b) ▷ a  and  a ≼ a

• c(b) ≼ pcase(lam x.b(x), c)

There exists a unique canonical form a for the left-hand side

c(b) ▷ a

By the evaluation rule for pcase, c(b) ▷ a and lam x.b(x) ▷ lam x.b(x) imply

pcase(lam x.b(x), c) ▷ a

• a↓ ⟹ b(a) ≼ let x be a in b(x) end

There exists a unique canonical form c for the left-hand side

b(a) ▷ c

From the premise a↓, there exists a term a′ such that

a ▷ a′

This implies a ≼ a′ which in turn implies b(a) ≼ b(a′) by the congruence result for ≼ (Theorem 3.4). Therefore, there exists a term c′ such that

b(a′) ▷ c′  and  c ≼ c′

By the evaluation rule for let, this implies

let x be a in b(x) end ▷ c′

Theorems 3.6, 3.7 and 3.8 are proved for term equality defined over closed terms. Now the definition of equality is extended to open terms in a uniform way.

Definition 3.8 For all open terms t and t′, t = t′ iff for all substitutions σ such that σ(t) and σ(t′) are closed σ(t) ≼ σ(t′).

It is straightforward to carry through the results for termination, congruence and conversion to open terms.

3.4 Types for L

As term equality (=) is a congruence relation over the term-formers of ι (Theorem 3.7), the elements of ι_{=} can be considered as values, and the term-formers of ι lifted up to term-formers of ι_{=}. The symbols z, s, lam, ⟨⟩, vcase, scase, pcase, split, rec and let are now used as the corresponding term-formers for ι_{=}.

Types are sets of equivalence classes of terminating programs. They formalise the observation that terminating programs evaluate to finite enumerations, functions and pairs; and allow inductive reasoning over the structure of programs. For products and functions, generalised (dependent) type-formers are used, as these allow a fine grain treatment of termination, and are convenient for specifying input/output behaviour (see §1.3). Inductive types are defined as least fixed points of monotonic functions; the predicate Mono formalises monotonicity for meta-functions τ ⇒ τ. Two destructors (scase and split) are defined for types in such a way that they behave as their namesakes for terms.

First, the syntax of types is presented with informal descriptions. Then, the typeformers are defined. Finally, predicates are defined for type inhabitation (a:A), the monotonicity of meta-functions (Mono(λX .B(X))) and type equality (A = B)—overloading the symbol =, which is already used for equality between terms.

3.4. Types for L 29

3.4.1 Syntax

Finite enumeration types are constructed from the empty (void) type V ∈ τ and the successor type-former S ∈ τ ⇒ τ, for example V, S(V) and S(S(V)) are the types of zero, one and two elements respectively. Generalised functions are constructed using the typeformer Π ∈ τ ⇒(ι_{=} ⇒τ)⇒τ, and generalised products using Σ ∈ τ ⇒(ι_{=} ⇒τ)⇒τ. Write Π(A, B) and Σ(A, B) as Πx:A.B(x) and Σx:A.B(x), and when there is no dependency as A →B and A × B respectively. Elements of a general function type are functions, for which the type of the codomain depends on the value to which the function is applied; elements of a general product type are pairs, for which the type of the second element depends on the value of the first. Inductive types are constructed as least fixed points of meta-functions over types, using the type-former μ ∈ (τ ⇒ τ) ⇒ τ and the predicate Mono ∈ (τ ⇒ τ) ⇒ o. Write μ(λX .B(X)) as μ X . B(X). Finally, arbitrary subtypes are constructed using the type-former {} ∈ τ ⇒ (ι_{=} ⇒ o) ⇒ τ. Write {}(A, λx.P (x)) as {x:A, P (x)}.

Two destructors are introduced that reduce to types rather than terms (note the overloading with the destructors for terms).

scase ∈ ι_{=} ⇒τ ⇒(ι_{=} ⇒τ)⇒τ
split ∈ ι_{=} ⇒(ι_{=} ⇒ι_{=} ⇒τ)⇒τ

3.4.2 Types and Type-Formers

Types are defined as sets of equivalence classes of terminating terms. The meta-type τ is the set of all types.

Definition 3.9 τ ≡ { A ∈ P(ι_{=}) | ∀ x∈A. x↓ }

where P(A) is the power set of A. The definition make sense because term equality respects termination (Theorem 3.3), and so the predicate ↓ can be lifted up to equivalences classes of terms (ι_{=}). The following two theorems are immediate consequences of this definition.

Theorem 3.9 For all A and B such that B ⊆ A, A ∈ τ implies B ∈ τ.

Theorem 3.10 For all terms a and types A, a ∈ A implies a↓.

Definition 3.10 The type-formers are defined as follows.

V ≡ ∅
S(A) ≡ {t ∈ ι_{=} | t = z ∨ (∃ a. t = s(a) ∧ a ∈ A) }
Π(A, B) ≡ {t ∈ ι_{=} | ∃ b. t = lam x.b(x) ∧ ∀ x. x ∈ A ⟹ b(x) ∈ B(x) }
Σ(A, B) ≡ {t ∈ ι_{=} | ∃ a b. t = ⟨a, b⟩ ∧ a ∈ A ∧ b ∈ B(a) }
μ X . B(X) ≡ ⋂{X ∈ τ | B(X) ⊆ X }
{x:A, P (x)} ≡ {x ∈ A | P (x) }

where set intersection is the meet operation on the complete poset (τ, ⊆). Note that the quantifiers in the above definitions are part of the meta-logic. In particular, the variable 30 Chapter 3. The Theory CCL

b in the definition of Π is of meta-type ι_{=} ⇒ι_{=}. From these definitions, the meta-types for the type-formers described above are proved. Theorem 3.11 The type-formers have the following meta-types

• V ∈ τ

• S ∈ τ ⇒τ

• Π ∈ τ ⇒(ι_{=} ⇒τ)⇒τ

• Σ ∈ τ ⇒(ι_{=} ⇒τ)⇒τ

• μ ∈ (τ ⇒τ)⇒τ

• {} ∈ τ ⇒(ι_{=} ⇒o)⇒τ Proof: The empty set V is clearly a member of τ. For the type-formers S, Π and Σ, their definitions imply that all members are equal to a canonical term, and therefore terminate (Theorem 3.6). For the type-former {}, every subset of a type is a type (Theorem 3.9), so A ∈ τ implies {x:A, P (x)} ∈ τ. For the type-former μ, the set of types (τ) is closed under arbitrary subsets, and therefore under intersection so that μ(B) ∈ τ.

3.4.3 Predicates for Types

Predicates are defined for monotonicity, type equality and type inhabitation. From the definitions, rules are derived for reasoning about the predicates.

The predicate Mono(f) holds iff the meta-function f ∈ τ ⇒τ is monotonic. Definition 3.11 Mono(f) iff ∀ x y ∈τ . x ⊆ y ⟹ f(x) ⊆ f(y) Type equality (= ∈ τ ⇒ τ ⇒ o) is just set equality. The destructors for types are defined to satisfy the same conversion rules as their namesakes for terms. Definition 3.12

scase(a, B, C) ≡ {x ∈ τ | (a = z ∧ x = B) ∨ (∃ y. a = s(y) ∧ x = C(y)) }
split(p, C) ≡ {x ∈ τ | ∃ a b. p = ⟨a, b⟩ ∧ x = C(a, b) }

Type inhabitation is set membership. Definition 3.13 a: A iff a ∈ A

Mono(λX .X)  Mono(λX .A)

\frac{Mono(λX .A(X))}{Mono(λX .S(A(X)))}  \frac{\begin{matrix}[ x: A ] & x \\ Mono(λX .B(X, x)) \end{matrix}}{Mono(λX .Π(A, B(X)))}

\frac{Mono(λX .A(X))  \begin{matrix}[ x: A(X) ] & x,X \\ Mono(λX .B(X, x)) \end{matrix}}{Mono(λX .Σ(A(X), B(X)))}  \frac{Mono(λX .A(X))}{Mono(λX .\{x:A(X), P (x)\})}

Figure 3.2: Monotonicity Rules for CCL

Theorem 3.12 (Monotonicity) The monotonicity rules of Figure 3.2 are derivable.

Proof: From the definition of Mono, it immediately follows that the identity function λX .X and the constant function λX .A are monotonic. The other rules follow from the definitions of the type-formers. For example,

• Prove that X ⊆ Y ⟹ Π(A, B(X)) ⊆ Π(A, B(Y)) for all X, Y ∈ τ, assuming

∀ x∈A. ∀ X Y ∈τ . X ⊆ Y ⟹ B(X, x) ⊆ B(Y, x) (1)

It suffices to prove that for an arbitrary element a : Π(A, B(X)) it follows that a: Π(A, B(Y)). From the definition of Π, there exists a meta-function b such that

a = lam x.b(x) ∧ ∀ x. x ∈ A ⟹ b(x) ∈ B(X, x) (2)

Since X ⊆ Y, (1) implies that B(X, x) ⊆ B(Y, x) and, therefore, that

∀ x. x ∈ A ⟹ b(x) ∈ B(Y, x) (3)

Hence, a ∈ Π(A, B(Y)).

The conversion rules for scase and split immediately follow from Definition 3.12. The predicate Mono justifies the expansion of inductive types. By the Knaster-Tarski Theorem [15], if a function f is monotonic (i.e. Mono(f) holds), then it has a least fixed-point lfp(f) such that lfp(f) = f(lfp(f)).

Theorem 3.13 (Type Conversion) The following conversions hold between types.

• scase(z, B, C) = B

• scase(s(a), B, C) = C(a)

• split(⟨a, b⟩ , C) = C(a, b)

• Mono(λX .B(X)) ⟹ μ X . B(X) = B(μ X . B(X))

From the definitions of the type-formers, a set of type rules is derived for the termformers of L (z-type, s-type, etc.). Theorem 3.14 The type rules of Figure 3.3 are derivable. Proof: Proofs of three of the rules serve as illustration. For rec-type, the definition of the predicate ≺_{R} is assumed; in §3.5, a ≺_{R} b holds iff R is well-founded over ι_{=}, and the pair (a, b) is in the ordering R.

• lam-type Prove lam x.b(x) ∈ Π(A, B), assuming ∀ x. x ∈ A ⟹ b(x) ∈ B(x) (1) By the definition of Π, (1) and lam x.b(x) = lam x.b(x) imply

lam x.b(x) ∈ Π(A, B)

• pcase-type Prove pcase(f, c) ∈ C(f), assuming f ∈ Π(A, B) (1) ∀ u. (∀ x. x ∈ A ⟹ u(x) ∈ B(x)) ⟹ c(u) ∈ C(lam x.u(x)) (2) By the definition of Π, (1) implies there exists u′ such that f = lam x.u′(x) and ∀ x. x ∈ A ⟹ u′(x) ∈ B(x) (3) By (2), this in turn implies c(u′) ∈ C(lam x.u′(x)) (4) By substitution, using (3) and pcase(lam x.u′(x), c) = c(u′) from Theorem 3.8, this gives

pcase(f, c) ∈ C(f)

• rec-type Prove rec(a, h) ∈ B(a), assuming a ∈ A (1) ∀ x u. x ∈ A ∧ (∀ y. y ∈ A ∧ y ≺_{R} x ⟹ u(y) ∈ B(y)) ⟹ h(x, u) ∈ B(x) (2) Note that the well-formedness of the rule ensures that R is well-founded over ι_{=}. So, by well-founded induction, it suffices to prove rec(a′, h) ∈ B(a′), assuming a′ ∈ A (3) ∀ u. u ∈ A ∧ u ≺_{R} a′ ⟹ rec(u, h) ∈ B(u) (4) By (2), (3) and (4) imply h(a′, λy.rec(y, h)) ∈ B(a′) (5) By substitution, using rec(a′, h) = h(a′, λx.rec(x, h)) from Theorem 3.8, this gives

rec(a′, h) ∈ B(a′)

\frac{a: V}{vcase : A}

z : S(A)  \frac{a: A}{s(a) : S(A)}  \frac{a: S(A)  b: B(z)  \begin{matrix}[ x: A ] & x \\ c(x) : B(s(x)) \end{matrix}}{scase(a, b, c) : B(a)}

\frac{\begin{matrix}[ x: A ] & x \\ b(x) : B(x) \end{matrix}}{lam x.b(x) : Π(A, B)}  \frac{f : Π(A, B)  \begin{matrix}[ \begin{matrix}[ x: A] & x \\ u(x) : B(x) \end{matrix} ] & u \\ c(u) : C(lam x.u(x)) \end{matrix}}{pcase(f, c) : C(f)}

\frac{a: A  b: B(a)}{⟨a, b⟩: Σ(A, B)}  \frac{p: Σ(A, B)  \begin{matrix}[ x: A ; y : B(x) ] & x,y \\ c(x, y) : C(⟨x, y⟩) \end{matrix}}{split(p, c) : C(p)}

\frac{a: A  \begin{matrix}[ x: A ; \begin{matrix}[ y : A ; y ≺_{R} x] & y \\ u(y) : B(y) \end{matrix}] & x,u \\ h(x, u) : B(x) \end{matrix}}{rec(a, h) : B(a)}  \frac{a: A  \begin{matrix}[ x: A ] & x \\ b(x) : B \end{matrix}}{let x be a in b(x) end : B}

\frac{a: A  P (a)}{a: \{x:A, P (x)\}}  \frac{a: \{x:A, P (x)\}  \begin{matrix}[ & a: A ; P (a) & ] \\ & Q \end{matrix}}{Q}

Figure 3.3: Type Rules for CCL

As types are defined over equivalence classes of terms under term equality, equal terms may be substituted. Moreover, type equality is just set equality, and therefore extensional. The following theorems hold for substitution.

Theorem 3.15 For all terms a and a′ and meta-functions C, if a = a′ then C(a) = C(a′).

Theorem 3.16 For all types A, A′ and meta-functions C, if A = A′ then C(A) = C(A′).

Theorem 3.17 For all terms a and a′ and types A and A′, if a = a′ and A = A′ then a: A iff a′ : A′.

3.5 Well-Founded Orderings

In §A.2, certain constructions over relations are shown to preserve well-foundedness. They are used as constructors for the meta-type of well-founded orderings (ω), so that wellfoundedness is a syntactic condition, which depends only on the well-formedness of elements of ω.

The primitive ordering pR is the irreflexive transitive closure of the immediate subterm relation on terms. For example, the following hold.

x ≺pR s(x)  x ≺pR s(s(x))  x ≺pR ⟨x, y⟩

The ordering lex(R, S) is the lexicographic ordering of R and S; map(f, R) is the image of the ordering R under the meta-function f; and restrict(A, R) is the ordering R restricted to the type A.

Formally, the meta-type ω is the set of well-founded relations over terms.

Definition 3.14 ω ≡ {R ∈ P(ι_{=}×ι_{=}) | Wfd_{ι_{=}}(R)}

The predicate Wfd_{A}(R), defined in §A.1, asserts that R is a well-founded relation over the type A.

Definition 3.15 The constructions for well-founded orderings are defined as follows.

pR ≡ ⋃_{a,b∈ι_{=}}{ (a, s(a)), (a, ⟨a, b⟩), (b, ⟨a, b⟩) }^{+}
lex(R, S) ≡ { (⟨a_{1}, a_{2}⟩ , ⟨b_{1}, b_{2}⟩) ∈ ι_{=}×ι_{=} | (a_{1}, b_{1}) ∈ R ∨ (a_{1} = b_{1} ∧ (a_{2}, b_{2}) ∈ S) }
map(f, R) ≡ { (a, b) ∈ ι_{=}×ι_{=} | (f(a), f(b)) ∈ R }
restrict(A, R) ≡ R ∩ A×A

Theorem 3.18 The constructors for well-founded orderings have the following metatypes.

• pR ∈ ω

• lex ∈ ω ⇒ω ⇒ω

• map ∈ (ι⇒ι)⇒ω ⇒ω

• restrict ∈ τ ⇒ω ⇒ω

Proof: The meta-types are justified by the theorems of §A.2. For example, lex(R, S) is defined as the lexicographic ordering of the orderings R and S. It is well-founded over ι_{=} if R and S are well-founded over ι_{=}, and therefore has the meta-type ω ⇒ω ⇒ω.

a ≺pR b  ↔  \begin{matrix}(b = s(a)) ∨ (∃ x. b = ⟨a, x⟩) ∨ \\ (∃ x. b = ⟨x, a⟩) ∨ (∃ x. a ≺pR x ∧ x ≺pR b) \end{matrix}
⟨a_{1}, a_{2}⟩ ≺_{lex(R,S)} ⟨b_{1}, b_{2}⟩  ↔  (a_{1} ≺_{R} b_{1}) ∨ (a_{1} = b_{1} ∧ a_{2} ≺_{S} b_{2})
a ≺_{map(f,R)} b  ↔  f(a) ≺_{R} f(b)
a ≺_{restrict(A,R)} b  ↔  a: A ∧ b: A ∧ a ≺_{R} b

Figure 3.4: Rules for Well-Founded Orderings in CCL

Theorem 3.19 The bi-implications in Figure 3.4 are derivable.

As well-founded orderings are defined over equivalences classes (ι_{=}), the following theorem holds for substitution.

Theorem 3.20 For all terms a, a′, b and b′ and well-founded orderings R, if a = a′ and b = b′, then a ≺_{R} b iff a′ ≺_{R} b′.

3.6 The Theory CCL

The computational logic CCL is based on classical first-order logic. In addition, metatypes are defined for terms (ι_{=}), types (τ) and well-founded orderings (ω), and predicates are defined for term equality (=), type equality (=), type inhabitation (:), monotonicity (Mono) and well-founded orderings (≺).

First-Order Logic

A natural deduction calculus for first-order logic is used, with introduction and elimination rules for the constants ∧, ∨, ⊃,∀ and ∃, an elimination rule for ⊥ and the rule classical to make the calculus classical (Figure 3.5). Quantification is over the meta-type of terms (ι_{=}) and the sort of types (τ). The remaining constants are defined by

\begin{matrix}¬P ≡ & P ⊃ ⊥ \\ ⊤ ≡ & ¬⊥ \\ P ↔ Q ≡ & (P ⊃ Q) ∧ (Q ⊃ P) \end{matrix}

Typed quantification is defined for terms by

\begin{matrix}∀ x:A.P (x) ≡ & ∀ x. x: A ⊃ P (x) \\ ∃ x:A.P (x) ≡ & ∃ x. x: A ∧ P (x) \end{matrix}

Equality

The predicate = is used for equality over both terms and types.

\begin{matrix}= ∈ & ι_{=} ⇒ι_{=} ⇒o \\ = ∈ & τ ⇒τ ⇒o \end{matrix}

∧-intr  \frac{P  Q}{P ∧ Q}  ∧-elim  \frac{P ∧ Q}{P}  \frac{P ∧ Q}{Q}

∨-intr \frac{P}{P ∨ Q}  \frac{Q}{P ∨ Q}  ∨-elim \frac{P ∨ Q  \begin{aligned}[ & P & ] \\ & R \end{aligned}  \begin{aligned}[ & Q & ] \\ & R \end{aligned}}{R}

⊃-intr  \frac{\begin{aligned}[ & P & ] \\ & Q \end{aligned}}{P ⊃ Q}  ⊃-elim  \frac{P  P ⊃ Q}{Q}

∀-intr  \frac{P (x)^{x}}{∀ x. P (x)}  ∀-elim  \frac{∀ x. P (x)}{P (t)}

∃-intr  \frac{P (t)}{∃ x. P (x)}  ∃-elim  \frac{∃ x. P (x)  \begin{matrix}[ P (x) ] & x \\ Q \end{matrix}}{Q}

⊥-elim  \frac{⊥}{P}  classical  \frac{\begin{aligned}[ & ¬P & ] \\ & P \end{aligned}}{P}

Figure 3.5: Natural Deduction Rules for First-Order Logic

\begin{matrix}a = a & \frac{a = b}{b = a} \\ \frac{a = b  b = c}{a = c} & \frac{a = b  P (a)}{P (b)} \end{matrix}

Figure 3.6: General Rules of Equality for CCL

scase(z, b, c) = b
scase(s(a), b, c) = c(a)
pcase(lam x.b(x), c) = c(b)
split(⟨a, b⟩ , c) = c(a, b)

rec(a, h) = h(a, λx.rec(x, h))

\frac{a: A}{let x be a in b(x) end = b(a)}

Figure 3.7: Conversion Rules for CCL

Figure 3.6 presents general rules for reasoning about equality. For terms, the rules for reflexivity, symmetry and transitivity are justified by Theorem 3.5, and for types by the properties of set equality. Equal terms may be substituted in terms (Theorem 3.7), in types and in predicates. As type equality, which is just set equality, is also a congruence, a general rule of substitution is admissible.

\frac{a = b P (a)}{P (b)}

The conversion rules for terms and, where appropriate, types (Figure 3.7) immediately follow from Theorems 3.8 and 3.13. The congruence rules for terms (Figure 3.8) follow from Theorem 3.7.

3.7 The Strength of CCL

CCL allows reasoning about the total correctness of programs of L. Although the programming language L is clearly Turing complete (it contains untyped λ-abstraction), there is, as yet, no characterisation of the class of programs that can be typed in CCL. Although all programs that can be typed in CCL terminate, it is not the case that all terminating programs can be typed—consider, for example, the program s(Ω). In fact, the typeable programs correspond more closely to Martin-Löf’s notion of hereditarily terminating programs [40]. But the class of typeable programs depends on the set of well-founded orderings that can be constructed. The constructors for well-founded orderings are not intended to be complete, although they are sufficient for the programs described in this dissertation.

\frac{a = a′}{s(a) = s(a′)}  \frac{b(x) = b′(x)^{x}}{lam x.b(x) = lam x.b′(x)}

\frac{a = a′  b = b′}{⟨a, b⟩ = ⟨a′, b′⟩}  \frac{a = a′  b = b′  c(x) = c′(x)^{x}}{scase(a, b, c) = scase(a′, b′, c′)}

\frac{f = f′ c(u) = c′(u)^{u}}{pcase(f, c) = pcase(f′, c′)} p = p′ c(x, y) = c′(x, y)^{x,y}

split(p, c) = split(p′, c′)

\frac{a = a′  h(x, u) = h′(x, u)^{x,u}}{rec(a, h) = rec(a′, h′)} \frac{a = a′  b(x) = b′(x)^{x}}{let x be a in b(x) end = let x be a′ in b′(x) end}

Figure 3.8: Congruence Rules for CCL

For example, multi-set orderings cannot be constructed, and so an algorithm for proof normalisation cannot be typed. A new constructor for multi-set orderings could, of course, be added.

A result is proved that puts a lower bound on the class of typeable programs, showing that any program that is feasibly computable, from a complexity viewpoint, can be typed in CCL. The result is of limited value; it shows what can be represented, but says nothing about how this is done. In fact, the proof relies only on primitive recursion being typeable in CCL.

Theorem 3.21 All those functions that are provably total in Peano Arithmetic(PA) can be represented as typed terms in CCL.

Proof: It is known that the closed terms of type Int → Int in Gödel’s system T are precisely those that are provably total in PA [19]. There is an embedding of system T in CCL, for which typeable functions in system T are mapped to typeable programs in CCL. Therefore, CCL can type at least the functions provably total in PA.

The calculus for Gödel’s system T is given in Figure 3.9, and its embedding in CCL is given below. A term t of system T is represented by the term t^{∘} of CCL.

(lam x.b(x))^{∘} ≡ lam x.b(x)^{∘}
⟨a, b⟩^{∘} ≡ ⟨a^{∘}, b^{∘}⟩
T^{∘} ≡ z
F^{∘} ≡ s(z)
0^{∘} ≡ ⟨z, z⟩
S(n)^{∘} ≡ ⟨s(z), n^{∘}⟩
(f ‘ a)^{∘} ≡ f^{∘} ‘ a^{∘}
I(p)^{∘} ≡ split(p^{∘}, λx y.x)

J(p)^{∘} ≡ split(p^{∘}, λx y.y) D^{∘} ≡ lam t.lam u.lam b.scase(b, t, λx.u) R^{∘} ≡ lam t.lam u.lam n.rec(n,

λx g.split(x, λy z.scase(y, t, λx.u ‘ g(x) ‘ x)))

Type A of system T is represented by the type A^{∘} of CCL.

(A → B)^{∘} ≡ Πx:A^{∘}.B^{∘} (A × B)^{∘} ≡ Σx:A^{∘}.B^{∘} Bool^{∘} ≡ S(S(V)) Int^{∘} ≡ μ X . Σx:S(S(V)).scase(x, S(V), λx.X)

The predicates : and ⇝ are represented by predicates in CCL.

(a : A)^{∘} ≡ a^{∘} : A^{∘} (t ⇝ a)^{∘} ≡ t^{∘} = a^{∘}

With these definitions, it is simple to prove that the rules of Figure 3.9 map to theorems of CCL.

lam  ‘  →
⟨⟩  I, J  ×
T, F  D  Bool
0, S  R  Int

Constants

\frac{\begin{matrix}[ x: A ] & x \\ b(x) : B \end{matrix}}{lam x.b(x) : A → B}  \frac{f : A → B  a: A}{f ‘ a: B}
\frac{a: A  b: B}{⟨a, b⟩: A × B}  \frac{p: A × B}{I(p) : A}  \frac{p: A × B}{J(p) : B}
T : Bool  F : Bool  \frac{t: A  u: A  b: Bool}{D ‘ t ‘ u ‘ b: A}
0 : Int  \frac{n: Int}{S(n) : Int}  \frac{t: A  u: A → (Int → A)  n: Int}{R ‘ t ‘ u ‘ n: A}

Type Rules (lam x.b(x)) ‘ a ⇝ b(a)

D ‘ u ‘ v ‘ T ⇝ u  R ‘ u ‘ v ‘ 0 ⇝ b(a)
D ‘ u ‘ v ‘ F ⇝ v  R ‘ u ‘ v ‘ S(t) ⇝ v ‘ (R ‘ u ‘ v ‘ t) ‘ t

Conversion Rules

Figure 3.9: Gödel’s System T

Implementation

This chapter describes the implementation of CCL and the development of a system for proving program correctness using the generic theorem prover Isabelle [55].

The natural deduction calculus for CCL presented in Chapter 3 is implemented in Isabelle. The basic rules provide inductive reasoning over the structure of programs and partial evaluation of terms; rules are also derived within CCL for more general forms of induction and the freeness of constructors. In addition, common programming data types are encoded using the primitive type-formers of CCL (V, S, Π, Σ and μ). There is potential, as yet unrealised, to define new data types and automatically derive facts about them from descriptions resembling datatype statements in ML.

Typing a program in CCL ensures its termination (Theorem 3.10). Moreover, using dependent type-formers and subtypes allows typing to ensure more fine grain behaviour (program correctness). Thus, CCL offers a framework in which to generate correctness conditions sufficient for a program to meet a specification. Tactics are developed for reasoning about program correctness, including type checking and rewriting. But explicit typing, which allows the encoding of general data types and the convenient specification of programs, makes the logic clumsy for proving facts within particular domains. Instead, lemmas can be proved in first-order logic extended with computational types, and then lifted up to CCL. This means sometimes choosing to work in a subtheory of CCL, in which typing is decidable and well known techniques for reasoning by induction and rewriting are applicable.

§4.1 presents an overview of the theorem prover Isabelle and describes the implementation of the basic rules of CCL. Additional rules are derived in §4.2. Common data types and constants are defined and facts proved about them in §4.3. §4.4 describes the tactics used for reasoning about program correctness. §4.5 describes how first-order logic is interpreted in CCL and used to prove lemmas that arise in proofs of program correctness. Finally, §4.6 summarises the complete implementation.

4.1 Encoding CCL in Isabelle

This section introduces the theorem prover Isabelle and describes the implementation of the basic rules of CCL.

4.1.1 Overview of Isabelle

Isabelle is a generic theorem prover (logical framework) written in ML that supports reasoning in object-logics by encoding them as natural deduction calculi in its meta-logic. The meta-logic is a fragment of intuitionistic higher-order logic including implication ⟹, universal quantification ⋀, equality ≡ and abstraction λ. Types of the meta-logic, metatypes, are classified into sorts, which are partially ordered by an inclusion relation ⋐ such that s_{1} ⋐ s_{2} iff every element of s_{1} is an element of s_{2}. Meta-type variables are restricted to range over elements of a particular sort, which provides a form of ordersorted polymorphism (cf. Nipkow [46] and the language Haskell [29]). Write α_{s} for a variable ranging over meta-types of sort s.

Isabelle’s basic meta-logic has two sorts: logic ⋐ any. Meta-types are constructed from the meta-type of propositions prop, of sort logic, and the meta-type former of metafunctions ⇒, which takes two meta-types of sort logic (or any) and produces a meta-type of sort logic (or any). The infix predicate :: denotes both meta-type membership and sort membership. Constants of the meta-logic have the following meta-types

⋀ :: (α_{logic} ⇒prop)⇒prop
⟹ :: prop⇒prop⇒prop
≡ :: α_{logic} ⇒α_{logic} ⇒prop

Additional sorts, meta-types and constants may be defined to encode new objectlogics. Isabelle imposes restrictions on the possible orderings of sorts to ensure that a ‘principal type property’ is retained for the Hindley-Milner style of type checking used in the meta-logic [14, 27]. Order-sorted polymorphism allows object-logic constants to be polymorphic—consider, for example, the equality relation of some first-order logics. Metalevel abstraction allows object-logics to be defined with the higher-order syntax described in §3.1. A pretty printer and parser provide concrete syntax.

The rule calculus of an object-logic is encoded as a set of axioms in the meta-logic. For each form of judgement in the object-logic, a meta-function istrue is defined to lift elements of that judgement up to propositions in the meta-logic. This allows ⟹ to represent entailment, ⋀ to bind variables and ≡ to encode definitions. Write [[ H1; H2; …]] ⟹ P for the sequence of hypotheses H1 ⟹ H2 ⟹ … ⟹ P. For example, Isabelle’s firstorder logic FOL has a single judgement of the truth of formulae (of meta-type o), for which the meta-function istrue :: o⇒prop is defined. Using this function, the ∧-intr rule

\frac{P Q}{P ∧ Q}

is encoded as

⋀ P .⋀ Q.[[ istrue(P); istrue(Q) ]] ⟹ istrue(P ∧ Q)

which captures the intended meaning that for all formulae P and Q, if P is true and if Q is true then P ∧ Q is true. Meta-level quantification can be used to bind variables as well as quantify over formulae (in the meta-logic they are both just terms). Writing ∀(λx.P (x)) as ∀x.P (x), the ∀-intr rule

\frac{P (x)^{x}}{∀x.P (x)}

is encoded as

⋀ P .(⋀ x.istrue(P (x))) ⟹ istrue(∀x.P (x))

which captures the intended meaning that for all predicates P, if P (x) is true for all x then ∀ x. P (x) is true. The eigenvariable condition is enforced by binding x within the hypothesis.

In Isabelle, proof rules are a generalised form of Horn clause. Axioms of an object-logic are used as proof rules. Derived theorems, having the same form as axioms, are used as proof rules with no extra cost. Isabelle supports logical variables, indicated by a leading question mark ?x. As in Prolog, these may appear in goals and become instantiated incrementally during proofs.

Proofs may be built up from rules in both a forward and backward direction. Stepping backward in a proof is by resolving a rule (an axiom or a theorem) with one of the current goals: variables quantified at the outermost level of the rule are replaced by logical variables; then the conclusion of the rule is unified with the selected goal, and on successful unification this goal is replaced by the instantiated premises. Higher-order unification [30] handles the inherent αβη-conversions. The procedure is incomplete and may yield an infinite set of unifiers. But in practice this rarely gives rise to problems; when it does, additional tactics can be employed to guide instantiation. Each step in a backward proof replaces one of the current goals by zero or more new goals; when no subgoals remain, the proof is complete. Forward reasoning is less well supported; rules may be ‘glued’ together by unifying the conclusion of one rule with a premise of another.

Individual steps in a proof are made by tactics. For example, assume_tac n solves subgoal n by assumption, and resolve_tac rls n uses resolution on subgoal n with the first rule in rls whose conclusion unifies with the subgoal. Tacticals allow tactics to be combined. For example, sequentially using tac_{1} THEN tac_{2}, as alternatives using tac_{1} ORELSE tac_{2} and repeatedly using REPEAT tac. More complex tacticals are coded in the programming language ML.

As resolve_tac uses a list of possible rules each of which may yield many results, it returns a possibly infinite stream of new proof states. Together with some non-deterministic tacticals, these produce alternatives in the proof tree that are maintained by Isabelle to allow backtracking, and with appropriate tacticals proof search. Prolog exhibits one possible search strategy, and in its pure form may be implemented as an Isabelle tactical.

Isabelle has a suite of tactics (including fast_tac) for automatically solving goals in first-order logic by natural deduction inference. These tactics use a set of introduction and elimination rules for first-order logic (FOL_cs) to which further rules can be added. In addition, Isabelle has a generic rewriting package for object-logics, the simplifier. Supplied with the basic theorems necessary to justify rewriting (namely reflexivity and transitivity) together with reductions and rules for case analysis, it returns a suite of simplification tactics. The simplifier may rewrite using several reduction relations at once, for example, term equality (=) and logical equivalence (↔) in first-order logic. Rewriting and congruence rules for the reduction relations are maintained in simplification sets. The simplification tactics provide various combinations of the following: rewriting using rules of the simplification set, rewriting using the assumptions in a goal and case analysis using split rules (e.g. for if then else ). In particular

• ASM_SIMP_TAC rewrites a goal using the set of simplification rules and any assumptions, and

• ASM_SIMP_CASE_TAC rewrites as ASM_SIMP_TAC and also uses case analysis.

4.1.2 The Encoding of CCL

With the exception of hypothetical hypotheses, the basic rules of CCL are directly encoded in Isabelle. The implementation CCL is an extension of Isabelle’s theory FOL, which is an implementation of typed first-order logic. Isabelle encodings are presented in typewriter font. Those symbols for which there is no transliteration are translated as follows:

λ becomes %  ⋀ becomes !!
≡ becomes ==  α_{s} becomes 'a::s
a ≺_{R} b becomes [a R b]

The Isabelle theory FOL is briefly introduced before the extension CCL.

FOL

FOL has only one meta-type o of sort logic, representing formulae. There is a single form of judgement encoded by the function istrue (see §4.1.1).

                            istrue :: o => prop

It is not explicitly shown again. The new sort term is introduced with the ordering

                            term ⋐ logic ⋐ any

which distinguishes meta-types of individuals from formulae, so that first-order quantification can be expressed.

The propositional connectives ∧,∨,¬,⊃ and ↔ are represented by the infix and prefix constants &,|,~,--> and <-> respectively, defined as meta-functions over the meta-type of formulae o. As the logic is first-order, quantification is restricted to individuals (the quantifiers are polymorphic over types of sort term).

                      All    :: ('a::term => o) => o
                      Exists :: ('a::term => o) => o

Concrete syntax provides

                  ALL x.P(x) in place of All(%x.P(x))
                   EX x.P(x) in place of Exists(%x.P(x))

The axioms of FOL are exactly the logical part of CCL (Figure 3.5).

CCL

CCL is an extension of FOL. Formulae of CCL correspond to formulae in FOL. Other syntactic classes are represented by the following new meta-types.

i :: term for the terms of L (ι_{=})
t :: term for the types of L (τ)
w :: logic for the well-founded relations (ω)

The higher-order syntax used in CCL (see §3.1) translates directly into Isabelle’s metalogic. At the level of concrete syntax, alternatives are provided for Π and Σ in the cases when they are truly dependent or not.

                PROD x:A.B(x) in place of Pi(A,%x.B(x))
                A -> B  in place of Pi(A,%x.B)
                SUM x:A.B(x) in place of Sigma(A,%x.B(x))
                A * B  in place of Sigma(A,%x.B)

The pretty printer is sophisticated enough to use these forms where appropriate.

At present, Isabelle does not provide tactics for handling subgoals with nested metaimplication, and so rules with hypothetical hypotheses cannot be used. Instead, the metalevel universal quantification and implication used to represent hypothetical hypotheses are replaced by universal quantification and implication in CCL. This is justified as the meta-logic is higher-order logic and the connectives of CCL are those of first-order logic. For example, the rule rec-type

a: A \begin{matrix}[ x: A ; \begin{matrix}[ y : A ; y ≺_{R} x] & y \\ u(y) : B(y) \end{matrix}] & x,u \\ h(x, u) : B(x) \end{matrix}

rec(a, h) : B(a)

is replaced by the rule

a: A \begin{matrix}[ x: A ; ∀ y:A.y ≺_{R} x ⊃ u(y) : B(y) ] & x,u \\ h(x, u) : B(x) \end{matrix}

rec(a, h) : B(a)

For convenience, rules are still written with hypothetical hypotheses, even though the Isabelle implementation uses object-level quantification and implication.

The rules of CCL, modified to remove hypothetical hypotheses, are the only axioms postulated in the Isabelle implementation. Further rules are all derived within the Isabelle theory CCL.

4.2 Derived Rules

From the basic rules of CCL, additional rules are derived within the theory for reasoning about program correctness. In particular, rules are derived for

• induction on the type-formers,

• strengthened type rules for destructors, and

• the freeness of constructors.

4.2.1 Induction Rules

The type rule for each destructor d ∈ DES provides case analysis on formulae d(\overline{x}) : A; rec-type provides induction on formulae rec(a, h) : B(a). For example, the rule scase-type

\frac{a: S(A)  b: B(z)  \begin{matrix}[ x: A ] & x \\ c(x) : B(s(x)) \end{matrix}}{scase(a, b, c) : B(a)}

provides case analysis over the canonical elements of S(A) only for formulae of the form scase(a, b, c) : B(a). Within CCL, more general forms of case analysis and induction are derived from these rules using the subtype type-former. From the rule scase-type, the following induction rule (scase-ind) is derived.

\frac{a: S(A)  P (z)  \begin{matrix}[ x: A ] & x \\ P (s(x)) \end{matrix}}{P (a)}

Derivation:^{1} Assuming a: S(A), P (z) and x: A ⟹ P (s(x)), prove P(a). By {}-elim, scase(a, z, λx.z) : {x:S(V), P (a)} implies P (a). Using scase-type, this can be reduced to the goals

1. a: S(A)

2. z : {x:S(V), P (z)}

3. y : A ⟹ z : {x:S(V), P (s(y))}

which follow from the assumptions, {}-intr and z-type.

There is an induction rule for each destructor. In particular, the rule vcase-ind asserts that the type V is uninhabited;

\frac{a: V}{P}

the rule pcase-ind is an induction(η) rule for lam;

\frac{f : Π(A, B) \begin{matrix}[ \begin{matrix}[ x: A] & x \\ u(x) : B(x) \end{matrix} ] & u \\ P (lam x.u(x)) \end{matrix}}{P (f)}

and the rule rec-ind is well-founded induction.

\frac{a: A \begin{matrix}[ x: A ; \begin{matrix}[ y : A ; y ≺_{R} x] & y \\ P (y) \end{matrix}] & x \\ P (x) \end{matrix}}{P (a)}

Note that defining L with application, instead of the more general destructor for functions pcase, would not have allowed the derivation of an η-rule.

1We use the term derivation for all proofs carried out using the Isabelle implementation of CCL.

4.2.2 Strong Type Rules

In type rules for destructors, the variable being reduced is replaced in the premises by the appropriate canonical forms. For example, in the rule scase-type

\frac{a: S(A)  b: B(z)  \begin{matrix}[ x: A ] & x \\ c(x) : B(s(x)) \end{matrix}}{scase(a, b, c) : B(a)}

the variable a in B(a) is replaced by the canonical forms z and s(x). But these implicit substitutions do not occur in any assumptions that might be present. To overcome this, strengthened rules are derived in which the substitutions explicitly appear as hypotheses in the premises. For example, the strengthened type rule for scase is

\frac{a: S(A)  \begin{matrix}[ & a = z & ] \\ & b: B(z) \end{matrix}  \begin{matrix}[ x: A ; a = s(x) ] & x \\ c(x) : B(s(x)) \end{matrix}}{scase(a, b, c) : B(a)}

in which the second and third premises are weakened by additional assumptions. Derivation: Assuming a: S(A), a = z ⟹ b: B(z) and [[ x: A; a = s(x) ]] ⟹ c(x) : B(s(x)), prove scase(a, b, c) : B(a). By ⊃-intr and refl, a = a ⊃ scase(a, b, c):B(a) implies scase(a, b, c):B(a). This is reduced by scase-ind to the goals

1. a: S(A)

2. a = z ⊃ scase(a, b, c) : B(z)

3. x: A ⟹ a = s(a) ⊃ scase(a, b, c) : B(s(a))

Note that not all occurrences of a in a = a ⊃ scase(a, b, c) : B(a) are replaced. These goals follow from the assumptions, subst and the conversion rules for scase.

A similar technique is used in Martin-Löf’s Type Theory. But in a type theory where proofs are identified with programs, the strengthened rules contain extra detail in their proof terms which is redundant—in CCL, the program fragment scase(a, b, c) remains unchanged when the rule is strengthened.

Similarly, the type rules for pcase and split are strengthened. But rules involving induction cannot be strengthened in this way. In particular, the strengthened version of rec-type

a: A \begin{matrix}[ x: A ; \begin{matrix}[ y : A ; y ≺_{R} x] & y \\ u(y) : B(y) \end{matrix}; a = x ] & x,u \\ h(x, u) : B(x) \end{matrix}

rec(a, h) : B(a)

is inconsistent in CCL, giving further motivation for the separation of case analysis and recursion. This is clearer for the more familiar case of mathematical induction. The rule

\frac{^{\begin{aligned}[ & n = 0 & ] \\ & P (0) \end{aligned} \begin{matrix}[ P (x) ; n = x + 1 ] & x \\ P (x + 1) \end{matrix}}}{P (n)}

allows the derivation of the fallacy n = 2 ⟹ n = 0. An instance of this rule, in which P (n) is n = 0, reduces the fallacy to the following subgoals.

• [[ n = 2; n = 0 ]] ⟹ 0 = 0

• [[ n = 2; x = 0; n = x + 1 ]] ⟹ x + 1 = 0

The first is trivial; the second has assumptions that lead to the contradiction 2 = 1, and so it holds as well.

4.2.3 Freeness of Constructors

Freeness of constructors is essential for reasoning about terms in CCL. Distinctness and injectivity of the constructors are derivable within CCL.

In Martin-Löf’s Type Theory, constructors are shown to be distinct by the differing reductions they induce in their destructor. But to show that these reductions are different, they must reduce to terms that are distinguishable within the logic. The only examples of this are in the universe of types, namely encodings of the empty type and a non-empty type [62]. Similarly in CCL, the terms z and s(a) are distinguished by their effect when used as arguments in λx.scase(x, V, λx.S(V)). In this case, the following rule can be derived.

\frac{z = s(a)}{P}

Derivation: Assuming z = s(a), prove P. By the conversion rules for scase and scase-ind, z : scase(z, V, λx.S(V)) implies P. Substituting s(a) for z, by assumption, reduces this to z : scase(s(a), V, λx.S(V)), which follows from the conversion rules for scase and z-type.

The injectivity of constructors follows from their behaviour in destructors that project their arguments (e.g. scase(s(a), b, λx.x) for the constructor s). For example, the following rule can be derived

\frac{s(a) = s(a′)}{a = a′}

Derivation: Assuming s(a) = s(a′), prove a = a′. By the conversion rules for scase, scase(s(a), b, λx.x) = scase(s(a′), b, λx.x) implies that a = a′. Substituting s(a) for s(a′) reduces this to scase(s(a), b, λx.x) = scase(s(a), b, λx.x) which follows by refl.

Similarly, pairing is injective.

\frac{⟨a, b⟩ = ⟨a′, b′⟩ \begin{aligned}[ & a = a′ ; b = b′ & ] \\ & P \end{aligned}}{P}

The constructor lam is also injective, though this is of little use in practice.

4.3 Definitions

CCL contains a core programming language L. This is enriched with definitions for locally declared functions and data types from which type and conversion rules are derived.

Executing a program in this enriched language uses derived evaluation rules to supplement those of L. The derived rules just provide short cuts in the evaluation of programs— the same result would be achieved by unfolding the definitions before execution. They do not add any expressive power to L, nor do they compromise the properties proved for evaluation.

4.3.1 Local Declarations

Two sets of constants are defined for introducing auxiliary functions that are non-recursive and recursive. Non-recursive functions of one or more arguments are introduced with the term-formers

letfun :: (ι⇒ι)⇒(ι⇒ι)⇒ι
letfun :: (ι⇒ι⇒ι)⇒(ι⇒ι)⇒ι
⋮

and recursive functions of one or more arguments with the term-formers

letrec :: (ι⇒ι⇒ι)⇒(ι⇒ι)⇒ι
letrec :: (ι⇒ι⇒ι⇒ι)⇒(ι⇒ι)⇒ι
⋮

Isabelle is able to resolve the overloadings that arise.

The unary cases are sufficient illustration. Write the term letfun(λx.a(x), λf .b(f)) as letfunf x be a(x) in b(f) end, and similarly write the term letrec(λx g.a(x, g), λf .b(f)) as letrecf x be a(x, f) in b(f) end. The term-former letfun is defined by

letfunf x be a(x) in b(f) end ≡ b(lam x.a(x))

from which the following type and conversion rules are derived.

\frac{^{\begin{matrix}[ x: A ] & x \\ a(x) : B(x) \end{matrix} \begin{matrix}[ \begin{matrix}[ x: A] & x \\ v ‘ x: B(x) \end{matrix} ] & v \\ b(v) : C \end{matrix}}}{letfunf x be a(x) in b(f) end : C}

letfunf x be a(x) in b(f) end = b(lam x.a(x))

Note that this definition of letfun has the same meaning as using let to declare functions.

letfunf x be a(x) in b(f) end ≡ let f be lam x.a(x) in b(f) end

But this is not derivable as an equality in CCL, because the conversion rule for let uses typeability to ensure termination, and typeability is stronger than the termination predicate ↓, which was not formalised in CCL.

Recursive functions of one argument are introduced with letrec, defined by

letrecf x be a(x, f) in b(f) end ≡ letfunf x be rec(x, λu g.a(u, lam v.g(v))) in b(f) end from which the following type and conversion rules are derived.

\frac{^{\begin{matrix}[ x: A ; \begin{matrix}[ y : A ; y ≺_{R} x] & y \\ u ‘ y : B(y) \end{matrix}] & x,u \\ a(x, u) : B(x) \end{matrix} \begin{matrix}[ \begin{matrix}[ x: A] & x \\ v ‘ x: B(x) \end{matrix} ] & v \\ b(v) : C \end{matrix}}}{letrecf x be a(x, f) in b(f) end : C}

letrecf x be a(x, f) in b(f) end = b(lam x.rec(x, λx g.a(x, lam x.g(x))))

The type rule differs from that for letfun only in the presence of an induction hypothesis.

4.3.2 Data Types

Using the basic type-formers of CCL, there are straightforward encodings of the following types: unit, boolean, disjoint union, natural numbers and lists. From these encodings, rules are derived for

• typing the term-formers,

• computation and congruence,

• the freeness of constructors,

• induction,

and, where appropriate,

• functionals for primitive recursion.

Finite enumerations (Unit and Bool) are encoded using the type-formers V and S (Figures 4.1 and 4.2). The term ucase(a, b) is encoded as the term scase(a, b, λx.vcase). For well-typed terms, λx.vcase is never executed. The same rules would be derivable if vcase was replaced by any other term; using vcase just indicates that this program fragment must be unused. If the typing judgement a : A was separated from other formulae then the use of vcase might be made mandatory; but, as this would prevent typing judgements appearing freely in formulae, the price is too great. Since scase is polymorphic in its result type, ucase and cond will also be polymorphic in their result types—they are defined as destructors that return terms and as destructors that return types.

The disjoint union A + B is encoded as a tagged record using the dependent typeformer Σ and the destructor cond (Figure 4.3). Once disjoint union is defined, other types, including inductive ones, may be introduced in a similar fashion to ML’s datatype statement. If they were not primitive, the types of natural numbers and lists would be defined in ML as

   datatype     Nat = zero | succ of Nat;
   datatype 'a List = nil  | :: of 'a * 'a List;

In CCL, their encodings are similar (Figures 4.4 and 4.5).

Nat ≡ μ X . Unit + X
List(A) ≡ μ X . Unit + A × X

\underline{4.4. Tactics 51}

Unit  ≡ S(V)
one  ≡ z
ucase(a, b) ≡ scase(a, b, λx.vcase)

Definitions

one : Unit \frac{a: Unit  b: B(one)}{ucase(a, b) : B(a)}

ucase(one, b) = b \frac{a = a′  b = b′}{ucase(a, b) = ucase(a′, b′)}

\frac{a: Unit P (one)}{P (a)}

DerivedRules

Figure 4.1: An Encoding of the Unit Data Type

Type rules for inductive types are derived using the conversion rule for μ, which requires that the argument to μ is monotonic. For example, the lemma

Mono(λX .Unit + X)

immediately follows from the rules for Mono and leads to the conversion rule

μ X . Unit + X = Unit + μ X . Unit + X

which is used to derive the type rules for Nat.

4.4 Tactics

This section introduces tactics for partially automating correctness proofs. These tactics provide type checking and rewriting, introduce recursive functions and local declarations, instantiate induction hypotheses, and solve some goals for well-founded orderings.

4.4.1 Type Checking

Type checking breaks down goals of the form a: A using the type rules of CCL. As there is only one type rule for each term-former, type checking breaks down goals in a unique way. If type A specifies the behaviour of program a, then type checking raises conditions for the correctness of a (including termination).

As CCL has subtypes, solving the goal a: A is in general undecidable, though it can be reduced to a set of correctness conditions (i.e. formulae not of the form a: A). Typeability, showing that there exists a type A such that a : A, is also undecidable, as this may rely on finding subtypes to ensure termination. For example, the following algorithm for subtractive division may not be simply typed as Nat →Nat →Nat, but requires that the divisor be non-zero: Nat →{x:Nat, ¬x = zero} →Nat.

Bool  ≡ S(S(V))
true  ≡ z
false  ≡ s(z)
cond(b, c, d) ≡ scase(b, c, λx.d)

Definitions

true : Bool false : Bool
\frac{b: Bool  c: B(true)  d: B(false)}{cond(b, c, d) : B(b)}

cond(true, c, d) = c
cond(false, c, d) = d

\frac{b = b′  c = c′  d = d′}{cond(b, c, d) = cond(b′, c′, d′)}

\frac{true = false}{P}  \frac{b: Bool  P (true)  P (false)}{P (b)}

DerivedRules

Figure 4.2: An Encoding of the Boolean Data Type

divide ≡ lam n.lam d. letrec div n d be cond(lt ‘ n ‘ d, zero,

succ(div ‘ (n − d) ‘ d))

in div ‘ n ‘ d end

Tactics are developed for reducing goals of the form a : A to correctness conditions. In addition to the primitive type rules of CCL, strengthened as described in §4.2, these tactics use derived rules for recursive calls and boolean valued functions.

Recursive Calls

The rules for recursive calls (rec-type and letrec-type) introduce induction hypotheses that use object-level quantification and implication to overcome Isabelle’s lack of hypothetical hypotheses. For example,the hypothesis introduced by rec-type is

∀ y:A.y ≺_{R} x ⊃ g(y) : B(y)

To type check a recursive call, this hypotheses must be broken down using ∀-elim and ⊃-elim. Rules are derived that implicitly carry out these inferences, so that recursive calls can be type checked by a single rule. For rec, the following rule is derived.

\frac{∀ y:A.y ≺_{R} x ⊃ g(y) : B(y)  \begin{matrix}[ & g(a) : B(a) & ] \\ & g(a) : D \end{matrix}  a: A  a ≺_{R} x}{g(a) : D}

Similar rules are derived for calls introduced by letrec.

A+B  ≡ Σx:Bool.cond(x, A, B)
inl(a)  ≡ ⟨true, a⟩
inr(b)  ≡ ⟨false, b⟩
when(a, c, d) ≡ split(a, λx y.cond(x, c(y), d(y)))

Definitions

\frac{a: A}{inl(a) : A+B}  \frac{b: B}{inr(b) : A+B}
\frac{a: A+B  \begin{matrix}[ x: A ] & x \\ c(x) : C(inl(x)) \end{matrix}  \begin{matrix}[ y : B ] & y \\ d(y) : C(inr(y)) \end{matrix}}{when(a, c, d) : C(a)}

when(inl(a), c, d) = c(a)

when(inr(a), c, d) = d(a)

\frac{a = a′ c(x) = c′(x)^{x} d(y) = d′(y)^{y}}{when(a, c, d) = when(a′, c′, d′)}

\frac{inl(a) = inr(b)}{P}  \frac{inl(a) = inl(a′)}{a = a′}  \frac{inr(b) = inr(b′)}{b = b′}

\frac{a: A+B \begin{matrix}[ x: A ] & x \\ P (inl(x)) \end{matrix} \begin{matrix}[ y : B ] & y \\ P (inr(y)) \end{matrix}}{P (a)}

a ≺pR inl(a)  b ≺pR inr(b)

DerivedRules Figure 4.3: An Encoding of the Disjoint Union Data Type

Nat  ≡ μ X . Unit + X
zero  ≡ inl(one)
succ(n)  ≡ inr(n)
ncase(n, b, c) ≡ when(n, λx.b, λy.c(y))
nrec(n, b, c) ≡ rec(n, λn g.ncase(n, b, λx.c(x, g(x))))

Definitions

zero : Nat  \frac{n: Nat}{succ(n) : Nat}
\frac{n: Nat  b: B(zero)  \begin{matrix}[ x: Nat ] & x \\ c(x) : C(succ(x)) \end{matrix}}{ncase(n, b, c) : B(n)}
ncase(zero, b, c) = b
ncase(succ(n), b, c) = c(n)

\frac{n = n′  b = b′  c(x) = c′(x)^{x}}{ncase(n, b, c) = ncase(n′, b′, c′)}

\frac{zero = succ(n)}{P}  \frac{succ(n) = succ(n′)}{n = n′}

n: Nat b: B(zero) \begin{matrix}[ x: Nat ; u: B(x) ] & x,u \\ c(x, u) : B(succ(x)) \end{matrix}

nrec(n, b, c) : B(n)

nrec(zero, b, c) = b
nrec(succ(n), b, c) = c(n, nrec(n, b, c))

n = n′  b = b′  c(x, u) = c′(x, u)^{x,u}

nrec(n, b, c) = nrec(n′, b′, c′)

\frac{n: Nat  P (zero)  \begin{matrix}[ x: Nat ; P (x) ] & x \\ P (succ(x)) \end{matrix}}{P (n)} n ≺pR succ(n)

DerivedRules Figure 4.4: An Encoding of the Natural Number Data Type

List(A)  ≡ μ X . Unit + A × X
[]  ≡ inl(one)
h • t  ≡ inr(⟨h, t⟩)
lcase(l, b, c) ≡ when(l, λx.b, λy.split(y, c))
lrec(l, b, c) ≡ rec(l, λl g.lcase(l, b, λh t.c(h, t, g(t))))

Definitions

[] : List(A)  \frac{h: A  t: List(A)}{h • t: List(A)}
l: List(A)  b: B([])  \begin{matrix}[ x: A ; y : List(A) ] & x,y \\ c(x, y) : B(x • y) \end{matrix}

lcase(l, b, c) : B(l)

lcase([], b, c) = b
lcase(h • t, b, c) = c(h, t)

l = l′  b = b′  c(x, y) = c′(x, y)^{x,y}

lcase(l, b, c) = lcase(l′, b′, c′)

\frac{[] = h • t}{P}  \frac{h • t = h′ • t′  \begin{aligned}[ & h = h′ ; t = t′ & ] \\ & P \end{aligned}}{P}
l: List(A)  b: B([])  \begin{matrix}[ x: A ; y : List(A) ; u: B(t) ] & x,y,u \\ c(x, y, u) : B(x • y) \end{matrix}

lrec(l, b, c) : B(l)

lrec([], b, c) = b
lrec(h • t, b, c) = c(h, t, lrec(t, b, c))

l = l′  b = b′  c(x, y, u) = c′(x, y, u)^{x,y,u}
lrec(l, b, c) = lrec(l′, b′, c′)
l: List(A)  P ([])  \begin{matrix}[ x: A ; y : List(A) ; P (y) ] & x,y \\ P (x • y) \end{matrix}

P (l) t ≺pR h • t

DerivedRules Figure 4.5: An Encoding of the List Data Type Boolean Valued Functions

Predicates in CCL are meta-functions (e.g. < :: ι ⇒ ι ⇒ o), whereas conditionals in the programming language L are boolean valued functions (e.g. lt : Nat →Nat →Bool). But there is a simple relationship between predicates and corresponding boolean valued functions. If a unary predicate P is computable, then there is a corresponding boolean valued function p such that for all well-typed a

P (a) ↔ p ‘ a = true

For the binary example above, for all m, n: Nat, it can be proved that

m < n ↔ lt ‘ m ‘ n = true

Type checking the goal cond(p ‘ a, t, u) : A generates the subgoals

p ‘ a = true ⟹ t: A
p ‘ a = false ⟹ u: A

for which the equivalence above can be used to replace the hypotheses with P (x) and ¬P (x) respectively. These replacements are incorporated into type checking using the following derived rule

\frac{b: \{x:Bool, P ↔ x = true\}  \begin{matrix}[ & P & ] \\ t: A \end{matrix}  \begin{aligned}[ & ¬P & ] \\ & u: A \end{aligned}}{cond(b, t, u) : A}

and a list of rules for boolean valued functions, whose conclusions resolve with the first premise.

Tactics for Type Checking

The following tactics are used to type check goals.

• typechk_step_tac rls n either solves goal n by appeal to an assumption or uses the first applicable rule from rls and those rules described above;

   • typechk_tac rls repeatedly applies typechk_step_tac rls n to all goals of the

form a: A in which a is at least partially instantiated (i.e. a is not a logical variable);

• itypechk_tac s rls n applied to a goal ?x : A, instantiates ?x with the term represented by the string s and calls typechk_tac rls restricted to goal n.

The tactic typechk_tac generates correctness conditions for goals of the form a: A. Only if program a is badly typed (i.e. a is instantiated but no rule is found to reduce the goal a:A) does typechk_tac fail. The tactic itypechk_tac allows programs to be instantiated in stages during proof and type checked only as far as the instantiation. In an interactive proof, the current proof state can be taken into account when considering further instantiations.

For simple types, type checking raises conditions for termination only. For example, the program lt determines if one natural number is less than another. lt ≡ lam m.lam n. letrec lt m n be ncase(n, false, λy.ncase(m, true, λx.lt ‘ x ‘ y))

in lt ‘ m ‘ n end

Applying typechk_tac to the goal

1. lt : Nat →Nat →Nat

which asserts that lt is a total function over the natural numbers, generates a single condition for termination.

1. x: Nat ⟹ x ≺_{?R} succ(x)

This is solved by choosing a well-founded relation for ?R in which x is ‘less-than’ succ(x). In fact, the ordering pR is sufficient (see §4.4.6).

If predicates are included in types (using subtypes), then type checking generates instances of these predicates. For example, applying typechk_tac to the goal

1. lt : Πm:Nat.Πn:Nat.{x:Bool, m < n ↔ x = true}

reduces it to the following correctness conditions.

1. [[m: Nat; n: Nat ]] ⟹ m < zero ↔ false = true

2. [[m: Nat; n: Nat ]] ⟹ zero < succ(n) ↔ true = true

3. [[m: Nat; n: Nat; m < n ↔ lt ‘ m ‘ n = true ]] ⟹ succ(m) < succ(n) ↔ lt ‘ m ‘ n = true

4. [[m: Nat; n: Nat ]] ⟹ ⟨m, n⟩ ≺_{?R} ⟨succ(m), succ(n)⟩

4.4.2 Rewriting

The congruence rules for bi-implication (iff_cong_rls) and for term and type equality (eq_cong_rls) allow arbitrary subformulae and subtypes to be manipulated within formulae. The Isabelle simplifier supports this style of reasoning, allowing subterms and subtypes to be rewritten using conversion rules, and subformulae to be simplified using logical equivalences.

However, the conversion rule for rec

rec(a, h) = h(a, λx.rec(x, h))

can be repeatedly applied, thereby compromising termination of the simplifier. Two forms of rewriting are, therefore, considered: the Isabelle simplifier with the conversion rule for rec added only when required (with the risk of non-termination), and a purpose built rewriter which reduces all terms that appear in a goal to their canonical forms. For the Isabelle simplifier, a basic simplification set is defined containing the standard simplification set of FOL together with the conversion and congruence rules of CCL.

The following tactics are used for rewriting.

• asm_simp_tac rs cs n uses ASM_SIMP_TAC from the simplifier with the additional rewrite rules rs and congruence rules cs to simplify goal n;

   • asm_simp_case_tac rs cs n uses ASM_SIMP_CASE_TAC from the simplifier with

the additional rewrite rules rs and congruence rules cs to simplify goal n; • eval_tac rls n solves goal n of the form t = a, where a is the canonical form of

t, by depth-first search using derived evaluation rules for L;

• equal_tac rls reduces every term in a goal to canonical form by breaking up formulae using the congruence rules for predicates (iff_cong_rls) and then applying eval_tac to goals of the form t =?x.

The tactics asm_simp_tac and asm_simp_case_tac are the most commonly used for rewriting. The tactic eval_tac is an interpreter for L; a program t is evaluated by solving the goal t =?x. For example, if \underline{0} represents zero, \underline{1} represents succ(zero) etc., then an application of lt may be evaluated by solving the goal

1. lt ‘ \underline{2} ‘ \underline{6} = ?x

using eval_tac []. This succeeds and ?x becomes instantiated with the canonical form of lt ‘ \underline{2} ‘ \underline{6}.

?x ⟵ true

4.4.3 Introducing Recursive Functions

A program specification typically begins with a series of Π type-formers prescribing the argument types.

?prog : Πx_{1}:A_{1}.. . . Πx_{n}:A_{n}.B(x_{1}, … x_{n})

in which each A_{j} may depend on all x_{i} for i < j. One program satisfying this specification has the form

lam x_{1}…. lam x_{n}.letrec f x_{1} … x_{n} be ?a(x_{1} … x_{n}, f) in f ‘ x_{1} … ‘ x_{n} end

The tactic rec_tac instantiates a program with this form by repeatedly applying the rule lam-type and then applying letrec-type with the appropriate number of arguments. The initial specification is replaced by the subgoal

1. [[ x_{1} : A_{1}, … x_{n} : A_{n};

∀ y_{1}:A_{1}.. . . ∀ y_{n}:A_{n}.⟨y_{1}, … y_{n}⟩ ≺_{?R} ⟨x_{1}, … x_{n}⟩ ⊃ f ‘ y_{1} … ‘ y_{n} : B(y_{1}, … y_{n}) ]] ⟹

?a(x_{1}, … x_{n}, f) : B(x_{1}, … x_{n})

leaving the body of the program ?a to be synthesised for well-typed arguments x_{1} … x_{n}, assuming an induction hypothesis for recursive calls to f. For example, a division algorithm may be specified as

1. ?divide : Πn:Nat.Πd:{d:Nat, ¬d = zero}.{q:Nat, DIV (n, d, q)}

where DIV (n, d, q) holds iff q is the integer quotient of n divided by d. Applying rec_tac instantiates ?divide with a template for a recursive program.

?divide ⟵ lam n.lam d.letrec div n d be ?a(n, d, div) in div ‘ n ‘ d end

and leaves the goal

1. [[ n: Nat; d: {x:Nat, ¬x = zero};
∀ u:Nat.∀ v:{x:Nat, ¬x = zero}.
⟨u, v⟩ ≺_{?R} ⟨n, d⟩ ⊃ div ‘ u ‘ v : {q:Nat, DIV (u, v, q)} ]] ⟹
?a(n, d, div) : {q:Nat, DIV (n, d, q)}

The induction hypothesis allows the behaviour of any recursive call div ‘x‘y to be assumed provided that the pair ⟨x, y⟩ is less-than the pair ⟨n, d⟩ in some, as yet undetermined, wellfounded ordering ?R.

4.4.4 Introducing Local Declarations

The type rules for let, letfun and letrec introduce uninstantiated type variables. For example, applying let-type

\frac{a: A \begin{matrix}[ x: A ] & x \\ b(x) : B \end{matrix}}{let x be a in b(x) end : B}

introduces a new type ?A. Proving a:?A first may instantiate ?A with a type that is too general for the second premise to hold; proving x:?A ⟹ b(x) : B first may instantiate ?A with a type that a does not inhabit. As they introduce uninstantiated type variables, these rules are too undirected to be used in a general tactic for type checking, except for simple instances of letfun-type and letrec-type in which the body is a direct application of the declared function (see, for example, the definition of lt in §4.4.1).

Instead, tactics are provided that explicitly introduce local declarations by hand. For example, the type rules for letfun introduce uninstantiated specifications for the auxiliary functions. The tactic letfun_tac ls n takes a list of type instantiations ls, of the form [A_{1}, … A_{n}, λx_{1} … x_{n}.B(x_{1} … x_{n})], and a goal n. It applies a letfun-type rule to goal n, with the auxiliary types instantiated by the corresponding elements of ls. The appropriate goal is inferred from the length of ls.

In the same way, recursive auxiliary functions, declared using letrec, are introduced with the tactic letrec_tac. For example, in the development of an algorithm for insertion sort, the following goal arises.

1. [[ h: A; t: List(A) ]] ⟹ ?a(h, t) : {x:List(A), SORT (h • t, x)}

where SORT (l, m) holds iff m is an ordered permutation of l. An auxiliary function for insertion is specified by the tactic

    letrec_tac [A,{l:List(A),ORD(l)}, %a l.{x:List(A),SORT(a::l,x)}] 1

where ORD(l) holds iff l is ordered. This instantiates

?a(h, t) ⟵ letrec insert x l be ?a(x, l) in ?b(h, t, insert) end

and produces the goals

1. ∀ u:A.∀ v:{x:List(A), ORD(x)}.insert ‘ u ‘ v : {x:List(A), SORT (u • v, x)} ⟹ ?b(h, t, insert) : {x:List(A), SORT (h • t, x)}

2. [[ u: A; v : {x:List(A), ORD(x)} ]] ⟹ ?a(u, v) : {x:List(A), SORT (u • v, x)}

The body of the sorting algorithm is then derived by solving the first subgoal, assuming the existence of an insert function; the second subgoal specifies this function.

4.4.5 Properties of Recursive Calls

The induction hypothesis produced by rec-type (or letrec-type) asserts the type of recursive calls, including any properties that this may imply. In the example for lt in §4.4.1, the induction hypothesis was instantiated by type checking. But if recursive calls occur inside constructors, then this does not happen (by modifying the type rules this can be avoided, see §6.2.2). Instead, the following derived rule generates the appropriate instantiations of the induction hypothesis for each correctness condition.

\frac{∀ y:A.y ≺_{R} x ⊃ g(y) : \{z:B, P (z)\}  \begin{matrix}[ & g(a) : B ; P (g(a)) & ] \\ & Q(g(a)) \end{matrix}  a: A  a ≺_{R} x}{Q(g(a))}

Resolution with this rule uses unification to specialise an induction hypothesis produced by rec-type to an instance of the recursive call present in the current subgoal.

Similar rules are derived for letrec. For example, the following goal specifies a complete division algorithm.

1. lam n.lam d.letrec div n d be cond(lt ‘ n ‘ d, zero, succ(div ‘ (n − d) ‘ d))

in div ‘ n ‘ d end : Πn:Nat.Πd:{x:Nat, ¬x = zero}.{q:Nat, DIV (n, d, q)}

Type checking raises a set of correctness conditions, including the following one for the recursive call.

1. [[ n: Nat; d: {x:Nat, ¬x = zero};
∀ u:Nat.∀ v:{x:Nat, ¬x = zero}.
⟨u, v⟩ ≺_{?R} ⟨n, d⟩ ⊃ div ‘ u ‘ v : {q:Nat, DIV (u, v, q)} ]] ⟹
succ(div ‘ (n − d) ‘ d) : {q:Nat, DIV (n, d, q)}

Applying the derived rule for letrec specialises the induction hypothesis to give, after some type checking,

1. [[ n: Nat; d: {x:Nat, ¬x = zero}; DIV (n − d, d, div ‘ (n − d) ‘ d) ]] ⟹

DIV (n, d, succ(div ‘ (n − d) ‘ d))

2. [[ n: Nat; d: {x:Nat, ¬x = zero} ]] ⟹ ⟨n − d, d⟩ ≺_{?R} ⟨n, d⟩

The first goal is the correctness condition with an instance of the induction hypothesis for the recursive call div ‘ (n − d) ‘ d. The second goal is the termination condition for this recursive call.

4.4.6 Well-Founded Orderings

When a program is type checked, each recursive call gives rise to a subgoal of the form

a ≺_{R} b

These are solved using the rules for well-founded orderings (Figure 3.4).

The tactic prel_tac solves a restricted class of these goals whether or not R is instantiated. prel_tac succeeds if R is, or can be instantiated to, the primitive ordering over terms (pR) or a projection from tuples to the primitive ordering and the goal can be solved without using the transitivity of pR, otherwise the tactic fails—it always terminates.

If a and b are tuples, then prel_tac considers each element of the tuples in turn using the following projections.

wfst(R) ≡ map(λp.split(p, λx y.x), R)
wsnd(R) ≡ map(λp.split(p, λx y.y), R)

For example, the following are solved by prel_tac

\begin{matrix}⟨n, a⟩ ≺_{?R} & ⟨succ(n), a′⟩ \\ ⟨a, ⟨b, t⟩⟩ ≺_{?R} & ⟨a′, ⟨b′, h • t⟩⟩ \end{matrix}

instantiating ?R with wfst(pR) and wsnd(wsnd(pR)) respectively.

The set of functions for which prel_tac succeeds includes all those that are primitive recursive in one of their arguments.

4.5 Interpretation of First-Order Theories

Dependent types and subtypes are convenient for specifying programs and stating their correctness with respect to these specifications. But proving simple facts about particular data (e.g. that addition on natural numbers is commutative) is more convenient in simply typed logics in which type checking is decidable and so can be relegated to a well-formedness condition (e.g. typed first-order logic and higher-order logic).

To define new data types easily and state program correctness clearly, CCL uses the generalised type-formers Π and Σ, and subtypes. But CCL admits a direct interpretation of first-order logic extended with computational data types, which provides formal justification for the extensions and allows theorems proved in the first-order logic to be lifted up to theorems of CCL. In this sense, CCL acts as a meta-theory in which to formalise firstorder logic with a collection of computational types. Not every term-former of CCL has a simply typed counterpart; the constant rec cannot be simply typed, although primitive recursive functionals such as nrec can.

As Isabelle does not yet support theory interpretation, the interpretation of firstorder logic with computational types was carried out by hand. But the theorems in CCL corresponding to axioms of first-order logic were all derived using Isabelle, so that the reasoning done by hand was straightforward and kept to a minimum.

This section describes how interpretations can be set up for simple data types, for sorts of data types that admit certain properties and for abstract data types in which equality is interpreted by a congruence relation other than term equality. These are all based on Isabelle’s implementation of classical first-order logic FOL, described in §4.1.2.

4.5.1 Simple Data Types

FOL can be extended with a meta-type of booleans bool (giving FOL+BOOL). The extension BOOL has constants,

true :: bool
false :: bool
cond :: bool ⇒α⇒α⇒α

and axioms for conversion, the freeness of constructors and induction (case analysis).

cond(true, c, d) = c
cond(false, c, d) = d

¬true = false

\frac{P (true) P (false)}{P (b)}

where P :: bool ⇒o, restricting its application to terms of meta-type bool.

By mapping meta-type membership (::) on to type membership in CCL (:) and = :: bool ⇒ bool ⇒ o on to term equality, this extension is directly interpreted by the type Bool. The meta-types of the constants are simply typed versions of the type rules for their namesakes in CCL. Conversion, freeness and induction all follow from the theorems for Bool in Figure 4.2.

Similarly, a meta-type of natural numbers (nat) can be added (giving FOL+BOOL+NAT). The extension NAT has constants

zero :: nat
succ :: nat ⇒nat
ncase :: nat ⇒(nat ⇒α)⇒α
nrec :: nat ⇒(nat ⇒α⇒α)⇒α

and axioms for conversion, congruence (of ncase and nrec), the freeness of constructors and induction. Again, there is a direct interpretation justifying the extension, which maps the meta-type nat to the type Nat and = :: nat ⇒nat ⇒o to term equality.

4.5.2 Sorts of Data Types

In the programming language Haskell, types can belong to classes [29]. Membership of a class implies that a type supports certain operations. Similarly in Isabelle, meta-types belong to sorts. Type variables in axioms can be restricted to range over the types of a particular sort, so that membership of a sort implies that a type has certain (axiomatised) properties.

Computational types in extended first-order logic can belong to sorts in the same way as types in Haskell belong to classes. The sorts of computational types are interpreted in CCL as predicates over types (since there is a universe of types, τ). These predicates formalise the properties of sorts. Inclusion of a type in some sort a is justified by proving that the interpretation of the type in CCL satisfies the predicate which interprets a. For example, some data types in CCL admit a test for equality. Consider the definition

EQTYPE(A) ≡ Πa:A.Πb:A.{x:Bool, x = true ↔ a = b}

to which the sort eqterm ⋐ term in extended first-order logic corresponds. For any type A in CCL, if the following holds for some program eq_{A}

eq_{A} : EQTYPE(A)

then a meta-type α interpreted by A is included in the sort eqterm. Isabelle can automatically infer sort membership from properties of type-formers. In this case, the product type-former preserves membership of eqterm whereas the function type-former does not.

4.5.3 Abstract Data Types

The substitution rule in FOL implies that equality on each meta-type is a congruence relation. Any interpretation of equality must reflect this. In the extensions to FOL described above, equality on each new meta-type A (= :: A ⇒ A ⇒ o) is mapped to term equality in CCL (= :: ι ⇒ ι ⇒ o), so that any implied congruence axioms will trivially hold in the interpretation.

Abstract data types are encoded in much the same way as they are in programming languages. A representation type is defined in which the abstract type and operations defined over it are implemented. Equality between objects of this abstract type is then interpreted in CCL by some relation weaker than term equality. But in the interpretation of an abstract type, the implied congruence axioms must be proved for the relation interpreting equality. This is illustrated by the following development of a theory of finite sets, in which equality between sets is defined to reflect the idempotent and commutative nature of set ‘cons’.

α_{=} set is the meta-type of finite sets of elements of equality type α_{=}. SET introduces the meta-type former set and constants for the empty set ∅, set ‘cons’ ⊙, set membership mem, subsets subseteq, cardinality card, collection {· | ·}, replacement {· | · , ·}, union ⋃ and power set Pow. Write finite sets x ⊙ ∅, x ⊙ y ⊙ ∅ etc. as { x }, { x, y } etc. The axioms of SET (Figure 4.6) provide

• induction over sets,

• conversions for mem , subseteq and card,

• set axioms for extensionality, collection, replacement, union and power sets, and

• congruence rules for the higher-order constants {· | ·} and {· | · , ·}.

Predicates for membership and subsets, and functions for set union, intersection and difference are defined (Figure 4.6). The usual theorems for finite sets can be developed within SET.

SET is interpreted in CCL by mapping α_{=} set on to the representation type List(T), where T is the equality type that interprets α_{=}, and defining a new relation =_{set}::ι⇒ι⇒o for set equality. The relation =_{set} is defined in CCL (using mem, ∈ and ⊆) as follows:

a mem A ≡ lrec(A, false, λx X g.(a eq_{T} x) or g)
a ∈ A ≡ a mem A = true
A ⊆ B ≡ ∀ x. x ∈ A ⊃ x ∈ B
A =_{set} B ≡ A ⊆ B ∧ B ⊆ A

It is simple to show that =_{set} is an equivalence relation. As intended, list ‘cons’ (•) is idempotent and commutative with respect to =_{set}—the following are theorems in CCL.

\begin{matrix}x • x • A =_{set} & x • A \\ x • y • A =_{set} & y • x • A \end{matrix}

The constants of SET are mapped on to the following terms in CCL.

∅ ↦ []
⊙ ↦ •
a mem A ↦ lrec(A, false, λx X g.(a eq_{T} x) or g)
A subseteq B ↦ lrec(A, true, λx X g.(x mem B) and g)
card(A) ↦ lrec(A, [], λx X g.cond(x mem X, g, succ(g)))
{x ∈ A | p(x)} ↦ lrec(A, [], λx X g.cond(p(x), x • g, g))
{y | x ∈ A , y = f(x)} ↦ lrec(A, [], λx X g.f(x) • g)
A ∪ B ↦ lrec(A, B, λx X g.x • g)
⋃(A) ↦ lrec(A, [], λx X g.x ∪ g)
Pow(A) ↦ lrec(A, [] • [], λx X g.{y | z ∈ g , y = x • z} ∪ g)

Note that set collection is mapped on to the list functional filter, replacement on to map, ∪ on to the function append and ⋃ on to a function that flattens lists of lists down to

¬∅ = a ⊙ A  \frac{P (∅)  \begin{matrix}[ P (X) ] & x,X \\ P (x ⊙ X) \end{matrix}}{P (A)}
a mem ∅ = false  a mem b ⊙ A = (a eq_{T} b) or a mem A
∅ subseteq A = true  a ⊙ A subseteq B = (a mem B) and (A subseteq B)
card(∅) = zero  card(a ⊙ A) = cond(a mem A, card(A), succ(card(A)))

\begin{matrix}A = B ↔ & (∀ x. x ∈ A ↔ x ∈ B) \\ a ∈ \{x ∈ A | p(x)\} ↔ & a ∈ A ∧ p(a) = true \\ a ∈ \{y | x ∈ A , y = f(x)\} ↔ & (∃ y. y ∈ A ∧ a = f(y)) \\ a ∈ ⋃ A ↔ & (∃ X . X ∈ A ∧ a ∈ X) \\ a ∈ Pow(A) ↔ & a ⊆ A \end{matrix}

\frac{A = A′  p(x) = p′(x)^{x}}{\{x ∈ A | p(x)\} = \{x ∈ A′ | p′(x)\}} ; \frac{A = A′  f(x) = f′(x)^{x}}{\{y | x ∈ A , y = f(x)\} = \{y | x ∈ A′ , y = f′(x)\}}

Axioms

a ∈ A ≡ a mem A = true
A ⊆ B ≡ A subseteq B = true
A ⊂ B ≡ A ⊆ B ∧ ¬A = B
A ∪ B ≡ ⋃{ A, B }
A ∩ B ≡ {x ∈ A | x ∈ B}
A − B ≡ {x ∈ A | ¬x ∈ B}

Definitions

Figure 4.6: Axioms for Finite Set Theory lists. Under this interpretation the axioms of Figure 4.6 are theorems in CCL. In addition, the following congruences hold (implied by the properties of equality in FOL), which justify the interpretation of = :: set ⇒set ⇒o by =_{set} :: ι⇒ι⇒o.

\frac{x = x′  A =_{set} A′}{x • A =_{set} x′ • A′}  \frac{x = x′  A =_{set} A′}{x mem A = x′ mem A′}

\frac{A =_{set} A′  B =_{set} B′}{A ⊆ B ↔ A′ ⊆ B′}  \frac{A =_{set} A′}{card(A) = card(A′)}

\frac{A =_{set} A′ p(x) = p′(x)^{x}}{\{x ∈ A | p(x)\} =_{set} \{x ∈ A′ | p′(x)\}}

\frac{A =_{set} A′ f(x) = f′(x)^{x}}{\{y | x ∈ A , y = f(x)\} =_{set} \{y | x ∈ A′ , y = f′(x)\}}

\frac{A =_{set} A′}{⋃ A =_{set} ⋃ A′}  \frac{A =_{set} A′}{Pow(A) =_{set} Pow(A′)}

4.6 Summary of Implementation

There are, effectively, two separate implementations: the theory CCL and first-order logic with extensions for computational types. Translation between these two theories is by hand; interpreting the axiomatisation of new types in FOL by types in CCL, and lifting lemmas proved in an extension of FOL up to theorems in CCL. But these translations are straightforward, requiring little more than cutting and pasting formulae between theories. For each new meta-type added to FOL, theorems are proved in CCL that correspond to the axioms added to FOL.

The Isabelle theory CCL is an extension of the existing theory FOL. From the axioms described in Chapter 3, the theorems of §4.2 are derived. For defined data types, the rules described in §4.3 are proved using simple tactics. The major piece of outstanding work required to automate this process is a parser for syntax in the style of an ML datatype statement. The complete set of tactics used in CCL is a little over 100 lines of ML code. The extensions to Isabelle’s FOL are axiomatised in §4.5. The standard Isabelle tactics are used for natural deduction inference (fast_tac) and rewriting and induction (using the simplifier). The fact that standard tactics already exist is one reason that these theories were used. They are also more efficient, as there is more information relevant to proof search in the meta-logic.

66 Chapter 4. Implementation

Proving Programs Correct

This chapter describes how the implementation of CCL is used to reason about program correctness.

In CCL, both termination and correctness are expressed as goals of the form a : A, which allows type checking to direct proofs. Correctness proofs are done in the following three stages: correctness is stated as a goal a: A, type checking reduces this goal to a set of correctness conditions, and these are then translated to an appropriate first-order logic and proved. Verification and derivation differ only in the degree to which a is initially instantiated. To give an indication of how suited CCL is to reasoning about program correctness, the derivation of Robinson’s unification algorithm is presented as an extended example.

§5.1 describes how CCL is used to reason about termination. §5.2 describes how specifications are developed in CCL. Verification and derivation are introduced in §5.3 and §5.4 respectively. In each case, separate goals arise for termination, which are identical to those described in §5.1. §5.5 describes how correctness conditions are proved in firstorder logic. Finally, §5.6 presents the extended example: unification. Hypotheses that are redundant or just assert simple type information are sometimes omitted from goals in the following examples to maintain legibility.

5.1 Termination

If a program of L is typeable in CCL, then it terminates (Theorem 3.10). Primitive recursive functions can be defined using functionals such as nrec and lrec introduced in §4.3.2. Proving that these functions terminate is simply a matter of type checking—as in Martin-Löf’s Type Theory, the type rules for primitive recursive functionals ensure termination. For example, the following goal asserts that an addition algorithm is total over the type Nat.

1. lam m.lam n.nrec(m, n, λx g.succ(g)) : Nat →Nat →Nat

Applying typechk_tac immediately solves the goal.

More generally, recursive programs are defined using the destructor rec or the derived forms of letrec. In these cases, type checking raises a termination condition for each recursive call in the program of the form

x ≺_{R} y where x is the tuple of arguments in the recursive call, and y is the tuple of formal parameters over which recursion is defined. These goals are solved and termination is proved by instantiating ?R with a well-founded ordering that orders every recursive call. If recursion is primitive in one of its arguments, then the tactic prec_tac finds a suitable ordering (namely a projection on to the primitive ordering pR) and automatically solves the termination conditions. For example, the primitive recursive algorithm for addition described above can be written using letrec and ncase instead of nrec. The following goal asserts that this version of addition is also total over the type Nat.

1. lam m.lam n. letrec add m n be ncase(m, n, λx.succ(add ‘ x ‘ n))
in add ‘ m ‘ n end : Nat →Nat →Nat

Applying typechk_tac reduces the goal to a single condition on termination (for the single recursive call).

1. ⟨x, n⟩ ≺_{?R} ⟨succ(x), n⟩

This is primitive recursive in its first argument, and so is immediately solved by prec_tac. Note that there is no disadvantage in considering recursion over a tuple of the function’s arguments.

In more complex recursion schemes, type checking still raises termination conditions, but these may not be solved by prec_tac. For example, the following goal asserts that Ackermann’s function is total over the type Nat.

1. lam m.lam n. letrec ack m n be ncase(m, succ(n),

λx.ncase(n, ack ‘ x ‘ succ(zero)

λy.ack ‘ x ‘ (ack ‘ succ(x) ‘ y)))

in ack ‘ m ‘ n end : Nat →Nat →Nat

Applying typechk_tac reduces the goal to the following three conditions on termination (one for each recursive call).

1. ⟨x, succ(zero)⟩ ≺_{?R} ⟨succ(x), zero⟩
2. ⟨succ(x), y⟩ ≺_{?R} ⟨succ(x), succ(y)⟩
3. ⟨x, ack ‘ succ(x) ‘ y⟩ ≺_{?R} ⟨succ(x), succ(y)⟩

Nested recursion is automatically handled in type checking. By the induction hypothesis generated from the rule letrec-type, the inner call ack ‘succ(x)‘y is of type Nat if subgoal (2) holds. Using the type of the inner call and the induction hypothesis again, the outer call is of type Nat if subgoal (3) holds. In fact, the nested recursion in Ackermann’s function is rather simple—termination depends only on the nested call being simply typed. In the unification algorithm, presented in §5.6, termination depends on deeper properties of the nested call.

The termination conditions for Ackermann’s function cannot be solved by prec_tac. The following lexicographic ordering is needed.

⟨a_{1}, a_{2}⟩ ≺ ⟨b_{1}, b_{2}⟩ iff a_{1} < b_{1} ∨ (a_{1} = b_{1} ∧ a_{2} < b_{2})

In CCL, the slightly weaker relation lex(pR, pR) can be used. The axiom for lex (see Figure 3.4) and the derived rule n ≺pR succ(n) (see Figure 4.4) allow the termination conditions to be solved.

Termination conditions may depend on complex properties. For example, the following goal asserts that a division algorithm is total over Nat for non-zero denominators (the algorithm clearly diverges for a denominator of zero).

1. lam n.lam d. letrec div n d be cond(lt ‘ n ‘ d, zero, succ(div ‘ (n − d) ‘ d))

in div ‘ n ‘ d end : Nat →{x:Nat, ¬x = zero} →Nat

Applying typechk_tac reduces the goal to the following termination condition.

1. [[ n: Nat; d: {x:Nat, ¬x = zero} ]] ⟹ ⟨n, n − d⟩ ≺_{?R} ⟨n, d⟩

Assuming the following lemmas for all x and y in Nat, provable in extended first-order logic, the goal is solved by instantiating ?R ⟵ wsnd(pR).

\begin{matrix}¬y = zero ⊃ & x − y < x \\ x < y ⊃ & x ≺pR y \end{matrix}

5.2 Specifying Correctness

In CCL, simple types provide a coarse level of specification that ensures termination. As described in §2.2, subtypes and the generalised function type-former Π can be used to specify the input/output behaviour of programs. The type

Πx:{x:A, P (x)}.{y:B, Q(x, y)}

is inhabited by functions which, when applied to any a:A such that P (a) holds, terminate with a result b: B such that the input/output relation Q(a, b) holds.

The connectives of first-order logic together with equality and type membership allow specifications to be conveniently expressed. For example, assuming programs for the usual arithmetic operators +, × and −, and a boolean valued function lt corresponding to the predicate < (see §4.4.1), the property of being the integer quotient q of n divided by d is expressed as

DIV (n, d, q) ≡ ∃ r:Nat.r < d ∧ n = q × d + r

Note that DIV (n, d, q) is unsatisfiable if d equals zero, since there exists no r such that r < zero. A program for division using non-zero divisors is specified by the following type.

Πn:Nat.Πd:{x:Nat, ¬x = zero}.{q:Nat, DIV (n, d, q)}

Similarly, the property of being the minimum element of a list l of type Nat is simply

MINL(l, a) ≡ a in l ∧ ∀ x:List(Nat).x in l ⊃ a ≤ x

where in is an infix predicate that holds iff the first argument is an element of the second. The predicate in is defined in terms of the program inp by

inp ≡ lam l.lam a.lrec(l, false, λx xs g.(a eq_{nat} x) or g)
a in l ≡ inp ‘ l ‘ a = true

A program for finding the minimum element of a non-empty list of elements of type Nat is specified by the following type.

Πl:{x:List(Nat), ¬x = []}.{a:Nat, MINL(l, a)}

A sorting algorithm should output an ordered permutation of its input. If ≤ is a computable ordering of some equality type A (with corresponding program le), then a predicate ORD is defined in terms of the program ord by

ord ≡ lam l.lrec(l, true, λx xs g.lcase(xs, true, λy ys.(le ‘ x ‘ y) and g))
ORD(l) ≡ ord ‘ l = true

so that ORD(l) holds iff the list l is ordered. Permutations are defined in terms of the program noccs, which returns the number of occurrences of a term a in the list l.

noccs ≡ lam a.lam l.lrec(l, zero, λx xs g.cond(a eq_{A} x, succ(g), g))
PERM (k, l) ≡ ∀ a∈A. noccs ‘ a ‘ k = noccs ‘ a ‘ l

By defining ord and noccs in terms of primitive recursive functionals, they can be immediately translated into extended first-order logic, allowing properties of ORD and PERM to be more easily derived. If ord and noccs were written using rec or letrec, then their conversion rules could be used as axioms instead, since rec and letrec cannot in general be simply typed.

A sorted list is defined as an ordered permutation of the original.

SORT (k, l) ≡ ORD(l) ∧ PERM (k, l)

Sorting algorithms are specified by the following type

Πl:List(A).{x:List(A), SORT (l, x)}

5.3 Verification

Checking that a program inhabits a simple type raises conditions sufficient for termination; checking that a program inhabits a more complete specification raises conditions for correctness as well as termination.

The tactics for type checking reduce goals of the form a : A to sets of correctness conditions. These conditions can be somewhat simplified before they are translated into extended first-order logic and proved. In particular,

• subtypes in hypotheses can be broken down into simple types and predicates (using {}-elim);

• substitutions that appear as hypotheses in a goal, generated by the strengthened type rules for destructors, can be carried out both in the goal’s conclusion and in its other hypotheses; and

• induction hypotheses can be specialised to recursive calls that appear in the conclusion or premises of each goal, unless a specialised hypothesis has already been produced by type checking (see §4.4.1).

All three kinds of simplification are illustrated in the following example. Consider a function that takes an element a and an ordered list l as arguments, and inserts a into l in a way that preserves the ordering. It is proved correct by solving the following goal.

1. lam a.lam l.letrec insert a l be
lcase(l, a • [], λx xs.cond(le ‘ a ‘ x, a • x • xs, x • (insert ‘ a ‘ xs)))

in insert ‘ a ‘ l end : Πa:A.Πl:{x:List(A), ORD(x)}.{x:List(A), SORT (a • l, x)} Applying typechk_tac reduces the goal to the following correctness conditions.

1. SORT (a • [], a • [])

2. [[ l: {x:List(A), ORD(x)}; l = h • t ]] ⟹ ORD(t)

3. l = h • t ⟹ ⟨a, t⟩ ≺_{?R} ⟨a, l⟩

4. [[ a ≤ h; l: {x:List(A), ORD(x)}; l = h • t ]] ⟹ SORT (a • h • t, a • h • t)

5. [[ ∀ u:A.∀ v:{x:List(A), ORD(x)}. ⟨u, v⟩ ≺_{?R} ⟨a, l⟩ ⊃
insert ‘ u ‘ v : {x:List(A), SORT (u • v, x)};

¬a ≤ h; l: {x:List(A), ORD(x)}; l = h • t ]] ⟹ SORT (a • h • t, h • (insert ‘ a ‘ t))

In goals (2) and (4), the subtype l: {x:List(A), ORD(x)} is broken down with {}-elim. In goals (2), (3) and (4), the hypothesis l = h • t is used to substitute h • t for l in other hypotheses and in the conclusion. In (5), the induction hypothesis is instantiated with the call insert ‘ a ‘ t. This leaves the following set of simplified correctness conditions.

1. SORT (a • [], a • [])

2. ORD(h • t) ⟹ ORD(t)

3. ⟨a, t⟩ ≺_{?R} ⟨a, h • t⟩

4. [[ a ≤ h; ORD(h • t) ]] ⟹ SORT (a • h • t, a • h • t)

5. [[ SORT (a • t, insert ‘ a ‘ t); ¬a ≤ h; ORD(h • t) ]] ⟹

SORT (a • h • t, h • (insert ‘ a ‘ t))

In principle, these simplifications could be included in a tactic for type checking, so that specifications of correctness are reduced to sets of simplified correctness conditions in a single step. Moreover, if theory interpretation was implemented, these conditions could be automatically translated into first-order logic. Consider such a tactic for automatically generating a set of correctness conditions in first-order logic. The following goal states that an algorithm meets the specification for division given earlier.

1. lam n.lam d. letrec div n d be cond(lt ‘ n ‘ d, zero, succ(div ‘ (n − d) ‘ d))

in div ‘ n ‘ d end : Πn:Nat.Πd:{x:Nat, ¬x = zero}.{q:Nat, DIV (n, d, q)}

It would be reduced by such a tactic to the following correctness conditions in first-order logic.

1. n < d ⟹ ∃ r. r < d ∧ n = zero × d + r

2. [[ ¬n < d; ∃ r. r < d ∧ n − d = q × d + r ]] ⟹ ∃ r. r < d ∧ n = succ(q) × d + r

3. ¬d = zero ⟹ ⟨n − d, d⟩ ≺_{?R} ⟨n, d⟩

5.4 Derivation

As type checking continues only as far as a term is instantiated, programs can be instantiated in a stepwise fashion during proof. Again, consider the example of subtractive division. Derivation starts with the following goal.

1. ?a : Πn:Nat.Πd:{x:Nat, ¬x = zero}.{q:Nat, DIV (n, d, q)}

The tactic letrec_tac instantiates the program

?a ← lam n.lam d.letrec div n d be ?b(n, d, div) in div ‘ n ‘ d end

and generates an induction hypothesis, leaving the following goal.

1. ∀ u:Nat.∀ v:{x:Nat, ¬x = zero}. ⟨u, v⟩ ≺_{?R} ⟨n, d⟩ ⊃
div ‘ u ‘ v : {x:Nat, DIV (u, v, x)} ⟹
?b(n, d, div) : {x:Nat, DIV (n, d, x)}

An obvious approach, according to Manna and Waldinger [34], is to consider solving the first conjunct in the predicate DIV , namely n < d. Partially instantiating the program

using itypechk_tac "cond(lt`n`d,?t,?u)" [] 1 generates the following subgoals.

1. n < d ⟹ ?t(n, d, div) : {x:Nat, DIV (n, d, x)}

2. ¬n < d ⟹ ?u(n, d, div) : {x:Nat, DIV (n, d, x)}

The first branch is further instantiated by itypechk_tac "zero" [] 1, giving

1. n < d ⟹ ∃ r:Nat.(r < d) ∧ (n = zero × d + r)

2. ¬n < d ⟹ ?u(n, d, div) : {x:Nat, DIV (n, d, x)}

Choosing r = n, (1) becomes n < d ⟹ n < d and n = zero × d + n, which are clearly solvable by arithmetic reasoning. The constructor succ is the only other possible result, and with some insight the appropriate recursion can be seen. Applying

itypechk_tac "succ(div`(m-n)`n)" [] gives

1. [[ ¬n ≤ d; DIV (n − d, d, div ‘ (n − d) ‘ d) ]] ⟹ DIV (n, d, succ(div ‘ (n − d) ‘ d))

2. ¬d = zero ⟹ ⟨n − d, d⟩ < ⟨n, d⟩

which may be solved by arithmetic reasoning.

Whether this example convincingly syntheses an algorithm is not relevant—though many papers have been written with such claims. The important point is that the outline of an algorithm may be considered, and the proof obligations inherent in it examined. If these prove satisfactory, then further instantiations can be made, and if necessary retracted, until the program is complete.

5.5 Proving Correctness Conditions

Proving termination, verifying correctness and deriving correct algorithms all raise correctness conditions. The major effort in any proof of correctness is in proving these conditions. In fact, the preliminary steps of correctness proofs are so straightforward that automation is feasible (see §6.2.3).

For convenience, correctness conditions are proved in first-order logic extended with computational types, and then lifted up to CCL using the interpretations described in §4.5. In first-order logic, standard theorem proving techniques are used for reasoning by induction (ind_tac), rewriting (asm_simp_tac and asm_simp_case_tac) and simple logical inference (fast_tac).

5.6 An Extended Example: Unification

In 1965, Robinson [58] described an algorithm to unify two expressions. If the expressions have a common instance then the algorithm generates a substitution to yield this instance, otherwise it indicates that the expressions have no such instance. The algorithm was called unification and has become central to logic programming and theorem proving. Much work has been done on subsequent improvements [38]; the original algorithm is considered here.

Unification is a good choice for an extended example. Although logically complex, it is a fairly small piece of code that can be succinctly presented and should be familiar to many in this field. It has previously been used as an example by Manna and Waldinger [35], who produced a derivation by hand using their deductive tableau system, and subsequently by Paulson [51], who verified the algorithm on machine using LCF. It has also been synthesised as a logic program by Eriksson [18]. In particular, it is a good choice for the logic CCL, as the proof of termination is rather delicate.

First, a formal specification of the algorithm is given. Then, the first-order theories that arise from this specification are described. Finally, a derivation of the algorithm is considered, and the correctness conditions proved. The majority of lemmas used in establishing correctness are proved by induction followed by rewriting and some propositional reasoning. Most are, therefore, listed without any detail of the proofs. The definitions used to formalise unification are fairly close to Paulson, except for the treatment of termination, which follows Manna and Waldinger. This is not intended to be a full description of the formal derivation of unification (which would needlessly repeat much of Manna and Waldinger’s paper), but rather an example that illustrates how proofs of correctness are handled in CCL.

5.6.1 A Formal Specification of Correctness

In the following development, programs are defined by primitive recursion over particular data types. To simplify the presentation, only conversion rules are given rather than complete definitions.

For simplicity, abstract terms are considered as binary trees. This is sufficient to represent Lisp S-expressions and combinator expressions. A term is

• a constant a, b, c, or

• a variable x, y, z, or

• a pair of terms (t, u).

In CCL, the types of constants and variables are taken as parameters of the extended example, and for each an equality function is assumed (eq_{const} and eq_{var} respectively). Terms are formalised as the inductive type Term.

Term ≡ μ X . Const + Var + X × X

with constructors const, var and comb respectively and destructors termcase and termrec. The usual rules for typing, conversion, congruence, the freeness of constructors and induction are derived.

The set of variables in a term, vars :: ι⇒ι, is defined inductively over the structure of terms so that the following conversions hold.

vars(const(c)) = ∅
vars(var(v))  = { v }
vars(comb(t, u)) = vars(t) ∪ vars(u)

Note that this uses the finite set theory described in §4.5.3.

The infix, boolean valued functions occs :: ι⇒ι⇒ι and occseq :: ι⇒ι⇒ι are defined so that t occs u evaluates to true iff t strictly occurs in u, and t occseq u evaluates to true iff t occurs in or equals u. The following conversions are immediate consequences of the definitions.

t occs const(c) = false
t occs var(v)  = false
t occs comb(u, v) = (t occseq u) or (t occseq v)
t occseq u  = (t eq_{term} u) or (t occs u)

where or is an infix boolean valued functions corresponding to the predicate ∨, namely lam a.lam b.cond(a, true, b).

Constants are fixed; variables can be replaced by terms. Write t/x for the replacement of x by t. A substitution θ is a finite set of replacements

{t_{1}/x_{1}, … t_{n}/x_{n}}

in which the variable names (x_{i}) are distinct and no replacement is trivial (x_{i}/x_{i}). Applying a substitution θ to a term t simultaneously replaces every occurrence in t of each variable that is in θ with its corresponding replacement term. The domain of a substitution is the set of variables that are so replaced; the range of a substitution is the set of variables that appear in the replacement terms. For example, applying the substitution {const(c)/x, var(x)/y}, whose domain is the set { x, y } and whose range is { x }, to the term

comb(comb(const(a), var(x)), comb(var(y), var(z)))

generates the term

comb(comb(const(a), const(c)), comb(var(x), var(z)))

Note that variables that do not occur in the domain remain unchanged, and as in this case the domain and range of a substitution need not be distinct.

Following Paulson [51], substitutions are represented by association lists rather than sets, as this is more convenient for the proof of correctness. They are formally represented by the inductive type Alist.

Alist ≡ μ X . Unit + Var × Term × X

with constructors anil and acons respectively and destructor alrec. Application is defined in two stages. First, the application of a substitution to a variable is defined by the function assoc :: ι ⇒ ι ⇒ ι. If variable v appears in substitution θ then assoc(v, θ) returns the term corresponding to the first occurrence, otherwise it returns the default term var(v). The following conversions hold.

assoc(v, anil) = var(v)
assoc(v, acons(w, t, θ)) = cond(v eq_{var} w, t, assoc(v, θ))

Secondly, the application of a substitution to a term is inductively defined over terms by the infix function ◁:: ι⇒ι⇒ι, so that the following conversions hold.

const(c) ◁ θ = const(c)
var(v) ◁ θ = assoc(v, θ)
comb(t, u) ◁ θ = comb(t ◁ θ, u ◁ θ)

This is one possible representation of the informal description above. Multiple occurrences of variables in substitutions are effectively removed, since assoc considers only the first occurrence. The choice of default term for assoc ensures that a trivial substitution behaves on application in the same way as an empty substitution.

Further term-formers over substitutions (for domain, range and equality) are defined in such a way that this representation of substitutions correctly interprets the informal description above. The domain of a substitution, dom :: ι⇒ι, is defined to exclude trivial substitutions, so that the following conversions hold.

dom(anil)  = ∅
dom(acons(v, t, θ)) = cond(var(v) eq_{var} t, dom(θ) − { v }, v ⊙ dom(θ))

The range of a substitution, range :: ι ⇒ ι, is defined in terms of its domain using set replacement (see §4.5).

range(θ) ≡ ⋃{y | x ∈ dom(θ) , y = vars(x ◁ θ)}

Equality between substitutions, =_{subst} :: ι⇒ι⇒o, is defined extensionally.

θ =_{subst} ϕ ≡ ∀ t:Term.t ◁ θ = t ◁ ϕ

These definitions permit the following congruences to be derived.

\frac{v_{1} = v_{2} θ_{1} =_{subst} θ_{2}}{assoc(v_{1}, θ_{1}) =_{subst} assoc(v_{2}, θ_{2})}

\frac{t_{1} = t_{2}  θ_{1} =_{subst} θ_{2}}{t_{1} ◁ θ_{1} = t_{2} ◁ θ_{2}}  \frac{θ_{1} =_{subst} θ_{2}}{dom(θ_{1}) =_{set} dom(θ_{2})}

This ensures that the formal representation captures the intended meaning, and allows the first-order theory SUBST in §5.6.2 to be interpreted. Note that =_{subst} is not a congruence relation with respect to the term-former alrec, which is therefore omitted in the theory

SUBST.

The composition of two substitutions is such that, for all terms, applying the composition is the same as applying the first substitution and then applying the second. Formally, composition is defined as the infix function ⋄:: ι⇒ι⇒ι, so that the following conversions hold.

anil ⋄ θ = θ
acons(v, t, ϕ) ⋄ θ = acons(v, t ◁ θ, ϕ ⋄ θ)

The definitions leading to the notion of a most general, idempotent unifier are now formally introduced. A substitution θ unifies two terms t and u iff applying the substitution makes the terms agree.

Unifies(θ, t, u) ≡ (t ◁ θ = u ◁ θ)

There may be many unifiers for a pair of terms. For example, the terms var(x) and var(y) can be unified by the substitutions {var(x)/y}, {var(y)/x}, or {t/x, t/y} for any term t. A substitution θ is more general than a substitution ϕ iff ϕ can be expressed as an instance of θ composed with some substitution ψ.

θ ≫ ϕ ≡ ∃ ψ:Alist.ϕ =_{subst} θ ⋄ ψ

A unifier θ of terms t and u is most general iff it is more general than every unifier of t and u.

MGU(θ, t, u) ≡ Unifies(θ, t, u) ∧ (∀ ϕ:Alist.Unifies(ϕ, t, u) ⊃ θ ≫ ϕ)

From this definition, every unifier of the terms t and u can be obtained from a most general unifier by composition with a further substitution. A substitution θ is idempotent iff it remains unchanged when composed with itself.

Idem(θ) ≡ θ ⋄ θ =_{subst} θ

For the algorithm to behave correctly, it must find a most general unifier, if one exists; for the proof of correctness to succeed, the unifier must also be idempotent.

BestUnifier(θ, t, u) ≡ MGU(θ, t, u) ∧ Idem(θ)

The absence of a unifier is indicated by using the following data type for optional results.

Opt(A) ≡ Unit + S(A)

with constructors none and some respectively and destructor optcase. The result a of trying to unify the terms t and u is defined as

TryBestUnifier(a, t, u) ≡ (a = none ∧ ∀ θ:Alist.¬Unifies(θ, t, u)) ∨
(∃ θ:Alist.a = some(θ) ∧ BestUnifier(θ, t, u))

Finally, a program for unification is specified by the type

Πt:Term.Πu:Term.{a:Opt(Alist), TryBestUnifier(a, t, u)}

5.6.2 First-Order Theories

Each data type defined in CCL interprets a meta-type in FOL. The data types introduced for unification (Term, Alist and Opt) lead to extensions of FOL (TERM, SUBST and OPT respectively). The interpretation of TERM and OPT are straightforward. The interpretation of SUBST uses the representation type Alist, and maps = :: subst ⇒subst ⇒o to =_{subst} in a similar way to the interpretation of finite set theory in §4.5.

TERM

TERM introduces the meta-type term with constants const, var, comb and termrec, and axioms for the freeness of constructors, induction and conversion for termrec. There is a straightforward interpretation of TERM by the type Term, in which = :: term ⇒ term ⇒ o maps to = :: ι⇒ι⇒o.

In TERM, the constants

vars :: term ⇒var set
occs :: term ⇒term ⇒bool
occseq :: term ⇒term ⇒bool

are defined as

vars(t) ≡ termrec(t, λc.∅, λv.{ v }, λx y g h.g ∪ h)
t occs u ≡ termrec(u, λc.false, λv.false, λx y g h.((t eq x) or g) or ((u eq x) or h))
t occseq u ≡ (t eq u) or (t occs u)

The conversion rules of §5.6.1 are immediately derived from these definitions.

Using induction and the freeness of constructors, theorems are derived for the wellfoundedness of terms

¬comb(t, u) = t ¬comb(t, u) = u

the transitivity of occs

t occs u = true ⊃ u occs v = true ⊃ t occs v = true

and, using transitivity, the irreflexivity of occs

t occs t = false

By rewriting, the following equivalences for vars are derived.

v ∈ vars(var(w)) ↔ w = v
v ∈ vars(t)  ↔ var(v) occseq t = true

OPT

OPT introduces the meta-type opt with constants none, some and optcase, and axioms for the freeness of constructors, induction and conversion for optcase. There is a straightforward interpretation of OPT by the type Opt, in which = :: α opt ⇒ α opt ⇒ o maps to = :: ι⇒ι⇒o.

¬anil = acons(v, t, θ) \frac{P (anil)  \begin{matrix}[ P (X) ] & X \\ P (acons(v, t, X)) \end{matrix}}{P (θ)}

θ = ϕ ↔ (∀ t. t ◁ θ = t ◁ ϕ)

assoc(v, anil) = var(v)  assoc(v, acons(w, t, θ)) = cond(v eq w, t, assoc(v, θ))
anil ⋄ θ = θ  acons(v, t, ϕ) ⋄ θ = acons(v, t ◁ θ, ϕ ⋄ θ)
dom(anil) = ∅
dom(acons(v, t, θ)) = cond(var(v) eq t, dom(θ) − { v }, v ⊙ dom(θ))

Axioms

t ◁ θ ≡ termrec(t, λc.const(c), λv.assoc(v, θ), λx y g h.comb(g, h))
range(θ) ≡ ⋃({y | x ∈ dom(θ) , y = vars(var(x) ◁ θ)})

Definitions

Figure 5.1: A Theory of Substitutions

SUBST

SUBST introduces the meta-type subst with constants

anil :: subst
acons :: var ⇒term ⇒subst ⇒subst
assoc :: var ⇒subst ⇒term
⋄ :: subst ⇒subst ⇒subst
dom :: subst ⇒var set

and the axioms shown in Figure 5.1 for induction, extensional equality and conversion, and definitions for substitution and range.

◁ :: term ⇒subst ⇒subst
range :: subst ⇒var set

There is an interpretation of SUBST in which the meta-type subst is mapped on to the representation type Alist and = :: subst ⇒ subst ⇒ o is mapped on to =_{subst}, and the necessary congruences for =_{subst} all hold.

In SUBST, conversion rules for ◁ are immediately derived. Using these and the other rewrite rules of SUBST, the facts shown in Figure 5.2 are derived. In this case, the Isabelle proof scripts are shown in Figure 5.4; hereafter, they are omitted. For the domain and range of substitutions, the facts in Figure 5.3 are derived.

t ◁ ϕ ⋄ θ = t ◁ ϕ ◁ θ
q ⋄ ϕ ⋄ θ = q ⋄ (ϕ ⋄ θ)
acons(v, var(v) ◁ θ, θ) = θ
t occs u = true ⊃ t ◁ θ occs u ◁ θ = true
var(v) occs t = false ⊃ t ◁ acons(v, t ◁ θ, θ) = t ◁ θ
t ◁ ϕ = t ◁ θ ↔ (∀ v. v ∈ vars(t) ⊃ var(v) ◁ ϕ = var(v) ◁ θ)
¬v ∈ vars(t) ⊃ t ◁ acons(v, u, θ) = t ◁ θ
v ∈ vars(t) ⊃ w ∈ vars(t ◁ acons(v, var(w), θ))

Figure 5.2: Facts about Substitutions

v ∈ dom(s) ↔ ¬var(v) ◁ s = var(v)
v ∈ range(s) ⊃ (∃ w. w ∈ dom(s) ∧ v ∈ vars(var(w) ◁ s))
t ◁ s = t ↔ dom(s) ∩ vars(t) = ∅

v ∈ dom(s) ⊃ ¬v ∈ range(s) ⊃ ¬v ∈ vars(t ◁ s) v ∈ dom(s) ⊃ v ∈ vars(t ◁ s) ⊃ v ∈ range(s)

v ∈ vars(t ◁ s) ⊃ v ∈ range(s) ∨ v ∈ vars(t)
dom(s) ∩ range(s) = ∅ ↔ (∀ t. dom(s) ∩ vars(t ◁ s) = ∅)

Figure 5.3: Facts about Domains and Ranges 80 Chapter 5. Proving Programs Correct

goal subst_thy  "t <| r <> s = t <| r <| s";
by (ind_tac "t" 1);
by (ind_tac "r" 2);
by (ALLGOALS (asm_simp_case_tac [substC2] []));
val subst_comp = result();
goal subst_thy  "q <> r <> s = q <> (r <> s)";
by (ind_tac "q" 1);
by (ALLGOALS (asm_simp_tac [subst_comp] []));
val comp_assoc = result();
goal subst_thy  "acons(w,var(w) <| s,s) = s";
br substeqI 1;
by (ind_tac "t" 1);
by (ALLGOALS (asm_simp_case_tac [substC2,eq_iff1] []));
val acons_trivial = result();
goal subst_thy  "t occs u = true --> t <| s occs u <| s = true";
by (ind_tac "u" 1);
by (ALLGOALS (asm_simp_tac [or_true,eq_iff1] []));
by (fast_tac FOL_cs 1);
val subst_mono = result();
goal subst_thy  "var(v) occs t = false --> t <| acons(v,t <| s,s) = t <| s";
by (cla_case_tac "t = var(v)" 1);
by (res_inst_tac [("P","\%x.~x=var(v) --> var(v) occs x=false --> x<|?t=x<|s")] term_ind 2);
by (ALLGOALS (simp_case_tac [substC2,or_false,eq_iff1,eq_iff2] []));
by (fast_tac FOL_cs 1);
val var_not_occs = result();
goal subst_thy  "t <| r = t <| s <-> (ALL v.v <: vars(t) --> var(v) <| r = var(v) <| s)";
by (ind_tac "t" 1);
by (ALLGOALS (asm_simp_tac [substC2,un_iff] []));
by (ALLGOALS (fast_tac FOL_cs));
val agreement = result();
goal subst_thy  "~ v<: vars(t) --> t <| acons(v,u,s) = t <| s";
by (asm_simp_case_tac [substC2,agreement,eq_iff1] [] 1);
val repl_invariance = result();
goal subst_thy  "v <: vars(t) --> w <: vars(t <| acons(v,var(w),s))";
by (ind_tac "t" 1);
by (ALLGOALS (asm_simp_tac [substC2,eq_refl,un_iff] []));
by (fast_tac FOL_cs 1);
val var_in_subst = result();

Figure 5.4: Isabelle Proofs for Substitutions

5.6.3 Derivation of Unification

The derivation follows what by now is a familiar pattern. The algorithm is progressively instantiated using itypechk_tac, generating a set of correctness conditions, which are then proved in first-order logic. A unification algorithm is derived by solving the goal

1. ?unify : Πt_{1}:Term.Πt_{2}:Term.{a:Opt(Alist), TryBestUnifier(a, t_{1}, t_{2})}

The most obvious approach is to use letrec_tac, which instantiates the general form of a recursive program

?unify ← lam t_{1}.lam t_{2}.letrec unify t_{1} t_{2} be ?b(t_{1}, t_{2}, unify) in unify ‘ t_{1} ‘ t_{2} end

and leaves the goal

1. [[ t_{1} : Term; t_{2} : Term; IH ]] ⟹
?b(t_{1}, t_{2}, unify) : {a:Opt(Alist), TryBestUnifier(a, t_{1}, t_{2})}

where IH is the induction hypothesis

∀ u:Term.∀ v:Term. ⟨u, v⟩ ≺_{?R} ⟨t_{1}, t_{2}⟩ ⊃

unify ‘ u ‘ v : {a:Opt(Alist), TryBestUnifier(a, u, v)}

Now, a little insight is needed. One obvious possibility is case analysis on the first argument t_{1}. Using the tactic

                  itypechk_tac "termcase(t1,?b,?c,?d)" 1

further instantiates the program with

?b(t_{1}, t_{2}, unify) ← termcase(t_{1},?d(t_{1}, t_{2}, unify),?e(t_{1}, t_{2}, unify),?f(t_{1}, t_{2}, unify))

and leaves the following goals.

1. [[ t_{1} : Term; t_{2} : Term; IH ; c: Const; t_{1} = const(c) ]] ⟹

?d(t_{1}, t_{2}, unify, c) : {a:Opt(Alist), TryBestUnifier(a, const(c), t_{2})}

2. [[ t_{1} : Term; t_{2} : Term; IH ; v : Var; t_{1} = var(v) ]] ⟹

?e(t_{1}, t_{2}, unify, v) : {a:Opt(Alist), TryBestUnifier(a, var(v), t_{2})}

3. [[ t_{1} : Term; t_{2} : Term; IH ; x: Term; y : Term; t_{1} = comb(x, y) ]] ⟹

?f(t_{1}, t_{2}, unify, x, y) : {a:Opt(Alist), TryBestUnifier(a, comb(x, y), t_{2})}

The first goal can then be reduced by case analysis on the second argument t_{2}. Continuing in this fashion, an algorithm for unification can be derived. The interesting part of this derivation is not the instantiation of the algorithm, which is fairly straightforward, but the lemmas that this generates for correctness. The complete program is

lam t_{1}.lam t_{2}.letrec unify t_{1} t_{2} be
termcase(t_{1},λc_{1}.termcase(t_{2},λc_{2}.cond(c_{1} eq_{const} c_{2}, some(anil), none),
λv_{2}.assign(v_{2}, const(c_{1})),
λx_{2} y_{2}.none),
λv_{1}.assign(v_{1}, t_{2}),
λx_{1} y_{1}.termcase(t_{2},λc_{2}.none,

λv_{2}.assign(v_{2}, comb(x_{1}, y_{1})),
λx_{2} y_{2}.optcase(unify ‘ x_{1} ‘ x_{2}, none,
λθ.optcase(unify ‘ (y_{1} ◁ θ) ‘ (y_{2} ◁ θ),none,
λϕ.some(θ ⋄ ϕ)))))
in unify ‘ t_{1} ‘ t_{2} end

where assign(v, t) ≡ cond(var(v) occs t, none, some(acons(v, t, anil))). Using itypechk_tac to instantiate ?unify with this algorithm, and then simplifying the correctness conditions raised using the tactics of §4.4 generates the following conditions for partial correctness:

C1. c_{1} = c_{2} ⟹ TryBestUnifier(some(anil), const(c_{1}), const(c_{2}))

C2. ¬c_{1} = c_{2} ⟹ TryBestUnifier(none, const(c_{1}), const(c_{2}))

C3. TryBestUnifier(assign(v_{2}, const(c_{1})), const(c_{1}), var(v_{2}))

C4. TryBestUnifier(none, const(c_{1}), comb(x_{2}, y_{2}))

C5. TryBestUnifier(assign(v_{1}, t_{2}), var(v_{1}), t_{2})

C6. TryBestUnifier(none, comb(x_{1}, y_{1}), const(c_{2}))

C7. TryBestUnifier(assign(v_{2}, comb(x_{1}, y_{1})), comb(x_{1}, y_{1}), var(v_{2}))

C8. TryBestUnifier(none, x_{1}, x_{2}) ⟹

TryBestUnifier(none, comb(x_{1}, y_{1}), comb(x_{2}, y_{2}))

C9. [[ TryBestUnifier(some(θ), x_{1}, x_{2}); TryBestUnifier(none, y_{1} ◁ θ, y_{2} ◁ θ) ]] ⟹

TryBestUnifier(none, comb(x_{1}, y_{1}), comb(x_{2}, y_{2}))

C10. [[ TryBestUnifier(some(θ), x_{1}, x_{2}); TryBestUnifier(some(ϕ), y_{1} ◁ θ, y_{2} ◁ θ) ]] ⟹

TryBestUnifier(some(θ ⋄ ϕ), comb(x_{1}, y_{1}), comb(x_{2}, y_{2}))

and the following conditions for termination:

T1. ⟨x_{1}, x_{2}⟩ ≺_{?R} ⟨comb(x_{1}, y_{1}), comb(x_{2}, y_{2})⟩
T2. TryBestUnifier(some(θ), x_{1}, x_{2}) ⟹
⟨y_{1} ◁ θ, y_{2} ◁ θ⟩ ≺_{?R} ⟨comb(x_{1}, y_{1}), comb(x_{2}, y_{2})⟩

Note that type checking does not instantiate the well-founded ordering ?R. The form of the goals (T1) and (T2) can be used to suggest an instantiation for ?R. Manna and Waldinger use the following lexicographic ordering in their proof.

⟨a_{1}, a_{2}⟩ ≺_{M+W} ⟨b_{1}, b_{2}⟩ ≡ vars(a_{1}) ∪ vars(a_{2}) ⊂ vars(b_{1}) ∪ vars(b_{2}) ∨

(vars(a_{1}) ∪ vars(a_{2}) = vars(b_{1}) ∪ vars(b_{2}) ∧

a_{1} occs b_{1} = true)

Informally, ⟨a_{1}, a_{2}⟩ ≺_{M+W} ⟨b_{1}, b_{2}⟩ holds iff the variables in a_{1} and a_{2} are a strict subset of those in b_{1} and b_{2}, or the variables are identical and the term a_{1} occurs in b_{1}. In CCL, it is simpler to formalise a slightly weaker relation that holds iff the cardinality of one set of variables is less-than the cardinality of the other, rather than one set actually being contained in the other. ?R is instantiated as follows:

?R ← map(f, lex(pR, pR))

where f is a function that maps pairs ⟨x, y⟩ to pairs ⟨n, x⟩, in which n is the cardinality of the set of variables in x or in y:

f ≡ lam p.split(p, λx y.⟨card(vars(x) ∪ vars(y)), x⟩)

With this instantiation for ?R, the termination conditions are simplified to the following goals.

T1. WFD(x_{1}, x_{2}, comb(x_{1}, y_{1}), comb(x_{2}, y_{2}))

T2. TryBestUnifier(some(θ), x_{1}, x_{2}) ⟹

WFD(y_{1} ◁ θ, y_{2} ◁ θ, comb(x_{1}, y_{1}), comb(x_{2}, y_{2}))

where

WFD(a_{1}, a_{2}, b_{1}, b_{2}) ≡ card(vars(a_{1}) ∪ vars(a_{2})) ≺pR card(vars(b_{1}) ∪ vars(b_{2})) ∨

(card(vars(a_{1}) ∪ vars(a_{2})) = card(vars(b_{1}) ∪ vars(b_{2})) ∧
a_{1} ≺pR b_{1})

The conditions for partial correctness and termination are now proved in first-order logic, using the facts already derived for substitutions and their domains and ranges.

For partial correctness, the conditions all follow from the lemmas of Figure 5.5. In particular, (C3), (C5) and (C7) are all instances of the following general result for unifying variables.

BestUnifier(assign(v, t), var(v), t)

Only (C10) is awkward, requiring careful direction of the rewriting.

Similarly, the conditions for termination are proved from the following lemmas.

x ⊂ y ⊃ card(x) < card(y)

BestUnifier(θ, t, u) ⊃ dom(θ) ⊆ vars(t) ∪ vars(u) BestUnifier(θ, t, u) ⊃ range(θ) ⊆ vars(t) ∪ vars(u)

though the last two require some effort to prove.

The complete derivation uses forty two lemmas. As an example, unification is a little misleading; proving the correctness of this algorithm is far more complex than it is for many other programs. But what it does clearly show, is how theory can be developed in a natural way and an algorithm specified, how type checking uses an algorithm to generate correctness conditions, and how these can be solved in typed first-order logic using induction and rewriting.

84 Chapter 5. Proving Programs Correct

anil ≫ θ Idem(anil)

MGU(θ, t, u) ↔ (∀ ϕ. Unifies(ϕ, t, u) ↔ θ ≫ ϕ)
BestUnifier(θ, t, u) ↔ Idem(θ) ∧ Unifies(θ, t, u) ∧

(∀ ϕ. Unifies(ϕ, t, u) ⊃ θ ≫ ϕ)

Idem(θ) ↔ dom(θ) ∩ range(θ) = ∅
vars(v) occs t = false ⊃ Idem(acons(v, t, anil))
BestUnifier(θ, t, u) ↔ BestUnifier(θ, u, t)

Figure 5.5: Lemmas for Partial Correctness

Conclusion

This chapter draws conclusions from the work presented in the dissertation and suggests areas for future research.

6.1 Results

The main contribution of this work is that the theory was actually implemented and formal correctness proofs carried out on machine. Although many features of programming languages remain to be addressed (e.g. modules, polymorphism and concurrency), proving the correctness of programs in CCL has given some indication of what is demanded of a system for formal correctness. It is clear from this work that

• although appealing from some philosophical standpoints, intuitionism is not necessary for a computational logic;

• dependent types are advantageous for expressing termination and for generating correctness conditions by type checking;

• general recursion can be reasoned about in a natural way using well-founded induction, and termination can be separated from partial correctness;

• interleaving programming and verification is an effective approach to derivation; it is far easier to write programs that should implement specifications than to prove that specifications can be satisfied; and

• an evaluation semantics is a suitable basis for a computational logic.

These last two points are considered further.

6.1.1 Interleaving Programming with Verification

In CCL, programs can serve as templates to direct proofs of correctness. As there is a single type rule for each term-former in the language, a goal of the form a : A is broken down uniquely by type checking. In program verification, the term a is fully instantiated, and type checking immediately reduces the goal a : A to a set of correctness conditions. In program derivation, the term a is progressively instantiated during the proof. At each stage, a program fragment is suggested for a, which by type checking generates a further set of correctness conditions and unfulfilled subspecifications. Derivation proceeds by interleaving programming and verification. The form of correctness conditions generated by possible algorithms can be easily examined; when these conditions appear unsolvable, backtracking allows the instantiation to be retracted and an alternative considered.

Experience with the interactive style of development encouraged by ML suggests an approach that lies between verification and derivation. In ML, individual functions (or parts thereof) are written and then passed to the type checker. Errors picked up by type checking can be corrected and the process repeated until the function is well-typed. Similarly, to develop correct code, individual functions are written and then verified. If the correctness conditions indicate errors, these can be corrected and the process repeated. Finally, the function is shown to be correct by proving the correctness conditions.

6.1.2 Denotational and Operational Approaches

In §1.3, a distinction was made between denotational and operational computational logics. Clearly, CCL falls into the latter category. Programs are represented by abstract syntax trees, and reasoning is based on an evaluation relation.

This work began, however, by taking a denotational approach. Terminating programs were represented by functions in ZF set theory, which required annotations for the types of λ-abstractions and for recursion (represented by well-founded recursion). The extra information present in program denotations made them awkward. Moreover, facts were proved about denotations and not the programs themselves; extra work was required to relate these facts to computational behaviour. This required significantly more effort than an operational approach—without any clear benefits.

Although CCL is an operational logic, it does not suffer the limitations of transformation systems since it permits specification. Reasoning about the correctness of programs in any case has an operational character; new theory is often developed hand-in-hand with an implementation, although occasionally theory is sometimes developed for its own sake (e.g. finite set theory is used to reason about the correctness of a unification algorithm in §5.6). But the development of set theory is not unduly awkward, and the implementation it entails would prove useful in other programs. If this style of development did prove to be inconvenient, CCL could be based on higher-order logic instead of first-order logic. So far, however, this has not proved necessary.

6.2 Future Work

The approach taken in deriving CCL from L can be adopted for other target languages with different evaluation semantics. Experience with the implementation of CCL suggests improvements to the tactics for type checking. In addition, it should be possible to extend the simple tactics described here to provide a more complete environment for the derivation of correct programs.

6.2.1 Other Target Languages

CCL arose directly from the evaluation semantics of its target language L. The same development could be carried out for other functional languages with eager as well as lazy evaluation. For CCL, development was carried out by hand and the resulting calculus implemented as a set of axioms in Isabelle. The effort required to derive the single theory CCL within Isabelle’s set theory (or higher-order logic) would outweigh any advantage that this mechanisation might give. But there would be advantages in establishing a general suite of theorems and tactics for developing computational logics from target programming languages. In particular, the consequences of small changes to a target language could be studied more easily.

One possible variation is from a lazy to an eager evaluation strategy. Following the development in Chapter 3, the computational logic CCL_{e} can be derived from the target language L_{e} (identical to L but with eager evaluation). The eager evaluation relation ▷_{e} differs from its lazy counterpart ▷ only in the rules for the constructors s and ⟨⟩ (as in languages such as ML, the constructor lam remains lazy).

\frac{u ▷_{e} a}{s(u) ▷_{e} s(a)}  \frac{u ▷_{e} a  v ▷_{e} b}{_{⟨u, v⟩ ▷_{e} ⟨a, b⟩}}

CCL_{e} differs from CCL only in the conversion rules involving these eager constructors.

a↓ ⟹ scase(s(a), b, c) = c(a)
[[ a↓; b↓ ]] ⟹ split(⟨a, b⟩ , c) = c(a, b)

The premises ensure the termination of terms, just as the conversion rule for let is conditional (Theorem 3.8). Using types to ensure termination, as in the conversion rule for let, leads to extra premises in many of the derived rules. For example, the injection rule for pairing in CCL_{e} is

\frac{⟨a, b⟩ = ⟨a′, b′⟩  \begin{aligned}[ & a = a′ ; b = b′ & ] \\ & P \end{aligned}  a: A  a′ : A′  b: B  b′ : B′}{P}

Although this puts a significant overhead on reasoning within CCL_{e} compared with CCL, reasoning in the corresponding interpreted first-order logic is no more onerous. The examples in this dissertation could be carried out in an eager regime with little extra effort.

6.2.2 Improving Type Checking

In CCL, goals of the form a: {x:A, P (x)} focus attention on program a in the proposition P (a). Type checking directs the proof of these goals using the program a, generating correctness conditions from specifications. But the type checking strategy described in this dissertation suffers two weaknesses, due to the type rules for local declarations and for constructors. These weaknesses and possible solutions are described; neither solution was implemented.

Firstly, as the rules for local declarations (i.e. let, letfun and letrec) introduce uninstantiated type variables, they are incompatible with a general tactic for type checking (see §4.4.4). The simplest solution to the problematic use of let-type is to apply the conversion rule for let before type checking, which has the effect of the following rule.

\frac{a: A b(a) : B}{let x be a in b(x) end : B}

The premises can now be independently proved, but at the cost of type checking each occurrence of a in b(a) separately. If local declarations are used with relatively few substitution instances, then this is a practical solution. This is generally the case, since more frequently used identifiers tend to be declared at top level. In fact, it is worthwhile performing all outstanding reductions in a term before type checking (except those for rec).

Secondly, as the type rules for constructors use only simple types, they cannot be applied to subtypes. For goals of the form a: {x:A, P (x)}, in which the outermost termformer of a is a constructor, {}-intr must be applied before the appropriate type rule. This removes the focussed style of goal, preventing further direction of the proof of P (a) by the program a. For example, type checking the goal

1. succ(n) : {x:Nat, P (x)}

uses {}-intr followed by succ-type, leaving the subgoals

1. n: Nat

2. P (succ(n))

Further type checking cannot direct the proof of P (n). Instead, if the derived rule

\frac{n : \{x:Nat, P (succ(x))\}}{succ(n) : \{x:Nat, P (x)\}}

is used, then {}-intr is no longer necessary and the resulting goal is

1. n : {x:Nat, P (succ(x))}

Further type checking will direct the proof of P (succ(n)).

For constructors with more than one argument, type judgements are nested; this is possible since a:A is just a formula in CCL. Type checking is first directed by one argument and then by the other. For example, the rule ⟨⟩-type

\frac{a: A b: B(a)}{⟨a, b⟩ : Σx:A.B(x)}

is replaced by the following derived rule.

\frac{a : \{x:A, b : \{y:B(x), P (⟨x, y⟩)\} \}}{⟨a, b⟩ : \{z:Σx:A.B(x), P (z)\}}

Subtypes are finally removed either by type rules for constructors with no arguments, such as

\frac{P (zero)}{zero : \{x:Nat, P (x)\}}

or by the type rules for recursive calls (see §4.4.1).

These rules have been derived within CCL, but a tactic for type checking using them has not been written. If these rules are implemented and used in type checking, it may be more convenient to make all types in CCL subtypes (Nat would then become an abbreviation for {x:Nat, ⊤}). This would obviate the need for both simple and subtyped rules for each type-former, and simplify the handling of subtypes in hypotheses.

6.2.3 An Environment for Program Correctness

For the formal synthesis of programs to be practical, theory and code should be developed within the same framework of modules. Extended ML takes this approach [60]. The work done in this dissertation should naturally extend to provide an environment for program synthesis.

Programs in CCL are logical theories. New functions and types are declared by extending a theory with definitions of new constants. Program modules structure these theories in the usual mathematical way; namely by restricting the scope of constants, introducing axioms that are justified by theorems in underlying theories, and declaring abstract data types that are implemented by underlying representation types. Program execution is by inference, using a simple set of rules (an evaluation semantics).

Viewed in this way, programs developed in conventional programming languages are theories in which the only possible inference is evaluation. Transformation systems extend program theories with a predicate for equality, which allows partial evaluation and substitution. The computational logic CCL extends transformation systems with a predicate for type membership, where types are sets of terminating programs, and the connectives of first-order logic, where quantification is over programs and types. This is useful because

• if two programs are equal then they evaluate to results that are equal, and

• if a program is typeable then its evaluation terminates.

Programs are evaluated in the context of a module; similarly, program correctness is asserted and proved in the context of a theory. While it is straightforward to determine the evaluation rules that are available in a particular context, determining the other inference rules that are available is more difficult. CCL can be viewed as a meta-theory in which to interpret extensions to first-order logic with computational types. These extensions can represent the sets of inference rules available in theories. Extensions can also be used to axiomatise behaviour that will not be proved correct.

Imagine an environment for deriving correct programs in which a single module system structures program declarations, extensions to first-order logic, and axiomatisations of program behaviour. The correctness of a program in some module is asserted and proved in that module. From the work in this dissertation, it is clear that much of the structure of the extensions to first-order logic can be automatically inferred from program declarations.

• For each new data type declared, a set of theorems for typing, conversion, etc. can be automatically derived (see §4.3.2).

• For each new abstract data type declared, a new equality can be defined provided that the resulting congruences are proved (see §4.5.3).

• Certain properties of data types (such as admitting a test for equality) can be inferred and the corresponding programs constructed. For example, the type List(A) admits a test for equality provided the type A does. Formalised in CCL, this is the following theorem.

\frac{eq_{A} : EQTYPE(A)}{listeq(eq_{A}) : EQTYPE(List(A))}

in which listeq(eq_{A}) is a program that determines if two lists are equal provided that eq_{A} determines equality on their elements. EQTYPE is defined in §4.5.2.

• For each theorem a: A, a set of conversions can be derived for the program a.

• Modules structure both code and theory; their signatures introduce new constants (program identifiers and types) and axioms. Interpreting one module in another requires theorem proving and is, therefore, interactive. Modules may be introduced to develop theory without appearing in programs; for example, the use of finite set theory in the development of unification.

Correctness assertions are proved in logical theories derived from the context in which they are made. Type checking in CCL generates correctness conditions from specifications, but the majority of any interactive reasoning is in the inferred extensions to first-order logic. In large programs, proving the correctness of the entire program is not always feasible; it is essential that correctness can be limited to parts of the code and assumptions made about the behaviour of other parts. In such circumstances, an environment for correctness must make explicit when axioms are introduced that are not discharged by underlying theories.

Appendix A

Well-Founded Induction

This appendix introduces well-founded relations, the principle of well-founded induction, and constructions over relations that preserve well-foundedness. In particular, the use of well-founded induction to support reasoning about general recursion is considered, subsuming amongst others the notions of structural induction and course-of-values induction.

§A.1 presents several equivalent definitions of well-foundedness, one of which gives rise to the principle of well-founded induction. §A.2 introduces constructions over relations that preserve well-foundedness.

A.1 Well-Founded Relations and Induction

A relation ≺ is well-founded over the set A if there exist no infinite descending chains of elements in A.

… ≺ x_{n} ≺ … ≺ x_{3} ≺ x_{2} ≺ x_{1}

Rather than using infinite chains, well-foundedness can be defined in terms of minimal element subsets. For the set A, an element a is ≺-minimal iff there is no element x ∈ A for which x ≺ a.

Definition A.1 (Well-foundedness I) A relation ≺ is well-founded over the set A iff every non-empty subset of A has an ≺-minimal element.

Assuming dependent choice, this definition is equivalent to the informal statement above since

• ≺-minimal subsets ⇒ no infinite descending chains Suppose there exists an infinite descending chain … ≺ x_{3} ≺ x_{2} ≺ x_{1} in A. The set of elements in this chain X = {x_{1}, x_{2}, …} has an ≺-minimal element, since X ⊆ A; but for every element x_{n} in the chain, there exists an element x_{n+1} such that x_{n+1} ≺ x_{n}—contradiction.

• no infinite descending chains ⇒ ≺-minimal subsets Suppose there exists a non-empty set X ⊆A for which there is no ≺-minimal element. For an element x_{1} ∈ X, there must exist another element x_{2} ∈ X such that x_{2} ≺ x_{1}. Repeating this argument for x_{2} gives x_{3} etc., generating an infinite descending chain—contradiction.

A well-founded relation cannot be reflexive (as this would permit the infinite chain … ≺ x ≺ x ≺ x ≺ x) or symmetric (… ≺ y ≺ x ≺ y ≺ x), though it may be transitive (Theorem A.3). For example, the predecessor relation is well-founded over natural numbers,

x ≺_{N} y ↔ y = x + 1

and the immediate sublist relation is well-founded over lists.

x ≺_{L} y ↔ y = (cons h x) for some h

There is an alternative formulation of well-foundedness, which leads to a rule of wellfounded induction.

Definition A.2 (Well-foundedness II) A relation ≺ is well-founded over the set A iff for every unary predicate P

( ∀ x∈A. (∀ y ∈A. y ≺ x ⊃ P (y)) ⊃ P (x) ) ⊃ ∀ x∈A. P (x)

The outermost implication in the above definition is often written as a bi-implication; as the missing implication is a tautology, its inclusion would add nothing. This definition is the only one that is intuitionistically meaningful. In a classical setting, it is equivalent to the first definition.

Theorem A.1 Definitions I and II, of well-foundedness, are equivalent.

Proof: For an arbitrary relation ≺ and set A, show that ≺ satisfies Definition I iff it satisfies Definition II.

Definition I holds iff for X = {x ∈ A, ¬P (x)}, where P is arbitrary, if set X is non-empty then it contains an ≺-minimal element. This is formally expressed as

(∃ x∈A. ¬P (x)) ⊃ ∃ x∈{x ∈ A, ¬P (x)}. ∀ y ∈{x ∈ A, ¬P (x)}. ¬y ≺ x

which by simplification is equivalent to the formula

(∃ x∈A. ¬P (x)) ⊃ ∃ x∈A. ¬P (x) ∧ ∀ y ∈A. y ≺ x ⊃ P (y) (1)

Taking the contrapositive form of (1) and again simplifying yields

( ∀ x∈A. (∀ y ∈A. y ≺ x ⊃ P (y)) ⊃ P (x) ) ⊃ ∀ x∈A. P (x)

which is just definition II.

Definition II leads to a principle of well-founded induction. Writing Wfd_{A}(≺) for the assertion that the relation ≺ is well-founded over set A, this is expressed by the following theorem.

Theorem A.2 (Well-founded induction) If

i. Wfd_{A}(≺),

ii. ∀ x∈A. (∀ y ∈A. y ≺ x ⊃ P (y)) ⊃ P (x)

then ∀ a∈A. P (a).

Proof: Trivially from the second definition of well-foundedness.

Expressed as a rule of natural deduction, this theorem has the following form (used in later proofs).

\frac{Wfd_{A}(≺)  a ∈ A  \begin{matrix}[ x ∈ A ; ∀ y ∈A. y ≺ x ⊃ P (y) ] & x \\ P (x) \end{matrix}}{P (a)}

Well-founded induction generalises the more familiar notions of structural induction and course-of-values induction. For example, structural induction over the natural numbers, more familiarly known as mathematical induction, corresponds to well-founded induction with the predecessor relation; course-of-values induction on natural numbers corresponds to well-founded induction with the less-than relation, which is the transitive closure of the predecessor relation.

A.2 Constructing Well-Founded Relations

Often the easiest way to prove that a relation is well-founded is by construction. The following constructions for relations are shown to preserve well-foundedness: the irreflexive transitive closure of a relation, the mapping of one relation on to another, and the lexicographic ordering of two relations. These constructions are sufficient for proving termination in many examples. One exception is an algorithm for proof normalisation in which recursion follows a multi-set ordering (though an additional constructor could be added for multi-set orderings).

A.2.1 Irreflexive Transitive Closure

The irreflexive transitive closure of a relation ≺, written ≺^{+}, is the least relation such that

a ≺^{+} b iff ( a ≺ b ∨ (∃x.a ≺^{+} x ∧ x ≺ b) ) ∧ a ≠ b

Theorem A.3 Let ≺ be a well-founded relation over the set A, then ≺^{+} is also wellfounded over A.

Proof: By the second definition of well-foundedness, assume

∀ x∈A. (∀ y ∈A. y ≺^{+} x ⊃ P (y)) ⊃ P (x) (1)

and prove ∀ a∈A. P (a). By (1), this holds if the following holds

(*) ∀ b∈A. b ≺^{+} a ⊃ P (b)

By well-founded induction, using relation ≺, (*) holds if assuming

∀ x∈A. x ≺ c ⊃ ∀ y ∈A. y ≺^{+} x ⊃ P (y) (2)

the formula ∀ b∈A. b ≺^{+} c ⊃ P (b) holds. By the definition of ≺^{+}, the hypothesis b ≺^{+} c can be rewritten to a disjunction, so that this holds if the following two formulae hold

(†) b ≺ c ⊃ P (b) (‡) (∃ x∈A. b ≺^{+} x ∧ x ≺ c) ⊃ P (b)

For (†), the hypothesis and (2) imply ∀ y ∈A. y ≺^{+} b ⊃ P (y), which by (1) implies P (b). For (‡), the hypothesis and (2) immediately imply P (b).

From this result, it follows that less-than < (i.e. ≺+_{N}) is well-founded over the natural numbers, and that the strict sublist relation ≺+_{L} is well-founded over lists.

A.2.2 Mapping

Theorem A.4 Let ≺_{B} be a well-founded relation over the set B and f ∈ A → B a total function. Then any relation ≺_{A} over A for which

x ≺_{A} y ⊃ f(x) ≺_{B} f(y) for all x, y ∈ A

is well-founded over A.

Proof: By the second definition of well-foundedness, assume

∀ x∈A. (∀ y ∈A. y ≺_{A} x ⊃ P (y)) ⊃ P (x) (1)

and prove ∀ a∈A. P (a). This can be strengthened to

(*) ∀ b∈B. ∀ a∈A. f(a) = b ⊃ P (a)

which clearly implies ∀ a∈A. P (a) in the case b = f(a). By well-founded induction, using relation ≺_{B}, (*) holds if assuming

∀ y ∈B. y ≺ b ⊃ ∀ a∈A. f(a) = y ⊃ P (a) (2)

the formula ∀ a∈A. f(a) = b ⊃ P (a) holds. By (1) and the hypothesis, f(a) = b, this holds if assuming

f(a) = b (3) y ≺_{A} a (4)

the formula P (y) holds. By the assumed property of ≺_{A}, (4) implies f(y) ≺_{B} f(a). Rewriting f(a), using (3), gives f(y) ≺_{B} b, which can be used in assumption (2) to give

∀ a∈A. f(a) = f(y) ⊃ P (a) (5)

For a = y, this immediately proves P (y).

As corollaries of the mapping theorem, the following results hold for induced relations, subrelations and subsets.

Theorem A.5 Let ≺_{B} be a well-founded relation over the set B and f ∈ A → B a total function. Then the relation ≺_{A} over A defined by

x ≺_{A} y iff f(x) ≺_{B} f(y) for all x, y ∈ A

is well-founded over A.

Theorem A.6 Let ≺ be a well-founded relation over the set A and ≺′ a relation over A for which ≺′ ⊆ ≺, then ≺′ is well-founded over A.

Theorem A.7 Let ≺ be a well-founded relation over the set A and B ⊆ A. Then ≺ is well-founded over B.

The following examples show how these results allow new relations to be constructed.

• From the mapping theorem, it follows that the strict subset relation is shown to be well-founded by the following property.

A ⊆ B ⊃ card(A) < card(B)

that is if A is a strict subset of B then the cardinality of A is less-than that of B.

• From the induced relation theorem, it follows that the relation induced by the length function for lists (length) is well-founded.

k ≺_{len} l ↔ length(k) < length(l)

• From the subrelation theorem, it follows that the predecessor relation is well-founded over natural numbers since the relation < is well-founded over natural numbers.

• From the subset theorem, it follows that the relation < is well-founded over natural evens since it is well-founded over the natural numbers.

A.2.3 Lexicographic Ordering

Theorem A.8 Let ≺_{A} and ≺_{B} be well-founded relations over the sets A and B respectively. Define a new relation ≺, the lexicographic ordering of these, as

⟨x, y⟩ ≺ ⟨x′, y′⟩ iff x ≺_{A} x′ ∨ x = x′ ∧ y ≺_{A} y′

then ≺ is well-founded over A × B.

Proof: By the second definition of well-foundedness, assume

∀ p∈A × B. (∀ q ∈A × B. q ≺ p ⊃ P (q)) ⊃ P (p) (1)

and prove ∀ r ∈A × B. P (r), that is

(*) ∀ a∈A. ∀ b∈B. P (⟨a, b⟩)

By well-founded induction, using relation ≺_{A}, (*) holds if assuming

∀ x∈A. x ≺_{A} a ⊃ ∀ b∈B. P (⟨x, b⟩) (2)

the formula ∀ b ∈ B . P (⟨a, b⟩) holds. By well-founded induction, using relation ≺_{B}, this holds if assuming ∀ y ∈B. y ≺_{B} b ⊃ P (⟨a, y⟩) (3)

the formula P (⟨a, b⟩) holds. By (1), this holds if assuming

⟨u, v⟩ ≺ ⟨a, b⟩ (4)

the formula P (⟨u, v⟩) holds. By the definition of ≺, (4) can be rewritten as a disjunction, and P (⟨u, v⟩) holds if the following two formulae hold (†) u ≺_{A} a ⊃ P (⟨u, v⟩) (‡) u = a ∧ v ≺_{B} b ⊃ P (⟨u, v⟩)

Now, (†) immediately follows from (2) and, after substituting u = a, (‡) follows from (3).

The result for lexicographic pairing can be extended to all finite tuples, by considering them as nested pairs. But the usual dictionary ordering over strings (i.e. lists of characters) does not fall into this category. The dictionary ordering is a lexicographic style of ordering extended to lists, rather than tuples of fixed length; it is not well-founded as the following example illustrates.

… aaab ≺ aab ≺ ab ≺ b

But ordering strings first by their length and then lexicographically is well-founded.

References

[1] Samson Abramsky. The lazy lambda calculus. In David Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

[2] Krzysztof R. Apt. Ten years of Hoare’s logic: A survey—Part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, 1981.

[3] R. Backhouse, P. Chisholm, G. Malcolm, and E. Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1(1):19–84, 1989.

[4] J. L. Bates and R. L. Constable. Proofs as programs. ACM Transactions on Programming Languages and Systems, 7(1):113–136, 1985.

[5] R. S. Bird. Formal derivation of a pattern matching algorithm. Science of Computer Programming, 12:93–104, 1989.

[6] R. S. Bird. A calculus of functions for program derivation. In David Turner, editor, Research Topics in Functional Programming, pages 287–307. Addison-Wesley, 1990.

[7] R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44–67, 1977.

[8] P. Chisholm. Derivation of a parsing algorithm in Martin-Löf’s theory of types. Science of Computer Programming, 8:1–42, 1987.

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

[10] Avra Cohn and Robin Milner. On using Edinburgh LCF to prove the correctness of a parsing algorithm. Technical Report CSR-113-82, Department of Computer Science, University of Edinburgh, May 1982.

[11] Avra J. Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127–139, 1989.

[12] R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall International, 1986.

[13] T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

[14] Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Symposium on Principles of Programming Languages, pages 207–212. ACM Press, 1982.

[15] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[16] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.

[17] Peter Dybjer. Program verification in a logical theory of constructions. In Functional Programming Languages and Computer Architecture, pages 334–349. Springer-Verlag, 1985. LNCS 201.

[18] Lars-Henrik Eriksson. Synthesis of a unification algorithm in a logic programming calculus. Journal of Logic Programming, 1(1):3–18, 1984.

[19] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proof and Types. Cambridge University Press, 1989.

[20] Michael J. C. Gordon. HOL: A proof generating system for higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer Academic Publishers, 1988.

[21] Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. Springer-Verlag, 1979. LNCS 78.

[22] D. Gries. The Science of Programming. Texts and Monographs in Computer Science. Springer-Verlag, 1981.

[23] Carl A. Gunter. Forms of semantic specification. Bulletin of EATCS, 45:98–113, 1991.

[24] Susumu Hayashi and Hiroshi Nakano. PX : A Computational Logic. Foundations of Computer Science. MIT Press, 1989.

[25] Martin C. Henson. Program development in the constructive set theory TK. Formal Aspects of Computing, 1:173–192, 1989.

[26] Arend Heyting. Intuitionism: An Introduction. North-Holland, 1956.

[27] R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, December 1969.

[28] Douglas J. Howe. Equality in lazy computation systems. In Symposium on Logic in Computer Science, pages 198–203. ieee Computer Society Press, 1989.

[29] Paul Hudak, Simon Peyton Jones, and Philip Wadler. Report on the programming language Haskell, version 1.1, August 1991.

[30] G. P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

[31] G. Kahn. Natural semantics. In F. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors, Symposium on Theoretical Aspects of Computer Science, pages 22–39. Springer-Verlag, 1987. LNCS 247.

[32] P. J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308–320, January 1964.

[33] Daniel Leivant. Contracting proofs to programs. In P. Odifreddi, editor, Logic and Computer Science, pages 279–327. Academic Press, 1990.

[34] Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90–121, 1980.

[35] Z. Manna and R. Waldinger. Deductive synthesis of the unification algorithm. Science of Computer Programming, 1:5–48, 1981.

[36] Z. Manna and R. Waldinger. The origins of a binary search paradigm. Science of Computer Programming, 9(1):37–83, 1987.

[37] Z. Manna and R. Waldinger. The Logical Basis for Computer Programming: Deductive Systems. Addison-Wesley, 1990.

[38] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

[39] Per Martin-Löf. Intuitionistic type theory. Bibliopolis, Napoli, 1984.

[40] Per Martin-Löf. Constructive mathematics and computer programming. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 167–184. Prentice-Hall International, 1985.

[41] J. McCarthy. A basis for a mathematical theory of computation. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33–70. North-Holland, 1963.

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

[43] Albert R. Meyer. Semantical paradigms: Notes for an invited lecture. In Symposium on Logic in Computer Science, pages 236–253. ieee Computer Society Press, 1988.

[44] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

[45] Christine Mohring. Algorithmic development in the calculus of constructions. In Symposium on Logic in Computer Science, pages 84–91. ieee Computer Society Press, 1986.

[46] Tobias Nipkow. Order-sorted polymorphism in Isabelle. In G. Huet, G. Plotkin, and C. Jones, editors, Proc. 2nd Workshop on Logical Frameworks, pages 307–321, 1991.

[47] B. Nordström. Programming in constructive set theory: Some examples. In Functional Programming Languages and Computer Architecture, pages 141–153. ACM Press, 1981.

[48] B. Nordström. Terminating general recursion. BIT, 28:605–619, 1988.

[49] Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.

[50] Christine Paulin-Mohring. Extracting F_{ω}’s programs from proofs in the calculus of constructions. In Symposium on Principles of Programming Languages, pages 89–104. ACM Press, 1989.

[51] Lawrence C. Paulson. Verifying the unification algorithm in LCF. Science of Computer Programming, 5:143–169, 1985.

[52] Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. Journal of Symbolic Computation, 2:325–355, 1986.

[53] Lawrence C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2. Cambridge University Press, 1987.

[54] Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990.

[55] Lawrence C. Paulson and Tobias Nipkow. Isabelle tutorial and user’s manual. Technical Report 189, University of Cambridge Computer Laboratory, 1990.

[56] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report FN–19, Computer Science Department, Aarhus University, September 1981.

[57] D. Prawitz. Natural Deduction: A Proof-Theoretical Study. Almquist and Wiksell, 1965.

[58] J. A. Robinson. Computational logic: The unification computation. Machine Intelligence, 6:63–72, 1971.

[59] Anne Salvesen and Jan M. Smith. The strength of the subset type in Martin-Löf’s type theory. In Symposium on Logic in Computer Science, pages 384–391. ieee Computer Society Press, 1988.

[60] Donald Sannella and Andrzej Tarlecki. Toward formal development of ML programs: Foundation and methodology. Technical Report ECS-LFCS-89-71, Department of Computer Science, University of Edinburgh, February 1989.

[61] P. Schroeder-Heister. A natural extension of natural deduction. Journal of Symbolic Logic, 49(4):1284–1300, December 1984.

[62] Jan M. Smith. On a nonconstructive type theory and program derivation. In Conference on Logic and its Applications. Plenum, 1986. Bulgaria.

[63] J. Traugott. Deductive synthesis of sorting programs. In J. Siekmann, editor, International Conference on Automated Deduction, pages 641–660. Springer-Verlag,

An Index to Notation

Introduced on page

‘  Call-by-name application in L.  23
ˆ  Call-by-value application in L.  23
+  A defined program type in CCL.  50
×  A defined program type in CCL.  29
:  The type membership relation in CCL.  30
{}  A constructor for program types in CCL.  29
⟨⟩  A constructor of L.  21
=  The equality relation on terms (and on types) in CCL.  26 (30)
↓  The termination predicate for programs of L.  24
→ A defined program type in CCL.  29
⇝  The reduction relation for L.  21
▷  The evaluation relation for L.  22
L  The target programming language.  21
ι  The set of program terms of L.  21

ι_{=} The set of equivalence classes of programs (ι) under term equality (=)—a meta-type in the Isabelle implementation.

27

τ The set of program types—a meta-type in the Isabelle implementation.

29

ω The set of well-founded orderings—a meta-type in the Isabelle implementation.

34

o Logical formulae of CCL—a meta-type in the Isabelle implementation.

19

μ  A constructor for program types in CCL.  29
≺_{R} The mebership relation on well-founded orderings in CCL.  19
Π  A constructor for program types in CCL.  29
Σ  A constructor for program types in CCL.  29

An Index to Notation contd.

Introduced on page

Bool  A defined program type in CCL.  50
BOOL An extension to the Isabelle theory FOL.  61
CCL An Isabelle theory. 44
CON The constructors of L.  22
DES  The destructors of L.  22
FOL  An Isabelle theory.  44
lam  A constructor of L.  21
let  A destructor of L.  22
letfun Overloaded as a collection of defined programs in CCL.  49
letrec Overloaded as a collection of defined programs in CCL.  49
lex  A constructor for well-founded orderings in CCL.  34
List  A defined program type in CCL.  50
map  A constructor for well-founded orderings in CCL.  34
Mono The monotonicity predicate in CCL.  30
Nat  A defined program type in CCL.  50
NAT  An extension to the Isabelle theory FOL.  62
OPT  An extension to the Isabelle theory FOL.  77
pcase A destructor of L.  21
pR  A constructor for well-founded orderings in CCL.  34
rec  A destructor of L.  22
restrict A constructor for well-founded orderings in CCL.  34
s  A constructor of L.  21
S  A constructor for program types in CCL.  29

scase A destructor of L (overloaded to give a conversion rule for types in CCL).

21 (30)

SET  An extension to the Isabelle theory FOL.  63

split A destructor of L (overloaded to give a conversion rule for types in CCL).

22 (30)

SUBST An extension to the Isabelle theory FOL.  77
TERM An extension to the Isabelle theory FOL.  77
Unit  A defined program type in CCL.  50
V  A constructor for program types in CCL.  29
wfst  A derived constructor for well-founded orderings.  60
wsnd A derived constructor for well-founded orderings.  60
z  A constructor of L.  21