To The Graduate School:

The members of the Committee approve the thesis of Tjark Weber presented on July 26, 2002.

James L. Caldwell, Chairman John R. Cowles Sylvia Hobart

APPROVED: Jeffrey Van Baalen, Head, Department of Computer Science Stephen E. Williams, Dean, The Graduate School Weber, Tjark, \underline{Program Transformations in Nuprl}, M.S., Department of Computer

Science, August, 2002

This thesis presents a formalization of program transformations and their general categorical framework in Nuprl. It gives formal definitions of catamorphisms and anamorphisms and formal, constructive proofs for when an arrow is a catamorphism or anamorphism. Necessary and sufficient conditions for when a function is a catamorphism are proved constructively, and a program transformation is extracted from the proofs. An instance of Bird’s fusion theorem for binary trees is verified in Nuprl, and applied to the Quicksort algorithm to formally prove the algorithm correct.

2 Program Transformations in Nuprl

by Tjark Weber

A thesis submitted to the Department of Computer Science and The Graduate School of The University of Wyoming

in partial fulfillment of the requirements for the degree of

Master of Science in Computer Science

Laramie, Wyoming August, 2002 ii \begin{matrix}c \\ ◯ \end{matrix} 2002 by Tjark Weber

iii iv

Acknowledgments

I would like to thank my advisor James L. Caldwell for his helpful comments and his guidance on this thesis. I appreciate his help as much as the fact that he let me work on my own whenever possible. He was also the one who asked me to join the Master’s Program in the Department of Computer Science at the University of Wyoming.

I would like to acknowledge support received from a Rockwell-Collins University grant.

This material is based upon work supported by the National Science Foundation under Grant No. CCR-9985239. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

Among the online resources I used are Google^{TM}, CiteSeer, and LEO. I would like to thank everyone there for making their services available freely.

Thorsten Altenkirch willingly answered my questions about [GHA01]. Natarajan Shankar provided me with some of his PVS files developed for [Sha96]. The L^{A}TEX template this thesis is based on was written by Thomas Böhne. I also want to thank him for proof-reading my thesis. Any remaining errors are of course my fault.

Last but not least I would like to thank my parents Klaus and Frauke Weber for their great support over many, many years. vi

Contents

List of Figures ix

1 Introduction 1 1.1 Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Background 5 2.1 Squiggol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Special-Purpose Transformation Tools . . . . . . . . . . . . . . . . . 6 2.3 General-Purpose Verification Tools . . . . . . . . . . . . . . . . . . . 6 2.4 Previous Formalizations of Category Theory . . . . . . . . . . . . . . 6

3 The Nuprl System 9 3.1 The Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.2 Constructive Aspects: Proofs as Programs . . . . . . . . . . . . . . . 11 3.3 Well-Formedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.4 Display Forms, Abstractions, Proofs . . . . . . . . . . . . . . . . . . . 12

4 Category Theory in Nuprl 15 4.1 Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 The Category of Types . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.3 Dual Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.4 Initial and Terminal Objects . . . . . . . . . . . . . . . . . . . . . . . 20 4.5 Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4.6 Algebras and Coalgebras . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.7 Homomorphisms and Cohomomorphisms . . . . . . . . . . . . . . . . 23 4.8 The Category of Algebras . . . . . . . . . . . . . . . . . . . . . . . . 24

4.8.1 The Composition of Homomorphisms . . . . . . . . . . . . . . 25 4.8.2 The Identity Homomorphism . . . . . . . . . . . . . . . . . . 27 4.8.3 Definition of the Category of Algebras . . . . . . . . . . . . . 29

4.9 The Category of Coalgebras . . . . . . . . . . . . . . . . . . . . . . . 30 5 Catamorphisms and Anamorphisms 33

5.1 Catamorphisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.2 When is an Arrow a Catamorphism? . . . . . . . . . . . . . . . . . . 37 5.3 Anamorphisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 5.4 When is an Arrow an Anamorphism? . . . . . . . . . . . . . . . . . . 42

6 When is a Function a Catamorphism? 45 6.1 A Non-Constructive Result . . . . . . . . . . . . . . . . . . . . . . . . 45 6.2 A Necessary Condition . . . . . . . . . . . . . . . . . . . . . . . . . . 46 6.3 A Sufficient Condition . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.4 Computing fold^{−1}: A Simple Example . . . . . . . . . . . . . . . . . 56 6.5 Two Counterexamples . . . . . . . . . . . . . . . . . . . . . . . . . . 60

7 Bird’s Fusion Transformation 65 7.1 Binary Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 7.2 The reduce Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 7.3 The unfold Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 7.4 The fun Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 7.5 Bird’s Fusion Theorem for Binary Trees . . . . . . . . . . . . . . . . . 75

8 Example: Quicksort 77 8.1 Quicksort in Nuprl . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 8.2 Quicksort by Fusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 8.3 A Formal Correctness Proof . . . . . . . . . . . . . . . . . . . . . . . 85

8.3.1 Quicksort Returns an Ordered List . . . . . . . . . . . . . . . 85 8.3.2 Quicksort Returns a Permutation of its Input . . . . . . . . . 91 8.3.3 Quicksort Returns a Permutation of its Input: A Second Proof 93

9 Conclusions 97 9.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 9.2 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 9.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99

Bibliography 101

List of Figures

4.1 id(B) · f = f and g · id(B) = g . . . . . . . . . . . . . . . . . . . . . 16 4.2 h · (g · f) = (h · g) · f . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.3 Abstraction category . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.4 Abstraction morphism . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.5 Abstraction large_category . . . . . . . . . . . . . . . . . . . . . . 18 4.6 Theorem category_if . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.7 Theorem large_category_wf . . . . . . . . . . . . . . . . . . . . . . 19 4.8 Abstraction dual_category . . . . . . . . . . . . . . . . . . . . . . . 20 4.9 Theorem dual_category_wf . . . . . . . . . . . . . . . . . . . . . . . 20 4.10 Abstractions initial and terminal . . . . . . . . . . . . . . . . . . 21 4.11 Abstraction exists_unique . . . . . . . . . . . . . . . . . . . . . . . 21 4.12 Abstraction functor . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.13 Abstractions algebra and coalgebra . . . . . . . . . . . . . . . . . . 23 4.14 h · f = g · F h . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.15 F h′ · f′ = g′ · h′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.16 Abstractions homomorphisms and cohomomorphisms . . . . . . . . . . 25

4.17 Abstractions homomorphisms_dom_cod and cohomomorphisms_dom_cod 25

4.18 Abstraction hom_composition . . . . . . . . . . . . . . . . . . . . . . 25 4.19 The Composition of Homomorphisms . . . . . . . . . . . . . . . . . . 26 4.20 Theorem hom_composition_wf . . . . . . . . . . . . . . . . . . . . . 26

4.21 Theorems hom_composition_dom and hom_composition_cod . . . . . 27

4.22 Theorem hom_composition_assoc . . . . . . . . . . . . . . . . . . . 27 4.23 Abstraction identity_hom . . . . . . . . . . . . . . . . . . . . . . . . 28 4.24 Theorem identity_hom_wf . . . . . . . . . . . . . . . . . . . . . . . 28 4.25 Theorems hom_dom_id and hom_cod_id . . . . . . . . . . . . . . . . . 28 4.26 Theorems hom_comp_id_l and hom_comp_id_r . . . . . . . . . . . . . 29 4.27 Abstraction algebra_category . . . . . . . . . . . . . . . . . . . . . 29 4.28 Theorem algebra_category_wf . . . . . . . . . . . . . . . . . . . . . 30 4.29 Abstraction coalgebra_category . . . . . . . . . . . . . . . . . . . . 31 4.30 Theorem coalgebra_category_wf . . . . . . . . . . . . . . . . . . . 31 5.1 (foldf) · in = f · F (foldf) . . . . . . . . . . . . . . . . . . . . . . . . 34 5.2 Display Form fold_df and Abstraction fold . . . . . . . . . . . . . . 36 5.3 Theorem fold_wf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.4 Theorem fold_exists_unique . . . . . . . . . . . . . . . . . . . . . 37 5.5 Abstraction left_invertible . . . . . . . . . . . . . . . . . . . . . . 38 5.6 Every Left-Invertible Arrow is a Catamorphism . . . . . . . . . . . . 39

5.7 Theorem left_invertible_implies_fold . . . . . . . . . . . . . . . 39
5.8 Extract of left_invertible_implies_fold . . . . . . . . . . . . . . 40

5.9 Simplified Extract of left_invertible_implies_fold . . . . . . . . 40 5.10 F (unfoldf) · f = out · (unfoldf) . . . . . . . . . . . . . . . . . . . . . 41 5.11 Display Form unfold_df and Abstraction unfold . . . . . . . . . . . 42 5.12 Theorem unfold_wf . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.13 Theorem unfold_exists_unique . . . . . . . . . . . . . . . . . . . . 42 5.14 Abstraction right_invertible . . . . . . . . . . . . . . . . . . . . . 43 5.15 Every Right-Invertible Arrow is an Anamorphism . . . . . . . . . . . 44

5.16 Theorem right_invertible_implies_unfold . . . . . . . . . . . . . 44
5.17 Simplified Extract of right_invertible_implies_unfold . . . . . . 44

6.1 Abstraction kernel . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

6.2 Theorem fold_implies_kernel_inclusion . . . . . . . . . . . . . . 47
6.3 Theorem postfactor_implies_kernel_inclusion . . . . . . . . . . 48
6.4 Theorem postfactor_implies_kernel_inclusion_cat . . . . . . . 48

6.5 Theorem prop_iff_exists . . . . . . . . . . . . . . . . . . . . . . . 49

6.6 Theorem kernel_inclusion_implies_fold . . . . . . . . . . . . . . 50
6.7 Theorem kernel_inclusion_implies_postfactor . . . . . . . . . . 51
6.8 Theorem kernel_inclusion_implies_postfactor_cat . . . . . . . 51

6.9 μF → A ≠ ∅ ⟹ F A → A ≠ ∅. . . . . . . . . . . . . . . . . . . . . 52 6.10 Theorem hom_fun_implies_algebra_fun . . . . . . . . . . . . . . . 52

6.11 Theorem surjective_iff_right_invertible . . . . . . . . . . . . . 54
6.12 Theorem surjective_iff_right_invertible_cat . . . . . . . . . . 54
6.13 Theorem kernel_inclusion_implies_postfactor_surjective . . . 55
6.14 Theorem kernel_inclusion_implies_postfactor_surjective_cat 55
6.15 Theorem kernel_inclusion_implies_fold_surjective . . . . . . . 56

6.16 Simplified Extract of Theorem kernel_inclusion_implies_fold . . 57 6.17 Abstraction list_and_2 . . . . . . . . . . . . . . . . . . . . . . . . . 57 6.18 Abstraction list_functor . . . . . . . . . . . . . . . . . . . . . . . . 58 6.19 Theorem list_functor_wf . . . . . . . . . . . . . . . . . . . . . . . 58 6.20 Abstraction list_functor_initial_algebra . . . . . . . . . . . . . 58

6.21 Theorem list_functor_initial_algebra_is_initial . . . . . . . 58

6.22 Theorem list_and_2_map_is_fold . . . . . . . . . . . . . . . . . . . 59 6.23 Simplified Extract of Theorem list_and_2_map_is_fold . . . . . . . 60 6.24 A Function g with and(map(p; ·)) = foldg . . . . . . . . . . . . . . . 61 6.25 A Catamorphism h where img(F h) is not Decidable . . . . . . . . . . 62 6.26 A Function h with ker(F h) ⊆ ker(h · in) that is not a Catamorphism 63

7.1 Abstraction binary_tree . . . . . . . . . . . . . . . . . . . . . . . . 66 7.2 Abstractions leaf and node . . . . . . . . . . . . . . . . . . . . . . . 66 7.3 Well-formedness theorems for leaf and node . . . . . . . . . . . . . . 66 7.4 Example: A binary tree . . . . . . . . . . . . . . . . . . . . . . . . . 67 7.5 Theorem binary_tree_example . . . . . . . . . . . . . . . . . . . . . 67 7.6 Abstraction treereduce . . . . . . . . . . . . . . . . . . . . . . . . . 68 7.7 Theorem treereduce_wf . . . . . . . . . . . . . . . . . . . . . . . . . 68 7.8 Abstraction treeheight . . . . . . . . . . . . . . . . . . . . . . . . . 69 7.9 Theorem treeheight_wf . . . . . . . . . . . . . . . . . . . . . . . . . 69 7.10 Theorem treereduce_example . . . . . . . . . . . . . . . . . . . . . 69 7.11 Abstraction Smaller . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 7.12 Abstraction treewellfnd . . . . . . . . . . . . . . . . . . . . . . . . 71 7.13 Abstraction treeunfold . . . . . . . . . . . . . . . . . . . . . . . . . 72 7.14 Theorem treeunfold_wf . . . . . . . . . . . . . . . . . . . . . . . . . 72 7.15 Example: bal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 7.16 Abstraction create_balanced . . . . . . . . . . . . . . . . . . . . . . 73 7.17 Theorem treeunfold_example . . . . . . . . . . . . . . . . . . . . . 74 7.18 Abstraction treefun . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 7.19 Theorem treefun_wf . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 7.20 Theorem fusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

8.1 Abstraction quicksort . . . . . . . . . . . . . . . . . . . . . . . . . . 78 8.2 Theorem list_length_filter . . . . . . . . . . . . . . . . . . . . . 79 8.3 Abstractions below and above . . . . . . . . . . . . . . . . . . . . . . 80 8.4 Theorem quicksort_wf . . . . . . . . . . . . . . . . . . . . . . . . . 81 8.5 Abstraction flatten and Theorem flatten_wf . . . . . . . . . . . . 82 8.6 Abstraction is_cons . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

8.7 Theorems is_cons_of_nil and is_cons_of_cons . . . . . . . . . . . 82

8.8 Abstraction unjoin . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 8.9 Theorem unjoin_wf . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 8.10 Abstraction mktree and Theorem mktree_wf . . . . . . . . . . . . . 84 8.11 Theorems mktree_of_nil and mktree_of_cons . . . . . . . . . . . . 84 8.12 Theorem quicksort_by_fusion . . . . . . . . . . . . . . . . . . . . . 85 8.13 Abstraction ordered . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 8.14 Abstraction tree_all_2 . . . . . . . . . . . . . . . . . . . . . . . . . 86 8.15 Abstraction treeordered . . . . . . . . . . . . . . . . . . . . . . . . 87 8.16 Theorem ordered_mktree . . . . . . . . . . . . . . . . . . . . . . . . 87 8.17 Theorem filter_all_2 . . . . . . . . . . . . . . . . . . . . . . . . . 87 8.18 Theorem list_all_2_filter_filter . . . . . . . . . . . . . . . . . 88 8.19 Theorem mktree_all_2 . . . . . . . . . . . . . . . . . . . . . . . . . 88 8.20 Theorem ordered_flatten . . . . . . . . . . . . . . . . . . . . . . . 89 8.21 Theorem list_all_2_append_lemma . . . . . . . . . . . . . . . . . . 89 8.22 Theorem ordered_append . . . . . . . . . . . . . . . . . . . . . . . . 89 8.23 Theorem flatten_all_2 . . . . . . . . . . . . . . . . . . . . . . . . . 90 8.24 Theorem list_all_2_implies_lemma . . . . . . . . . . . . . . . . . 90 8.25 Theorem list_all_2_if_all . . . . . . . . . . . . . . . . . . . . . . 90 8.26 Theorem ordered_quicksort . . . . . . . . . . . . . . . . . . . . . . 91 8.27 Theorem list_count_quicksort . . . . . . . . . . . . . . . . . . . . 91

8.28 Theorem list_count_over_filter_lemma . . . . . . . . . . . . . . . 92
8.29 Theorem list_count_filter_filter_lemma . . . . . . . . . . . . . 92

8.30 Theorem list_count_below_above . . . . . . . . . . . . . . . . . . . 92 8.31 Abstraction permutation . . . . . . . . . . . . . . . . . . . . . . . . 93 8.32 Theorem permutation_transitive . . . . . . . . . . . . . . . . . . . 94

8.33 Theorem permutation_over_append_lemma . . . . . . . . . . . . . . 94
8.34 Theorem permutation_filter_filter_lemma . . . . . . . . . . . . . 94

8.35 Theorem permutation_below_above . . . . . . . . . . . . . . . . . . 94 8.36 Theorem permutation_quicksort . . . . . . . . . . . . . . . . . . . 95 All men by nature desire to know.

Aristotle, 350 B.C.

Chapter 1

Introduction

Writing good software is difficult. Large computer programs consist of several million lines of code, and with current techniques, it appears to be almost impossible to write programs that are both correct and fast.

Hundreds of programming languages and CASE^{1} tools have been developed over the past decades to deal with the increasing complexity of software systems. Formal methods have successfully been applied to verify the correctness of critical systems [BM92, BS93, Sto96, HE99, Her00].

But good software should not only be correct and easy to write, understand and maintain. Despite the increasing speed of personal computers and declining hardware costs, programs should also be efficient. Unfortunately, the easy and the efficient solutions to a problem are often not the same.

Program transformations are a way to address both the issue of correctness and the issue of efficiency. By expressing algorithms in certain patterns, we can apply many standardized proof and optimization techniques [Hut98, GJ98, Hut99]. The following example was taken from [GJS93].

Example 1.0.1. Suppose we want to write a function all that tests whether all elements in a list L satisfy a predicate p. In the programming language Haskell [Bir98], all could be written as follows:

1Computer Aided Software Engineering

                       all p L = and (map p L)

The function map applies p to every element in L, creating an intermediate list of boolean values. The function and then computes the conjunction of those values.

Creating the intermediate list requires time and memory. The following is a more efficient version of all that operates directly on the structure of L, and thereby avoids creating a second list:

                        all' p L = f L, where

                           f []    =  True,
                           f h::t  =  p h && f t

Here [] denotes the empty list, and h :: t denotes a list with head h and tail t.

Deforestation [Dav87, Wad88, GJS93] can be used to transform the first version of all into the second, less concise, but more efficient version all'.

Applying program transformations manually is error-prone and—in the case of larger programs—practically impossible. Therefore the transformation process needs to be mechanized. Many compilers make use of program transformations to improve the performance of the generated code [KH89, BGS94, Jon96]. Thus it is important that we can express transformations as algorithms, and that we have clear criteria for when a program transformation can be applied. Furthermore, we want to have proof that the transformation does not change the semantics of a program.

Nuprl [CAB^{+}86, Jac94] is a proof development system that supports the interactive creation of programs and formal mathematical proofs. Functional programs can be written in Nuprl’s base language, a form of typed λ-calculus, and then proved to be correct by formal proofs in Nuprl’s constructive type theory. On the other hand, algorithms that are ‘correct by construction’ can be extracted from a Nuprl proof [How93]. The Nuprl system is described in greater detail in Chapter 3.

1.1 Objectives

We will formalize catamorphisms, anamorphisms and the required notions of category theory in Nuprl. We will formally prove conditions for when an arrow in a category is a catamorphism or anamorphism. We will give a constructive characterization of the non-constructive results from [GHA01], and we will show that those results do not, in general, hold constructively. For a certain class of constructive functions, we will present a transformation that writes such a function as a catamorphism. We will verify an instance of Bird’s fusion transformation [Bir95] for binary trees in Nuprl. We will then implement the well-known Quicksort algorithm [Hoa61], apply the fusion transformation to it, and formally prove the algorithm correct.

1.2 Organization

This thesis is organized as follows:

Chapter 2, Background, briefly discusses previous work about program transformations and approaches to their mechanization.

Chapter 3, The Nuprl System, explains the key elements of the Nuprl system and discusses some features of Nuprl that are frequently used in this thesis.

Chapter 4, Category Theory in Nuprl, defines some basic notions of category theory and presents a formalization of those notions in Nuprl.

Chapter 5, Catamorphisms and Anamorphisms, defines catamorphisms and anamorphisms using notions of category theory from Chapter 4. Necessary and sufficient conditions for when an arrow is a catamorphism or an anamorphism are formalized and proved in Nuprl.

Chapter 6, When is a Function a Catamorphism?, studies the special case of arrows in the category of sets, i.e. (total) functions. A proof is given that the results in [GHA01] are not valid constructively, conditions are identified under which a constructive function h is a catamorphism, and an algorithm is presented that computes a function g with h = foldg in this case.

Chapter 7, Bird’s Fusion Transformation, presents a program transformation that replaces the composition of an anamorphism and a catamorphism with a single function, thereby eliminating the intermediate data structure that is constructed by the anamorphism. An instance of Bird’s fusion transformation for binary trees is formalized and verified in Nuprl.

Chapter 8, Example: Quicksort, applies the fusion transformation to the well-known Quicksort algorithm. The algorithm is implemented in Nuprl, and a formal proof of its correctness is given.

Chapter 9, Conclusions, finally lists our contributions, summarizes the results, and points out possible future work.

4 CHAPTER 1. INTRODUCTION

Chapter 2

Background

In this chapter we give a brief overview of previous work on program transformations and approaches to their mechanization. Program transformation, also known as ‘software generation’, ‘program synthesis’ or ‘program calculation’, is the process of changing one program into another. We distinguish between rephrasings—transformations where the source and target language are the same—and translations, i.e. transformations with different source and target languages. This thesis will only consider the former kind of transformations.

2.1 Squiggol

In the 1980s, Richard Bird [Bir84] and Lambert Meertens [Mee86] developed a calculus for functional programs. This calculus is now known as the ‘Bird-Meertens Formalism’, or ‘Squiggol’. Its goal is to provide an algebra that allows the derivation of efficient programs from less efficient, but obviously correct specifications. A simple example of this approach was given in Chapter 1.

The Squiggol calculus originally only considered recursion functionals on lists. Catamorphisms (from the Greek preposition κατα meaning ‘downwards’) are recursive functions that destruct a list. The all function defined in Chapter 1 is an example of a catamorphism. Anamorphisms (from the Greek ανα meaning ‘upwards’) are functions that construct a list. The flatten function that flattens a binary tree into a list (see Chapter 8) is an example of an anamorphism. Catamorphisms are also frequently called ‘folds’, and ‘unfolds’ is another term for anamorphisms. With the introduction of category theory however, Squiggol was generalized to other recursive data types [Mal90], and the terms catamorphism and anamorphism (or fold and unfold) are now used in a more general sense. The Squiggol calculus and its extensions from category theory provide the theoretical foundation for our work.

2.2 Special-Purpose Transformation Tools

Several special-purpose software tools are commercially available for program transformations. The ‘DMS^{®} Software Reengineering Toolkit’ [Bax01], the ‘Kestrel Interactive Development System (KIDS)’ [Smi90], ‘Stratego’ [Vis01a], the ‘Transformation Assisted Multiple Program Realization System (TAMPR)’ [BHW97], and the ‘TXL Transformation System’ [Cor00] are among the more noteworthy ones that are not purely of academical interest. E. Visser gives an overview of the techniques used by these and other systems in [Vis01b]. Since we will formalize and verify program transformations using the general-purpose system Nuprl in this thesis, we do not describe any of those special-purpose systems in detail here.

2.3 General-Purpose Verification Tools

General-purpose verification and proof development tools like Nuprl were not specifically designed for reasoning about program transformations. Therefore formalizing a transformation and proving its correctness (i.e. that it does not change the semantics of a program) can be a challenge in a general-purpose system. The only other application of a general-purpose theorem prover to program transformations that we are aware of is by N. Shankar [Sha96], who used the ‘PVS Specification and Verification System’ [OSR95] to implement Bird’s fusion transformation (see Chapter 7) and Wand’s continuation-based transformation [Wan80]. PVS is similar to Nuprl in many ways. It supports recursive definitions, subtyping, dependent function and product types, parametric theories, induction, and many other features essential for the formalization of program transformations. The main difference between the two systems originates from Nuprl having a constructive type theory as its logical foundation.

2.4 Previous Formalizations of Category Theory

While general-purpose theorem provers apparently have not been applied to program transformations frequently, the basic notions of category theory however have been formalized in a number of systems before, also to some extend in Nuprl.

