The Functional Approach to Programming

Cover
Description Page
Title Page
Copyright Page
Table of Contents
Preface
Introduction
I Basic Principles
	1 Expressions
		1.1 Expressions and Definitions
			1.1.1 Expressions
			1.1.2 Definitions
			1.1.3 Local Definitions
		1.2 Elementary Types
			1.2.1 Integers
			1.2.2 Floating-Point Numbers
			1.2.3 Floating Mode
			1.2.4 Booleans
			1.2.5 Character Strings
			1.2.6 Characters
		1.3 Cartesian Product
		1.4 Functions
			1.4.1 Defining Simple Functions
			1.4.2 Function Expressions
			1.4.3 Higher Order Function Expressions
			1.4.4 Recursive Functions
			1.4.5 Mutually Recursive Functions
			1.4.6 Functions Defined by Case
			1.4.7 The function Construction
			1.4.8 The match with Construction
		1.5 Polymorphism
			1.5.1 Type Variables
			1.5.2 Type Synthesis
		1.6 About Syntax
			1.6.1 Application Notation
			1.6.2 Syntactic Analysis of Caml Expressions
			1.6.3 Infix Operators Defined by the User
		1.7 Scope of Identifiers
		1.8 More about Function Types: Equivalent Function Spaces
			1.8.1 The Types of Predefined Operators
		1.9 Examples: Expressive Power
			1.9.1 Bounded Iterations
			1.9.2 Unbounded Iterations
			1.9.3 Binary Method
			1.9.4 Newtons Method
			1.9.5 About Iteration
			1.9.6 Summations
		1.10 Summary
	2 Data Structures
		2.1 Record or Named Cartesian Products
		2.2 Sums with Constructors
			2.2.1 Constant Constructors
			2.2.2 Constructors with Arguments
			2.2.3 Types with Only One Constructor and Abbreviations ...
			2.2.4 Recursive Types
			2.2.5 Polymorphic Types
			2.2.6 Lists
			2.2.7 Recursive Definitions of Values
			2.2.8 Abstract Types
			2.2.9 Concrete Syntax of Data Structures
			2.3 Lists
		2.3.1 General Functional for Lists
			2.3.2 Partitioning and Sorting
			2.3.3 Representing Sets by Lists
			2.3.4 Searching in a List
		2.4 Summary
	3 Semantics
		3.1 Evaluation
			3.1.1 Evaluation as Rewriting Expressions
			3.1.2 Evaluation Strategies
			3.1.3 How to Deal with Recursion
			3.1.4 Another Way of Handling Recursion
			3.1.5 Behavior of Evaluation Processes
		3.2 Defining Strategies
			3.2.1 The Caml Strategy, or Evaluation by Value
			3.2.2 Another Strategy: Delayed Evaluation
			3.2.3 Extending Delayed Evaluation to Data Structures
		3.3 Program Semantics
			3.3.1 Rewrite Semantics
			3.3.2 Denotational Semantics
		3.4 Proving the Correctness of Programs
			3.4.1 Equational Reasoning
			3.4.2 Taking Functions as Values into Account
			3.4.3 Reasoning by Case
			3.4.4 Reasoning by Induction
			3.4.5 Proof of Termination
			3.4.6 First Example: Mirror Image of Trees
			3.4.7 Second Example: Associativity of append
			3.4.8 Example: Using Generalization
			3.4.9 Example: Using Lemmas
			3.4.10 Example: Proof under Hypothesis or Proof by Assumption
		3.5 Typing Expressions
		3.6 Summary
		3.7 To Learn More
	4 Imperative Aspects
		4.1 Exceptions
			4.1.1 Examples of Exceptions
			4.1.2 Defining Exceptions
			4.1.3 Creating an Exceptional Value
			4.1.4 Filtering Exceptional Values
			4.1.5 Using Exceptions
		4.2 Input and Output
			4.2.1 Sequence
			4.2.2 The Type unit
			4.2.3 I/O Functions
			4.2.4 Example: Print Function
			4.2.5 Example: Interaction
		4.3 Character Streams
			4.3.1 Constructing Streams
		4.4 Modifiable Data Structures
			4.4.1 Vectors
			4.4.2 Records with Modifiable Fields
			4.4.3 References
			4.4.4 Circular Lists
			4.4.5 Doubly Linked Lists
			4.4.6 Comparing with Pascal, C, and Lisp
		4.5 Semantics of Destructive Operations
		4.6 Summary
