计算机科学课之-集合论与代数:数学建模导论( 2013 ) pdf版

Set Theory and Algebra in Computer Science A Gentle Introduction to Mathematical Modeling
Jos´e Meseguer University of Illinois at Urbana-Champaign Urbana, IL 61801, USA
c
Jos´e Meseguer, 2008–2013; all rights reserved.
August 28, 2013

目录
Contents
I BasicSetTheory 5
1 IntroductiontoPartI 7
2 SetTheoryasanAxiomaticTheory 11
3 TheEmptySet,Extensionality,andSeparation 15

3.1 The Empty Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

3.2 Extensionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

3.3 The Failed Attempt of Comprehension . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3.4 Separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
4 Pairing,Unions,Powersets,andInfinity 19

4.1 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

4.2 Unions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.3 Powersets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

4.4 Infinity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
5 Relations,Functions,andFunctionSets 29

5.1 Relations and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

5.2 Formula, Assignment, and Lambda Notations . . . . . . . . . . . . . . . . . . . . . . . . 30

5.3 Images . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

5.4 Composing Relations and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

5.5 Abstract Products and Disjoint Unions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

5.6 Relating Function Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
6 SimpleandPrimitiveRecursion,andthePeanoAxioms 43

6.1 Simple Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

6.2 Primitive Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

6.3 The Peano Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
7 BinaryRelationsonaSet 49

7.1 Directed and Undirected Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

7.2 Transition Systems and Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

7.3 Relation Homomorphisms and Simulations . . . . . . . . . . . . . . . . . . . . . . . . . 52

7.4 Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

7.5 Sups and Infs, Complete Posets, Lattices, and Fixpoints . . . . . . . . . . . . . . . . . . . 57

7.6 Equivalence Relations and Quotients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

7.7 Constructing Z and Q . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
8 SetsComeinDifferentSizes 65

8.1 Cantor’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

8.2 The Schroeder-Bernstein Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

9 IndexedSets 67

9.1 Indexed Sets are Surjective Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

9.2 Constructing Indexed Sets from other Indexed Sets . . . . . . . . . . . . . . . . . . . . . 71

9.3 Indexed Relations and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
10 FromIndexedSetstoSets,andtheAxiomofChoice 75

10.1 Some Constructions Associating a Set to an Indexed Set . . . . . . . . . . . . . . . . . . 75

10.2 The Axiom of Choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
11 Well-FoundedRelations,andWell-FoundedInductionandRecursion 83

11.1 Well-Founded Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83

11.1.1 Constructing Well-Founded Relations . . . . . . . . . . . . . . . . . . . . . . . . 84

11.2 Well-Founded Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

11.3 Well-Founded Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86

11.3.1 Examples of Well-Founded Recursion . . . . . . . . . . . . . . . . . . . . . . . . 86

11.3.2 Well-Founded Recursive Definitions: Step Functions . . . . . . . . . . . . . . . . 86

11.3.3 The Well-Founded Recursion Theorem . . . . . . . . . . . . . . . . . . . . . . . 88
II UniversalAlgebra,EquationalLogicandTermRewriting 89

12 Algebras 91

12.1 Unsorted Σ-Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

12.2 Many-Sorted Σ-Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

12.3 Order-Sorted Σ-Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

12.4 Terms and Term Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96

12.5 A Set-Theoretic Construction of Term Algebras . . . . . . . . . . . . . . . . . . . . . . . 97

12.6 More on Order-Sorted Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
13 TermRewritingandEquationalLogic 103

13.1 Terms, Equations, and Term Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103

13.1.1 Term Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

13.1.2 Equational Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105

13.2 Term Rewriting and Equational Reasoning Modulo Axioms . . . . . . . . . . . . . . . . . 106

13.3 Sort-Decreasingness, Confluence, and Termination . . . . . . . . . . . . . . . . . . . . . 108

13.4 Canonical Term Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

13.5 Sufficient Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
14 ConditionalRewritingandConditionalEquationalLogic 115

14.1 Conditional Term Rewriting and Conditional Equality . . . . . . . . . . . . . . . . . . . . 115

14.1.1 Conditional Term Rewriting and Conditional Equality as Inference . . . . . . . . . 116

14.1.2 Proofs for Conditional Term Rewriting and Conditional Equality . . . . . . . . . . 117

14.2 Conditional Term Rewriting Modulo Axioms . . . . . . . . . . . . . . . . . . . . . . . . 120

14.3 Executability Conditions for Conditional Rewrite Theories . . . . . . . . . . . . . . . . . 121

14.3.1 Confluence and the Church-Rosser Property in the Conditional Case . . . . . . . . 121

14.3.2 Operational Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122

来了,老弟
-------------    本文结束  感谢您的阅读    -------------
0%