A significant amount of category theory has been formalized in the Mizar system [Miz], a formal system based on Tarski Grothendieck set theory. Rydeheard and Burstall considered computational aspects of category theory in their 1988 book [RB88]. In Nuprl, some formalization of category theory has been done previously [AP90]. However, this work was in a much earlier version of the system. In the Coq system [BBC^{+}97], Carvalho [Car98] has implemented a segment of category theory based on Huet and Saibi’s formalization [HS98]. Aczel [Acz93] has formalized categories in the LEGO system [LP92].

8 CHAPTER 2. BACKGROUND

The Nuprl System

The ‘Nuprl Proof Development System’ is “a computer system which [...] supports the interactive creation of proofs, formulas, and terms in a formal theory of mathematics” [CAB^{+}86]. Its first version was developed by R. Constable and J. Bates around 1985. Until today, Nuprl’s constructive type theory and its approach to displaying and editing mathematical text distinguish Nuprl from other theorem provers. Coq [BBC^{+}97], LEGO [LP92], and ALF [MN94] are all formal constructive systems, but Nuprl’s type theory is unique in its expressive power: Nuprl proof extracts are untyped λ-terms, while the systems mentioned above are limited to the typed λ-calculus. Thus Nuprl can extract general recursion functions, not just primitive recursive [Cal02].

A comprehensive description of Nuprl is given in [CAB^{+}86], and more up-to-date information can be found in [Jac94]. The Nuprl project also has its own web site at http://www.nuprl.org/. For this thesis we used Version 4.2 of the Nuprl system. Some of Nuprl’s more important features are discussed in this chapter. Other, more technical aspects of the system are explained throughout the thesis when necessary.

3.1 The Type Theory

The Nuprl type theory is the logical foundation of the Nuprl system. It is a constructive type theory based on [ML82]. The relationship between types and sets is non-trivial, e.g. see [Acz99, Wer97]. One of the main differences between classical set theory and Nuprl’s type theory is that equality of sets is extensional (i.e. sets are equal if and only if they contain the same elements), whereas type equality is intensional (i.e. types are equal if and only if they have the same ‘structure’). For the most part however, we will just model sets as types in this thesis. Issues related to the differences between sets and types will be specifically mentioned.

Types are constructed out of a few basic types by the use of type constructors. Among the types and constructors used in this thesis are the following:

Basic types. The empty type Void, the type of integers, ℤ, and the subtype ℕ = {z ∈ ℤ | z ≥ 0}. Also the type 𝔹 = {tt, ff} of boolean values, and the type Unit = {·}, which contains a single element.

Dependent product. Suppose A is a type, and B_{x} is a type for every x ∈ A. Then x:A × B_{x} is a type, containing all pairs (a, b) such that a ∈ A and b ∈ B_{a}. If B_{x} is the same for all x ∈ A, we simply write A×B to denote the cartesian product of A and B. The ‘spread’ operator is a destructor for the product type.

Dependent function. Suppose A is a type, and B_{x} is a type for every x ∈ A. Then x: A → B_{x} is a type, containing all functions f from A to ∪_{x∈A}B_{x} such that f(a) ∈ B_{a} for all a ∈ A. If B_{x} is the same for all x ∈ A, we simply write A → B to denote the type of all total functions^{1} from A to B.

Disjoint union. Suppose A and B are types. Then A + B is a type, containing all elements of the form inl(a) for a ∈ A, and inr(b) for b ∈ B. Nuprl provides an operator ‘decide’ that can be used to destruct the disjoint union type.

Subtype. Suppose A is a type and P_{a} is a proposition in which a of type A may occur free. Then {a : A | P_{a}} is the type of all a ∈ A for which P_{a} is true.

Recursive types. Nuprl has a built-in recursive data type List of (finite) lists, with constructors [] for the empty list, and :: for concatenation. It also provides a way of defining other recursive types, as well as recursive functions.

Type universes. Types in Nuprl are elements of so-called type universes. Nuprl has a cumulative hierarchy of universes 𝕌_{1}, 𝕌_{2}, 𝕌_{3}, ..., where each universe contains all previous type universes (i.e. 𝕌_{i} ∈ 𝕌_{j} for all i < j). Type universes are closed under the type constructors listed above. Most of our definitions and theorems are generic in the universe level; then we simply write 𝕌_{i} or 𝕌. We use 𝕌′ and 𝕌_{i′} as short notations for 𝕌_{i+1}.

1Since Nuprl’s type theory is constructive, these are really just all computable functions.

3.2 Constructive Aspects: Proofs as Programs

Logical propositions in Nuprl are defined via the type constructors:

• False is defined as Void.

• A ∧ B is defined as A × B.

• A ∨ B is defined as A + B.

• A ⟹ B is defined as A → B.

• ∀x:T. P (x) is defined as x:T → P_{x}.

• ∃x:T. P (x) is defined as x:T × P_{x}.

• ¬P is defined as P → False.

Thus every proposition corresponds to a type, and a proposition is provable if and only if the corresponding type is inhabited. Proving a proposition is equivalent to constructing a term that inhabits the corresponding type.

As a consequence, the law of excluded middle does not hold, i.e. p ∨ ¬p is not true for every proposition p. Instead, p ∨ ¬p only holds when we know which of the two possible cases p or ¬p is true. Although many classical theorems with proofs relying on the law of excluded middle will be unprovable in Nuprl, it has the advantage that proofs in Nuprl are constructive. Proving a theorem of the form

∀x_{1}, x_{2}, …, x_{k}. ∃y_{1}, y_{2}, …, y_{n}. R(x_{1}, x_{2}, …, x_{k}, y_{1}, y_{2}, …, y_{n})

(where R is some relation) yields an algorithm that takes k arguments x_{1}, x_{2}, …, x_{k} and returns n + 1 values y_{1}, y_{2}, …, y_{n}, ρ such that ρ is a proof of

R(x_{1}, x_{2}, …, x_{k}, y_{1}, y_{2}, …, y_{n}).

For instance, proving a theorem like ‘for every list of integers L exists a list M such that M is an ordered permutation of L’ would yield a sorting algorithm for lists of integers, together with evidence that M is indeed an ordered permutation of L. Which algorithm we get depends on the proof we give; different algorithms correspond to different proofs.

Thus we have two essentially different ways of reasoning about algorithms in Nuprl [How93, Cal98]: On the one hand, we can implement an algorithm (as a term in Nuprl’s type theory) and then formally verify the algorithm by stating and proving its relevant properties. This is done for the Quicksort algorithm in Chapter 8 of this thesis. On the other hand, we can get an algorithm that is ‘correct by construction’ out of a formal proof. This approach is used to extract a program transformation in Chapter 6.

3.3 Well-Formedness

We say a term is well-formed if and only if it is a member of some type. Nuprl requires well-formedness proofs for all terms used in the statement of a theorem; i.e. to prove a theorem, we do not only have to show that is is valid, but we also have to show that it is well-formed.

Often Nuprl can discharge well-formedness goals automatically. But in general, the problem of checking well-formedness is not decidable, so manual interaction is required in some cases. Also the structure of Nuprl’s proof rules sometimes forces us to prove the well-formedness of the same expression several times. One means of avoiding this is to prove well-formedness goals separately—in this case they are usually discharged automatically. However, sometimes proving well-formedness of a theorem can be the most difficult part of proving the theorem. This is one of the major reasons why even simple informal proofs can turn out to be remarkably tedious in Nuprl.

3.4 Display Forms, Abstractions, Proofs

Mathematical content in Nuprl is stored in ‘theory’ files. A theory is a list of (usually closely related) definitions (‘abstractions’), display forms, theorems and comments. Abstractions, which can have any number of arguments, are used to express one term by another. Each abstraction usually has an associated well-formedness theorem and an associated display form. The well-formedness theorem often simply states that the abstraction has a type; it is used automatically when Nuprl tries to prove the well-formedness of terms containing the abstraction. Display forms control how an abstraction is displayed by the Nuprl system. They can be used quite effectively to retain the usual mathematical notation. Display forms allow the use of special symbols (e.g. ‘∀’), they can define rules for parenthesis and whitespacing, they can hide arguments, and much more. Of course their flexibility can also be misused to implement an ‘abuse of notation’ that can turn understanding abstractions into a game of luck.

Display forms, abstractions, theorems and their proofs are created interactively. A Nuprl proof of a theorem has tree structure. To prove a theorem, tactics are applied to the proof goal. These tactics, which are based on the combination and repeated application of a few simple rewrite rules, can generate zero, one or more new subgoals, thereby mapping a partial proof to a complete or partial proof. Nuprl has predefined tactics for reasoning about integer arithmetic and systems of inequalities, for (mathematical, complete, and measure) induction, for rewriting and substituting expressions, for structural induction on recursively defined types, and many more. Further tactics can be defined by the user. The Auto tactic combines several simple tactics and is often useful to prove less complex proof goals in a single step. Nuprl also provides tacticals (e.g. Then, Repeat) to apply different tactics in a single proof step. However, with the increasing amount of computing power that is available, the system could probably benefit from a more powerful Auto tactic. Currently, despite the existence of fairly advanced tactics, very elementary proofs can be quite tedious sometimes.

The Nuprl type theory, the concepts of theory files, display forms, abstractions and theorems, the available tactics and tacticals, and many other aspects of the Nuprl system are described in greater detail in [CAB^{+}86] and [Jac94]. Also we did not describe the Nuprl editor and user interface in this chapter since knowledge of it is not necessary for understanding this thesis.

14 CHAPTER 3. THE NUPRL SYSTEM

Category Theory in Nuprl

Category theory is “a general mathematical theory of structures and sy[s]tems of structures” [Mar02]. This comparatively new field of mathematics arose in the study of certain group-theoretic and topological properties by S. Eilenberg and S. McLane [EM42, EM45] around 1942. Thanks to their general nature, categories have successfully been applied to problems in topology, algebra, geometry, functional analysis, and computer science.

This chapter presents some basic notions of category theory, and a formalization in Nuprl. We will need the notions presented here in Chapter 5 again to give a general definition of catamorphisms and anamorphisms.

4.1 Categories

A category consists of a class of objects, together with a class of arrows between these objects, which fulfill certain properties. The following definition is based on [Mac97].

Definition 4.1.1 (Category). A category C is a six-tuple

C = (Obj , Arr, dom, cod, ·, id),

where Obj is a class of objects, Arr is a class of arrows, and dom : Arr → Obj and cod : Arr → Obj are functions denoting an arrow’s domain and codomain respectively. · : Arr → Arr →^{p} Arr is a partial function, the composition operator, and id : Obj → Arr is the identity operator.

The operations are subject to the following properties:

[figure: A; f; f; B; id(B); g; B; g; C]

Figure 4.1: id(B) · f = f and g ·
id(B) = g

\xymatrix{A \ar[r]^{f} \ar[dr]_{g·f} & B \ar[d]^{g} \ar[dr]^{h·g} \\ & C \ar[r]_{h} & D} Figure 4.2: h · (g · f) = (h · g) · f

1. For all f, g ∈ Arr, g · f is defined if and only if cod(f) = dom(g), and in this case, dom(g · f) = dom(f) and cod(g · f) = cod(g). We say that f and g are composable in C if and only if cod(f) = dom(g).

2. For all A ∈ Obj , dom(id(A)) = cod(id(A)) = A. id(A) is called the identity arrow on A.

3. Unit Law: For all B ∈ Obj and f ∈ Arr with cod(f) = B, id(B) · f = f. For all B ∈ Obj and g ∈ Arr with dom(g) = B, g · id(B) = g (see Figure 4.1).

4. Associativity: For all f, g, h ∈ Arr with cod(f) = dom(g) and cod(g) = dom(h), h · (g · f) = (h · g) · f (see Figure 4.2).

Figure 4.3 shows a natural formalization of the type of categories in Nuprl. The dependent product type is used extensively here to state the properties that the composition operator and the identity operator must satisfy. The well-formedness proof for the category type requires manual verification of the two properties dom(h · g) = dom(g) (if g and h are composable) and cod(f) = dom(id(cod(f))). Altogether, the proof is about twelve steps long.^{1}

We also define six projection functions (with associated display forms and well-

formedness-theorems) cat_obj, cat_arr, cat_dom, cat_cod, cat_op, and cat_id

to map a category to its first, second, third, …, component in Nuprl. These projection functions give us easy access to the specific components of a category that we need in the statement of a theorem or a proof. Also we are free to chose more selfexplanatory names and display forms for them than C.2.2.2.1 for example, which would be the standard Nuprl notation for the fourth component (i.e. the codomain operator) of a category C. Furthermore, when C is of type Cat{i}, Nuprl does not

1In Nuprl, several proof tactics can be combined into a single proof step by so-called ‘tacticals’, e.g. Then. We do not count tactics that were combined in this way as separate steps. Therefore a single proof step often involves the application of two, three or even more different tactics.

 * ABS category
 Cat{i} ==
 Obj:𝕌
 × A:𝕌
 × dom:(A → Obj)
 × cod:(A → Obj)
 × o:{o:g:A → f:{f:A| cod f = dom g} →
     {h:A| dom h = dom f ∧ cod h = cod g} |
     ∀f,g,h:A. cod f = dom g ∧ cod g = dom h ⇒
     (h o g) o f = h o (g o f)}
 × {id:p:Obj → {f:A| dom f = p ∧ cod f = p} |
     ∀f:A. (id (cod f)) o f = f ∧ f o (id (dom f)) = f}

Figure 4.3: Abstraction category

know that C.1 is of type 𝕌 (unless we decompose C). It does, however, know that C_Obj is of type 𝕌 since we proved this as a well-formedness theorem. We will define similar projection functions for every component of every product type defined in this thesis.

We use the terms morphism and arrow interchangeably. Given a category C, the morphisms from p to q (in C) are those arrows in C with domain p and codomain q. Figure 4.4 shows a Nuprl implementation for the type of all morphisms from p to q. Here the well-formedness goal, i.e. to show that for every category C and for every object p and q in C, morphism[C](p,q) is a type, is discharged in a single step by the Auto tactic.

 * ABS morphism
 Mor[C](p,q) == {f:C_Arr| C_dom f = p ∧ C_cod f = q}

Figure 4.4: Abstraction morphism

To simplify notation, we write f : A → B for an arrow f with domain A and codomain B.

4.2 The Category of Types

One obvious interpretation of a category is to think of the objects as sets and of the arrows as functions. In fact we will need the category of sets, SET , later in this thesis.^{2} The objects of SET are all sets, the arrows are all (total) functions between sets, and the domain operator and codomain operator map a function to its domain and codomain respectively. Composition in SET is the usual composition of functions, and the identity arrow on a set A is simply the identity function on A.

When we try to define the category of types in Nuprl, there are two major differences that must be considered. Firstly, the class of all sets is not a set itself. Similarly, the notion ‘type of all types’ leads to contradictions [Gir72]. Therefore the type of objects in the category of types cannot contain all (other) types. The solution is to make it contain only all types up to a certain (but arbitrary) universe level i. The arrows are all functions between those types.^{3}

Secondly, an arrow cannot just be a function f : A → B: There is no constructive means to extract the function’s domain and codomain. Using the dependent product type, we formalize an arrow as a triple (A, B, f), where A is the domain, B is the codomain, and f : A → B. Thus the category’s domain operator just maps every arrow to its first component, while the codomain operator maps every arrow to its second component. Of course the definitions of the composition and identity operator must be compatible with this realization of arrows. Figure 4.5 shows the final definition of the category of types, or large category, in Nuprl.

 * ABS large_category
 large_category{i} ==
 <𝕌
 , A:𝕌 × B:𝕌 × (A → B)
 , λf.f.1
 , λf.f.2.1
 , λg,f.<f.1, g.2.1, g.2.2 o f.2.2>
 , λp.<p, p, λx.x> >

Figure 4.5: Abstraction large_category

To prove that the category of types is in fact a category, we should essentially only have to verify the unit law and the associativity of the composition operator. However, if we try a direct proof, Nuprl also generates a number of well-formedness goals and auxiliary subgoals when we decompose the category product type. Proving them is rather tedious, and the difficulties are propagated when we want to prove that other structures (with more complex objects and arrows than in the category of types) are categories. Therefore we prove a lemma category_if first (see Figure 4.6).^{4} The lemma states that every six-tuple with components of the appropriate types is in fact a category if the unit law holds and if the composition operator is associative. This way we have to deal with the additional well-formedness goals and auxiliary subgoals only once, namely when we prove the lemma. All future proofs in Nuprl that verify that some six-tuple is a category can then be simplified by using this lemma.

2While is is often convenient to think of the objects as sets and of the arrows as functions, SET is, however, just one example of a category.

3This gives us a different ‘category of types’ for each universe level i. However, all theorems that we prove in this thesis hold for any universe level.

 * THM category_if
 ∀Obj,A:𝕌. ∀dom,cod:A → Obj.
 ∀o:g:A → f:{f:A| cod f = dom g} →
     {h:A| dom h = dom f ∧ cod h = cod g} .
 ∀id:p:Obj → {f:A| dom f = p ∧ cod f = p} .
 (∀f,g,h:A. cod f = dom g ∧ cod g = dom h ⇒
     (h o g) o f = h o (g o f))
 ⇒ (∀f:A. (id (cod f)) o f = f ∧ f o (id (dom f)) = f)
 ⇒ <Obj, A, dom, cod, o, id> ∈ Cat{i}

Figure 4.6: Theorem category_if