II Applications
	5 Formal Terms, Pattern Matching, Unification
		5.1 Trees
			5.1.1 A Few Useful Functions
			5.1.2 Functional for Trees
			5.1.3 Occurrences in a Tree
			5.1.4 Trees and Abstract Syntax
		5.2 Terms with Variables
			5.2.1 Introducing Variables
			5.2.2 Substitutions
			5.2.3 Filtering and Pattern Matching
			5.2.4 Unification
		5.3 Application: Type Synthesis
			5.3.1 Constraints on Types
			5.3.2 Generating Constraints
			5.3.3 Constraint Resolution
		5.4 Summary
		5.5 To Learn More 1626 Balanced Trees
	6.1 Binary Trees
		6.2 Tree Traversals and Morphisms
		6.3 Order and Pre-Order Relations
		6.4 Binary Search Trees
			6.4.1 Searching for an Element
			6.4.2 Adding an Element
			6.4.3 Adding an Element to the Root
			6.4.4 Removing an Element
		6.5 Balanced Trees
			6.5.1 Rotations
			6.5.2 AVL TYees
			6.5.3 Adding Elements to an AVL Tree
		6.5.4 Removing Elements from an AVL Tree
		6.6 Dictionaries
		6.7 Ordered Sets
		6.8 Functional Queues
		6.9 Summary
		6.10 To Learn More
	7 Graphs and Problem Solving
		7.1 Algorithms to Explore Graphs
			7.1.1 Naive Breadth-First Search
			7.1.2 Naive Depth-First Search
			7.1.3 Optimal Breadth-First Search
			7.1.4 Variations and Improvements
			7.1.5 Optimal Depth-First Search
			7.1.6 Exhaustive Search
			7.1.7 Computing Connected Components
		7.2 The Red Donkey
		7.3 The Game of Solitaire
		7.4 Summary
		7.5 To Learn More
	8 Syntactic Analysis
		8.1 Regular Expressions
		8.2 Context-Free Grammar
			8.2.1 Types and Values
			8.2.2 Ambiguities
		8.3 Recognizers
			8.3.1 Recognizer Constructors
			8.3.2 Limitations
			8.3.3 Recognizers for Regular Expressions
			8.3.4 Recognizers for Grammars
			8.3.5 Various Derived Forms
		8.4 Analysis = Recognition + Values
			8.4.1 Constructors for Analyzers
			8.4.2 A Lexical Analyzer
			8.4.3 Analyzer for Nested Parentheses
			8.4.4 Derived Forms and Higher Order Analyzers
			8.4.5 An Analyzer for Arithmetic Expressions
			8.4.6 Predictive Analysis
		8.5 Streams and Pattern Matching
			8.5.1 Streams
			8.5.2 Stream Pattern Matching
			8.5.3 Lexical Analysis by Stream Pattern Matching
			8.5.4 Higher Order Analyzers
			8.5.5 Syntactic Analysis by Stream Pattern Matching
		8.6 Compiling Regular Expressions
			8.6.1 Finite Automata
			8.6.2 Abstract Syntax Trees for Regular Expressions
			8.6.3 Computing Null, First, and Last
			8.6.4 Computing follow
			8.6.5 Representing Automata
			8.6.6 Computing Automata
			8.6.7 Interpreting a Deterministic Finite Automaton
		8.7 Summary
		8.8 To Learn More
			8.8.1 Comparing with Other Methods of Syntactic Analysis . . .
			8.8.2 Further References
	9 Geometry and Drawings
		9.1 Meet MLgraph
			9.1.1 Geometric Plane
			9.1.2 Geometric Elements
			9.1.3 Constructing Images
		9.2 Drawing Trees
			9.2.1 Drawing Principles
			9.2.2 Computing the Reduction Coefficients
		9.3 Tiling
			9.3.1 The Method Used
			9.3.2 Generating Transformations
			9.3.3 Colored Tilings
			9.3.4 Handling Transformations Formally
		9.4 Tiling a Hyperbolic Plane
			9.4.1 Complex Arithmetic
			9.4.2 Hyperbolic Isometries
			9.4.3 Eschers Fish
			9.4.4 The Isometry Group
			9.4.5 Eschers Circle Limit III
		9.5 Summary
		9.6 To Learn More
			9.6.1 About PostScript
			9.6.2 About Drawing Trees
			9.6.3 About Tilings
	10 Exact Arithmetic
		10.1 Representing Integers by Lists
			10.1.1 Choosing a Base
			10.1.2 Operations with the Least Significant Digit at the Head . .
			10.1.3 Comparisons as Operations
			10.1.4 Division as an Operation
			10.1.5 A Type for Natural Numbers (Integers for Counting) ....
			10.1.6 Exponentiation
			10.1.7 Computing Square Roots
			10.1.8 Reading and Printing Natural Numbers
		10.2 Other Representations of Natural Numbers
			10.2.1 Doubly Linked Circular Lists
			10.2.2 Arrays
		10.3 Signed Integers, Both Negative and Positive
		10.4 Rational Numbers
		10.5 An Application: Computing 7r
		10.6 Summary
Part III Implementation
	11 Evaluation
		11.1 Evaluation with the Help of Environments
		11.2 Writing an Evaluator in Caml
		11.3 Evaluation by Necessity = Lazy Evaluation = Delayed Evaluation
		11.4 Summary
		11.5 To Learn More
	12 Compilation
		12.1 A Simplified Model of Computer Memory
		12.2 Implementation of Data Structures
			12.2.1 Coding Data
			12.2.2 CONS as an Operation
			12.2.3 Sharing Data
			12.2.4 Representing Other Types of Data
			12.2.5 Recovering Allocated Memory
		12.3 Producing Code
			12.3.1 List of Instructions
			12.3.2 Principle behind Compilation
			12.3.3 About the Compilation Scheme
		12.4 Implementation
			12.4.1 Code Simulation
			12.4.2 Producing Code
		12.5 Examples
		12.6 Summary
	13 Type Synthesis
		13.1 Type Rules
			13.1.1 Polymorphism by Substitution
			13.1.2 Parametric Polymorphism
			13.1.3 Generalizing Type Schemes
			13.1.4 Instantiation
			13.1.5 Type Rules with Parametric Polymorphism
		13.2 Writing a Program to Synthesize Types
			13.2.1 Generalizing a Type
			13.2.2 Instantiation
			13.2.3 A Few Utilities
			13.2.4 Main Function
			13.2.5 Examples
		13.3 Synthesizing Types by Destructive Unification
			13.3.1 Destructive Unification
			13.3.2 Instantiation and Generalization
			13.3.3 The Algorithm for Synthesis
		13.4 Summary
		13.5 To Learn More
Quick Reference to the Syntax of Caml Light
How to Get Caml, MLgraph, and the Examples
References
Index