You are previewing Nominal Sets.
O'Reilly logo
Nominal Sets

Book Description

Nominal sets provide a promising new mathematical analysis of names in formal languages based upon symmetry, with many applications to the syntax and semantics of programming language constructs that involve binding, or localising names. Part I provides an introduction to the basic theory of nominal sets. In Part II, the author surveys some of the applications that have developed in programming language semantics (both operational and denotational), functional programming and logic programming. As the first book to give a detailed account of the theory of nominal sets, it will be welcomed by researchers and graduate students in theoretical computer science.

Table of Contents

  1. Cover
  2. Half Title
  3. Title Page
  4. Copyright
  5. Dedication
  6. Contents
  7. Preface
  8. 0 Introduction
    1. 0.1 Atomic names
    2. 0.2 Support and freshness
    3. 0.3 Abstract syntax with binders
    4. 0.4 Name abstraction
    5. 0.5 Orbit-finiteness
    6. 0.6 Alternative formulations
    7. 0.7 Prerequisites
    8. 0.8 Notation
  9. Part One: Theory
    1. 1. Permutations
      1. 1.1 The category of G-sets
      2. 1.2 Products and coproducts
      3. 1.3 Natural numbers
      4. 1.4 Functions
      5. 1.5 Power sets
      6. 1.6 Partial functions
      7. 1.7 Quotient sets
      8. 1.8 Finite permutations
      9. 1.9 Name symmetries
      10. Exercises
    2. 2. Support
      1. 2.1 The category of nominal sets
      2. 2.2 Products and coproducts
      3. 2.3 Natural numbers
      4. 2.4 Functions
      5. 2.5 Power sets
      6. 2.6 FM-sets
      7. 2.7 Failure of choice
      8. 2.8 Partial functions
      9. 2.9 Quotient sets
      10. 2.10 Non-finite support
      11. Exercises
    3. 3. Freshness
      1. 3.1 Freshness relation
      2. 3.2 Freshness quantifier
      3. 3.3 Fresh names
      4. 3.4 Separated product
      5. Exercises
    4. 4. Name abstraction
      1. 4.1 α-Equivalence
      2. 4.2 Nominal set of name abstractions
      3. 4.3 Concretion
      4. 4.4 Functoriality
      5. 4.5 Freshness condition for binders
      6. 4.6 Generalized name abstraction
      7. 4.7 Many sorts of names
      8. Exercises
    5. 5. Orbit-finiteness
      1. 5.1 Orbits
      2. 5.2 Atomic nominal sets
      3. 5.3 Finitely presentable objects
      4. 5.4 Orbit-finite subsets
      5. 5.5 Uniformly supported subsets
      6. Exercises
    6. 6. Equivalents of Nom
      1. 6.1 Sets with name swapping
      2. 6.2 Continuous G-sets
      3. 6.3 The Schanuel topos
      4. 6.4 Named sets
      5. Exercises
  10. Part Two: Applications
    1. 7. Inductive and coinductive definitions
      1. 7.1 Inductively defined subsets
      2. 7.2 Rule induction
      3. 7.3 Equivariant rules
      4. 7.4 Tarski’s fixed-point theorem
      5. 7.5 Equivariant fixed-points
      6. 7.6 Coinductively defined subsets
      7. Exercises
    2. 8. Nominal algebraic data types
      1. 8.1 Signatures
      2. 8.2 α-Equivalence
      3. 8.3 Algebraic functors
      4. 8.4 Initial algebra semantics
      5. 8.5 Primitive recursion
      6. 8.6 Induction
      7. Exercises
    3. 9. Locally scoped names
      1. 9.1 The category of nominal restriction sets
      2. 9.2 Products and coproducts
      3. 9.3 Functions
      4. 9.4 λν-Calculus
      5. 9.5 Free nominal restriction sets
      6. 9.6 ν-Calculus
      7. 9.7 Total concretion
      8. Exercises
    4. 10. Functional programming
      1. 10.1 Types of names
      2. 10.2 Name abstraction types
      3. 10.3 Dynamically allocated names
      4. 10.4 Name swapping
      5. 10.5 Freshness relation
      6. 10.6 Name abstraction expressions
      7. 10.7 Name abstraction patterns
      8. 10.8 λFML
      9. 10.9 Type assignment
      10. 10.10 Contextual equivalence
      11. 10.11 Step-indexed logical relation
      12. 10.12 Abstractness
      13. 10.13 Purity
      14. Exercises
    5. 11. Domain theory
      1. 11.1 Nominal posets
      2. 11.2 Discontinuity of name abstraction
      3. 11.3 Uniform directed complete posets
      4. 11.4 Recursive domain equations
      5. 11.5 Nominal Scott domains
      6. Exercises
    6. 12. Computational logic
      1. 12.1 Unification
      2. 12.2 Term rewriting
      3. 12.3 Logic programming
      4. Exercises
  11. References
  12. Index of notation
  13. Index