The proof of the lemma requires about 36 steps, most of them to prove the wellformedness goals and auxiliary subgoals. The formal proof that large_category is a category (see Figure 4.7) then requires about 13 steps, one of which is of course the instantiation of the lemma. The easier well-formedness subgoals are discharged by Nuprl’s Auto tactic. The lemma comp_assoc, which is part of the FUN_1 library, is used to prove that composition of functions is associative. The lemmata comp_id_l and comp_id_r from the same library prove that the identity function is a left–identity and right–identity, respectively, for function composition. The polymorphic universe level i′ used in the well-formedness theorem is short Nuprl notation for i + 1.

 * THM large_category_wf
 large_category{i} ∈ Cat{i'}
                 Figure 4.7: Theorem large_category_wf

4.3 Dual Categories

Given any category C, we get the dual category of C by swapping every arrow’s domain and codomain, and swapping the order of arrow composition as well (i.e. g ·f becomes f · g).

4This is really a specialized well-formedness lemma for the pairing constructor and would automatically be invoked by Nuprl if we had named it pair_wf_category.

Definition 4.3.1 (Dual Category). Suppose C = (Obj , Arr, dom, cod, ·, id) is a category. Then

C^{op} = (Obj , Arr, cod, dom, ·^{op}, id)

is a category, where g ·^{op} f is defined as f · g. C^{op} is the dual category of C.

The Nuprl abstraction defining the dual category is shown in Figure 4.8. The wellformedness theorem shown in Figure 4.9 proves that the dual category is in fact a category. The proof is straightforward and requires about six steps, including the instantiation of the lemma category_if.

 * ABS dual_category
 Cˆ op == <C_Obj, C_Arr, C_cod, C_dom, λg,f.f C_op g, C_id>

Figure 4.8: Abstraction dual_category

 * THM dual_category_wf
 ∀C:Cat{i}.  Cˆ op ∈ Cat{i}

Figure 4.9: Theorem dual_category_wf

In this thesis we will not actually construct the dual category for any given category. We will however define several terms that are dual to each other, e.g. initial and terminal objects, algebras and coalgebras, homomorphisms and cohomomorphisms, and—last but not least—catamorphisms and anamorphisms. Therefore the concept of duality will be important throughout the rest of this chapter.

4.4 Initial and Terminal Objects

Initial objects are objects that have exactly one arrow going from them to every object in the category. Terminal objects are objects that have exactly one arrow coming to them from every object in the category. In other words, terminal objects are initial objects in the dual category.

Definition 4.4.1 (Initial Object). Suppose C is a category. We say an object A in C is initial (in C) if and only if for every object B in C, there exists a unique arrow f : A → B.

Definition 4.4.2 (Terminal Object). Suppose C is a category. We say an object B in C is terminal (in C) if and only if for every object A in C, there exists a unique arrow f : A → B.

This implies that if A is initial or terminal, the only arrow A → A is the identity arrow on A. In general, a category can have zero, one or more initial and terminal objects. In the category SET , for example, the empty set is the only initial object, and every singleton set (i.e. every set with exactly one element) is a terminal object. The corresponding Nuprl abstractions initial and terminal are shown in Figure 4.10. The well-formedness theorems for these abstractions are proved in a single step each by the Auto tactic.

 * ABS initial
 C-initial(p) == ∀q:C_Obj. ∃!f:C_Arr.  C_dom f = p ∧ C_cod f = q
 * ABS terminal
 C-terminal(p) == ∀q:C_Obj. ∃!f:C_Arr.  C_dom f = q ∧ C_cod f = p

Figure 4.10: Abstractions initial and terminal

Here ‘∃!’ is short for ‘there exists a unique’. An abstraction defining this quantifier in terms of ‘∃’ and ‘∀’ is shown in Figure 4.11.

 * ABS exists_unique
 ∃!x:T. B[x] == ∃x:T. B[x] ∧ (∀y:T. B[y] ⇒ y = x)

Figure 4.11: Abstraction exists_unique

4.5 Functors

Functors are arrows between categories. A functor from C to D, where C and D are categories, maps objects in C to objects in D and arrows in C to arrows in D such that these maps are compatible with the categories’ domain operators, the codomain operators, the composition of arrows, and with the identity operators.

Definition 4.5.1 (Functor). Suppose C = (Obj_{C}, Arr_{C}, dom_{C}, cod_{C}, ·_{C}, id_{C}) and D = (Obj_{D}, Arr_{D}, dom_{D}, cod_{D}, ·_{D}, id_{D}) are categories. Let F_{O} : Obj_{C} → Obj_{D}, and F_{M} : Arr_{C} → Arr_{D}. The pair F = (F_{O}, F_{M}) is a functor from C to D (write F : C → D) if and only if 1. ∀f ∈ Arr_{C} : dom_{D}(F_{M}(f)) = F_{O}(dom_{C}(f)),

2. ∀f ∈ Arr_{C} : cod_{D}(F_{M}(f)) = F_{O}(cod_{C}(f)),

3. ∀f, g ∈ Arr_{C} : dom_{C}(g) = cod_{C}(f) ⟹ F_{M}(g ·_{C} f) = F_{M}(g) ·_{D} F_{M}(f),

4. ∀A ∈ Obj_{C} : F_{M}(id_{C}(A)) = id_{D}(F_{O}(A)).

To simplify notation, we write F A for F_{O}(A) if A is an object in C, and F f for F_{M}(f) if f is an arrow in C. To formalize the type of all functors from C to D in Nuprl, we define a functor as a four-tuple, where the first component is the functor’s domain (i.e. C), the second component is the codomain (i.e. D), and the other two components are the object function F_{O} and the arrow function F_{M}. Since we restrict the first and second component of the functor to be of type Cat{i}, where i is a universe level, we also need to specify the universe level i in the definition of the functor type. This level should be greater than or equal to the maximum of the universe levels of C and D. Typically the universe levels of C and D will be i, and so we use level i for the type of functors between C and D.

 * ABS functor
 Functor{i}(C,D) ==
 {C:Cat{i}}
 × {D:Cat{i}}
 × O:(C_Obj → D_Obj)
 × {M:C_Arr → D_Arr|
 (∀f:C_Arr.  D_dom (M f) = O (C_dom f) ∧ D_cod (M f) = O (C_cod f))
 c∧ ((∀f:C_Arr. ∀g:{g:C_Arr| C_dom g = C_cod f} .
     M (g C_op f) = (M g) D_op (M f))
 ∧ (∀p:C_Obj.  M (C_id p) = D_id (O p)))}

Figure 4.12: Abstraction functor

Figure 4.12 shows the Nuprl abstraction defining the functor type. The proof of the associated well-formedness theorem requires about nine steps: We have to verify that if f and g are in Arr_{C} with dom_{C}(g) = cod_{C}(f), then dom_{D}(F_{M}(g)) = cod_{D}(F_{M}(f)) to prove that F_{M}(g) ·_{D} F_{M}(f) is well-formed in this case.

4.6 Algebras and Coalgebras

Given a category C and a functor F : C → C, an algebra over F is a pair (A, f), where A is an object and f : F A → A is an arrow in C. A coalgebra is a pair (A′, f′), where A′ is an object and f′ : A′ → F A′ is an arrow in C. In other words, coalgebras are algebras over the dual category.

Definition 4.6.1 (Algebra). Suppose C is a category and F : C → C is a functor. An algebra (over F) is a pair (A, f), where A is an object in C and f : F A → A is an arrow in C.

Definition 4.6.2 (Coalgebra). Suppose C is a category and F : C → C is a functor. A coalgebra (over F) is a pair (A, f), where A is an object in C and f : F → F A is an arrow in C.

For example, if F is the identity functor on C (mapping every object and arrow in C to itself), then for every object A in C, (A, id(A)) is both an algebra and a coalgebra over F. However, algebras and coalgebras for a given functor F may or may not exist.

 * ABS algebra
 Algebra(F) == p:F_dom_Obj ×
     {f:F_dom_Arr| F_dom_dom f = F_O p ∧ F_dom_cod f = p}
 * ABS coalgebra
 Coalgebra(F) == p:F_dom_Obj ×
     {f:F_dom_Arr| F_dom_dom f = p ∧ F_dom_cod f = F_O p}

Figure 4.13: Abstractions algebra and coalgebra

Using the dependent product type, defining the types of all algebras and coalgebras over a functor F : C → C is straightforward in Nuprl. The corresponding abstractions are shown in Figure 4.13. The proofs of the two well-formedness theorems algebra_wf and coalgebra_wf, showing that Algebra(F) and Coalgebra(F) are well-formed types for every functor F : C → C, require about four steps each, mainly because we must prove that the functor’s domain and codomain are equal.

4.7 Homomorphisms and Cohomomorphisms

Given two algebras (A, f) and (B, g) over the same functor F, a homomorphism from (A, f) to (B, g) is an arrow h : A → B such that the diagram shown in Figure 4.14 commutes. Similarly, a cohomomorphism from (A′, f′) to (B′, g′), where (A′, f′) and (B′, g′) are coalgebras over F, is an arrow h′ : A′ → B′ that makes the square shown in Figure 4.15 commute.

\xymatrix{F A \ar[d]_{f} \ar[rr]^{F h} &  & F B \ar[d]^{g} & A′ \ar[d]_{f′} \ar[rr]^{h′} &  & B′ \ar[d]^{g′} \\ A \ar[rr]_{h} &  & B & F A′ \ar[rr]_{F h′} &  & F B′ \\  & Figure 4.14: h · f = g · F h &  &  & Figure 4.15: F h′ · f′ = g′ · h′}

Definition 4.7.1 (Homomorphism). Suppose C is a category, F : C → C is a functor, and (A, f) and (B, g) are algebras over F. A homomorphism from (A, f) to (B, g) is an arrow h : A → B such that h · f = g · F h.

Definition 4.7.2 (Cohomomorphism). Suppose C is a category, F : C → C is a functor, and (A′, f′) and (B′, g′) are coalgebras over F. A cohomomorphism from (A′, f′) to (B′, g′) is an arrow h′ : A′ → B′ such that F h′ · f′ = g′ · h′.

The definition of the type of all homomorphisms (and similarly, all cohomomorphisms) over a functor F in Nuprl is relatively straightforward again and shown in Figure 4.16. We use the dependent product type to include the homomorphism’s domain (A, f) and codomain (B, g). Thus a homomorphism is a triple (instead of just an arrow h : A → B, from which we could only get A and B by applying the domain and codomain operators, but neither f or g). The same technique was used for arrows in the category of types and for the functor type before. The well-formedness theorems

homomorphisms_wf and cohomomorphisms_wf are proved in about eight steps each;

the main work is to verify that the arrows f and h and F h and g are composable (analogous F h′ and f′ and g′ and h′ for cohomomorphism).

In analogy to the morphism type, we also define the type of all homomorphisms over F from a given algebra (A, f) to another given algebra (B, g) (and similarly, the type of all cohomomorphisms with a given domain and codomain), see Figure 4.17. The corresponding well-formedness theorems are proved in a single step each.

4.8 The Category of Algebras

We can think of homomorphisms as arrows between algebras. Once we define a composition of homomorphisms that is associative, and for every algebra an identity homomorphism that satisfies the unit law, we have a new category: The category with algebras (over a functor F) as objects, and with homomorphisms (between those algebras) as arrows.

 * ABS homomorphisms
 Hom(F) ==
 A:Algebra(F)
 × B:Algebra(F)
 × {f:F_dom_Arr|
     (F_dom_dom f = A_obj) c∧ (F_dom_cod f = B_obj) c∧
     (f F_dom_op A_arr = B_arr F_dom_op (F_M f))}
 * ABS cohomomorphisms
 Cohom(F) ==
 A:Coalgebra(F)
 × B:Coalgebra(F)
 × {f:F_dom_Arr|
     (F_dom_dom f = A_obj) c∧ (F_dom_cod f = B_obj) c∧
     ((F_M f) F_dom_op A_arr = B_arr F_dom_op f)}
        Figure 4.16: Abstractions homomorphisms and cohomomorphisms
 * ABS homomorphisms_dom_cod
 Hom[F](A,B) == {f:Hom(F)| f_dom = A ∧ f_cod = B}
 * ABS cohomomorphisms_dom_cod
 Cohom[F](A,B) == {f:Cohom(F)| f_dom = A ∧ f_cod = B}
Figure 4.17: Abstractions homomorphisms_dom_cod and cohomomorphisms_dom_cod

4.8.1 The Composition of Homomorphisms

Homomorphisms are arrows in a category C. The obvious approach to define their composition is to simply define it as the composition in C. Figure 4.18 shows the Nuprl abstraction hom_composition. The formal definition of course has to be compatible with our realization of homomorphisms as triples.

 * ABS hom_composition
 g o_hom[F] f == <f_dom, g_cod, g_arr F_dom_op f_arr>

Figure 4.18: Abstraction hom_composition

However, we have to verify that the composition of two homomorphisms is again a homomorphism. Suppose (A, f), (B, g) and (C, h) are algebras, and a : (A, f) → (B, g) and b : (B, g) → (C, h) are homomorphisms. Then b · a is a homomorphism from

\xymatrix{F A \ar[d]_{f} \ar[r]^{F a} & F B \ar[d]^{g} \ar[r]^{F b} & F C \ar[d]^{h} \\ A \ar[r]_{a} & B \ar[r]_{b} & C}

Figure 4.19: The Composition of Homomorphisms

(A, f) to (C, h): Clearly b · a : A → C, and

(b · a) · f
= { associativity }
b · (a · f)
= { homomorphisms }
b · (g · F a)
= { associativity }
(b · g) · F a
= { homomorphisms }
(h · F b) · F a
= { associativity }
h · (F b · F a)
= { functors }
h · F (b · a).

In other words, the diagram shown in Figure 4.19 commutes.

In Nuprl, we state this result as a well-formedness theorem for hom_composition (see Figure 4.20). The formal proof, although it is based on the calculation shown above, requires about 95 steps: Many of the transformations used above generate one or two well-formedness subgoals which require several steps to be proved.

 * THM hom_composition_wf
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀K,L,M:Algebra(F). ∀f:Hom[F](K,L).
 ∀g:Hom[F](L,M). g o_hom[F] f ∈ Hom[F](K,M)
                Figure 4.20: Theorem hom_composition_wf

Now we prove two useful lemmata about the composition of homomorphisms and their domain and codomain: The domain of g · f is equal to the domain of f, and the codomain of g · f is equal to the codomain of g (see Figure 4.21). Both lemmata are proved in two steps each.

 * THM hom_composition_dom
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀K,L,M:Algebra(F). ∀f:Hom[F](K,L).
 ∀g:Hom[F](L,M). (g o_hom[F] f)_dom = f_dom
 * THM hom_composition_cod
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀K,L,M:Algebra(F). ∀f:Hom[F](K,L).
 ∀g:Hom[F](L,M). (g o_hom[F] f)_cod = g_cod
    Figure 4.21: Theorems hom_composition_dom and hom_composition_cod

We finally have to prove that the composition of homomorphisms is associative (see Figure 4.22). Informally this is immediate because we simply defined the composition of homomorphisms as the composition in C, which is associative by the second axiom of category theory. In Nuprl however, we have to show equality in the homomorphisms type, and including all well-formedness goals and auxiliary subgoals that we end up with, the proof is about 140 steps long (which makes it one of the longest proofs in

the CATEGORY_THEORY library).
 * THM hom_composition_assoc
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀K,L,M,N:Algebra(F). ∀f:Hom[F](K,L).
     ∀g:Hom[F](L,M). ∀h:Hom[F](M,N).
 h o_hom[F] (g o_hom[F] f) = (h o_hom[F] g) o_hom[F] f
               Figure 4.22: Theorem hom_composition_assoc

4.8.2 The Identity Homomorphism

For every algebra (A, f), the identity arrow on A is a homomorphism from (A, f) to (A, f): Clearly id(A) : A → A, and

id(A) · f
= { unit law }
f
= { unit law }
f · id(F A)
= { functors }
f · F (id(A)).

Hence the following definition makes sense.

Definition 4.8.1 (Identity Homomorphism). Suppose C is a category, F : C → C is a functor, and (A, f) is an algebra over F. Then the identity homomorphism on (A, f) is defined as the identity arrow on A.

Figure 4.23 shows the Nuprl abstraction identity_hom. Recall, we defined homomorphisms to be triples. The formal proof that this is in fact a homomorphism (see Figure 4.24) is about 23 steps long.

 * ABS identity_hom
 id_hom[F](A) == <A, A, F_dom_id A_obj>

Figure 4.23: Abstraction identity_hom

 * THM identity_hom_wf
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀A:Algebra(F).
     id_hom[F](A) ∈ Hom[F](A,A)

Figure 4.24: Theorem identity_hom_wf

Before we use this definition, we prove two lemmata again, namely that the domain and the codomain of the identity homomorphism on (A, f) are both equal to (A, f). Both lemmata (see Figure 4.25) are proved in a single step each.

 * THM hom_dom_id
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀A:Algebra(F). id_hom[F](A)_dom = A
 * THM hom_cod_id
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀A:Algebra(F). id_hom[F](A)_cod = A

Figure 4.25: Theorems hom_dom_id and hom_cod_id

The identity homomorphism satisfies the unit law for the composition of homomorphisms (see Figure 4.26). This follows immediately from the unit law for the identity arrow. The formal proof, however, is surprisingly tedious. We have to verify that certain arrows are composable several times. Altogether, the proof that the identity homomorphism cancels out on the left is about 60 steps long, and the proof that it cancels out on the right has approximately the same length.

 * THM hom_comp_id_l
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀h:Hom(F).
     id_hom[F](h_cod) o_hom[F] h = h
 * THM hom_comp_id_r
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀h:Hom(F).
     h o_hom[F] id_hom[F](h_dom) = h
          Figure 4.26: Theorems hom_comp_id_l and hom_comp_id_r

4.8.3 Definition of the Category of Algebras

We are now ready to define the category of algebras. As said before, this category has as objects all algebras over a given functor F : C → C (where C is a category), and as arrows all homomorphisms between these algebras. The domain operator and codomain operator map each homomorphism to its domain algebra and codomain algebra respectively. The composition of homomorphisms is defined as the usual composition of arrows in C, and the identity operator maps each algebra A to the identity homomorphism on A. Figure 4.27 shows the Nuprl abstraction algebra_category.

 * ABS algebra_category
 algebra_category(F) ==
 <Algebra(F)
 , Hom(F)
 , λh.h_dom
 , λh.h_cod
 , λh,g.h o_hom[F] g
 , λA.id_hom[F](A)>

Figure 4.27: Abstraction algebra_category

Theorem algebra_category_wf (see Figure 4.28) proves that this is in fact a category. The formal proof is about 29 steps long and uses several lemmata: category_if to get rid of a number of well-formedness goals, hom_composition_wf to prove that the composition of two homomorphisms is again a homomorphism, hom_composition_dom and hom_composition_cod to prove that the composition operator returns arrows with the proper domain and codomain, hom_composition_assoc to prove that it is associative, identity_hom_wf to prove that the identity homomorphism is in fact a homomorphism, hom_dom_id and hom_cod_id to prove that it has the proper domain and codomain, and hom_comp_id_l and hom_comp_id_r to prove the unit law. A few proof steps use other lemmata to deal with the (somewhat technical) difference

between the types homomorphisms and homomorphisms_dom_cod.
 * THM algebra_category_wf
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). algebra_category(F) ∈ Cat{i}
                Figure 4.28: Theorem algebra_category_wf

4.9 The Category of Coalgebras

The category of coalgebras can be defined completely analogous to the category of algebras. The composition of cohomomorphisms is defined as the composition of arrows in the original category C (just like the composition of homomorphisms before), and the identity cohomomorphism on a coalgebra (A, f) is simply the identity arrow on A again. With these definitions, we can easily verify that the composition of two cohomomorphisms always is a cohomomorphism again, and that associativity and the unit law are satisfied. The proofs are not identical to the proofs presented for homomorphisms and algebras, but dual—meaning that we have to swap domain and codomain, A and F A, and the order of arrow composition sometimes.

This is probably best illustrated by a small example, so we verify that the identity cohomomorphism on a coalgebra (A, f) is in fact a cohomomorphism from (A, f) to (A, f): Clearly id(A) : A → A, and

F (id(A)) · f
= { functors }
id(F (A)) · f
= { unit law }
f
= { unit law }
f · id(A).

Compared to the proof given for the identity homomorphism, the steps of reasoning are pretty much the same, with a few adjustments made for duality.

Unfortunately, ByDuality however is not a valid proof tactic (and would be hard to implement, because the use of dual notions does not only require us to give dual arguments, but it can also change the order in which subgoals occur in a Nuprl proof tree). Therefore all proofs from the previous section had to be modified for cohomomorphisms and coalgebras by hand, and their size is about the same as for homomorphisms and algebras before. Figures 4.29 and 4.30 show the main results of this section: A formal definition of the category of coalgebras, together with a Nuprl theorem proving that this is in fact a category.

 * ABS coalgebra_category
 coalgebra_category(F) ==
 <Coalgebra(F)
 , Cohom(F)
 , λh.h_dom
 , λh.h_cod
 , λh,g.h o_cohom[F] g
 , λA.id_cohom[F](A)>

Figure 4.29: Abstraction coalgebra_category

 * THM coalgebra_category_wf
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). coalgebra_category(F) ∈ Cat{i}
               Figure 4.30: Theorem coalgebra_category_wf

The following chapter defines catamorphisms and anamorphisms as certain arrows in the category of algebras and in the category of coalgebras, respectively.

32 CHAPTER 4. CATEGORY THEORY IN NUPRL

Catamorphisms and Anamorphisms

Catamorphisms (‘folds’) and anamorphisms (‘unfolds’) are certain arrows in the category of algebras and in the category of coalgebras, respectively. They can be used to specify many algorithms on lists, streams, trees and other recursive data types. More importantly, various optimization and proof techniques are known for algorithms that are expressed as a catamorphism or anamorphism [Hut98, GJ98, Hut99].

This chapter defines catamorphisms and anamorphisms using notions from category theory that were introduced in the previous chapter. Necessary and sufficient conditions for when an arrow is a catamorphism or an anamorphism are formalized and proved in Nuprl.

5.1 Catamorphisms

Suppose C is a category and F : C → C is a functor. Recall the category of algebras over F defined in Chapter 4. We say an algebra (μF, in) is initial if and only if it is an initial object in this category; that is, for every algebra (A, f), there exists a unique homomorphism h : (μF, in) → (A, f).

Example 5.1.1. Let 1 = {·} denote a set with exactly one element, and let + denote the disjoint union. For a set X, consider the functor L_{X} : SET → SET , defined by L_{X}(A) = 1 + (X × A) and L_{X}(f) = id(1) + (id(X) × f). This functor has an initial algebra (μL_{X}, in) = (List(X), nil + cons), where List(X) is the set of all finite lists over X, and nil : 1 → List(X) and cons : X × List(X) → List(X) are constructors

\xymatrix{F (μF) \ar[d]_{in} \ar[r]^{F (fold f)} & F A \ar[d]^{f} \\ μF \ar@{.>}[r]_{fold f} & A}

Figure 5.1: (foldf) · in = f · F (foldf)

for this set.^{1} We write [] for nil(·), the empty list, and x :: L for cons(x, L).

Fixing an initial algebra (μF, in), we define foldf to be this unique homomorphism from (μF, in) to (A, f). Hence foldf is the unique arrow that makes the square shown in Figure 5.1 commute.

Definition 5.1.2 (fold). Suppose C is a category, F : C → C is a functor and (μF, in) is an initial algebra. Then for every algebra (A, f),

foldf

is defined as the unique homomorphism from (μF, in) to (A, f).

We say an arrow h is a catamorphism if and only if it can be written as foldf for some arrow f.

Example 5.1.3. Consider the functor L_{X} with its initial algebra (List(X), nil+cons). Suppose (A, f) is an algebra over L_{X}. Then f : 1 + (X × A) → A can be written as f = f_{0} + f_{1}, where f_{0} : 1 → A and f_{1} : (X × A) → A. We can prove by structural induction on List(X) that every catamorphism h : List(X) → A satisfies the two equations

h([]) = f_{0}(·),
h(x :: L) = f_{1}(x, h(L)).

On the other hand, every function h that can be written in this form is a catamorphism on List(X). Examples are

length([]) = 0,
length(x :: L) = 1 + length(L)

1A formal proof of this is given in Chapter 6.

to compute the length of a list,

∑([]) = 0,
∑(x :: L) = x + ∑(L)

to compute the sum of a list of numbers, or the functions

and([]) = True,
and(x :: L) = x ∧ and(L)

and

(map p)([]) = [],
(map p)(x :: L) = p(x) :: (map p)(L)

mentioned in Chapter 1.

Definition 5.1.2 implies the following universal property of the fold operator [Mal90].

Theorem 5.1.4 (Universal Property of fold). Suppose C is a category, F : C → C is a functor and (μF, in) is an initial algebra. Furthermore, suppose that (A, f) is an algebra and that h : μF → A. Then

h = foldf ⟺ h · in = f · F h.

Proof. If h : μF → A is equal to foldf, then by definition of fold, h is a homomorphism from (μF, in) to (A, f). Therefore h · in = f · F h. This proves the ‘⇒’ direction of the theorem.

For the other direction, assume h : μF → A satisfies the equation h · in = f · F h. Then h is a homomorphism from (μF, in) to (A, f). Since there exists only one such homomorphism (namely foldf), we have h = foldf.

Although we defined fold as an operator mapping algebras over F to arrows of C, we did not actually specify an algorithm to compute foldf, given an algebra (A, f). We only know that foldf is the unique homomorphism from (μF, in) to (A, f), but this may be the most specific way of describing foldf that we have.

Therefore defining fold in Nuprl is not straightforward. One possible approach is to prove the existence of a function fold_fun from Algebra(F), the type of all algebras over F, into the type C_{Arr} of all arrows in C, such that fold_fun(A, f) · in = f · F (fold_fun(A, f)) for every algebra (A, f). The actual fold operator would then be defined as (the first component of) the extract of a proof of this theorem.

 * DISP fold_df
 <h:arrow:*>=fold[<C:category:*>,<F:functor:*>,<I:algebra:*>]
     (<f:algebra:*>)
 == fold(<C>; <F>; <I>; <f>; <h>)
 * ABS fold
 h=fold[C,F,I](f) ==
 (F_dom_dom h = I_obj) c∧ (F_dom_cod h = f_obj) c∧
 (h F_dom_op I_arr = f_arr F_dom_op (F_M h))

Figure 5.2: Display Form fold_df and Abstraction fold

We decided to define fold in a different way that completely avoids dealing with proof extracts. In Nuprl, fold is defined as a relation Algebra(F) → C_{Arr} → ℙ such that fold((A,f),h) holds if and only if h · in = f · F h. We use Nuprl’s display form facility [Jac94] to display fold((A,f),h) as an equation h = fold(A,f) (see Figure 5.2).

 * THM fold_wf
 ∀C:Cat{i}. ∀F:Functor{i}(C,C).
 ∀I:{I:Algebra(F)| algebra_category(F)-initial(I)} .
 ∀f:Algebra(F). ∀h:F_dom_Arr.
 h=fold[C,F,I](f) ∈ ℙ

Figure 5.3: Theorem fold_wf

The well-formedness theorem fold_wf which is shown in Figure 5.3 simply proves that h = fold(A,f) is a well-formed proposition. The proof is about twelve steps long. In particular, we have to verify that in and h and F h and f are composable arrows when h : μF → A. Since the composition of two arrows is defined only if the second arrow’s domain is equal to the first arrow’s codomain, the equation h · in = f · F h is not well-formed for arbitrary arrows h. We ensured that h has the proper domain and codomain by using Nuprl’s c∧ operator in the definition of fold. This operator can be characterized by the following proof rule:

\underline{Γ ⊢ ϕ Γ, ϕ ⊢ ψ} ; Γ ⊢ ϕ c∧ ψ ,

i.e. we may assume ϕ in the proof of ψ.

Now it is not hard to prove in Nuprl that for every algebra (A, f), there exists a unique arrow h such that h = foldf. The theorem fold_exists_unique proving this

 * THM fold_exists_unique
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀I:Algebra(F).
 algebra_category(F)-initial(I) ⇒
     (∀f:Algebra(F). ∃!h:F_dom_Arr.  h=fold[C,F,I](f) )
                 Figure 5.4: Theorem fold_exists_unique

is shown in Figure 5.4. The existence of h follows from the existence of a homomorphism from (μF, in) to (A, f), and the uniqueness of h follows from the uniqueness of this homomorphism. Note the difference between Figure 5.3 and Figure 5.4 in the way we stated that I is an initial algebra. In Nuprl using a hypothesis of the form x ∈ {y ∈ T | P [y]} gives us P [x] as a ‘hidden’ hypothesis—that is, we cannot use it unless we can prove that either P [x] or the proof goal has no computational content (i.e. is ‘squash-stable’). In the proof of fold_exists_unique however, we need the fact that I is an initial algebra to get our hands on a homomorphism from I to (A, f). So neither the hypothesis nor the proof goal are squash-stable in this case, and therefore having ‘I is an initial algebra’ as a hidden hypothesis is not strong enough, i.e. we must make it an explicit antecedent to the theorem. This means that the computational content will be a function that expects an argument that is evidence of I being initial. Proving the existence of h requires about 20 proof steps, and proving its uniqueness requires about 66 steps in Nuprl. Together with a few preparatory steps, the proof is about 96 steps long.

5.2 When is an Arrow a Catamorphism?

The universal property of fold provides a technically complete answer to this question. An arrow h : μF → A is a catamorphism if and only if h · in = f · F h for some arrow f : F A → A. However, usually only the arrow h is given—how would we know if an arrow f exists such that the above equation holds? And more importantly, how would we construct f from h?

No general answer seems to be known to this question. The composition of a catamorphism and a homomorphism is a catamorphism [Bir95], and other results are known for other specific kinds of arrows. In this section we prove a result from [MFP91] in Nuprl: That every left-invertible arrow is a catamorphism.

Definition 5.2.1 (Left-Invertible). Suppose C is a category and f is an arrow in C. We say f is left-invertible (in C) if and only if there exists an arrow g in C such that g · f = id(dom(f)).

Of course we made the implicit assumption dom(g) = cod(f) in the above definition, because otherwise g · f is not defined. For the same reason, we have to make this assumption explicit in the Nuprl abstraction left_invertible, which is shown in Figure 5.5. The associated well-formedness theorem, showing that left_invertible is a proposition, is then proved in two steps.

 * ABS left_invertible
 left-invertible[C](f) ==
     ∃g:{g:C_Arr| C-composable(f,g)} .  g C_op f = C_id (C_dom f)

Figure 5.5: Abstraction left_invertible

Equipped with this definition, we can now prove that every left-invertible arrow is a catamorphism.

Theorem 5.2.2. Suppose C is a category, F : C → C is a functor with an initial algebra (μF, in), and h : μF → A is a left-invertible arrow in C. Then

h = foldf

for some arrow f : F A → A.

Proof. Let g : A → μF be an arrow in C such that g · h = id(μF) (such a g exists since h is left-invertible). Then we have

h · in
= { unit law }
h · in · id(F (μF))
= { functors }
h · in · F (id(μF))
= { assumption }
h · in · F (g · h)
= { functors }
h · in · (F g · F h)
= { associativity }
(h · in · F g) · F h.

Therefore h = fold(h · in · F g) by the universal property of fold.

