# Type Theory And Formal Proof.

2y ago
23 Views
1.50 MB
7 Pages
Last View : 5d ago
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

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 diﬀer from one another in the same way that a traditional proof diﬀers 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