Contents Preface to the Second Edition Preface to the First Edition I Judgments and Rules IEW 1 Abstract Syntax 3 1.1 Abstract Syntax Trees..... 4 1.2 Abstract Binding Trees 6 1.3 Notes.·.·.···· 10 2 Inductive Definitions 13 2.1 Judgments 13 2.2 Inference Rules 44444 14 2.3 Derivations....·.·. 15 2.4 Rule Induction..。.·...···· 16 2.5 Iterated and Simultaneous Inductive Definitions... 18 2.6 Defining Functions by Rules..,. 19 2.7 Notes.········ 20 3 Hypothetical and General Judgments 23 3.1 Hypothetical Judgments 23 3.1.1 Derivability ....... 23 3.1.2 Admissibility··..·...· 25 3.2 Hypothetical Inductive Definitions ... 26 3.3 General Judgments...············ 3.4 Generic Inductive Definitions 29 3.5 Notes...··············· 30PREVIEW Contents Preface to the Second Edition iii Preface to the First Edition v I Judgments and Rules 1 1 Abstract Syntax 3 1.1 Abstract Syntax Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Abstract Binding Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2 Inductive Definitions 13 2.1 Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.4 Rule Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.5 Iterated and Simultaneous Inductive Definitions . . . . . . . . . . . . . . . . . . . . . 18 2.6 Defining Functions by Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.7 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3 Hypothetical and General Judgments 23 3.1 Hypothetical Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1.1 Derivability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1.2 Admissibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2 Hypothetical Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.3 General Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3.4 Generic Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30