\xymatrix{F (μF) \ar[d]_{in} \ar[r]_{F h} & F A \ar@{.>}[d]^{f} \ar[l]_{F g} \\ μF \ar[r]_{h} & A \ar[l]_{g}}

Figure 5.6: Every Left-Invertible Arrow is a Catamorphism

The diagram in Figure 5.6 illustrates the proof idea. We need an arrow f : F A → A that makes the diagram commute. Clearly h · in · F g does the trick.^{2}

The Nuprl theorem left_invertible_implies_fold is shown in Figure 5.7. The formal proof takes about 70 steps, mainly because of several well-formedness goals that need to be verified.

 * THM left_invertible_implies_fold
 ∀C:Cat{i}. ∀F:Functor{i}(C,C).
 ∀I:{I:Algebra(F)| algebra_category(F)-initial(I)} .
 ∀h:{h:F_dom_Arr| F_dom_dom h = I_obj} .
 left-invertible[F_dom](h) ⇒ (∃f:Algebra(F). h=fold[C,F,I](f) )
            Figure 5.7: Theorem left_invertible_implies_fold

Since this theorem proves the existence of an object (namely of an arrow f such that h = foldf), the proof extract—which is shown in Figure 5.8—is also worth a look. The extract is a function with five arguments: a category C, a functor F, an initial algebra I, an arrow h, and a proof that h is left-invertible, denoted as % in the extract. In Nuprl, a proof that h is left-invertible is technically a pair (g, %1), where g is an arrow and %1 is a proof of g · h = id(dom(h)). Similarly, the value returned by the function in this extract is a pair ((A, f), %%), where (A, f) is an algebra such that h = foldf, and %% is a proof of this equality.

This becomes more evident if we reduce those λ-terms in the extract for which we know the argument. A few reduction steps give us the term shown in Figure 5.9. Now we can clearly see the witness term: It is the algebra <F_dom_cod h, h F_dom_op

2The diagram also illustrates another observation: We do not actually need h to be leftinvertible. The proof works when we only assume that F h is left-invertible. This is implied by the left-invertibility of h, but the converse is not true, so it is actually a weaker condition. If g · F h = id(F (μF)) for some arrow g, then h = fold(h · in · g).

 λC,F,I,h,%.
 let <g,%1> = %
 in
 (λ%2.(λ%3.(λ%4.(λ%5.(λ%6.(λ%7.
     <<F_dom_cod h, h F_dom_op (I_arr F_dom_op (F_M g))>
     , Ax
     , Ax
     , Ax>)
 Ax)
 Ax)
 Ax)
 Ax)
 ((λ%3.Ax) ext{functor_dom_cod_equal}{i:l}))
 ((λ%2.%2 C C F) ext{functor_dom_wf}{i:l})
           Figure 5.8: Extract of left_invertible_implies_fold

(I_arr F_dom_op (F_M g))>. This is of course the same witness that our informal proof above used, only in Nuprl notation.

 λC,F,I,h,%.
 let <g,%1> = %
 in
     <<F_dom_cod h, h F_dom_op (I_arr F_dom_op (F_M g))>
     , Ax
     , Ax
     , Ax>
       Figure 5.9: Simplified Extract of left_invertible_implies_fold

5.3 Anamorphisms

Anamorphisms are the dual notion to catamorphisms. While catamorphisms are homomorphisms from an initial algebra in the category of algebras, anamorphisms are defined as cohomomorphisms to a terminal coalgebra in the category of coalgebras. A formalization of this category in Nuprl was presented in Chapter 4.

We say a coalgebra (νF, out) is terminal if and only if it is a terminal object in the category of coalgebras; that is, for every coalgebra (A, f), there exists a unique cohomomorphism h : (A, f) → (νF, out).

\xymatrix{A \ar[d]_{f} \ar@{.>}[r]^{unfold f} & νF \ar[d]^{out} \\ F A \ar[r]_{F (unfold f)} & F (νF)}

Figure 5.10: F (unfoldf) · f = out · (unfoldf)

Definition 5.3.1. Suppose C is a category, F : C → C is a functor and (νF, out) is a terminal coalgebra. Then for every coalgebra (A, f),

unfoldf

is defined as the unique cohomomorphism from (A, f) to (νF, out).

Figure 5.10 illustrates this situation. We say an arrow h is an anamorphism if and only if it can be written as unfoldf for some arrow f. Recall the universal property of fold; a similar universal property holds for the unfold operator:

Theorem 5.3.2 (Universal Property of unfold). Suppose C is a category, F : C → C is a functor and (νF, out) is a terminal coalgebra. Furthermore, suppose that (A, f) is a coalgebra and that h : A → νF. Then

h = unfoldf ⟺ F h · f = out · h.

Proof. Suppose h : A → νF is equal to unfoldf. Then h is a cohomomorphism from (A, f) to (νF, out). Hence F h · f = out · h.

For the ‘⇐’ direction, suppose h : A → νF satisfies the equation F h · f = out · h. Then h is a cohomomorphism from (A, f) to (μF, out). Since there exists only one such cohomomorphism (namely unfoldf), we have h = unfoldf.

Using this universal property, we define unfold, similar to fold before, as a relation Coalgebra(F) → C_{Arr} → ℙ. Nuprl’s display form facility is used to display unfold as an equality nevertheless (see Figure 5.11).

The well-formedness theorem unfold_wf (see Figure 5.12) is proved in about twelve steps; the proof is dual to the proof of fold_wf. Again we use the c∧ operator in the definition of unfold to ensure that h has the proper domain and codomain, so that F h · f and out · h are both well-defined.

 * DISP unfold_df
 <h:arrow:*>=unfold[<C:category:*>,<F:functor:*>,<T:coalgebra:*>]
     (<f:coalgebra:*>)
 == unfold(<C>; <F>; <T>; <f>; <h>)
 * ABS unfold
 h=unfold[C,F,T](f) ==
 (F_dom_dom h = f_obj) c∧ (F_dom_cod h = T_obj) c∧
 ((F_M h) F_dom_op f_arr = T_arr F_dom_op h)

Figure 5.11: Display Form unfold_df and Abstraction unfold

 * THM unfold_wf
 ∀C:Cat{i}. ∀F:Functor{i}(C,C).
 ∀T:{T:Coalgebra(F)| coalgebra_category(F)-terminal(T)} .
 ∀f:Coalgebra(F). ∀h:F_dom_Arr.
 h=unfold[C,F,T](f) ∈ ℙ

Figure 5.12: Theorem unfold_wf

As we did for fold above, we can now prove the existence of a unique arrow h such that h = unfoldf for every coalgebra (A, f). The proof of unfold_exists_unique, which is shown in Figure 5.13, is dual to the proof of fold_exists_unique and also about 96 steps long.

 * THM unfold_exists_unique
 ∀C:Cat{i}. ∀F:Functor{i}(C,C). ∀T:Coalgebra(F).
 coalgebra_category(F)-terminal(T) ⇒
     (∀f:Coalgebra(F). ∃!h:F_dom_Arr.  h=unfold[C,F,T](f) )
               Figure 5.13: Theorem unfold_exists_unique

In the following section, we prove a result dual to the one that every left-invertible arrow is a catamorphism: that every right-invertible arrow is an anamorphism.

5.4 When is an Arrow an Anamorphism?

Again, a technically complete—but nevertheless unsatisfactory—answer is provided by the universal property of unfold. An arrow h : A → νF is an anamorphism if and only if F h · f = out · h for some arrow f : A → F A. This answer is unsatisfactory because it is not at all clear how to check if such an arrow f exists, and neither is it clear how to express f in terms of h even if we know that such a f exists. E. Meijer, M. Fokkinga, and R. Paterson [MFP91] dualized their result that every left-invertible arrow is a catamorphism to anamorphisms: Every right-invertible arrow is an anamorphism. Definition 5.4.1 (Right-Invertible). Suppose C is a category and f is an arrow in C. We say f is right-invertible (in C) if and only if there exists an arrow g in C such that f · g = id(cod(f)).

The corresponding Nuprl abstraction is shown in Figure 5.14. The well-formedness theorem for it simply states that this abstraction is a proposition, and is proved in two steps.

 * ABS right_invertible
 right-invertible[C](f) ==
     ∃g:{g:C_Arr| C-composable(g,f)} .  f C_op g = C_id (C_cod f)

Figure 5.14: Abstraction right_invertible

Theorem 5.4.2. Suppose C is a category, F : C → C is a functor with a terminal coalgebra (νF, out), and h : A → νF is a right-invertible arrow in C. Then

h = unfoldf

for some arrow f : A → F A.

Proof. Let g : νF → A be an arrow in C such that h · g = id(νF) (such a g exists since h is right-invertible). Then we have

out · h
= { unit law }
id(F (νF)) · out · h
= { functors }
F (id(νF)) · out · h
= { assumption }
F (h · g) · out · h
= { functors }
(F h · F g) · out · h
= { associativity }
F h · (F g · out · h).

\xymatrix{A \ar@{.>}[d]_{f} \ar[r]_{h} & νF \ar[d]^{out} \ar[l]_{g} \\ F A \ar[r]_{F h} & F (νF) \ar[l]_{F g}}

Figure 5.15: Every Right-Invertible Arrow is an Anamorphism

Therefore h = unfold(F g · out · h) by the universal property of unfold.

This situation is illustrated by the commutative diagram shown in Figure 5.15.^{3} The Nuprl theorem right_invertible_implies_unfold shown in Figure 5.16 is proved in about 70 steps.

 * THM right_invertible_implies_unfold
 ∀C:Cat{i}. ∀F:Functor{i}(C,C).
 ∀T:{T:Coalgebra(F)| coalgebra_category(F)-terminal(T)} .
 ∀h:{h:F_dom_Arr| F_dom_cod h = T_obj} .
 right-invertible[F_dom](h) ⇒ (∃f:Coalgebra(F). h=unfold[C,F,T](f) )
          Figure 5.16: Theorem right_invertible_implies_unfold

Figure 5.17 shows the simplified extract of the proof. We can clearly see our witness term in Nuprl notation: The witness term is given by the coalgebra <F_dom_dom h,

(F_M g) F_dom_op (T_arr F_dom_op h)>.
 λC,F,T,h,%.
 let <g,%1> = %
 in
     < <F_dom_dom h, (F_M g) F_dom_op (T_arr F_dom_op h)>
     , Ax
     , Ax
     , Ax>
     Figure 5.17: Simplified Extract of right_invertible_implies_unfold

In the following chapter we further study the case when h is an arrow in the category of sets, i.e. a (total) function.

3The diagram also shows that again we do not actually need the right-invertibility of h, but only the weaker condition that F h is right-invertible.

When is a Function a Catamorphism?

In the previous chapter we formally proved sufficient conditions for when an arbitrary arrow is a catamorphism or an anamorphism. In this chapter we want to further study the special case when h is an arrow in the category of sets (i.e. a function). The questions that we are trying to answer are still the same: Given an arrow h of the appropriate type, is h a catamorphism? If so, how can we construct an arrow g such that h = foldg?

6.1 A Non-Constructive Result

For the special case of the category SET , with sets as objects and functions as arrows, J. Gibbons, G. Hutton, and T. Altenkirch [GHA01] proved the following necessary and sufficient condition for when an arrow is a catamorphism.

Theorem 6.1.1 (Gibbons, Hutton, Altenkirch). Suppose F : SET → SET is a functor with an initial algebra (μF, in), A is a set, and h : μF → A. Then

(∃g : F A → A. h = foldg) ⟺ ker(F h) ⊆ ker(h · in).

Here ker f, the kernel of a function f : A → B, is defined as a binary relation on A containing all pairs of elements in A that are mapped to the same element in B.

Definition 6.1.2 (Kernel). Suppose f : A → B. Then

ker f = {(a_{1}, a_{2}) ∈ A × A | f(a_{1}) = f(a_{2})}

is the kernel of f.

Figure 6.1 shows the Nuprl abstraction kernel. The well-formedness theorem for it is proved in a single step by the Auto tactic.

 * ABS kernel
 ker[A,B] f == {aa:A × A| f aa.1 = f aa.2}

Figure 6.1: Abstraction kernel

Theorem 6.1.1 gives an exhaustive answer to our first question: h is a catamorphism if and only if ker(F h) ⊆ ker(h·in). Unlike the universal property of fold, this property only depends on h, so we do not have to know a function g with h = foldg beforehand to verify it. Unfortunately however, only the proof of the ‘⇒’ direction of Theorem 6.1.1 is constructive.^{1} The proof of the ‘⇐’ direction that is given in [GHA01] uses the law of excluded middle several times: “However, our proofs are set-theoretic, and make essential use of classical logic and the Axiom of Choice; hence our results do not generalize to categories of constructive functions.” Thus it is possible that the ‘⇐’ direction of Theorem 6.1.1 tells us a function h can be written as foldg for some function g, but even though we know such a g exists, we are still not able to compute it. What we would like to have is an algorithm to compute g from h—or equivalently, a constructive proof of the ‘⇐’ direction of Theorem 6.1.1.

6.2 A Necessary Condition

As said above, the ‘⇒’ direction of Theorem 6.1.1 can be proved constructively. In this section we present a constructive proof (which is essentially the same as the proof of the ‘⇒’ direction given in [GHA01]), together with a formalization of the theorem in Nuprl.

Theorem 6.2.1. Suppose F : SET → SET is a functor with an initial algebra (μF, in), A is a set, and h : μF → A. Then

(∃g : F A → A. h = foldg) ⟹ ker(F h) ⊆ ker(h · in).

The corresponding Nuprl theorem fold_implies_kernel_inclusion is shown in Figure 6.2. The key to its proof is the observation that the existence of ‘postfactors’ implies the inclusion of kernels. We say g : B → C is a postfactor of f : A → B for h : A → C if and only if h = g · f.

