NUMMSQUARED 2006A0 EXPLAINED, INCLUDING A NEW WELL-FOUNDED FUNCTIONAL FOUNDATION FOR LOGIC, MATHEMATICS AND COMPUTER SCIENCE by Samuel Howse Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy at Dalhousie University Halifax, Nova Scotia October 2006 © Copyright by Samuel Howse, 2006 ivi Library and Bibliotheque et Archives Canada Archives Canada Published Heritage Direction du Branch Patrimoine de l'édition 395 Wellington Street 395, rue Wellington Ottawa ON K1A 0N4 Ottawa ON K1A 0N4 Canada Canada Your file Votre référence ISBN: 978-0-494-19613-7 Our file Notre référence ISBN: 978-0-494-19613-7 NOTICE: AVIS: The author has granted a non- L'auteur a accordé une licence non exclusive exclusive license allowing Library permettant a la Bibliotheque et Archives and Archives Canada to reproduce, Canada de reproduire, publier, archiver, publish, archive, preserve, conserve, sauvegarder, conserver, transmettre au public communicate to the public by par télécommunication ou par I'Internet, préter, telecommunication or on the Internet, distribuer et vendre des théses partout dans loan, distribute and sell theses le monde, a des fins commerciales ou autres, worldwide, for commercial or non- sur support microforme, papier, électronique commercial purposes, in microform, et/ou autres formats. paper, electronic and/or any other formats. The author retains copyright L'auteur conserve la propriété du droit d'auteur ownership and moral rights in et des droits moraux qui protége cette these. Neither the thesis Ni la thése ni des extraits substantiels de nor substantial extracts from it celle-ci ne doivent être imprimés ou autrement may be printed or otherwise reproduits sans son autorisation.
reproduced without the author's permission. In compliance with the Canadian Conformément a la loi canadienne Privacy Act some supporting sur la protection de la vie privée, forms may have been removed quelques formulaires secondaires from this thesis. ont été enlevés de cette these. While these forms may be included Bien que ces formulaires in the document page count, aient inclus dans la pagination, their removal does not represent il n'y aura aucun contenu manquant.
any loss of content from the thesis. Canada DALHOUSIEUNIVERSITY To comply with the Canadian Privacy Act the National Library of Canada has requested that the following pages be removed from this copy of the thesis: Preliminary Pages Examiners Signature Page (pii) Dalhousie Library Copyright Agreement (piii) Appendices Copyright Releases (if applicable) For the inspirational Dr. River, and Nummists everywhere. Visit http: //nummist.
iv TABLE OF CONTENTS LISTOFTABILES. << ¬ eee xx ABSTRACT. sce senee aiar are XXỈỈ ACKNOWLEDGMENTS. ¬ eee eee oe ee es» XXỈỈ CHAPTER 2 NUMMSQUARED OVERVIEW AND COMPARISON .1 UNTYPED LAMBDA CALCULUS AND IMPROVEMENTS .2 SET THEORY, VON NEUMANNANDJONES.5 WELL-FOUNDEDNESS AND COEROION.ee eee 9 27 REFLECTION.
Q Q ee ee ee ee 10 2. ee HH ee ene 11 2. cc ee ee eee ee ee ee eens 12 CHAPTER4 WHERETO FIND THEFORMALPART. ee ee ee ees 17 6.
ee ee ee ee ee ee 17 63 BOOLEANS. cc ce ee ee es 17 6. Q Q Q Q Q ee ee ko 18 6. ee ko eee ee 19 6.8 WELL-FOUNDED RELATONS.1 SMALL FUNCTION EXTENSIONS.2 DOMAIN AND SPECIFIC RESULT OF A SMALL FUNC- TION EXTENSION .3 RANK OF A SMALL FUNCTION EXIENSION.4 IDENTITY SMALL FUNCTION EXTENSIONS.
ce ee eee en 29 7.6 DOMAIN, DOMAIN EXTENSION AND SPECIFIC RESULT OF A DOMAIN EXTENSION FAMIIY.7 DOMAIN, RANK AND VALIDITY OF A DOMAIN EXTENSION .8 DOMAIN EXTENSION IRRELEVANCE THEOREM .10 TAGGED SMALL FUNCTION EXTENSIONS.11 UNTAGGED, TAG IRRELEVANCE THEOREM, TAGGED AND TAGGABLE. ee ee et ee ee 4] 7.12 DOMAIN, DOMAIN EXTENSION, SPECIFIC RESULT AND RANK OF A TAGGED SMALL FUNCTION EXTENSION .13 IDENTITY TAGGED SMALL FUNCTION EXTENSIONS .14 COERCION OF A TAGGED SMALL FUNCTION EXTEN- SION, AND COERCION STABILITY THEOREM.15 RESULT OF A TAGGED SMALL FUNCTION EXTENSION .17 SOME TAGGED SMALL FUNCTION EXTENSIONS.18 LARGE FUNCTION EXTENSIONS AND TRUTH.19 SOME COMPUTATIONAL LARGE FUNCTION EXTENSIONS .20 SOME COMPUTATIONAL COMBINATIONS OF LARGE FUNCTION EXTENSIONS.21 SOME NON-COMPUTATIONAL LARGE FUNCTION EXTENSIONS AND COMBINATIONS.2 EXTENSION AND TRUTH OF A NORMALIZED LARGE FUNCTION .3 REDUCTION: COMPUTED OF A NORMALIZED LARGE FUNCTION.4 NORMAL FORM OF ANATURALNUMBER.5 QUOTED OF A NORMALIZED LARGEFUNCTION .6 UNQUOTED OF A NORMALIZED LARGE FUNCTION. eee eee ee ee es 87 8.8 SUBSTITUTION AND SUBSTITUTION THEOREM. ee ee ee ee et ee ene 88 8.12 DEFINITIONS, DEFINITION LISTS, MODULES AND ABSTRACTPROGRAMS.O ee HH HH HH ee ko 102 8.14 NORMAL FORM OFAPRIMITIVE.15 NORMAL FORM OF A NORMALIZED CONSTANT.16 NORMAL FORM OF A GLOBALNAME.18 NORMAL FORM OFALOCALNAME.19 LOCAL TUPLE ACCESSOR CHECK.20 NORMAL FORM OF A COMPUTATIONAL NON- NORMALIZED CONSTANT OR COMPUTATIONAL COMBINATION.
ee ee ee ees 108 8. ee ee es 114 8. 0 cee ee es 114 8.12 DEPENDENT PRODUCT RESULT .15 RECURSION RIGHT-HAND-SIDE. ee ee ee ee 120 8.21 NORMAL FORM OF A NON-COMPUTATIONAL NON- NORMALIZED CONSTANT OR NON-COMPUTATIONAL COMBINATION.
eee ee ee ee ens 121 8.3 UNARY UNIVERSAL QUANTIFICATION .4 SMALL UNIVERSAL QUANTIFICATION.5 EQUAISRIGHT-HAND-SIDE. cece eee eee 127 8.22 NORMAL FORM AND VALIDITY OF ALARGE FUNCTION .23 NORMAL FORM AND VALIDITY OF A DEFINITION, DEFINITION LIST OR ABSTRACT PROGRAM .25 SOME TRUE LARGE FUNCTION EXTENSIONS. ce eee eee eee eee 131 8. ee ee et ee ee 133 8.
ee ee et ee ee 134 8. ee ee ee ee es 136 8. ee ee eee 137 8. ee ee eee 138 8.
ee ee eee ee ee ee 142 8.ỘOOQ HQ HH ee 147 8.15 IF-THEN-ELSE. ee eee ee ee eee eee 150 8. ee ee eee 151 8. ce ee ee ee ee ee 152 8.
eee ee ee et ee 153 8. eee eee eee ee ee ee 154 8.26 SOME INFERENCES FROM TRUE LARGE FUNCTION EXTENSIONS. ce eee ee eee 156 8.27 SOME TRUE NORMALIZED LARGEFUNCTIONS.28 SOME INFERENCES FROM TRUE NORMALIZED LARGE FUNCTIONS. ee ee es 158 8.30 PROPOSITION AND VALIDITY OF A PROOF AND SOUNDNESSTHEOREM.32 PROOF UNQUOTED OF A NORMALIZED LARGEFUNCTION.
162 91 PREFACE TO THEFORMALPART.1 COQ TERMS, CONTEXTS, ENVI- RONMENTS, TYPE-CHECKING, REDUCTION, NORMAL FORMS AND CONVERTIBILITY.4 COQ DEPENDENT PRODUCTS, FUNCTIONS AND APPLICATIONS .6 COQ MODULES, COMMANDS AND GLOBAL DECLARATIONS .7 NAMING OF COQ MODULES AND GLOBALDECLARATONS. 167 913 NUMMSQUARED FORMALLY STYLE .1 MAKE DESIRED TYPES EXPLICIT USING TYPECASI1S.3 MAKE REUSABLE TERMS INTO SEPARATE GLOBAL DECLARATIONS .4 USE UNDERSCORE FOR HIERARCHI- CALNAMING.2 FUNDAMENTALS:OPERATORS:MAIN.O ee ee So 169 9.6 | CONNECTIVE BINARY OPERATORS .12 CONNECTIVE QUATERNARY OPERATORS .15 CONNECTIVE QUINARY OPERATORS. 172 93 EFUNDAMENTAILS:PROPOSITONS:MAIN. THECONSTANT PROPOSITIONAL PREDICATE.4 | BINARY PROPOSITIONAL PREDICATES .5 CONNECTTVE BINARY PROPOSITIONAL PREDICATES .6 | TRINARY PROPOSITIONAL PREDICATES.7 CONNECTIVE TRINARY PROPOSITIONAL PREDICATES.8 | QUATERNARY PROPOSITIONAL PREDICATES .9 CONNECTIVE QUATERNARY PROPOSITIONAL PREDICATES .10 QUINARY PROPOSITIONAL PREDICATES .11 _CONNECTIVE QUINARY PROPOSITIONAL PREDICATES.
176 FUNDAMENTALS: BOOLEANS: MAIN. cece e ee ee eee 176 9.6 CONNECTIVE BINARY BOOLEAN PREDICATES.9 | QUATERNARY BOOLEAN PREDICATES.10 CONNECTIVE QUATERNARY BOOLEAN PREDICATES.12 CONNECTIVE QUINARY BOOLEAN PREDICATES. cece 180 FUNDAMENTALS: NATURALS:MAIN. ABBREVIATIONS FOR SOME NATURAL NUMBERS.6 FUNDAMENTALS: NATURALS: EFFICIENT: MAIN .7 FUNDAMENTAIS:UNITS:MAIN.Q QQ ee kia 187 973 UNITEQUAIS.8 FUNDAMENTAIS:OPTIONALS:MAIN.
Q ee HH So 188 983 OPTIONALRELATEDTO .4 OPTIONAL RELATED TO, CONNECTIVE .9 OPTIONAL SELECT, TOELEMENT.9 FUNDAMENTALS: BOOLEANS: AND OPTIONALS .10 FUNDAMENTALS: CHOICES:MAIN.11 FUNDAMENTALS: PAIRS: MAIN .12 FUNDAMENTALS: LISTS: MAIN. eee eee eee 202 9. LH HQ HH HH na 204 9.Q Q Q Q Q HQ HH HH K 205 9128 2 LISTNON-EMPTY.OQ Q Q eee ee ko 206 9. ee eee ee he 206 9.12 THELIST SINGLETON OPERATOR .13 THE LIST SINGLETON BINARY OPERATOR.
eee ee ee ee 208 9.20 NON-EMPTY LIST RELATED TO, CONNECTIVE.21 NON-EMPTY LIST SINGLETON .23 THE NON-EMPTY LIST HEAD OPERATOR. ee ee eee 212 9.13 FUNDAMENTALS: OPTIONALS:ANDLISTS.15 FUNDAMENTAIS:NATURALS:ANDLISTS.16 FUNDAMENTALS: NATURALS: EFFICGIENT:ANDHISIS.2 EFFICIENT NATURAL NUMBERLISTS .3 EFFICIENT NATURAL NUMBER LIST EQUALS .17 FUNDAMENTALS: PAIRS:ANDHISTS.2 PAIROF HEAD AND REST TO NON-EMPTYLIST .18 FUNDAMENTAILS:LISTS:SELECT.Q Q Q Q HH HQ HH ees 217 9.6 LIST SELECT TO ELEMENTSIMPLE.7 LIST SELECT, TO ELEMENTITERATE.9 LIST SELECT, BY ELEMENT, SIMPLE .10 LIST SELECT, BY ELEMENT, ITERATE .11 LIST SELECT, BY ELEMENT, INTRODUCED .12 LIST SELECT, BY ELEMENT, TERMINATED .13 LIST SELECT, BY ELEMENT, SEPARATED .14 LIST SELECT, BY ELEMENT, TOELEMENT.15 LIST SELECT, BY ELEMENT, TO ELEMENT, SIMPLE .16 LIST SELECT, BY ELEMENT, TO ELEMENT, ITERATE .17 LIST SELECT, BY PREFIX, RECURSIVE .19 LIST SELECT, BY PREFRX SIMPLE.20 LIST SELECT, BY PREFIX, ITERATE .21 LIST SELECT, BY PREFIX, TOELEMENT .22 LIST SELECT, BY PREFIX, TO ELEMENT, SIMPLE .23 LIST SELECT, BY PREFIX, TO ELEMENT, ITERATE. ce ee ee es 228 9.31 LIST INTERSECTION, FIRST, CONNECTIVE .32 LISTINTERSECTION,NON-EMPTY.33 LIST INTERSECTION, NON-EMPTY, CONNECTIVE .34 LISTTO BOOLEAN PREDICATE.19 FUNDAMENTALS: OPTIONALS: AND LISTS SELECT.20 FUNDAMENTALS: LISTFUNCTIONS:MAIN.3 LISTFUNCTION TO BOOLEAN PREDICATE .5 SIMPLE LISTFUNCTION TO BOOLEAN PREDICATE .7 SIMPLE LISTFUNCTION ITERATE, CURRY2.8 SIMPLE LISTFUNCTION ITERATE, CUMULATIVE .21 NUMMSQUARED: SYNTAX: ABSTRACT: MAIN .2 NUMMSQUARED DIGIT CHARACTERS.3 NUMMSQUARED DIGIT CHARACTER EQUALS.4 NUMMSQUARED IDENTIFIER START CHARACTERS .5 NUMMSQUARED IDENTIFIER START CHARAC- TER EQUAIS.6 NUMMSQUARED IDENTIFIER CONTINUE CHARACTERS.7 NUMMSQUARED IDENTIFIER CONTINUE CHARACTEREQUALS.9 NUMMSQUARED COMMENT EQUALS.10 NUMMSQUARED SIMPLE IDENTIFIERS .11 NUMMSQUARED SIMPLE IDENTIFIER EQUALS .13 NUMMSQUARED IDENTIFIER EQUALS .14 NUMMSQUARED SIMPLE IDENTIFIER TO NUMMSQUAREDIDENTIFIER.15 NUMMSQUARED NATURAL NUMBER PRIMITIVES .16 NUMMSQUARED NATURAL NUMBER PRIMI- TIVEEQUALS.17 NUMMSQUARED CHARACTER PRIMITIVES .18 NUMMSQUARED CHARACTER PRIMITIVE EQUALS .19 NUMMSQUARED STRING PRIMITIVES.20 NUMMSQUARED STRING PRIMITIVE EQUALS .23 NUMMSQUARED COMPUTATIONAL NORMAL- LZEDCONSTANIS.24 NUMMSQUARED NON-COMPUTATIONAL NORMALZEDCONSTANIS.25 NUMMSQUARED NORMALIZED CONSTANTS .26 NUMMSQUARED COMPUTATIONAL NON- NORMALIZED CONSTANIS.27 NUMMSQUARED NON-COMPUTATIONAL NON-NORMALIZED CONSTANTS.28 NUMMSQUARED NON-NORMALIZED CONSTANTS .30 NUMMSQUARED LARGE FUNCTIONS.31 NUMMSQUARED LOCAL TUPLE ACCESSOR LISTS .36 NUMMSQUARED ABSTRACT PROGRAMS. 266 CHAPTER 10 CONCLUSION Sn ee e ) 267 BIBLIOGRAPHY.
Y LIST OF TABLES 2.1 VON NEUMANN’S AXIOMATIZATION AND COMBINA- TORY LOGICROUGHIYCOMPARED. LIST OF FIGURES 7.1 SMALL FUNCTION EXTENSIONS ee © © © © © © ee ee 6 8 óc 98 lll ell ABSTRACT NummSquared Explained is the thesis version of the comprehensive formal docu- ment NummSquared 2006a0 Done Formally, which is available at http: //nummist. Set theory is the standard foundation for mathematics, but often does not include rules of reduction for function calls. Therefore, for computer science, the untyped lambda calculus or type theory is usually preferred.
The untyped lambda calculus (and several improvements on it) make functions fundamental, but suffer from non- terminating reductions and have partially non-classical logics. Type theory is a good foundation for logic, mathematics and computer science, except that, by making both types and functions fundamental, it is more complex than either set theory or the un- typed lambda calculus. This document proposes a new foundational formal language called NummSquared that makes only functions fundamental, while simultaneously ensuring that reduction terminates, having a classical logic, and attempting to follow set theory as much as possible. NummSquared builds on earlier works by John von Neumann in 1925 and Roger Bishop Jones in 1998 that have perhaps not received suffi- cient attention in computer science.
A soundness theorem for NummSquared is proved. Usual set theory, the work of Jones, and NummSquared are all well-founded. NummSquared improves upon the works of von Neumann and Jones by having reduc- tion and proof, by supporting computation and reflection, and by having an interpreter called NsGo (work in progress) so the language can be practically used. NummSquared is variable-free.
For enhanced reliability, NsGo is an F#/C# .NET assembly that is mostly automati- cally extracted from a program of the Coq proof assistant. As a possible step toward making formal methods appealing to a wider audience, NummSquared minimizes constraints on the logician, mathematician or programmer. Because of coercion, there are no types, and functions are defined and called without proof, yet reduction terminates. NummSquared supports proofs as desired, but not required.
ACKNOWLEDGMENTS Many thanks to Dr. Malcolm Heywood, my PhD supervisor at Dalhousie Univer- sity, for unbounded good ideas, patience and support throughout the lengthy PhD process. Thanks to Dr. Peter Hitchcock for insights into software engineering and pro- gram correctness.
Thanks to Dr. Anthony Cox for discussions about programming lan- guages, and for suggesting many useful improvements to the thesis. Thanks to Dr. Paul Gilmore for discussions about his Intensional Type Theory, and for suggesting many useful improvements to the thesis.
Thanks to Hugo Herbelin for discussions about Coq and type theory, and for suggesting many useful improvements to the thesis.
