Type Theory And Formal Proof.

2y ago
23 Views
2 Downloads
1.50 MB
7 Pages
Last View : 5d ago
Last Download : 4m ago
Upload by : Gideon Hoey
Transcription

TYPE THEORY AND FORMAL PROOFAn IntroductionROB N E DERPELTEindhoven University of Technology,The NetherlllndsH E RMAN G E UVERSRlldboud University Nijmegen.andEindhoven University l!f Tech nology,The NetherlandsUCAMBRIDGE'iU NIVERSITY PRESS

ContentsForeword, by Henk BarendregtPrefaceAcknowledgementsGreek alphabetpage xiiixvXXVllxxviii1Untyped lambda calculus1.1 Input -output behaviour of functions1.2 The essence of fu nctions1.3 Lambda-terms1.4 Free and bound variables1.5 Alpha conversion1.6 Substitution1.7 Lambda-terms modulo a-equivalence1.8 Beta reduction1.9 Normal forms and confluence1.10 Fixed Point Theorem1.11 Conclusions1.12 Furt her readingExercises11248911141619242627292Simply typed lambda calculus2.1 Adding types2.2 Simple types2.3 Church-typing and Curry-typing2.4 Derivation rules for Church 's A-t2.5 Different form ats for a derivation in A-t2.6 Kinds of problems to be solved in type theory2.7 Well-typedness in A-t2.8 Type Checking in A-t2.9 Term Finding in A-t33333436394446475051

VlllContents2.10 General properties of ).--- 2.11 Reduction and ).--- 2.12 Consequences2.13 Conclusions2.14 Further readingExercises5359636465663Second order typed lambda calculus3.1 Type-abstraction and type-application3.2 II-types3.3 Second order abstraction and application rules3.4 The system ),23.5 Example of a derivation in ),23.6 Properties of ),23.7 Conclusions3.8 Further readingExercises696971727376788080824Types dependent on types4.1 Type constructors4.2 Sort-rule and var-rule in ). 4.3 The weakening rule in ). 4.4 The formation rule in ). 4.5 Application and abstraction rules in4.6 Shortened derivations4.7 The conversion rule4.8 Properties of ). 4.9 Conclusions4.10 Further readingExercises). 8585889093949597991001001015Types dependent on terms5.1 The missing extension5.2 Derivation rules of ).P5.3 An example derivation in ).P5.4 Minimal predicate logic in ).P5.5 Example of a logical derivation in ).P5.6 Conclusions5.7 Further readingExercises1031031051071091151181191216The Calculus of Constructions6.1 The system )'C6.2 The ).-cube123123125

Contents6.36.46.5Properties of ACConclusionsFurther readingExercises7T he encoding of logical not ions in AC7.1 Absurdity and negation in type t heory7.2 Conjunction and disjunction in type theory7.3 An example of propositional logic in AC7.4 Classical logic in AC7.5 Predicate logic in AC7.6 An example of predicate logic in AC7.7 Conclusions7.8 Further readingExercises8D efini tionsThe nature of definitionsInductive and recursive definitionsThe format of definitionsInstantiations of definitionsA formal format for definitionsDefinitions depending on assumptionsGiving names to proofsA general proof and a specialised versionMathematical statements as formal definitionsConclusionsFurther 19Extension of AC w ith definit ions9.1 Extension of AC to the system ADo9.2 Judgements extended with definitions9.3 The rule for adding a definition9.4 The rule for instantiating a defin ition9.5 Definition unfolding and 5-conversion9.6 Examples of 5-conversion9.7 The conversion rule extended with 9.8 The derivation rules for ADo9.9 A closer look at the derivation rules of ADo9.10 Conclusions9.11 Further 89189190192193197200202203204206207208

xContents10Rules and properties of AD10.1 Descriptive versus primitive definitions10.2 Axioms and axiomatic notions10.3 Rules for primitive definitions10.4 Properties of AD10.5 Normalisation and confluence in AD10.6 Conclusions10.7 Further style natural deduction in AD11.1 Formal derivations in AD11 .2 Comparing formal and flag-style AD11.3 Conventions about fl ag-style proofs in AD11 .4 Introduction and elimination rules11.5 Rules for constructive propositional logic11.6 Examples of logical derivations in AD11 .7 Suppressing unaltered parameter lists11.8 Rules for classical propositional logic11.9 Alternative natural deduction rules for V11.10 Rules for constructive predicate logic11.11 Rules for classical predicate logic11.12 Conclusions11.13 Further 4925225325412Mathematics in AD: a first attempt12.1 An example to start with12.2 Equality12.3 The congruence property of equality12.4 Orders12.5 A proof about orders12.6 Unique existence12.7 The descriptor L12.8 Conclusions12.9 Further 3Sets13.113 .213.313.4279279282287288and subsetsDealing with subsets in ADBasic set-theoretic notionsSpecial subsetsRelations