1It is no surprise that this direction has a constructive proof: The right side of the theorem is a subset relation, so it does not contain any computational information. In other words, there is nothing to construct.

 * THM fold_implies_kernel_inclusion
 ∀F:Functor{i'}(large_category{i},large_category{i}).
 ∀I:{I:Algebra(F)| algebra_category(F)-initial(I)} .
 ∀h:F_dom_Arr.
 (∃g:Algebra(F). h=fold[large_category{i},F,I](g) )
 ⇒ ker[F_O I_obj,large_category{i}_cod (F_M h)] (F_M h).2.2
     ⊆ ker[F_O I_obj,large_category{i}_cod (h F_dom_op I_arr)]
     (h F_dom_op I_arr).2.2
           Figure 6.2: Theorem fold_implies_kernel_inclusion

Lemma 6.2.2. Suppose that f : A → B and h : A → C, where A, B, C are sets. Then

(∃g : B → C. h = g · f) ⟹ ker f ⊆ ker h.

Proof. Assume that g : B → C with h = g · f. Then

(a_{1}, a_{2}) ∈ ker f
⟺  { kernels }
f(a_{1}) = f(a_{2})
⟹  { substitutivity }
g(f(a_{1})) = g(f(a_{2}))
⟺  { h = g · f }
h(a_{1}) = h(a_{2})
⟺  { kernels }
(a_{1}, a_{2}) ∈ ker h.

The Nuprl version of this lemma is shown in Figure 6.3. It is proved in about eight steps. However, we formalized arrows in the category of types not just as functions, but as triples (A, B, f : A → B) (see Chapter 4). Therefore we prove a second version of the lemma for arrows in the category of types. Even though this second lemma (see Figure 6.4) is just a ‘lifted’ version of postfactor_implies_kernel_inclusion and its proof relies on the first version of the lemma, the proof is about 36 steps long.

Using Lemma 6.2.2, the proof of Theorem 6.2.1 becomes quite simple.

 * THM postfactor_implies_kernel_inclusion
 ∀A,B,C:𝕌. ∀f:A → B. ∀h:A → C.
 (∃g:B → C. h = g o f) ⇒ ker[A,B] f ⊆ ker[A,C] h
         Figure 6.3: Theorem postfactor_implies_kernel_inclusion
 * THM postfactor_implies_kernel_inclusion_cat
 ∀A,B,C:large_category{i}_Obj. ∀f:Mor[large_category{i}](A,B).
 ∀h:Mor[large_category{i}](A,C).
 (∃g:Mor[large_category{i}](B,C). h = g large_category{i}_op f)
 ⇒ ker[A,B] f.2.2 ⊆ ker[A,C] h.2.2
       Figure 6.4: Theorem postfactor_implies_kernel_inclusion_cat

Proof.

∃g : F A → A. h = foldg
⟺  { universal property }
∃g : F A → A. h · in = g · F h
⟹  { Lemma 6.2.2 }
ker(F h) ⊆ ker(h · in).

The formal proof in Nuprl requires about 70 steps. Most of those steps are needed to discharge the well-formedness goals that are created by the instantiation of the

postfactor_implies_kernel_inclusion_cat lemma.

6.3 A Sufficient Condition

The proof that is given for the ‘⇐’ direction of Theorem 6.1.1 in [GHA01] is not constructive. However, by analyzing the proof, we were able to identify additional conditions that allow us to prove the ‘⇐’ direction constructively. But before we state these conditions, we have to deal with two problems that are not caused by the differences between classical and constructive logic, but by the differences between set theory and type theory.

So far we simply formalized sets as types in Nuprl. Up to this point this has not caused any problems. Types are also propositions in Nuprl, and we can prove the following equivalence (see Figure 6.5):

P ⟺ (∃x : P. T rue).

 * THM prop_iff_exists
 ∀P:ℙ.  P ⟺ (∃x:P. True)

Figure 6.5: Theorem prop_iff_exists

This suggests formalizing A ≠ ∅ as A (which is equivalent to (∃x : A. T rue)), and formalizing A = ∅ as ¬A (which is equivalent to ¬(∃x : A. T rue)). Now the problem is that there is no unique empty type. When two sets contain no elements, we can conclude that they are both equal to the empty set ∅, and therefore equal to each other. This conclusion is one step in the proof of the ‘⇐’ direction. However, when two types contain no elements, they can still be different. Types are equal only when they have the same ‘structure’; unlike equality of sets, equality of types is not extensional. The types Void and {x : ℤ. x < x}, for example, are distinguished as types even though they are extensionally equal, i.e. neither is inhabited. Thus we will have to find a different proof that does not rely on extensional type equality.

The second problem is that ker(F h) ⊆ ker(h · in) is not well-formed in Nuprl unless ker(F h) is actually a subset of ker(h · in). The subtype relation A ⊆ B is defined as (∀x : A. x ∈ B). If provable, the inhabitant is always equivalent to λx.Ax, where Ax is a Nuprl constant that is the inhabitant of a membership goal. Therefore x ∈ B is either true or not well-formed. So to prove that ker(F h) ⊆ ker(h · in) is well-formed, we have to prove that for every x ∈ ker(F h), x ∈ ker(h · in) is well-formed—which means we have to prove it is true, which means we have to prove ker(F h) ⊆ ker(h·in). But this subset relation is not true (and hence not provable) in general! If it was, we would not need it as an assumption to our proof.

This was not a problem when we stated the ‘⇒’ direction of Theorem 6.1.1 since ker(F h) ⊆ ker(h · in) was a conclusion then (hence something we could prove), but it clearly is a problem with the ‘⇐’ direction. We cannot even solve this problem by making (reasonable) additional assumptions. No matter how we try to state that every element of ker(F h) is an element of ker(h · in), the well-formedness problem remains.^{2} We finally decided to use Nuprl’s Fiat tactic to prove the well-formedness of ker(F h) ⊆ ker(h·in). Since we only use Fiat on a well-formedness subgoal however, this does not affect the correctness of the proof extract. If ker(F h) ⊆ ker(h · in) is in fact true, we still get a valid algorithm out of the proof that computes a function g with h = foldg given a function h. This being said, we state this section’s main result.

2For the same reason, there is no well-formedness theorem for the subtype abstraction in the standard Nuprl libraries.

Theorem 6.3.1. Suppose F : SET → SET is a functor with an initial algebra (μF, in), A is a set such that we can decide whether A is empty, and h : μF → A. Furthermore, suppose for every b ∈ F A we can decide whether b = (F h)(a) for some a ∈ F (μF). Then

(∃g : F A → A. h = foldg) ⟸ ker(F h) ⊆ ker(h · in).

Figure 6.6 shows a type-theoretic formalization of this theorem in Nuprl. The proof depends on two lemmata, namely that the inclusion of kernels implies the existence of postfactors, and that the existence of a function h : μF → A implies the existence of a function g : F A → A. We prove the former lemma first.

 * THM kernel_inclusion_implies_fold
 ∀F:Functor{i'}(large_category{i},large_category{i}).
 ∀I:{I:Algebra(F)| algebra_category(F)-initial(I)} .
 ∀A:large_category{i}_Obj. ∀h:Mor[large_category{i}](I_obj,A).
 Dec(A)
 ⇒ (∀b:F_O A. Dec(∃a:F_O I_obj.  b = (F_M h).2.2 a))
 ⇒ ((∃g:Algebra(F). h=fold[large_category{i},F,I](g) )
     ⇐ ker[F_O I_obj,large_category{i}_cod (F_M h)] (F_M h).2.2
     ⊆ ker[F_O I_obj,large_category{i}_cod (h F_dom_op I_arr)]
     (h F_dom_op I_arr).2.2)
           Figure 6.6: Theorem kernel_inclusion_implies_fold

Lemma 6.3.2. Suppose f : A → B and h : A → C. Furthermore, suppose we can decide whether C is empty, and for every b ∈ B we can decide whether b = f(a) for some a ∈ A. Then

(∃g : B → C. h = g · f) ⟸ (ker f ⊆ ker h ∧ B → C ≠ ∅).

Proof. Assume ker f ⊆ ker h and B → C ≠ ∅.

If C = ∅, then B = ∅ since B → C ≠ ∅, and A = ∅ since f : A → B. Therefore f = h = id(∅), and if we choose g = id(∅), clearly g : B → C and h = g · f.

If C ≠ ∅, let c be an arbitrary element in C. Let choice : {b ∈ B | ∃a ∈ A. b = f(a)} → A be a function with f(choice(b)) = b for all b ∈ B.^{3} For b ∈ B define g(b) ∈ C as follows: If b = f(a) for some a ∈ A, then g(b) = h(choice(b)). Otherwise, g(b) = c.

3To prove that such a function choice exists, we need the Axiom of Choice. Interestingly, this axiom has a proof (!) in Nuprl that is based simply on the representation of functions and of the quantifiers ∀ and ∃.

Now let a ∈ A. Since f(choice(f(a))) = f(a) by definition of choice, we have (choice(f(a)), a) ∈ ker f ⊆ ker h. Hence g(f(a)) = h(choice(f(a))) = h(a), and therefore h = g · f.

To give a constructive proof that the inclusion of kernels implies the existence of postfactors, we made two additional assumptions compared to the statement of this lemma in [GHA01]: that we can decide whether the codomain of h is empty, and that we can decide whether an element in the codomain of f is in the image of f. The

Nuprl theorem kernel_inclusion_implies_postfactor is shown in Figure 6.7.

The formal proof is about 43 steps long; the well-formedness of ker f ⊆ ker h is proved by the Fiat tactic.

 * THM kernel_inclusion_implies_postfactor
 ∀A,B,C:𝕌. ∀f:A → B. ∀h:A → C.
 Dec(C)
 ⇒ (∀b:B. Dec(∃a:A. b = f a))
 ⇒ ((∃g:B → C. h = g o f) ⇐ ker[A,B] f ⊆ ker[A,C] h ∧ B → C)
         Figure 6.7: Theorem kernel_inclusion_implies_postfactor

Figure 6.8 shows a ‘lifted’ version of the lemma for arrows in the category of sets. Despite the use of the original lemma in the proof of the lifted version, the proof is about 71 steps long.

 * THM kernel_inclusion_implies_postfactor_cat
 ∀A,B,C:large_category{i}_Obj. ∀f:Mor[large_category{i}](A,B).
 ∀h:Mor[large_category{i}](A,C).
 Dec(C)
 ⇒ (∀b:B. Dec(∃a:A. b = f.2.2 a))
 ⇒ ((∃g:Mor[large_category{i}](B,C). h = g large_category{i}_op f)
     ⇐ ker[A,B] f.2.2 ⊆ ker[A,C] h.2.2
     ∧ Mor[large_category{i}](B,C))
       Figure 6.8: Theorem kernel_inclusion_implies_postfactor_cat

The second lemma that we need to prove Theorem 6.3.1 is stated below.

Lemma 6.3.3. Suppose F : SET → SET is a functor with an initial algebra (μF, in), and A is a set such that we can decide whether A is empty. Then

μF → A ≠ ∅ ⟹ F A → A ≠ ∅.

Figure 6.9: μF → A ≠ ∅ ⟹ F A → A ≠ ∅.^{[figure: F (μF); in; F A; f; F g; μF; h; A; g]}

Proof. If A ≠ ∅, then trivially F A → A ≠ ∅.

If A = ∅, then the embedding g : A ↪ μF is a function from A to μF. Thus F g : F A → F (μF) by the properties of functors. Hence h · in · F g : F A → A.

Therefore F A → A ≠ ∅ in either case.

Figure 6.9 illustrates the situation: Given a function h : μF → A, we can find a function f : F A → A. The functions g : A → μF and F g : F A → F (μF) are needed only in the case A = ∅. If A ≠ ∅, they may not exist—but we can construct a function f : F A → A directly then. Note that the lemma is not true for arbitrary categories. The proof of the lemma given above is different from the proof that was given in [GHA01]^{4}, but the theorem hom_fun_implies_algebra_fun (which is shown in Figure 6.10) is proved along the same lines. The formal proof is about 49 steps long.

 * THM hom_fun_implies_algebra_fun
 ∀F:Functor{i'}(large_category{i},large_category{i}).
 ∀I:{I:Algebra(F)| algebra_category(F)-initial(I)} .
 ∀A:large_category{i}_Obj.
 Dec(A)
 ⇒ Mor[large_category{i}](I_obj,A)
 ⇒ Mor[large_category{i}](F_O A,A)
            Figure 6.10: Theorem hom_fun_implies_algebra_fun

We are now ready to prove Theorem 6.3.1.

4mainly because of the problem mentioned earlier that there is no unique empty type, but also because we avoided using the classical version of the contrapositive, (¬p ⟹ ¬q) ⟹ (q ⟹ p), which is not true constructively

Proof.

ker(F h) ⊆ ker(h · in)
⟺  { Lemma 6.3.3, h : μF → A }
ker(F h) ⊆ ker(h · in) ∧ F A → A ≠ ∅
⟹  { Lemma 6.3.2 }
∃g : F A → A. h · in = g · F h
⟺  { universal property }
∃g : F A → A. h = foldg.

Although this proof is relatively simple, a number of well-formedness goals have to be dealt with in the formal proof of the kernel_inclusion_implies_fold theorem. Therefore the formal proof is about 115 steps long.

Clearly we can decide whether an element in F A is in the image of F h when F h is surjective (onto). We will show that F h is surjective if h is. Therefore every surjective function that satisfies the condition of kernel inclusion is a catamorphism if we can decide whether its codomain A is empty.^{5} We could relatively easily prove this as a corollary to Theorem 6.3.1. Closer inspection of the proof of Theorem 6.3.1 however shows that when h is surjective, we do not need the additional assumption that we can decide whether A is empty.

Theorem 6.3.4. Suppose F : SET → SET is a functor with an initial algebra (μF, in), and h : μF → A is surjective. Then

(∃g : F A → A. h = foldg) ⟸ ker(F h) ⊆ ker(h · in).

We first prove that a function is surjective if and only if it is right-invertible in SET .

Lemma 6.3.5. Suppose f : A → B. Then

f is surjective ⟺ f is right-invertible in SET .

Proof. For the ‘⇒’ direction, suppose f is surjective. Then there exists a function g : B → A such that f(g(b)) = b for all b ∈ B (by the Axiom of Choice). Hence f · g = id(B), so f is right-invertible.

For the ‘⇐’ direction, suppose f is right-invertible in SET . Then f · g = id(B) for some function g : B → A. Now let b ∈ B. Then f(g(b)) = (f · g)(b) = (id(B))(b) = b. Therefore f is surjective.

5Note that every injective (one-to-one) function is a catamorphism by Theorem 5.2.2.

Figure 6.11 shows a formalization of the lemma in Nuprl. The formal proof is about 33 steps long and makes use of the ax_choice lemma from the FUN_1 library.

 * THM surjective_iff_right_invertible
 ∀A,B:𝕌. ∀f:A → B.
     Surj(A;B;f) ⟺ right-invertible[large_category{i}](<A, B, f>)
          Figure 6.11: Theorem surjective_iff_right_invertible

We also state and prove a ‘lifted’ version of the lemma for arrows in the category of types. This lifted version is shown in Figure 6.12. Lifting the lemma requires about 11 proof steps; of course we use the lemma surjective_iff_right_invertible in

the proof of surjective_iff_right_invertible_cat.
 * THM surjective_iff_right_invertible_cat
 ∀f:large_category{i}_Arr
     Surj(large_category{i}_dom f;large_category{i}_cod f;f.2.2)
     ⟺ right-invertible[large_category{i}](f)
        Figure 6.12: Theorem surjective_iff_right_invertible_cat

We now prove a lemma similar to Lemma 6.3.2, but for surjective functions.

Lemma 6.3.6. Suppose f : A → B is surjective, and suppose h : A → C. Then

(∃g : B → C. h = g · f) ⟸ ker f ⊆ ker h.

Proof. Assume ker f ⊆ ker h.

Let choice : B → A be a function with f(choice(b)) = b for all b ∈ B (such a function choice exists by the Axiom of Choice since f is surjective). Define g : B → C by g(b) = h(choice(b)) for every b ∈ B.

Now h = g · f by construction of g: Let a ∈ A. Since f(choice(f(a))) = f(a) by definition of choice, (choice(f(a)), a) ∈ ker f ⊆ ker h. Therefore g(f(a)) = h(choice(f(a))) = h(a).

Figure 6.13 shows a formalization of this lemma in Nuprl. The formal proof requires about 14 steps. It is similar to the proof of kernel_inclusion_implies_postfactor, but slightly simpler—just like the informal proof. The well-formedness of ker f ⊆ ker h is again proved by the Fiat tactic.

As for the kernel_inclusion_implies_postfactor lemma above, we prove a ‘lifted’

version of this lemma for arrows in the category of types. The lifted version is shown

 * THM kernel_inclusion_implies_postfactor_surjective
 ∀A,B,C:𝕌. ∀f:A → B. ∀h:A → C.
 Surj(A;B;f) ⇒ ((∃g:B → C. h = g o f) ⇐ ker[A,B] f ⊆ ker[A,C] h)
   Figure 6.13: Theorem kernel_inclusion_implies_postfactor_surjective
 * THM kernel_inclusion_implies_postfactor_surjective_cat
 ∀A,B,C:large_category{i}_Obj. ∀f:Mor[large_category{i}](A,B).
 ∀h:Mor[large_category{i}](A,C).
 Surj(A;B;f.2.2)
 ⇒ ((∃g:Mor[large_category{i}](B,C). h = g large_category{i}_op f)
     ⇐ ker[A,B] f.2.2 ⊆ ker[A,C] h.2.2)
 Figure 6.14: Theorem kernel_inclusion_implies_postfactor_surjective_cat

in Figure 6.14. Its proof is similar to the proof of the lifted lemma for functions with a decidable image (see Figure 6.8) and requires about 47 steps.

Using the two Lemmata 6.3.5 and 6.3.6, we can now prove Theorem 6.3.4.

Proof. We first show that F h : F (μF) → F A is surjective. Since h is surjective, h is right-invertible by Lemma 6.3.5. Let g : A → μF be a function with h · g = id(A). Then

F h · F g
= { functors }
F (h · g)
= { assumption }
F (id(A))
= { functors }
id(F A).

Hence F h is right-invertible, and therefore surjective (again by Lemma 6.3.5). Now

ker(F h) ⊆ ker(h · in)
⟹  { Lemma 6.3.6 }
∃g : F A → A. h · in = g · F h
⟺  { universal property }
∃g : F A → A. h = foldg

completes the proof.

See Figure 6.15 for a statement of this theorem in Nuprl. We use the lemma ker-

nel_inclusion_implies_postfactor_surjective_cat to prove the existence of g,
and surjective_iff_right_invertible_cat to prove that F h is surjective. Alto-

gether the formal proof requires about 145 steps. Fiat is used to prove the wellformedness of ker(F h) ⊆ ker(h · in).

 * THM kernel_inclusion_implies_fold_surjective
 ∀F:Functor{i'}(large_category{i},large_category{i}).
 ∀I:{I:Algebra(F)| algebra_category(F)-initial(I)} .
 ∀A:large_category{i}_Obj. ∀h:Mor[large_category{i}](I_obj,A).
 Surj(I_obj;A;h.2.2)
 ⇒ ((∃g:Algebra(F). h=fold[large_category{i},F,I](g) )
     ⇐ ker[F_O I_obj,large_category{i}_cod (F_M h)] (F_M h).2.2
     ⊆ ker[F_O I_obj,large_category{i}_cod (h F_dom_op I_arr)]
     (h F_dom_op I_arr).2.2)
      Figure 6.15: Theorem kernel_inclusion_implies_fold_surjective

We now have two simple conditions for when a constructive function h that satisfies the condition of kernel inclusion is a catamorphism: h is a catamorphism if the image of F h is decidable and we can decide whether the codomain of h is empty, and h is a catamorphism if h is surjective.

6.4 Computing fold^{−1}: A Simple Example

In the previous section we gave a constructive proof for when a function h is a catamorphism. Embedded in the proof is an algorithm to compute a function g such that h = foldg. Figure 6.16 shows a simplified version of the extract of the proof of theorem kernel_inclusion_implies_fold (the original extract was about six pages long). We can see how the function g in the witness term (A, g) is constructed by

instantiating the kernel_inclusion_implies_postfactor_cat theorem. The argu-

ment %@0 is a proof that we can decide whether A is empty, %13 proves that for every b ∈ F A we can decide whether b = (F h)(a) for some a ∈ F (μF), and %14 finally proves the kernel inclusion.

In this section we apply the kernel_inclusion_implies_fold theorem to the all function defined in Chapter 1 to write this function as a catamorphism. Recall the definition of all:

                       all p L = and (map p L)

6.4. COMPUTING FOLD^{−1}: A SIMPLE EXAMPLE 57

 λF,I,A,h,%@0,%13,%14.
 (let <g,%24> =
     (ext{kernel_inclusion_implies_postfactor_cat}{i:l}
     (F_O I_obj)
     (large_category{i}_cod (F_M h))
     (large_category{i}_cod (h F_dom_op I_arr))
     (F_M h)
     (h F_dom_op I_arr)
     (%@0)
     (λb.%13 b)
     <λ.Ax, (ext{hom_fun_implies_algebra_fun}{i:l} F I A %@0 h) >)
 in
     <<A, g>, Ax, Ax, Ax>

Figure 6.16: Simplified Extract of Theorem kernel_inclusion_implies_fold

Here L is a list over some type T, and p : T → 𝔹. Figure 6.17 shows a formalization of the and function in Nuprl. The corresponding well-formedness theorem shows that list_and_2 is a boolean value if L is a list of booleans. It is proved in about six steps by structural induction on L. The second function that we need to define all, the map function, is already defined in the LIST_1 library.

 * ABS list_and_2
 ∧_{b}(L) == (letrec recfun(L) =
     case L of [] => tt | h::t => h ∧_{b} recfun t esac ) L

Figure 6.17: Abstraction list_and_2

Before we can prove that all is a catamorphism, we have to show that List(T) is the object of an initial algebra. Consider the functor L_{T} : SET → SET again, defined by L_{T} (A) = 1 + (T × A) and L_{T} (f) = id(1) + (id(T) × f). Figure 6.18 shows the Nuprl abstraction defining this functor. The corresponding well-formedness theorem is shown in Figure 6.19. Verifying that list_functor is in fact a functor (from SET to SET ) takes about 54 proof steps.

This functor has an initial algebra (μL_{T} , in) = (List(T), nil + cons), which is defined formally in Figure 6.20. The corresponding well-formedness theorem shows that list_functor_initial_algebra is in fact an algebra. It is proved in about six steps.

To verify that this is an initial algebra, we have to show that for every other algebra (A, f) there exists a unique homomorphism h from (List(T), nil + cons) to (A, f). Since h is a homomorphism, i.e. h · (nil + cons) = (id(1) + (id(T) × h)) · f, we have

 * ABS list_functor
 ListF{i}(T) ==
 <large_category{i}
 , large_category{i}
 , λA.Unit + T × A
 , λf.<Unit + T × large_category{i}_dom f
     , Unit + T × large_category{i}_cod f
     , λx.case x of inl(y) => x |
     inr(z) => let <t,a> = z in inr <t, f.2.2 a> >>

Figure 6.18: Abstraction list_functor

 * THM list_functor_wf
 ∀T:𝕌.  ListF{i}(T) ∈ Functor{i'}(large_category{i},large_category{i})

Figure 6.19: Theorem list_functor_wf

 * ABS list_functor_initial_algebra
 InitialAlgebra(ListF(T)) ==
 <T List
 , Unit + T × T List
 , T List
 , λx.case x of inl(y) => [] | inr(z) => let <h,t> = z in h::t>
          Figure 6.20: Abstraction list_functor_initial_algebra

h([]) = f(inl ·) and h(u :: v) = f(inr (u, h(v))) for all u ∈ T, v ∈ List(T). Both that h is a homomorphism and that h is unique can be proved by structural induction on lists.

The corresponding Nuprl theorem list_functor_initial_algebra_is_initial is

shown in Figure 6.21. The proof of this theorem is quite technical and complicated by our inevitable formalization of algebras, homomorphisms and arrows in the category of types as tuples. With approximately 211 proof steps, it is the longest proof in this thesis. About 140 of those steps are required only to show the uniqueness of h.

 * THM list_functor_initial_algebra_is_initial
 ∀T:𝕌.  algebra_category(ListF{i}(T))-initial(InitialAlgebra(ListF(T)))
      Figure 6.21: Theorem list_functor_initial_algebra_is_initial

Using the kernel_inclusion_implies_fold theorem, we can now prove that the composition of map and and is a catamorphism. We do, however, need one more assumption: that we can decide for all b ∈ 𝔹 whether there exists a list L ∈ List(T) with b = and(map(p; L)).^{6} If b = true, then b = and([]) = and(map(p; [])). Therefore it is sufficient if we can decide whether p(t) = false for some t ∈ T: If so, then false = and(map(p; t :: [])). Otherwise and(map(p; L)) = true for all L ∈ List(T); this can be proved by structural induction on L. Figure 6.22 shows the Nuprl

theorem list_and_2_map_is_fold.

 * THM list_and_2_map_is_fold
 ∀T:𝕌. ∀p:T → 𝔹.
 Dec(∃t:T. p t = ff)
 ⇒ (∃g:Algebra(ListF{i}(T))
     <T List, 𝔹, λL.∧_{b}(map(p;L))> =
     fold[large_category{i},ListF{i}(T),InitialAlgebra(ListF(T))](g) )
              Figure 6.22: Theorem list_and_2_map_is_fold

The extract of this theorem (see Figure 6.23) is a function that takes three arguments: a type T, a predicate p : T → 𝔹, and a proof % that we can decide whether p(t) = false for some t ∈ T. The kernel_inclusion_implies_fold theorem is used to create the witness algebra (A, g). The by far longest expression in the extract (‘λb.case b of …’) is just a proof that we can decide whether some element in L_{T} (𝔹) = 1 + (T × 𝔹) is in the image of L_{T} (and(map(p; ·))).

We can further unfold the extracts of the kernel_inclusion_implies_fold lemma and of other lemmatas that were used in its proof. Eventually, we obtain the actual function g with and(map(p; ·)) = foldg. This function (with a few simplifications made by hand) is shown in Figure 6.24. It is a triple with its first and second component being its domain and codomain, respectively. The if-then-else statement is used to determine whether b ∈ 1+(T ×𝔹) is in the image of L_{T} (and(map(p; ·))). Three cases need to be differentiated: b = inl ·, b = inr (y1, true), and b = inr (y1, false). The latter can only occur if p(t) = false for some t ∈ T; whether such a t exists is determined by the value of %. If b is in the image of L_{T} (and(map(p; ·))), the then part is used to apply and(map(p; ·))·(nil +cons) to an element z ∈ 1+(T ×List(T)) with (L_{T} (and(map(p; ·))))(z) = b. Otherwise, true is returned in the else part. Using and(map(p; [])) = true and and(map(p; t :: [])) = false, we could simplify the then part even further.

6We also need to be able to decide whether 𝔹 is empty. Since true ∈ 𝔹, 𝔹 is not empty.

 λT,p,%.
 ext{kernel_inclusion_implies_fold}{i:l}
 ListF{i}(T)
 InitialAlgebra(ListF(T))

𝔹

 <T List, 𝔹, λL.∧_{b}(map(p;L))>
 (inl tt )
 (λb.case b
     of inl(x) => inl <inl · , Ax>
     | inr(y) => let <y1,y2> = y
     in
     case y2
     of inl(x) => inl <inr <y1, []> , Ax>
     | inr(y) => case %
     of inl(%2) => let <t,%3> = %2
     in
     inl <inr <y1, t::[]> , Ax>
     | inr(%3) => inr (λ%.let <a,%4> = %
     in
     case a
     of inl(x) => Ax
     | inr(y) => let <y2,y3> = y
     in
     any (rec-case(y3)
     of [] => λ%.Ax
     | u::v => %.λ%4.any (%3 <u, Ax>) Ax))
 )
 (λx.Ax)

Figure 6.23: Simplified Extract of Theorem list_and_2_map_is_fold

6.5 Two Counterexamples

We claimed that the proof of Theorem 6.1.1 given in [GHA01] is not constructive, and that we need essentially two additional assumptions to turn it into a constructive proof: Firstly, that we can decide whether the set A is empty, and secondly, that we can decide whether an element in F A is in the image of F h.

However, decidability of the image of F h is not a necessary condition for a constructive function h to be a catamorphism. We prove this by giving a function with a nondecidable image that can still be written as a fold. We then prove that ker(F h) ⊆ ker(h·in) is not a sufficient constructive condition for a function to be a catamorphism

 < (ListF{i}(T)_O 𝔹)
 , 𝔹
 , λb.if case b
     of inl(x) => tt
     | inr(y) => let <y1,y2> = y
     in
     case y2
     of inl(x) => tt
     | inr(y) => case %
     of inl(%2) => tt
     | inr(%3) => ff
 then (<T List, 𝔹, λL.∧_{b}(map(p;L))> ListF{i}(T)_dom_op
     InitialAlgebra(ListF(T))_arr).2.2
     (case b
     of inl(x) => <inl ·, Ax>
     | inr(y) => let <y1,y2> = y
     in
     case y2
     of inl(x) => <inr <y1, []> , Ax>
     | inr(y) => case %
     of inl(%2) => let <t,%3> = %2
     in
     <inr <y1, t::[]>, Ax>
     | inr(%3) => any Ax.1)
 else tt
 fi >

Figure 6.24: A Function g with and(map(p; ·)) = foldg

by giving a computable function h that satisfies this condition, and a proof that no function g with h = foldg is computable.^{7}

Recall the functor L_{X} defined in Chapter 5 which has (List(X), nil + cons) as an initial algebra. Let TM denote the set of all Turing machines, and let H denote the set of all Turing machines that halt after a finite number of steps (when applied to the empty input). Clearly H ⊆ TM , and H is not decidable [Tur36]. Consider the embedding h_{0} : List(H) ↪ List(TM ). Now img L_{H}(h_{0}) = 1 + H × List(H) is not decidable in 1 + H × List(TM ) = L_{H}(List(TM )). Therefore the construction given in the proof of Theorem 6.3.1 fails. However, we can still find a function g : 1 + H × List(TM ) → List(TM ) such that h_{0} · in = g · L_{H}(h_{0}): Simply map (·) to

7Of course a (possibly non-computable) function g with h = foldg must exist by Theorem 6.1.1.

\xymatrix{1 + (H × List(H)) \ar[d]_{nil+cons} \ar@{^{(}->}[r]^{L_{H}(h_{0})} & 1 + (H × List(TM )) \ar[d]^{g=nil+cons} \\ List(H) \ar@{^{(}->}[r]_{h_{0}} & List(TM )}

Figure 6.25: A Catamorphism h where img(F h) is not Decidable

[], and a pair (M, L) (where M is a Turing machine in H, and L is a list of Turing machines) to M :: L. That is, g = nil + cons on 1 + H × List(TM ) (see Figure 6.25). Now h_{0} ·in = g ·L_{H}(h_{0}) is immediate. Therefore h_{0} = foldg by the universal property of fold, so h_{0} is a catamorphism.

Our second counterexample, which proves that not every function h of the appropriate type with ker(F h) ⊆ ker(h · in) is a catamorphism when we restrict ourselves to constructive (i.e. computable) functions, needs to be more elaborate. Consider the functor L_{ℕ} : SET → SET with its initial algebra (List(ℕ), nil + cons). Assume TM = {M_{1}, M_{2}, M_{3}, …}.^{8} Define a function h_{1} : List(ℕ) → ℕ + TM as follows: If L ∈ List(ℕ) is of even length, then h(L) is defined as the sum of the elements in L. That is, h(L) = ∑ L in this case, where ∑ : List(ℕ) → ℕ is defined by the two equations

∑[] = 0,
∑(n :: L) = n + ∑ L.

If L is of odd length, then L has at least one element, so say L = n :: L′. In this case, let h_{1}(L) = h_{1}(n :: L′) be the (n + 1). Turing machine in TM that halts after exactly ∑ L′ steps (when applied to the empty input). We can compute h_{1}(n :: L′) as follows: Simulate M_{1} for (at most) ∑ L′ steps to check whether it halts after exactly ∑ L′ steps. Then simulate M_{2} for (at most) ∑ L′ steps, then M_{3}, and so on, until we have found the (n + 1). Turing machine in TM that halts after exactly ∑ L′ steps. This algorithm is guaranteed to terminate since for every number of steps, there exist infinitely many Turing machines in TM that terminate after exactly that many steps. Hence h_{1} is computable.

The function L_{ℕ}(h_{1}) : 1 + (ℕ × List(ℕ)) → 1 + (ℕ × (ℕ + TM )) maps a pair (n, L), where n is a natural number and L is a list of natural numbers, to the pair

8The set of all Turing machines is countable, and we can enumerate this set in some (computable)

way—e.g. based on the length of the representation of Turing machines.

\xymatrix{1 + (ℕ × List(ℕ)) \ar[d]_{nil+cons} \ar[r]^{L_{ℕ}(h_{1})} & 1 + (ℕ × (ℕ + TM )) \ar[d]^{g} \\ List(ℕ) \ar[r]_{h_{1}} & ℕ + TM}

Figure 6.26: A Function h with ker(F h) ⊆ ker(h · in) that is not a Catamorphism

(n, h_{1}(L)) ∈ ℕ × (ℕ + TM ). To prove ker(L_{ℕ}(h_{1})) ⊆ ker(h_{1} · in), we have to verify that h_{1}(L) = h_{1}(M) implies h_{1}(n :: L) = h_{1}(n :: M) for all L, M ∈ List(ℕ) and n ∈ ℕ. So assume h_{1}(L) = h_{1}(M). If L is of even length, then h_{1}(L) = ∑ L. Hence M is also of even length and ∑ L = h_{1}(L) = h_{1}(M) = ∑ M. Since h_{1}(n :: L) is the (n + 1). Turing machine in TM that halts after exactly ∑ L steps, and h_{1}(n :: M) is the (n + 1). Turing machine in TM that halts after exactly ∑ M steps, we have h_{1}(n :: L) = h_{1}(n :: M). If L is of odd length, then L = l :: L′ for some l ∈ ℕ and L′ ∈ List(ℕ). In this case h_{1}(L) is the (l + 1). Turing machine that halts after exactly ∑ L′ steps. So M is also of odd length, say M = m :: M′ for some m ∈ ℕ and M′ ∈ List(ℕ), and h_{1}(M) is the (m + 1). Turing machine that halts after exactly ∑ M′ steps. Since h_{1}(L) = h_{1}(M), we have ∑ L′ = ∑ M′, and M_{i} ≠ M_{j} for i ≠ j implies l = m. Therefore h_{1}(n :: L) = ∑(n :: L) = n + ∑ L = n + l + ∑ L′ = n + m + ∑ M′ = n + ∑ M = ∑(n :: M) = h_{1}(n :: M).

Figure 6.26 shows the sets and functions involved in this counterexample. Since a Turing machine M ∈ TM halts if and only if it is the (n + 1). Turing machine to halt after s steps for some n, s ∈ ℕ (we assume 0 ∈ ℕ), we have img(h_{1}) = ℕ + H and img(L_{ℕ}(h_{1})) = 1 + (ℕ × (ℕ + H)).

Now assume h_{1} = foldg for some function g : 1 + (ℕ × (ℕ + TM )) → ℕ + TM . We use reduction to the halting problem to prove that g is not computable. Assume g is computable. Consider any pair (k, M) ∈ ℕ × H, and assume M is the (n + 1). Turing machine to halt after s steps. Since h_{1} · in = g · L_{ℕ}(h_{1}), we have g(k, M) = k + n + s. Therefore g(k, M) ≥ s, so any Turing machine M ∈ H halts after at most g(0, M) steps. Thus it is enough to run a Turing machine T ∈ TM for g(0, T) steps to find out if T halts (on the empty input); if it does not halt until then, it will never halt. This gives us a decision procedure for the halting problem—a contradiction, therefore g is not computable.

64 CHAPTER 6. WHEN IS A FUNCTION A CATAMORPHISM?

Bird’s Fusion Transformation

Many algorithms can be specified as the composition of a function that constructs an intermediate data structure from the given input, and another function that traverses the intermediate data structure to extract the requested information. A simple example was given in Chapter 1.

Bird’s fusion theorem [Bir95] proves that if the first function is an anamorphism and the second function is a catamorphism, these two functions can be combined into a single function, thereby eliminating the intermediate data structure constructed by the anamorphism.

This chapter presents a formalization of the fusion theorem for the special case where the underlying data structure is the type of binary trees. The formalization presented here is partially based on a formalization of Bird’s fusion transformation in PVS by N. Shankar [Sha96].

7.1 Binary Trees

A binary tree (over some type T) is a type of data structure in which each element is attached to zero or two elements directly beneath it. We use the following inductive definition after [CLRS01].

Definition 7.1.1 (Binary Trees). Suppose T is a type.

• A leaf is a binary tree over T.

• If t ∈ T and B_{1}, B_{2} are binary trees over T, then node(t, B_{1}, B_{2}) is a binary tree over T.

BinTree(T) is the type of all binary trees over T.

According to this definition, leafs do not carry information (i.e. elements from T). All information is stored in the nodes, and in the structure of the tree itself.

 * ABS binary_tree
 BinTree(T) == rec(t.Unit + T × t × t)

Figure 7.1: Abstraction binary_tree

The Nuprl abstraction defining binary trees is shown in Figure 7.1. Due to the use of the disjoint product type +, a binary tree in Nuprl now is equal to either inl · or inr < t, B_{1}, B_{2} >, where t ∈ T and B_{1}, B_{2} are binary trees. We define leaf as an abbreviation for inl ·, and node(t,B_1,B_2) as an abbreviation for inr <t, B_{1}, B_{2} >, as shown in Figure 7.2. The fact that leaf and node(t,B_1,B_2) are binary trees is captured by the two well-formedness theorems shown in Figure 7.3. The theorems are proved in two steps each.

 * ABS leaf
 leaf == inl ·
 * ABS node
 node(t,b1,b2) == inr <t, b1, b2>

Figure 7.2: Abstractions leaf and node

 * THM leaf_wf
 ∀T:𝕌.  leaf ∈ BinTree(T)
 * THM node_wf
 ∀T:𝕌. ∀t:T. ∀B1,B2:BinTree(T). node(t,B1,B2) ∈ BinTree(T)

Figure 7.3: Well-formedness theorems for leaf and node

Example 7.1.2. node(0, leaf , node(1, leaf , leaf )) represents a binary tree with value 0 at its root node, an empty left branch, and a single node with value 1 in its right branch. Figure 7.4 shows a graphical representation of this tree.

See Figure 7.5 for a theorem stating that node(0, leaf , node(1, leaf , leaf )) is in fact a binary tree (over ℕ). The theorem is proved in a single step by Nuprl’s Auto tactic.

\xymatrix{ & 0 \ar[dl] \ar[dr] \\ leaf &  & 1 \ar[dl] \ar[dr] \\  & leaf &  & leaf}

Figure 7.4: Example: A binary tree

 * THM binary_tree_example
 node(0; leaf; node(1; leaf; leaf)) ∈ BinTree(ℕ)
                Figure 7.5: Theorem binary_tree_example

7.2 The reduce Operator

Suppose T and R are types, c ∈ R and g : T × R × R → R. We want to define a function f : BinTree(T) → R by the following recursion over binary trees:

f(leaf ) = c
f(node(t, B_{1}, B_{2})) = g(t, f(B_{1}), f(B_{2}))

The reduce operator is defined such that f = reduce(c; g). Note that every function f that can be written as reduce(c; g) for some c and g is a catamorphism on binary trees.

Definition 7.2.1 (reduce). Suppose T and R are types, c ∈ R and g : T ×R ×R → R. Define reduce(c; g) : BinTree(T) → R recursively by

reduce(c; g)(B) = \{ \begin{matrix}c & if B = leaf \\ g(t, reduce(c; g)(B_{1}), reduce(c; g)(B_{2})) & if B = node(t, B_{1}, B_{2}) \end{matrix}

for all B ∈ BinTree(T).

The corresponding abstraction treereduce is shown in Figure 7.6. We use a curried function g : T → R → R → R in the treereduce abstraction instead of a function with domain T × R × R and codomain R. Avoiding the cartesian product (and consequently, tuples as function arguments) simplifies the Nuprl notation.

Since reduce is defined recursively, we have to verify that this recursion always terminates to make sure that reduce(c; g) is well-defined, i.e. that reduce(c; g)(B) is in R for all binary trees B.

 * ABS treereduce
 reduce(c;g)(B) ==
 (letrec recfun(B) = case B
 of inl(x) => c
 | inr(y) => let t,B1,B2 = y in g t (recfun B1) (recfun B2) )
 B

Figure 7.6: Abstraction treereduce

Lemma 7.2.2. Suppose T and R are types, c ∈ R and g : T × R × R → R. Then

reduce(c; g)(B) ∈ R

for all B ∈ BinTree(T).

Proof. Let B ∈ BinTree(T). We use structural induction on B.

Base case (B = leaf ): reduce(c; g)(B) = c ∈ R.

Inductive step (B = node(t, B_{1}, B_{2})): By the induction hypothesis, reduce(c; g)(B_{1}) ∈ R and reduce(c; g)(B_{2}) ∈ R. Therefore

reduce(c; g)(B) = g(t, reduce(c; g)(B_{1}), reduce(c; g)(B_{2})) ∈ R.

The proof of the formal theorem treereduce_wf, which is shown in Figure 7.7, proceeds along the same lines. The RecElimination tactic is used for structural induction on B. The base case is then proved by the Auto tactic after we unfold the definition of treereduce. The induction hypothesis is used to prove the inductive step. Altogether the proof is about nine steps long.

 * THM treereduce_wf
 ∀T,R:𝕌. ∀c:R. ∀g:T → R → R → R. ∀B:BinTree(T).
 reduce(c;g)(B) ∈ R

Figure 7.7: Theorem treereduce_wf

Example 7.2.3. The height of a binary tree (over an arbitrary type T) can be defined recursively. The height of a leaf is 0, and the height of a node is one more than the maximum of the heights of the node’s left and right subtree:

height(leaf ) = 0,
height(node(t, B_{1}, B_{2})) = 1 + max(height(B_{1}), height(B_{2})).

 * ABS treeheight
 |B| ==
 (letrec recfun(B) = case B
 of inl(x) => 0
 | inr(y) => let t,B1,B2 = y in 1 + imax(recfun B1;recfun B2) )
 B

Figure 7.8: Abstraction treeheight

See Figure 7.8 for a formal definition.

Clearly height(B) ∈ ℕ for all binary trees B; this fact is proved by the theorem treeheight_wf shown in Figure 7.9. Again the RecElimination tactic is used for structural induction on B in the proof of this theorem. The formal proof is about 27 steps long, mainly because we have to overcome a few technical difficulties caused by the use of ℕ and ℤ.

 * THM treeheight_wf
 ∀T:𝕌. ∀B:BinTree(T). |B| ∈ ℕ

Figure 7.9: Theorem treeheight_wf

Alternatively, height can be defined in terms of reduce. Define g : T × ℕ × ℕ → ℕ by g(t, m, n) = 1 + max(m, n). Then height(B) = reduce(0; g)(B) for all binary trees B, as shown in Figure 7.10. The proof of this theorem is about ten steps long and uses both the RecElimination tactic and the treeheight_wf lemma, as well as a few other lemmata.

 * THM treereduce_example
 ∀T:𝕌. ∀B:BinTree(T). |B| = reduce(0;λt,m,n.1 + imax(m;n))(B)
                Figure 7.10: Theorem treereduce_example

7.3 The unfold Operator

The reduce operator extracts some information from a binary tree. It provides a general pattern to define catamorphisms on binary trees. Now suppose S is a type, and we want to define an operator unfold that constructs a binary tree from some input x ∈ S as follows. First, a given predicate p is applied to x. If p(x) is true, we apply a function f to x that computes a node value a and two new input values y and z. unfold is then recursively applied to y and z to compute the left and right subtree of the node. If p(x) is false, unfold simply returns leaf .

However, there is a problem with this ‘definition’. If y and z are allowed to be arbitrary input values, this recursion is not guaranteed to terminate: Assume p(x) is true for every input x, and consider the function f : S → S × S × S, defined by f(x) = (x, x, x). Then

unfold(p; f)(x) = node(x, unfold(p; f)(x), unfold(p; f)(x))
= node(x,
node(x, unfold(p; f)(x), unfold(p; f)(x)),
node(x, unfold(p; f)(x), unfold(p; f)(x)))
= …

To guarantee that the recursion terminates, we require y and z to be ‘smaller’ than x, where the ‘size’ of an input is just a natural number.^{1}

Definition 7.3.1 (Smaller). Suppose S is a type, size : S → ℕ, and x ∈ S. Then we define

Smaller(S, size, x) = {y ∈ S | size(y) < size(x)}

to be the type of all elements in S with a size less than the size of x.

The formal definition of Smaller is shown in Figure 7.11. The well-formedness theorem smaller_wf proves that Smaller(S,size,x) is a type if S is a type, size : S → ℕ, and x ∈ S. It is proved in a single step by the Auto tactic.

 * ABS smaller
 Smaller(S,size,x) == {y:S| size y < size x}

Figure 7.11: Abstraction Smaller

Now we are ready to define the type of functions that we allow as a parameter to unfold. Note that to compute unfold(p; f)(x), we only need to evaluate f(x) when p(x) is true. Therefore the domain of f does not need to be S, but it can be restricted to the subtype {x ∈ S | p(x) = true}.

1As pointed out by N. Shankar [Sha96], any well-founded ordering could be used here instead of the less-than relation on natural numbers.

Definition 7.3.2 (WellFnd). Suppose S and T are types, p : S → 𝔹, and size : S → ℕ. Then we define

WellFnd(S, p, size, T) =
{f : {x ∈ S | p(x) = true} → T × S × S |
∀x ∈ {x ∈ S | p(x) = true} :
f(x) ∈ T × Smaller(S, size, x) × Smaller(S, size, x)}.

In Nuprl, the dependent function type can be used to define WellFnd more elegantly: The codomain does not have to be a single type, but it can depend on the function argument x. Thus given x, we can require f(x) to be in T × Smaller(S, size, x) × Smaller(S, size, x). Figure 7.12 shows the corresponding abstraction treewellfnd.

 * ABS treewellfnd
 WellFnd(S,p,size,T) ==
 x:{x:S| p[x] = tt} → (T × Smaller(S,size,x) × Smaller(S,size,x))

Figure 7.12: Abstraction treewellfnd

The well-formedness theorem for treewellfnd simply states that this is a type if S and T are types, p : S → 𝔹, and size : S → ℕ. It is proved in a single step by Nuprl’s Auto tactic. Using the type WellFnd of ‘well-founded’ functions, we can now precisely define unfold.

Definition 7.3.3 (unfold). Suppose S and T are types, p : S → 𝔹, size : S → ℕ, and f ∈ WellFnd(S, p, size, T). Define unfold(p; f) : S → BinTree(T) recursively by

unfold(p; f)(x) = \{ \begin{matrix}node(a, unfold(p; f)(y), unfold(p; f)(z)) & if p(x) is true \\ leaf & if p(x) is false \end{matrix}

for all x ∈ S, where f(x) = (a, y, z).

See Figure 7.13 for the definition of treeunfold in Nuprl.

The restrictions imposed on f allow us to prove that unfold is well-defined, i.e. that the recursion always terminates.

Lemma 7.3.4. Suppose S and T are types, p : S → 𝔹, size : S → ℕ, and f ∈ WellFnd(S, p, size, T). Then

unfold(p; f)(x) ∈ BinTree(T)

for all x ∈ S.

 * ABS treeunfold
 unfold(p;f)(x) ==
 (letrec recfun(x) = if p[x]
 then let a,y,z = (f x) in node(a; (recfun y); (recfun z))
 else leaf
 fi )
 x

Figure 7.13: Abstraction treeunfold

Proof. Let x ∈ S. We show unfold(p; f)(x) ∈ BinTree(T) by complete induction on size(x). Assume unfold(p; f)(y) ∈ BinTree(T) for all y ∈ S with size(y) < size(x).

Case 1: Assume p(x) is false. Then unfold(p; f)(x) = leaf ∈ BinTree(T).

Case 2: Assume p(x) is true. Let f(x) = (a, y, z). Then y, z ∈ Smaller(S, size, x) since f ∈ WellFnd(S, p, size, T). Hence size(y) < size(x) and size(z) < size(x). Thus unfold(p; f)(y) ∈ BinTree(T) and unfold(p; f)(z) ∈ BinTree(T) by the induction hypothesis. Therefore

unfold(p; f)(x) = node(a, unfold(p; f)(y), unfold(p; f)(z)) ∈ BinTree(T).

In Nuprl we state this lemma as a well-formedness theorem for treeunfold. This well-formedness theorem is shown in Figure 7.14. The formal proof uses Nuprl’s InvImageInd tactic in combination with the CompNatInd tactic for complete induction on the size of x. The IfThenElse tactic is then used for the case split on p(x). The proof is about 15 steps long.

 * THM treeunfold_wf
 ∀S:𝕌. ∀p:S → 𝔹. ∀size:S → ℕ. ∀T:𝕌. ∀f:WellFnd(S,p,size,T).
 ∀x:S. unfold(p;f)(x) ∈ BinTree(T)

Figure 7.14: Theorem treeunfold_wf

The unfold operator, just like reduce, can be used to specify a number of algorithms. We give a simple example below, and a more elaborate example in the following chapter.

Example 7.3.5. We say a binary tree B is balanced if and only if every leaf in B has the same height. Consider a function bal : ℕ → BinTree(ℕ) that, given a natural number n, creates a balanced binary tree of height n in which every node is labelled leaf_{(a) bal(0)}

\xymatrix{ &  &  & 2 \ar[dll] \ar[drr] \\  & 1 \ar[dl] \ar[dr] &  &  &  & 1 \ar[dl] \ar[dr] \\ leaf &  & leaf &  & leaf &  & leaf}

(b) bal(2)

Figure 7.15: Example: bal

with its height (i.e. the root node is labelled with n, the two nodes directly beneath it are labelled with n − 1, and so on). See Figure 7.15 for two examples.

More precisely, let bal : ℕ → BinTree(ℕ) be defined inductively by

bal(0) = leaf ,
bal(n + 1) = node(n + 1, f(n), f(n)).

The Nuprl abstraction defining bal is shown in Figure 7.16. The well-formedness

theorem create_balanced_wf proves that create_balanced(n) is in BinTree(ℕ) for

every n ∈ ℕ. We use the NatInd tactic in the proof of create_balanced_wf for mathematical induction on n. The proof is about six steps long.

 * ABS create_balanced
 create_balanced(n) ==
 (letrec recfun(n) = if (n =_{z} 0)
 then leaf
 else node(n; (recfun (n - 1)); (recfun (n - 1)))
 fi )
 n

Figure 7.16: Abstraction create_balanced

Now define p : ℕ → 𝔹 by p(n) ⟺ (n ≠ 0), and define g : ℕ \ {0} → ℕ × ℕ × ℕ by g(n) = (n, n − 1, n − 1). Then bal(n) = unfold(p; g)(n) for all n ∈ ℕ, as proved by the theorem treeunfold_example shown in Figure 7.17. The proof uses Nuprl’s NatInd tactic for mathematical induction on n. It is about 92 steps long, mainly because several well-formedness goals need to be verified.

 * THM treeunfold_example
 ∀n:ℕ.  create_balanced(n) =
 unfold((λn.¬_{b}(n =_{z} 0)); (λn.<n, n - 1, n - 1>); n)
                Figure 7.17: Theorem treeunfold_example

7.4 The fun Operator

The composition of unfold and reduce can be used to specify a large number of algorithms, e.g. the Quicksort algorithm (see Chapter 8 for details). However, unfold first constructs a binary tree, and reduce then consumes the tree. Bird’s fusion transformation allows us to replace reduce · unfold with a single operator fun (defined below) that does not construct an intermediate tree. This is an instance of deforestation [Dav87, Wad88, GJS93], a program optimization technique that fuses adjacent phases to eliminate the intermediate data structures.

Definition 7.4.1 (fun). Suppose S, T, R are types, p : S → 𝔹, size : S → ℕ, and f ∈ WellFnd(S, p, size, T). Furthermore, suppose c ∈ R and g : T × R × R → R. Define fun(p; f; c; g) : S → R by

fun(p; f; c; g)(x) = \{ \begin{matrix}g(a, fun(p; f; c; g)(y), fun(p; f; c; g)(z)) & if p(x) is true \\ c & if p(x) is false \end{matrix}

for all x ∈ S, where f(x) = (a, y, z).

Figure 7.18 shows the corresponding Nuprl abstraction treefun. Again we avoid tuples as function arguments by using a curried function g.

 * ABS treefun
 fun(p;f;c;g)(x) ==
 (letrec recfun(x) = if p[x]
 then let a,y,z = (f x) in g a (recfun y) (recfun z)
 else c
 fi )
 x

Figure 7.18: Abstraction treefun

The operator fun, like reduce and unfold before, is defined recursively. Therefore we need to verify that it is well-defined, i.e. that the recursion terminates for every input x ∈ S.

Lemma 7.4.2. Suppose S, T, R are types, p : S → 𝔹, size : S → ℕ, and f ∈ WellFnd(S, p, size, T). Furthermore, suppose c ∈ R and g : T × R × R → R. Then

fun(p; f; c; g)(x) ∈ R

for all x ∈ S.

Proof. Let x ∈ S. We show fun(p; f; c; g)(x) ∈ R by complete induction on size(x). Assume fun(p; f; c; g)(y) ∈ R for all y ∈ S with size(y) < size(x).

Case 1: Assume p(x) is false. Then fun(p; f; c; g)(x) = c ∈ R.

Case 2: Assume p(x) is true. Let f(x) = (a, y, z). Then y, z ∈ Smaller(S, size, x) since f ∈ WellFnd(S, p, size, T). Hence size(y) < size(x) and size(z) < size(x). Thus fun(p; f; c; g)(y) ∈ R and fun(p; f; c; g)(z) ∈ R by the induction hypothesis. Therefore

fun(p; f; c; g)(x) = g(a, fun(p; f; c; g)(y), fun(p; f; c; g)(z)) ∈ R.

The formal well-formedness theorem is shown in Figure 7.19. Its proof is about eleven steps long and uses the InvImageInd tactic in combination with CompNatInd for complete induction on the size of x.

 * THM treefun_wf
 ∀S:𝕌. ∀p:S → 𝔹. ∀size:S → ℕ. ∀T:𝕌. ∀f:WellFnd(S,p,size,T).
 ∀R:𝕌. ∀c:R. ∀g:T → R → R → R. ∀x:S.
 fun(p;f;c;g)(x) ∈ R

Figure 7.19: Theorem treefun_wf

7.5 Bird’s Fusion Theorem for Binary Trees

As mentioned before, we want to replace reduce · unfold with fun to eliminate the intermediate tree. In this section we prove that reduce ·unfold and fun are equivalent, in the sense that they compute the same function.

Theorem 7.5.1 (Bird’s Fusion Theorem for Binary Trees). Suppose S, T, R are types, p : S → 𝔹, size : S → ℕ, and f ∈ WellFnd(S, p, size, T). Furthermore, suppose c ∈ R and g : T × R × R → R. Then

(reduce(c; g) · unfold(p; f))(x) = fun(p; f; c; g)(x)

for all x ∈ S.

Proof. Let x ∈ S. We show (reduce(c; g)·unfold(p; f))(x) = fun(p; f; c; g)(x) by complete induction on size(x). Assume (reduce(c; g) · unfold(p; f))(y) = fun(p; f; c; g)(y) for all y ∈ S with size(y) < size(x).

Case 1: Assume p(x) is false. Then

(reduce(c; g) · unfold(p; f))(x) = reduce(c; g)(unfold(p; f)(x))
= reduce(c; g)(leaf )
= c
= fun(p; f; c; g)(x).

Case 2: Assume p(x) is true. Let f(x) = (a, y, z). Then y, z ∈ Smaller(S, size, x) since f ∈ WellFnd(S, p, size, T). Hence size(y) < size(x) and size(z) < size(x). Thus (reduce(c; g) · unfold(p; f))(y) = fun(p; f; c; g)(y) and (reduce(c; g) · unfold(p; f))(z) = fun(p; f; c; g)(z) by the induction hypothesis. Therefore

(reduce(c; g) · unfold(p; f))(x) = reduce(c; g)(unfold(p; f)(x)) = reduce(c; g)(node(a, unfold(p; f)(y), unfold(p; f)(z))) = g(a, reduce(c; g)(unfold(p; f)(y)), reduce(c; g)(unfold(p; f)(z))) = g(a, (reduce(c; g) · unfold(p; f))(y), (reduce(c; g) · unfold(p; f))(z)) = g(a, fun(p; f; c; g)(y), fun(p; f; c; g)(z)) = fun(p; f; c; g)(x)

as required.

Figure 7.20 shows the formal fusion theorem. The proof uses the usual combination of the tactics InvImageInd and CompNatInd for complete induction on the size of x; it is about 27 steps long.

 * THM fusion
 ∀S:𝕌. ∀p:S → 𝔹. ∀size:S → ℕ. ∀T:𝕌. ∀f:WellFnd(S,p,size,T).
 ∀Range:𝕌. ∀c:Range. ∀g:T → Range → Range → Range. ∀x:S.
 reduce(c;g)(unfold(p;f)(x)) = fun(p;f;c;g)(x)

Figure 7.20: Theorem fusion

In the following chapter we apply the fusion transformation to the Quicksort algorithm.

Example: Quicksort

The Quicksort algorithm was first published by C.A.R. Hoare [Hoa61] in 1961. It is “one of the fastest, the best known, the most generalized, … and the most widely used algorithms for sorting an array of numbers” [ES95]. Both R. Bird [Bir95] and N. Shankar [Sha96] chose it as an example to apply the fusion transformation to.

Despite its speed, Quicksort is a relatively simple algorithm. It can be described as follows.

1. If the list is empty, there is nothing to do.

2. Otherwise pick an element from the list to be the ‘partition element’.

3. Divide the other elements into those less than or equal to the partition element, and those greater than the partition element.

4. Arrange the elements in the list such that the order is the elements below the partition element, the partition element itself, and the elements above the partition element.

5. Recursively invoke Quicksort on the smaller elements.

6. Recursively invoke Quicksort on the larger elements.

As we can see from this description, Quicksort can be used for any type on which an order relation ≤ is defined.^{1}

1Note that even when ≤ is not an order relation, we can still formally apply Quicksort. In fact, we will prove that Quicksort returns a permutation of its input when ≤ is an arbitrary relation on the type of the list elements. However, we will need to put certain constraints on ≤ to prove that the list returned by Quicksort is ordered.

8.1 Quicksort in Nuprl

Figure 8.1 shows an implementation of the Quicksort algorithm in Nuprl. We define quicksort as a recursive function that takes a relation ≤ and a list L as arguments and returns a list (Nuprl’s built-in data type list is used here). If L is the empty list, denoted as [], then the empty list is returned. Otherwise the head of L is picked as the partition element. Then quicksort is invoked recursively on a list of all elements in the tail of L that are smaller than or equal to (‘below’) the head of L, and on a list of all elements in the tail of L that are larger than (‘above’) the head of L. Both lists are generated by the filter function: filter(p;L) returns a list with those elements in L that satisfy the predicate p. Finally append (@) and cons (::) are used to concatenate the two lists and the partition element in the proper order.

 * ABS quicksort
 quicksort(≤,L) ==
 (letrec recfun(L) = case L of
 [] => []
 a::y => recfun filter((λb.b below(≤) a);y)
 @ (a::(recfun filter((λb.b above(≤) a);y)))
 esac )
 L

Figure 8.1: Abstraction quicksort

The quicksort function is defined recursively. We prove that it is well-defined by complete induction on the length of the input list L.

Lemma 8.1.1. Suppose T is a type and ≤ : T × T → 𝔹. Then

quicksort(≤, L) ∈ List(T)

for all L ∈ List(T).

We first prove another lemma, namely that the list returned by filter(p; L) is at most as long as L.

Lemma 8.1.2. Suppose T is a type, and f : T → 𝔹. Then

|filter(f, L)| ≤ |L|

for all L ∈ List(T).

The filter abstraction is part of the LIST_3 library, as is the abstraction defining list_length.^{2} Here we define filter as follows.

Definition 8.1.3 (filter). Suppose T is a type, f : T → 𝔹, and L ∈ List(T). Define filter(f; L) ∈ List(T) recursively by

filter(f; L) = \{ \begin{matrix}[] & if L = [] \\ filter(f; t) & if L = h :: t and f(h) is false \\ h :: filter(f; t) & if L = h :: t and f(h) is true \end{matrix} .

With this definition we can easily prove Lemma 8.1.2.

Proof. The proof is by structural induction on L.

Base case (L = []): |filter(f; L)| = |[]| = |L|.

Inductive step (L = h :: t): By the induction hypothesis, |filter(f; t)| ≤ |t|. If f(h) = true,

|filter(f; L)| = |h :: filter(f; t)| = 1 + |filter(f; t)| ≤ 1 + |t| = |L|.

If f(h) = false,

|filter(f; L)| = |filter(f; t)| ≤ |t| = |L| − 1 < |L|.

Figure 8.2 shows the corresponding Nuprl theorem list_length_filter. The proof of the formal theorem uses the ListInd tactic for structural induction on L, and the IfThenElseCases tactic for the case split on f(h). The proof is about six steps long; most of the work is done by Nuprl’s Auto tactic.

 * THM list_length_filter
 ∀T:𝕌. ∀f:T → 𝔹. ∀L:T List.  |·| filter(f;L) ≤ |·| L
                 Figure 8.2: Theorem list_length_filter

Given a type T and a relation ≤ : T × T → 𝔹, we define b below(≤) a as b ≤ a, and b above(≤) a as ¬(b below(≤) a) for a, b ∈ T. The corresponding Nuprl abstractions below and above are shown in Figure 8.3.

The well-formedness theorems below_wf and above_wf prove that b below(≤) a and b above(≤) a are in 𝔹 if T is a type, ≤ : T × T → 𝔹, and a, b ∈ T. They are proved in a single step each. Now we are ready to prove Lemma 8.1.1.

2The abstraction defining length in Nuprl, however, is part of the LIST_1 library.

 * ABS below
 b below(≤) a == b ≤ a
 * ABS above
 b above(≤) a == ¬_{b}b below(≤) a

Figure 8.3: Abstractions below and above

Proof. By complete induction on the length of L. Assume quicksort(≤, M) ∈ List(T) for all M ∈ List(T) with |M| < |L|.

Case 1: Assume L = []. Then quicksort(≤, L) = [] ∈ List(T).

Case 2: Assume L = h :: t, where h ∈ T and t ∈ List(T). By Lemma 8.1.2, |filter(b below(≤) h; t)| ≤ |t| < |L| and |filter(b above(≤) h; t)| ≤ |t| < |L|. Thus

quicksort(≤, filter(b below(≤) h; t)) ∈ List(T)

and quicksort(≤, filter(b above(≤) h; t)) ∈ List(T)

by the induction hypothesis. Therefore

quicksort(≤, L)

= quicksort(≤, filter(b below(≤) h; t))

@ (h :: quicksort(≤, filter(b above(≤) h; t)))

∈ List(T).

The Nuprl theorem quicksort_wf is shown in Figure 8.4. Note the use of a curried function ≤ : T → T → 𝔹 to avoid tuples as function arguments. The formal proof uses the ListLenInd tactic for complete induction on the length of the list L. Then Cases is used to do a case split on L = [] and L = h :: t. The case L = [] is proved by an invocation of the ListInd tactic, because even though we know that L is equal to [], we cannot substitute [] for L in the proof goal quicksort(≤, L) ∈ List(T) without creating unprovable well-formedness goals. For the same reason, we cannot simply substitute h :: t for L in the other case. We circumvent this problem by eliminating L from all hypotheses first (by substituting h :: t for L, or by moving them to the conclusion), and by decomposing the declaration of L as a list then. With 26 steps altogether, the proof is relatively short, but surprisingly tricky.

 * THM quicksort_wf
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀L:T List.  quicksort(≤,L) ∈ T List

Figure 8.4: Theorem quicksort_wf

8.2 Quicksort by Fusion

If we compare our implementation of Quicksort (Figure 8.1) to the treefun operator (Figure 7.18) defined in the previous chapter, it is almost obvious that Quicksort can be written as treefun, and hence—by the fusion theorem—that Quicksort is equal to the composition of an anamorphism and a catamorphism. In this section we make a few necessary definitions before we finally prove this equality.

Using a binary tree, we can split Quicksort into two phases. The first phase constructs an ordered binary tree that contains the same elements as the input list L as follows: The partition element becomes the tree’s root value. The left subtree and the right subtree are recursively constructed from a list of those elements in the tail of L that are below the partition element, and from a list of those elements in L that are above the partition element. The empty list [] simply becomes a leaf.

The second phase flattens the ordered binary tree into an ordered list by an in-order search: First the left subtree is flattened, then the root value is inserted at the end of the list, then the right subtree is flattened.

Flattening a binary tree is a catamorphism that can easily be defined in terms of reduce.

Definition 8.2.1 (flatten). Suppose T is a type. Let g : T × List(T) × List(T) → List(T) be defined by g(a, x, y) = x@(a :: y). Define flatten : BinTree(T) → List(T) by

flatten(B) = reduce([]; g)(B).

The formal definition of flatten is shown in Figure 8.5. The well-formedness theorem flatten_wf proves that flatten(B) is a list over T for every type T and every B ∈ BinTree(T). It is proved in two steps by instantiating the treereduce_wf lemma.

Defining the first phase of Quicksort in terms of unfold requires a little more effort. Firstly we define a simple predicate is_cons : List(T) → 𝔹 such that is_cons(L) is true if and only if L = h :: t for some h ∈ T, t ∈ List(T). The abstraction is_cons is shown in Figure 8.6.

The well-formedness theorem is_cons_wf states that is_cons : List(T) → 𝔹 for every type T. It is proved in a single step by the Auto tactic. We also prove two

 * ABS flatten
 flatten(B) == reduce([];λa,x,y.x @ (a::y))(B)
 * THM flatten_wf
 ∀T:𝕌. ∀B:BinTree(T). flatten(B) ∈ T List

Figure 8.5: Abstraction flatten and Theorem flatten_wf

 * ABS is_cons
 is_cons == λL.case L of [] => ff | h::t => tt esac

Figure 8.6: Abstraction is_cons

useful lemmata, namely that is_cons([]) is false and that is_cons(h :: t) is true (see Figure 8.7). The lemmata are proved in a single step each by unfolding the definition of is_cons and applying the Auto tactic afterwards.

 * THM is_cons_of_nil
 is_cons [] = ff
 * THM is_cons_of_cons
 ∀T:𝕌. ∀u:T. ∀v:T List.  is_cons (u::v) = tt
         Figure 8.7: Theorems is_cons_of_nil and is_cons_of_cons

We then define a function unjoin(≤) : {L ∈ List(T) | is_cons(L)} → T × List(T) × List(T) that maps a non-empty list L to the triple that has hd(L) as its first component, the list of all elements in tl(L) that are below hd(L) as its second element, and finally the list of all elements in tl(L) that are above hd(L) as its third element.

Definition 8.2.2 (unjoin). Suppose T is a type and ≤ : T × T → 𝔹. Define unjoin(≤) : {L ∈ List(T) | is_cons(L)} → T × List(T) × List(T) by

unjoin(≤)(L) =

(hd(L), filter(· below(≤) hd(L); tl(L)), filter(· above(≤) hd(L); tl(L)))

for all L ∈ List(T) with is_cons(L) = true.

The Nuprl abstraction unjoin is shown in Figure 8.8. We want to use unjoin as an argument to the unfold operator defined in Chapter 7, so we have to verify that unjoin is a ‘well-founded’ function.

 * ABS unjoin
 unjoin(≤) ==
 λx.<hd(x),
     filter((λb.b below(≤) hd(x));tl(x)),
     filter((λb.b above(≤) hd(x));tl(x))>

Figure 8.8: Abstraction unjoin

Lemma 8.2.3. Suppose T is a type and ≤ : T × T → 𝔹. Then

unjoin(≤) ∈ WellFnd(List(T), is_cons, | · |, T).

Proof. Clearly unjoin(≤) : {L ∈ List(T) | is_cons(L)} → T × List(T) × List(T). We have to verify

filter(· below(≤) hd(L); tl(L)) ∈ Smaller(List(T), | · |, L)

and filter(· above(≤) hd(L); tl(L)) ∈ Smaller(List(T), | · |, L)

for all L in List(T) with is_cons(L) = true.

Both statements follow from Lemma 8.1.2 in combination with |tl(L)| = |L| − 1 < |L|.

We prove this lemma as a well-formedness theorem unjoin_wf in Nuprl (see Figure 8.9). The formal proof is about 24 steps long. It uses a number of lemmata, including list_length_filter and length_tl. The latter proves |tl(L)| = |L| − 1. It can be found in the LIST_1 library. The final proof step for each of the two statements invokes the SupInf tactic which handles integer inequalities in Nuprl.

 * THM unjoin_wf
 ∀T:𝕌. ∀≤:T → T → 𝔹.  unjoin(≤) ∈ WellFnd(T List,is_cons,|·|,T)

Figure 8.9: Theorem unjoin_wf

We can now define a function mktree(≤) : List(T) → BinTree(T) that implements the first phase of Quicksort, that is, the generation of an ordered binary tree from a list.

Definition 8.2.4 (mktree). Suppose T is a type, and ≤ : T × T → 𝔹. Define mktree(≤) : List(T) → BinTree(T) by

mktree(≤)(L) = unfold(is_cons; unjoin(≤))(L)

for all L ∈ List(T).

The mktree abstraction and the associated well-formedness theorem mktree_wf are shown in Figure 8.10. The well-formedness theorem is proved in a single step by the Auto tactic.

 * ABS mktree
 mktree(≤)(x) == unfold(is_cons;unjoin(≤))(x)
 * THM mktree_wf
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀L:T List.  mktree(≤)(L) ∈ BinTree(T)

Figure 8.10: Abstraction mktree and Theorem mktree_wf

Like for is_cons before, we prove two simple, yet useful lemmata about mktree that can later be used when we do structural induction on a list L. The first lemma proves mktree(≤)([]) = leaf , and the second lemma proves mktree(≤)(u :: v) = node(u, mktree(≤)(filter(· below(≤) u; v)), mktree(≤)(filter(· above(≤) u; v)). The lemmata are shown in Figure 8.11. The proof of mktree_of_nil is about seven steps long, and proving mktree_of_cons requires about nine steps—mainly just unfolding definitions.

 * THM mktree_of_nil
 ∀T:𝕌. ∀≤:T → T → 𝔹.  mktree(≤)([]) = leaf
 * THM mktree_of_cons
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀u:T. ∀v:T List.
 mktree(≤)(u::v) =
     node(u,
     mktree(≤)(filter((λb.b below(≤) u);v)),
     mktree(≤)(filter((λb.b above(≤) u);v)))
          Figure 8.11: Theorems mktree_of_nil and mktree_of_cons

We have a second way of stating the Quicksort algorithm now: quicksort is equal to the composition of mktree and flatten.

Theorem 8.2.5. Suppose T is a type and ≤ : T × T → 𝔹. Then

quicksort(≤, L) = flatten(mktree(≤)(L))

for all L ∈ List(T).

The theorem quicksort_by_fusion shown in Figure 8.12 formalizes this result in Nuprl. To prove it, we first replace flatten · mktree with fun using the fusion theorem. The ListLenInd tactic is then used to prove the resulting equality by complete induction on the length of L. A minor complication is introduced by the fact that the Fold tactic does not work for certain abstractions,^{3} which forces us to work with the unfolded terms in some places. The proof is about 31 steps long.

 * THM quicksort_by_fusion
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀L:T List.
     quicksort(≤,L) = flatten(mktree(≤)(L))
                Figure 8.12: Theorem quicksort_by_fusion

8.3 A Formal Correctness Proof

Quicksort is a sorting algorithm: For every list L, it should return an ordered permutation of that list. We prove that Quicksort is correct by first proving that it returns an ordered list, and secondly by proving that it returns a permutation of its input. The first proof is based on the representation of quicksort as flatten · mktree, while the second proof uses the definition of quicksort directly.

8.3.1 Quicksort Returns an Ordered List

We say a list L is ordered if the elements in L are in ascending order (with respect to a relation ≤).

Definition 8.3.1 (ordered). Suppose T is a type and ≤ : T × T → 𝔹. Define ordered(≤, L) ∈ 𝔹 recursively by

ordered(≤, L) = \{ \begin{matrix}true & if L = [] \\ (∀x ∈ t. h ≤ x) ∧ ordered(≤, t) & if L = h :: t \end{matrix} .

By checking whether the head of the list is below every other element in the list (instead of just checking whether it is below the second element), we avoid having to check if there exists a second element in the list. The Nuprl abstraction defining ordered is shown in Figure 8.13. The well-formedness theorem ordered_wf proves ordered(≤, L) ∈ 𝔹 if T is a type, ≤ : T ×T → 𝔹 and L ∈ List(T). The well-formedness theorem is proved by structural induction on L using the ListInd tactic.

3Folding abstractions that contain so_apply seems to be a problem in some cases.

 * ABS ordered
 ordered(≤,L) ==
 (letrec recfun(L) = case L
 of [] => tt
 | h::t => ∀x∈_{2}t.(h ≤ x) ∧_{b} recfun t esac )
 L

Figure 8.13: Abstraction ordered

To prove that the list returned by quicksort = flatten · mktree is ordered, we first prove that mktree creates an ordered tree. Before we can define what it means for a binary tree to be ordered, we need to define a function that computes whether some predicate P [x] holds for every element x in a tree. The abstraction defining tree_all_2 is shown in Figure 8.14. The name of the function ends with ‘_2’ to indicate that a boolean value is returned (as opposed to a proposition in ℙ), thereby following the naming scheme for the list_all functions defined in the LIST_3 library.

 * ABS tree_all_2
 ∀x∈_{2}B.P[x] ==
 (letrec recfun(B) = case B
 of inl(y) => tt
 | inr(z) => let t,B1,B2 = z in P[t] ∧_{b} recfun B1 ∧_{b} recfun B2 )
 B

Figure 8.14: Abstraction tree_all_2

The well-formedness theorem tree_all_2_wf shows that (∀x ∈_{2} B.P [x]) is a boolean value for every type T, P : T → 𝔹, and B ∈ BinTree(T). It is proved in about eight steps; we use the RecElimination tactic in its proof for structural induction on B. We can now define when a binary tree is ordered.

Definition 8.3.2 (treeordered). Suppose T is a type and ≤ : T × T → 𝔹. Define ordered(≤, B) ∈ 𝔹 recursively by

ordered(≤, B) = \{ \begin{matrix}true & if B = leaf \\ (∀z ∈ B_{1}. z ≤ t) ∧ (∀z ∈ B_{2}. ¬(z ≤ t)) & if B = node(t, B_{1}, B_{2}) \\ ∧ordered(≤, B_{1}) ∧ ordered(≤, B_{2}) \end{matrix} .

The corresponding Nuprl abstraction treeordered is shown in Figure 8.15. As usual, we prove a well-formedness theorem for it: treeordered_wf just shows that for every type T, ≤ : T × T → 𝔹, and B ∈ BinTree(T), ordered(≤, B) ∈ 𝔹. It is proved in about six steps by structural induction on B.

 * ABS treeordered
 ordered(≤,B) ==
 (letrec recfun(B) = case B
 of inl(x) => tt
 | inr(y) => let t,B1,B2 = y in ∀z∈_{2}B1.(z ≤ t)
 ∧_{b} ∀z∈_{2}B2.(¬_{b}(z ≤ t))
 ∧_{b} recfun B1
 ∧_{b} recfun B2 )
 B

Figure 8.15: Abstraction treeordered

Lemma 8.3.3. Suppose T is a type and ≤ : T × T → 𝔹. Then

ordered(≤, mktree(≤)(L))

for all L ∈ List(T).

Figure 8.16 shows the Nuprl theorem ordered_mktree. The arrow ‘↑’ (assert) is used to turn the boolean value ordered(≤, mktree(≤)(L)) into a proposition, i.e. tt becomes True, ff becomes False.

 * THM ordered_mktree
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀L:T List.
 ↑ordered(≤,mktree(≤)(L))

Figure 8.16: Theorem ordered_mktree

To prove the formal theorem, we need three lemmata: Firstly, that f[x] holds for all x in filter(f; L) assuming T is a type, f : T → 𝔹 and L ∈ List(T). Secondly, that P [x] holds for all x ∈ L if and only if P [x] holds for all x in filter(f; L) and for all x in filter(¬f; L) assuming T is a type, P, f : T → 𝔹, and L ∈ List(T). Finally, that f[x] holds for all x in L if and only if f[x] holds for all x in mktree(≤)(L) assuming T is a type, ≤ : T × T → 𝔹, f : T → 𝔹, and L ∈ List(T). The lemmata are shown in Figures 8.17, 8.18, and 8.19 respectively.

 * THM filter_all_2
 ∀T:𝕌. ∀f:T → 𝔹. ∀L:T List. ↑∀x∈_{2}filter(f;L).f[x]

Figure 8.17: Theorem filter_all_2

The filter_all_2 lemma is proved in about eight steps by structural induction on L using the ListInd tactic. The base case is proved in a single step by the Auto tactic. For the case L = u :: v, the IfThenElseCases tactic is used to do a case split on f[u].

 * THM list_all_2_filter_filter
 ∀T:𝕌. ∀f,P:T → 𝔹. ∀L:T List.
 ∀x∈_{2}L.P[x] = ∀x∈_{2}filter(f;L).P[x] ∧_{b} ∀x∈_{2}filter((λz.¬_{b}f[z]);L).P[x]
             Figure 8.18: Theorem list_all_2_filter_filter

The list_all_2_filter_filter lemma is also proved by structural induction on L. The case L = [] is proved in a single step again, and for the case L = u :: v, we do a case split on f[u] by IfThenElseCases. The resulting equalities are proved using the associativity and commutativity of ∧_{b}. The proof is about eleven steps long.

 * THM mktree_all_2
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀f:T → 𝔹. ∀L:T List.
 ∀x∈_{2}L.f[x] = ∀x∈_{2}mktree(≤)(L).f[x]

Figure 8.19: Theorem mktree_all_2

Proving the mktree_all_2 lemma is slightly more complicated. We start by using the ListLenInd tactic for complete induction on the length of L, followed by the ListInd tactic to differentiate between the two cases L = [] and L = u :: v. For the base case, we instantiate the lemma mktree_of_nil, and for the case L = u :: v, we use the mktree_of_cons lemma. The induction hypothesis is then used on the two lists filter(· below(≤) u; v) and filter(· above(≤) u; v). Finally the list_all_2_filter_filter lemma is used to prove the equivalence of (∀x ∈_{2} v.f[x])) and (∀x ∈_{2} filter(· below(≤) u; v).f[x]) ∧ (∀x ∈_{2} filter(· above(≤) u; v).f[x]). The proof is about 23 steps long.

The proof of ordered_mktree then requires about 26 steps. It is based on complete induction on the length of L, using the ListLenInd tactic followed by ListInd. About 20 of those steps are needed to prove the case L = u :: v.

Our next step in proving that quicksort returns an ordered list is to show that flatten(B) is an ordered list if B is an ordered tree.

Lemma 8.3.4. Suppose T is a type, ≤ : T ×T → 𝔹 is transitive and total (i.e. x ≤ y or y ≤ x for all x, y ∈ T), and B ∈ BinTree(T). Then

ordered(≤, B) ⟹ ordered(≤, flatten(B)).

 * THM ordered_flatten
 ∀T:𝕌.
 ∀≤:{≤:T → T → 𝔹| Trans(T;x,y.↑≤[x;y]) ∧ Connex(T;x,y.↑≤[x;y])} .
 ∀B:BinTree(T).
 ↑ordered(≤,B) ⇒ ↑ordered(≤,flatten(B))

Figure 8.20: Theorem ordered_flatten

The corresponding Nuprl theorem ordered_flatten is shown in Figure 8.20.

We need a number of fairly self-evident lemmata before we can formally prove this theorem. The list_all_2_append_lemma lemma shown in Figure 8.21 proves that a property P [x] holds for all x in L@M if and only if it holds for all x in L and for all x in M. In other words, ‘∀’ distributes over append. Using the ListInd tactic for structural induction on L, the lemma is proved in about four steps.

 * THM list_all_2_append_lemma
 ∀T:𝕌. ∀P:T → 𝔹. ∀L,M:T List.
 ∀x∈_{2}(L @ M).P[x] = ∀x∈_{2}L.P[x] ∧_{b} ∀x∈_{2}M.P[x]
              Figure 8.21: Theorem list_all_2_append_lemma

Figure 8.22 shows a lemma proving that a list of the form L@(t :: M) is ordered if and only if L is ordered, M is ordered, x ≤ t for all x in L, and t ≤ x for all x in M. To prove the lemma, we use structural induction on L, the list_all_2_append_lemma lemma and a number of other lemmata. A nested induction on M and several case splits are required for the case where L = u :: v. The proof is about 60 steps long.

 * THM ordered_append
 ∀T:𝕌. ∀≤:{≤:T → T → 𝔹| Trans(T;x,y.↑≤[x;y])} . ∀L,M:T List.
 ∀t:T.
 ordered(≤,L @ (t::M)) =
     ∀x∈_{2}L.(x ≤ t) ∧_{b} ∀x∈_{2}M.(t ≤ x) ∧_{b} ordered(≤,L) ∧_{b} ordered(≤,M)

Figure 8.22: Theorem ordered_append

The flatten_all_2 lemma (see Figure 8.23) shows that a property f[x] holds for all x in a binary tree B if and only if it holds for all x in flatten(B). This lemma is similar to the mktree_all_2 lemma proved earlier. The proof is by structural induction on B. It requires about 29 steps, including one instantiation of the list_all_2_append_lemma lemma.

 * THM flatten_all_2
 ∀T:𝕌. ∀f:T → 𝔹. ∀B:BinTree(T). ∀x∈_{2}B.f[x] = ∀x∈_{2}flatten(B).f[x]

Figure 8.23: Theorem flatten_all_2

Figure 8.24 shows another lemma that we need, list_all_2_implies_lemma. It proves that if P [x] and (P [x] ⟹ Q[x]) hold for all x in a list L, then Q[x] holds for all x in L. The lemma is proved in about 13 steps by structural induction on L; many of those steps just deal with the fairly technical difference between boolean values and propositions.

 * THM list_all_2_implies_lemma
 ∀T:𝕌. ∀P,Q:T → 𝔹. ∀L:T List.
 ↑∀x∈_{2}L.P[x] ∧ ↑∀x∈_{2}L.(P[x] ⇒_{b} Q[x]) ⇒ ↑∀x∈_{2}L.Q[x]
             Figure 8.24: Theorem list_all_2_implies_lemma

Our last lemma for now is shown in Figure 8.25. The list_all_2_if_all lemma proves that a property P [x] holds for all x in a list L ∈ List(T) if it holds for all x ∈ T. It is proved in about six steps by structural induction on L.

 * THM list_all_2_if_all
 ∀T:𝕌. ∀P:T → 𝔹. ∀L:T List.  (∀x:T. ↑P[x]) ⇒ ↑∀x∈_{2}L.P[x]

Figure 8.25: Theorem list_all_2_if_all

Given these lemmata, the proof of ordered_flatten requires about 58 steps. The RecElimination tactic is used for structural induction on B. The base case is then proved in about six steps simply by unfolding definitions. Proving the case B = node(t, B_{1}, B_{2}) requires the use of the lemmata ordered_append, flatten_all_2,

list_all_2_implies_lemma and list_all_2_if_all.

We proved that mktree always creates an ordered tree, and that flatten flattens an ordered tree into an ordered list. Given the quicksort_by_fusion theorem from Section 8.2, the proof that Quicksort always returns an ordered list is quite simple now.

To prove the ordered_quicksort theorem shown in Figure 8.26, we first replace quicksort(≤, L) with flatten(mktree(≤)(L)) using the quicksort_by_fusion theorem. After using the ordered_flatten lemma then, we only have to prove that mktree(≤)(L) is ordered. This is proved by the ordered_mktree lemma. All wellformedness goals are discharged by Nuprl’s Auto tactic, so the whole proof requires only about three steps.

 * THM ordered_quicksort
 ∀T:𝕌.
 ∀≤:{≤:T → T → 𝔹| Trans(T;x,y.↑≤[x;y]) ∧ Connex(T;x,y.↑≤[x;y])} .
 ∀L:T List.
 ↑ordered(≤,quicksort(≤,L))

Figure 8.26: Theorem ordered_quicksort

8.3.2 Quicksort Returns a Permutation of its Input

In the previous subsection we proved that Quicksort always returns an ordered list. To prove that Quicksort is a sorting algorithm, it remains to show that the list returned by Quicksort is a permutation of the input list.

Theorem 8.3.5. Suppose T is a type, eq : T × T → 𝔹 is a function with eq(x, y) = true if and only if x = y for all x, y ∈ T (in other words, equality in T is decidable), and ≤ : T × T → 𝔹. Furthermore, suppose x ∈ T and L ∈ List(T). Then x occurs in quicksort(≤, L) exactly as often as in L.

The idea of counting the occurrences of an element in L and in quicksort(≤, L) is borrowed from [Sha96]. Figure 8.27 shows the Nuprl theorem list_count_quicksort. We used the abstractions discrete_equality, which can be found in the DISCRETE library, and list_count from the LIST_3 library to state the theorem. We need a decidable equality on T in order to be able to count the occurrences of a given element x ∈ T in the two lists L and quicksort(≤, L): If we could not tell whether two elements x, y ∈ T are equal, we could not compare x to the elements in L and quicksort(≤, L).

 * THM list_count_quicksort
 ∀T:𝕌. ∀eq:{T=_{2}}. ∀≤:T → T → 𝔹. ∀L:T List. ∀x:T.
 |x∈quicksort(≤,L)| = |x∈L|
               Figure 8.27: Theorem list_count_quicksort

We do not prove this theorem directly. Instead, we prove three lemmata first. The first lemma, list_count_over_filter_lemma, is shown in Figure 8.28. It proves that an element x occurs in the list filter(f; L) exactly as often as in L if f[x] is true, and zero times otherwise. The lemma is proved in about 33 steps using the ListInd tactic for structural induction on L, combined with several applications of the IfThenElseCases tactic for case splits on f[x] and—in the case L = u :: v—on

 * THM list_count_over_filter_lemma
 ∀T:𝕌. ∀eq:{T=_{2}}. ∀f:T → 𝔹. ∀L:T List. ∀x:T.
 |x∈filter(f;L)| = if f[x] then |x∈L| else 0 fi
            Figure 8.28: Theorem list_count_over_filter_lemma

f[u]. The fact that we can decide whether x is equal to u (via the eq function) is crucial to the proof.

The second lemma, shown in Figure 8.29, states that an element x occurs in L exactly as often as in the two lists filter(f; L) and filter(¬f; L) together. It is proved in about 16 steps. We apply the list_count_over_filter_lemma lemma twice in its proof: first to the list filter(f; L), and then to the list filter(¬f; L).

 * THM list_count_filter_filter_lemma
 ∀T:𝕌. ∀eq:{T=_{2}}. ∀f:T → 𝔹. ∀L:T List. ∀x:T.
 |x∈filter(f;L)| + |x∈filter((λz.¬_{b}f[z]);L)| = |x∈L|
           Figure 8.29: Theorem list_count_filter_filter_lemma

Figure 8.30 shows the third lemma. This lemma is simply a specialized version of list_count_over_filter_lemma for the predicates below and above. Using the

list_count_over_filter_lemma lemma, it is proved in two steps.
 * THM list_count_below_above
 ∀T:𝕌. ∀eq:{T=_{2}}. ∀≤:T → T → 𝔹. ∀L:T List. ∀u,x:T.
 |x∈filter((λb.b below(≤) u);L)| + |x∈filter((λb.b above(≤) u);L)|
     = |x∈L|
              Figure 8.30: Theorem list_count_below_above

The proof of list_count_quicksort now requires about 55 steps. The ListLenInd tactic is used for complete induction on the length of L, followed by the ListInd tactic two differentiate between the two possible cases L = [] and L = u :: v. The case L = [] is proved in a single step by the Auto tactic after unfolding the definition of quicksort. For the case L = u :: v, we apply the list_count_over_append_lemma lemma from the LIST_3 library to the two lists quicksort(≤, filter(· below(≤) u; v)) and u :: quicksort(≤, filter(· above(≤) u; v)). The induction hypothesis is then applied to the two lists quicksort(≤, filter(· below(≤) u; v)) and quicksort(≤, filter(· above(≤) u; v)). Finally list_count_below_above is used on the two lists filter(· below(≤) u; v) and filter(· above(≤) u; v).

This does not only complete the proof that Quicksort returns a permutation of its input list, but it is also the last step in our correctness proof for Quicksort. The next section presents an alternative approach to proving that Quicksort returns a permutation of its input.

8.3.3 Quicksort Returns a Permutation of its Input: A Second Proof

To prove that Quicksort returns a permutation of its input in the previous section, we counted the number of occurrences of elements in the lists L and quicksort(≤, L). We cannot do this unless equality on T is decidable. This is not a real restriction if ≤ is a decidable order relation on T: Then x = y ⟺ (x ≤ y ∧ y ≤ x) for all x and y in T.^{4} However, all theorems that we proved in the previous section only required ≤ to be total (i.e. x ≤ y ∨ y ≤ x for all x, y ∈ T) and transitive (i.e. (x ≤ y ∧ y ≤ z) ⟹ x ≤ z for all x, y, z ∈ T), and there is a different approach to proving that Quicksort returns a permutation of its input—an approach that does not require equality on T to be decidable.

This approach is based on the inductive definition of permutation shown in Figure 8.31. The definition can be found in the LIST_3 library.

 * ABS permutation
 perm(L,M) ==
 (letrec perm(L)(M) = case L
 of [] => case M
     of [] => True
     | h::t => False
 esac
 | h::t => case M
     of [] => False
     | h'::t' => ∃N,N':T List.  M = N @ (h::N') ∧ perm t (N @ N')
 esac
 esac )
 L
 M

Figure 8.31: Abstraction permutation We also need two self-evident lemmata: that permutation is transitive, and that permutation distributes over append. The former is shown in Figure 8.32, and the latter in Figure 8.33.

4The ‘⇒’ direction follows from the reflexivity of ≤, and the antisymmetry of ≤ implies the ‘⇐’ direction.

 * THM permutation_transitive
 ∀T:𝕌. ∀L,M,N:T List.  perm(L,M) ⇒ perm(M,N) ⇒ perm(L,N)
              Figure 8.32: Theorem permutation_transitive

 * THM permutation_over_append_lemma
 ∀T:𝕌. ∀A,B,X,Y:T List.  perm(A,X) ∧ perm(B,Y) ⇒ perm(A @ B,X @ Y)
           Figure 8.33: Theorem permutation_over_append_lemma

We now prove a lemma similar to the list_count_filter_filter_lemma lemma shown in Figure 8.29: L is a permutation of filter(f; L)@filter(¬f; L). This lemma, which is shown in Figure 8.34, is proved in about 23 steps by structural induction on L.

 * THM permutation_filter_filter_lemma
 ∀T:𝕌. ∀f:T → 𝔹. ∀L:T List.
 perm(L,filter(f;L) @ filter((λz.¬_{b}f[z]);L))
          Figure 8.34: Theorem permutation_filter_filter_lemma

The permutation_below_above lemma (see Figure 8.35) simply results from applying the permutation_filter_filter_lemma lemma to the two predicates below and above. It is proved in about three steps.

 * THM permutation_below_above
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀L:T List. ∀u:T.
 perm(L,filter((λb.b below(≤) u);L) @ filter((λb.b above(≤) u);L))
              Figure 8.35: Theorem permutation_below_above

We can now show that quicksort(≤, L) is a permutation of L. Figure 8.36 shows the corresponding Nuprl theorem. It is proved by complete induction on the length of L using the ListLenInd tactic, followed by the ListInd tactic to differentiate between L = [] and L = u :: v. The case L = [] is then proved in a single step by unfolding definitions and the Auto tactic. Proving the case L = u :: v requires approximately 8.3. A FORMAL CORRECTNESS PROOF 95

 * THM permutation_quicksort
 ∀T:𝕌. ∀≤:T → T → 𝔹. ∀L:T List.  perm(L,quicksort(≤,L))
               Figure 8.36: Theorem permutation_quicksort

34 steps. A number of lemmata are instantiated in this part of the proof. Altogether, the proof is about 39 steps long. This completes our second proof that Quicksort returns a permutation of its input.

96 CHAPTER 8. EXAMPLE: QUICKSORT

Conclusions

In this thesis we presented a formalization of program transformations and their general categorical framework in Nuprl. This chapter summarizes our results and points out possible future work.

9.1 Contributions

We formalized substantial parts of category theory in Nuprl. We gave formal definitions of catamorphisms and anamorphisms and formal, constructive proofs for when an arrow is a catamorphism or anamorphism. We showed that the result from [GHA01] for when a function is a catamorphism is not constructively valid, and we found conditions under which the result can be applied to constructive functions. We verified an instance of Bird’s fusion theorem [Bir95] for binary trees in Nuprl, and applied it to the Quicksort algorithm to formally prove the algorithm’s correctness.

9.2 Summary

In Chapter 4 we presented the notions of category theory that are needed for a definition of catamorphisms and anamorphisms. We showed that Nuprl’s constructive type theory is well-suited to formalize these concepts. Using subtypes and the dependent product type, the formalization in Nuprl was straightforward, although verifying well-formedness was sometimes tedious. Many well-formedness goals arose from the fact that the composition of two arrows is defined only if the second arrow’s domain is equal to the first arrow’s codomain. The category_if lemma shows how we can greatly simplify many proofs by proving specialized well-formedness lemmas.

Catamorphisms and anamorphisms were defined in Chapter 5. For the most part, this was a straightforward extension of the formalization of category theory presented in Chapter 4. The formal definitions of fold and unfold presented a minor difficulty because we cannot express foldg directly as a function of g. Therefore we defined fold and unfold as binary relations (as opposed to functions). We showed how Nuprl’s display forms can be used to retain the common mathematical notation nevertheless. Also, dualizing our results from catamorphisms to anamorphisms was straightforward. Parts of the proofs of dual theorems could simply be copied from the original theorems in Nuprl. Manual interaction was still needed however, and a complete automatization of the dualization process is well beyond the scope of this thesis.

Perhaps our most significant theoretical results can be found in Chapter 6. In this chapter we addressed the question of when a constructive function is a catamorphism. Not only did we give a counterexample to a theorem proved in [GHA01] (thereby proving that the theorem is not constructively valid), but we also found a simple additional condition that allowed us to give a constructive proof. Whereas the results from [GHA01] could only be used to find out when two phases of a program cannot be fused into a single catamorphism, our results can also be used to find out when two phases can be fused—and for this case, we presented a transformation that actually writes the given function as a fold. Therefore our results are not only of theoretical interest, but they have practical applications in program optimization as well. It was only in this chapter that the differences between set theory and Nuprl’s type theory caused any problems that required reformulation of the results in [GHA01] stated in terms of constructive category theory.

We verified an instance of Bird’s fusion theorem in Chapter 7. Here we made extensive use of recursive types and functions. Many of Nuprl’s powerful induction strategies where frequently used in the proofs. N. Shankar [Sha96] had to write a tactic similar to InvImageInd when he verified Bird’s fusion theorem in PVS. We did not have to write a single tactic in Nuprl; instead, we just employed existing tactics from the YINDUCTIONS library. For the most part, well-formedness goals were not an issue in this chapter.

In Chapter 8 we applied the fusion transformation to the Quicksort algorithm. Implementing Quicksort in Nuprl was no problem, but the proof of the associated well-formedness theorem presented a few technical difficulties. Other proofs were slightly more complicated than necessary because of a problem with the Fold tactic. The overall development however was fairly straightforward. The correctness proof, although a few hundred steps long in total, was simplified and structured by the use of several lemmata, some of which we had to state and prove ourselves, and some of which were already in the basic Nuprl libraries. Our experience from Chapters 7 and 8 shows that Nuprl, as a general-purpose proof development system, is quite well suited for reasoning about program transformations as well.

9.3 Future Work

The partial formalization of category theory presented in Chapter 4 is only part of a much larger project: the formalization of (constructive) mathematics in Nuprl. Many have contributed to this project [Kre86, How87, For93, Jac95, CJNU97, Cal98], and work on it will certainly continue.

More research should be done on the question when a constructive function is a catamorphism or anamorphism. In Chapter 6 we gave a partial answer based on results for non-constructive functions, but not a complete classification. Also the results from Chapter 6 were not dualized to anamorphisms in this thesis.

Finally, it remains to be seen whether the transformation presented in Chapter 6, which writes certain functions as a fold, and which we manually applied to a small example in this thesis, is simple and useful enough to be actually implemented in an optimizing compiler.

100 CHAPTER 9. CONCLUSIONS

Bibliography

[Acz93] P. Aczel. Galois: A theory development project. Report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks, 1993.

[Acz99] P. Aczel. On relating type theories and set theories. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs (TYPES ’98), volume 1657 of LNCS, pages 1–18, 1999.

[AP90] James A. Altucher and Prakash Panangaden. A mechanically assisted constructive proof in category theory. In Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Computer Science. Springer-Verlag, July 1990.

[Bax01] Ira D. Baxter. DMS: Practical code generation and enhancement by program transformation, 2001.

[BBC^{+}97] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq proof assistant reference manual : Version 6.1. Technical Report RT-0203, INRIA, 1997.

[BGS94] David F. Bacon, Susan L. Graham, and Oliver J. Sharp. Compiler transformations for high-performance computing. ACM Computing Surveys, 26(4):345–420, 1994.

[BHW97] J. Boyle, T. Harmer, and V. Winter. The TAMPR program transformation system: Design and applications. In E. Arge, A. M. Bruaset, and H. P. Langtangen, editors, Modern Software Tools for Scientific Computing. Brikhauser, 1997.

[Bir84] Richard Bird. The promotion and accumulation strategies in transformational programming. ACM Transactions on Programming Languages and Systems, 6(4), October 1984.

[Bir95] Richard S. Bird. Functional algorithm design. In Bernhard Moller, editor, Mathematics of Program Construction ’95, volume 947 of Lecture Notes in Computer Science, pages 2–17. Springer-Verlag, 1995.

[Bir98] Richard Bird. Introduction to Functional Programming using Haskell. Prentice-Hall, second edition, 1998.

[BM92] L. M. Barroca and J. A. McDermid. Formal methods: use and relevance for the development of safety-critical systems. The Computer Journal, 35(6):579–599, 1992.

[BS93] J. P. Bowen and V. Stavridou. Safety-critical systems, formal methods and standards. IEE/BCS Software Engineering Journal, 8(4):189–209, 1993.

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

[Cal98] J. L. Caldwell. Classical propositional decidability via Nuprl proof extraction. In Proc. 11th International Theorem Proving in Higher Order Logics Conference, pages 105–122, 1998.

[Cal02] James Caldwell. Extracting recursion operators in Nuprl’s type-theory. In A. Pettorossi, editor, Eleventh International Workshop on Logic -based Program Synthesis, LOPSTR-02, volume 2372 of LNCS, pages 124–131. Springer, 2002.

[Car98] A. Carvalho. Category theory in COQ. Technical report, 1049-001 Lisboa, Portugal, 1998.

[CJNU97] Robert L. Constable, Paul B. Jackson, Pavel Naumov, and Juan Uribe. Constructively formalizing automata theory, 1997.

[CLRS01] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms. MIT Press, 2001.

[Cor00] James R. Cordy. The TXL Compiler/Interpreter User’s Guide Version 10. TXL Software Research Inc., Kingston, Canada, January 2000.

[Dav87] M. Davis. Deforestation: Transformation of functional programs to eliminate intermediate trees. Master’s thesis, Oxford University, 1987.

[EM42] Samuel Eilenberg and Saunders MacLane. Group extensions and homology. Annals of Mathematics, 43:757–831, 1942.

[EM45] Samuel Eilenberg and Saunders MacLane. General theory of natural equivalences. Transactions of the American Mathematical Society, 58:231–294, 1945.

[ES95] William F. Eddy and Mark J. Schervish. How many comparisons does Quicksort use? Journal of Algorithms, 19(3):402–431, November 1995.

[For93] Max B. Forester. Formalizing constructive real analysis. Technical Report TR93-1382, Computer Science Department, Cornell University, Ithaca, NY, 1993.

[GHA01] Jeremy Gibbons, Graham Hutton, and Thorsten Altenkirch. When is a function a fold or an unfold? In Andrea Corradini, Marina Lenisa, and Ugo Montanari, editors, Proceedings 4th Workshop on Coalgebraic Methods in Computer Science, CMCS’01, Genova, Italy, 6–7 Apr. 2001, volume 44(1). Elsevier, Amsterdam, 2001.

[Gir72] Jean-Yves Girard. Interprétation Fonctionelle et Élimination des Compures de l’Arithmétic d’Ordre Supérieur. PhD thesis, Université Paris VII, 1972.

[GJ98] Jeremy Gibbons and Geraint Jones. The under-appreciated unfold. In Proceedings 3rd ACM SIGPLAN Int. Conf. on Functional Programming, ICFP’98, Baltimore, MD, USA, 26–29 Sept. 1998, volume 34(1), pages 273–279. ACM Press, New York, 1998.

[GJS93] A. Gill, Launchbury J., and Peyton Jones S.L. A short cut to deforestation. In Conference on Functional Programming Languages and Computer Architecture, pages 223–232, June 1993.

[HE99] M. G. Hinchey and J. P. Bowen (Eds.). Industrial-Strength Formal Methods in Practice. Springer, 1999.

[Her00] Debra S. Herrmann. Software Safety and Reliability: Techniques, Approaches, and Standards of Key Industrial Sectors. IEEE, 2000.

[Hoa61] C. A. R. Hoare. ACM Algorithm 64: Quicksort. Communications of the ACM, 4(7):321, July 1961.

[How87] Douglas J. Howe. Implementing number theory: An experiment with Nuprl. In 8th International Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, pages 404–415. Springer-Verlag, 1987.

[How93] Douglas J. Howe. Reasoning about functional programs in Nuprl. In Peter F. Lauer, editor, Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693, pages 145–164. Springer-Verlag, 1993.

[HS98] G. Huet and A. Saibi. Constructive category theory. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998.

[Hut98] Graham Hutton. Fold and unfold for program semantics. In Proceedings 3rd ACM SIGPLAN Int. Conf. on Functional Programming, ICFP’98, Baltimore, MD, USA, 26–29 Sept. 1998, volume 34(1), pages 280–288. ACM Press, New York, 1998.

[Hut99] Graham Hutton. A tutorial on the universality and expressiveness of fold. Journal of Functional Programming, 9(4):355–372, 1999.

[Jac94] Paul B. Jackson. The Nuprl Proof Development System, Version 4.1 Reference Manual and User’s Guide. Cornell University, Ithaca, NY, 1994.

[Jac95] Paul B. Jackson. Enhancing the nuprl proof development system and applying it to computational abstract algebra. Technical Report TR95-1509, Computer Science Department, Cornell University, Ithaca, NY, 18, 1995.

[Jon96] Simon L. Peyton Jones. Compiling haskell by program transformation: A report from the trenches. In European Symposium on Programming, pages 18–44, 1996.

[KH89] Richard Kelsey and Paul Hudak. Realistic compilation by program transformation. In Symposium on Principles of Programming Languages, pages 281–292, 1989.

[Kre86] Christoph Kreitz. Constructive automata theory implemented with the Nuprl proof development system, 1986.

[LP92] Z. Luo and R. Pollack. LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992.

[Mac97] Saunders MacLane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 2nd edition, 1997. (1st ed., 1971).

[Mal90] G. Malcolm. Algebraic data types and program transformation. Science of Computer Programming, 14(2–3):255–280, 1990.

[Mar02] Jean-Pierre Marquis. Category theory. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab at the Center for the Study of Language and Information, Stanford University, Stanford, CA, Summer 2002.

[Mee86] Lambert Meertens. Algorithmics: Towards programming as a mathematical activity. In J. W. de Bakker, M. Hazewinkel, and J.K. Lenstra, editors, Proceedings of the CWI Symposium on Mathematics and Computer Science, volume 1 of CWI Monographs, pages 289–334, North–Holland, 1986.

[MFP91] Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In J. Hughes, editor, Proceedings 5th ACM Conf. on Functional Programming Languages and Computer Architecture, FPCA’91, Cambridge, MA, USA, 26–30 Aug 1991, volume 523, pages 124–144. Springer-Verlag, Berlin, 1991.

[Miz] The Mizar Home Page. http://www.mizar.org.

[ML82] Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175, 1982.

[MN94] Lena Magnusson and Bengt Nordström. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 213–237. Springer-Verlag LNCS 806, 1994.

[OSR95] S. Owre, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System. CSL, 1995.

[RB88] David Rydeheard and Rod Burstall. Computational Category Theory (Prentice Hall International Series in Computer Science). Prentice Hall, 1988.

[Sha96] Natarajan Shankar. Steps toward mechanizing program transformations using PVS. Science of Computer Programming, 26(1-3):33–57, 1996.

[Smi90] D. R. Smith. KIDS: A semiautomatic program development system. IEEE Transactions on Software Engineering, 16(9):1024–1043, 1990.

[Sto96] Neil Storey. Safety-Critical Computer Systems. Addison-Wesley, 1996.

[Tur36] Alan Turing. On computable numbers, with an application to the Entscheidungsproblem. In Proceedings of the London Mathematical Society, Series 2, volume 42, pages 230–265, 1936.

[Vis01a] Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. System description of Stratego 0.5. In A. Middeldorp, editor, Rewriting Techniques and Applications (RTA’01), volume 2051 of Lecture Notes in Computer Science, pages 357–361. Springer-Verlag, May 2001.

[Vis01b] Eelco Visser. A survey of strategies in program transformation systems. In B. Gramlich and S. Lucas, editors, Workshop on Reduction Strategies in Rewriting and Programming (WRS’01), volume 57/2 of Electronic Notes in Theoretical Computer Science, Utrecht, The Netherlands, May 2001. Elsevier Science Publishers.

[Wad88] P. Wadler. Deforestation: Transforming programs to eliminate trees. In ESOP ’88. European Symposium on Programming, Nancy, France, 1988, volume 300 of Lecture Notes in Computer Science, pages 344–358. Berlin: Springer-Verlag, 1988.

[Wan80] Mitchell Wand. Continuation-based program transformation strategies. Journal of the ACM, 27(1):164–180, 1980.

[Wer97] Benjamin Werner. Sets in types, types in sets. In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, Third International Symposium, (TACS ’97), volume 1281 of Lecture Notes in Computer Science, pages 530–546. Springer, 1997.