Contentsxi13.5 Maps13.6 Representation of mathematical notions13.7 Conclusions13.8 Further readingExercises29129529629730214N umbers and arithmetic in AD14.1 The Peano axioms for natural numbers14.2 Introducing integers the axiomatic way14.3 Basic properties of the 'new' N14.4 In teger addition14.5 An example of a basic computation in AD14.6 Arithmetical laws for addition14.7 Closure under addition for natural and negative numbers14.8 Integer subtraction14.9 The opposite of an integer14.10 Inequality relations on Z14.11 Multiplication of integers14.12 Divisibility14.13 Irrelevance of proof14.14 Conclusions14.15 Further 3533834034134334415An elaborated example15.1 Formalising a proof of Bezout's Lemma15.2 Preparatory work15.3 P art I of the proof of Bezout 's Lemma15.4 Part II of the proof15.5 Part III of the proof15.6 The holes in the proof of Bezout's Lemma15.7 The Minimum Theorem for Z15.8 The Division Theorem15.9 Conclusions15.10 Further 7616Further perspectives16.1 Useful applications of AD16.2 Proof assistants based OIl type theory16.3 Future of the field16.4 Conclusions16.5 Further reading379379380384386387

ContentsXliAppendixA.1A.2A.3A.4A Logic in ADConstructive propositional logicClassical propositional logicConstructive predicate logicClassical predicate logicAppendix BArithmetical axioms, definitions and lemmas391391393395396397Appendix C Two complete example proofs in ADC.1 Closure under addition in NC.2 The Minimum Theorem403403405Derivation rules for AD409Appendix DReferencesIndex of namesIndex of definitionsIndex of symbolsIndex of subjects411419421423425

8.2 Inductive and recursive definitions 167 8.3 The format of definitions 168 8.4 Instantiations of definitions 170 8.5 A formal format for definitions 172 8.6 Definitions depending on assumptions 174 8.7 Giving names to proofs 175 8.8 A general proof and a specialised version 178 8.9 Mathematical statements as formal definitions 180

Related Documents:

PROOF MARKS: BELGIAN PROOF MARKSPROOF MARKS: BELGIAN PROOF MARKS, cont. BELGIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1852 Liege provisional black powder proof for breech loading guns and rifled barrels - Liege- double proof marking for unfurnished barrels - Liege- triple proof provisional marking for

since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARKS: ITALIAN PROOF MARKS, cont. ITALIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1951 Brescia provisional proof for all guns since 1951 Gardone provisional proof for all guns

2154 PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARK CIRCA PROOF HOUSE TYPE OF PROOF AND GUN since 1950 E. German, Suhl repair proof since 1950 E. German, Suhl 1st black powder proof for smooth bored barrels since 1950 E. German, Suhl inspection mark since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont.

PROOF MARKS: GERMAN PROOF MARKSPROOF MARKS: GERMAN PROOF MARKS, cont. GERMAN PROOF MARKS Research continues for the inclusion of Pre-1950 German Proofmarks. PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1952 Ulm since 1968 Hannover since 1968 Kiel (W. German) since 1968 Munich since 1968 Cologne (W. German) since 1968 Berlin (W. German)

spectacular example is Gonthier's formal proof of the four-color theorem. His starting point is the second-generation proof by Robertson et al. Although the traditional proof uses a computer and Gonthier uses a computer, the two computer processes differ from one another in the same way that a traditional proof differs from a formal proof.

2. Lubin-Tate spaces 45 2.1. The height of a formal A-module 46 2.2. Lubin-Tate spaces via formal group laws 49 2.3. Lazard's theorem for formal A-modules 52 2.4. Proof of the lemma of Lazard and Drinfeld 60 2.5. Consequences for formal A-modules 66 2.6. Proof of representability of Lubin-Tate spaces 76 3. Formal schemes 82 3.1. Formal .

Type theory [58] was introduced by Per Martin-L of with the intention of providing a foundation for constructive mathematics [69]. A part of constructive mathe-matics is type theory itself, hence we should be able to say what type theory is using the formal language of type theory. In addition, metatheoretic properties

1. Community using formal proofs is relatively small Market for formal proofs is small - proof technology not widely used in software - proof technology not widely used in science and math - proof technology not widely used in education Formal proving is still hard work - expansion factor - shallow base of basic mathematical facts