πŸ—„οΈ
math-debrief
  • Math Debrief
  • Math: TIMELINE
  • 100-fundamentals
    • debrief-name: math section-code: 000 section-name: general section-desc: Elementary topics pervasive
      • About Mathematics
      • abstraction-in-math
      • About Math
      • Axiom schema
      • Basic concepts in math
      • Collections
      • Elementary concepts in objects
      • Elements of mathematics
      • math-as-a-language
      • Mathematical structures
      • List of mathematics-based methods
      • Mathematics and Reality
      • Mathematics: General
      • Controversial mathematics
      • the-elements-of-math
      • What is mathematics
    • The foundation of mathematics
      • Mathematical foundations
      • Foundations of Mathematics
      • Axiomatization of mathematics
      • Foundational crisis of mathematics
      • Foundations
      • Hilbert's problems
      • impl-of-math-in-set-theory
      • GΓΆdel's Incompleteness Theorem
      • Theorems in the foundations of mathematics
      • The list of FOM candidates
      • Logicism
    • Philosophy of mathematics
      • Constructive mathematics
      • Constructive mathematics
      • Metamathematics
      • Philosophy of mathematics
      • Schools of mathematics
    • terms
      • Terms
      • Arithmetic
      • Axiom
      • The Axiomatic Method
      • discrete-math
      • 201 Discrete mathematics
      • Euclidean space
      • Formal system
      • Function
      • Generalization
      • Geometry
      • Higher-order
      • Impredicativity
      • Level of measurement
      • Mathematical definition
      • FAQ
      • Mathematical function
      • Mathematical induction
      • Mathematical object
      • Mathematical object
      • Equivalent definitions of mathematical structures
      • Mathematics
      • Mathematical model
      • mathematical-notation
      • Mathematical pages
      • Mathematical terminology
      • Mathematical adjective
      • Numbers
      • plane
      • Primer: Set Theory
      • Mathematical primitive
      • Set
      • Space
      • theory
      • Variable
  • 200 Set and Set theory
    • Sets: Hierarchy
    • set.TERMS
    • SETS β€Ί TOPICS
    • 201 Set concepts
      • Mathematical collections
      • The notion of sets
      • Specification of sets
    • Set cardinality
      • Cardinality of the continuum
      • Cardinality
      • Set Cardinality
      • cardinality2
      • Set cardinality
    • Set operations
      • Disjoint sets
      • Overlapping sets
      • Product
      • set-interactions
      • Set qualities
      • Set relations
    • Set properties
      • Basic set properties
      • Set properties
    • Set relations
      • Basic set relations
      • Disjoint sets
      • Inclusion relation
      • Membership Relation
      • Set membership
    • Summary
      • Set FAQ
      • Sets: Summary
    • Set theories
      • Axiomatic set theory
      • Set Theories
      • Naive Set Theory
      • Morse-Kelley set theory
      • von Neumann-Bernays-GΓΆdel Set Theory
      • Quine's New Foundations (NF)
      • Cantor's set theory
      • Zermelo-Fraenkel set theory
    • Axioms of set theory
      • axiom-of-choice
      • The Axiom of Extensionality
      • Axiom of infinity
      • axiom-of-pairing
      • Axiom of powerset
      • Axiom of Regularity
      • Axiom of replacement
      • Axiom of union
      • Axiom of well-ordering
      • axiom-schema-of-comprehension
      • Axiom Schema of Specification
      • Axioms of set theories
      • List of axioms in set theory
      • ZFC Axioms
    • Sets: Terms
      • Bell Number
      • Cardinal number
      • Class (set theory)
      • Closure
      • empty-set
      • Extended set operations
      • Extensions by definitions
      • Family of sets
      • Fundamental sets
      • fundamental-sets2
      • Georg Cantor
      • History of set theory
      • Implementation of mathematics in set theory
      • Indexed family of sets
      • Extensional and intensional definitions
      • Involution
      • list-of-axioms-of-set-theory
      • Implementation of mathematics in set theory
      • Set membership
      • Naive Set Theory
      • Number of relations
      • empty-relation
      • Set Partitioning
      • Powerset
      • Russell's paradox
      • Set-builder notation
      • Set equivalence
      • Set Notation in latex
      • Set notation
      • Set partition
      • Intensional and extensional set specification
      • Set notation
      • Basic concepts in set theory
      • set-theory
      • Set Types
      • set
      • subset
      • Transfinite number
      • Tuples
      • ur-elements
  • Relations
    • basic-concepts
      • algebraic-axioms
      • Elements of a relation
      • Types of Relations
      • Named Relations
      • Relation theory
      • Relations
      • Types of relations
    • Relations
      • Definitions
      • Reflexivity
      • Symmetry
      • Transitivity
    • relation-properties
      • Uniqueness properties of relations
    • Types of relations
      • Transitivity
      • Binary Relation
      • Congruence relation
      • Connex relation
      • axioms-sets-zfc
      • Endorelation
      • Equivalence relation
      • Euclidean
      • Finitary relation
      • Heterogeneous relation
      • Homogeneous relation
      • Transitivity
      • Partial equivalence relation
      • Transitivity
      • Transitivity
      • Reflexive relation
      • Reflexivity
      • Index of relations
      • Serial relation
      • Symmetry
      • Transitivity
      • Ternary relation
      • Trichotomy
      • Universal relation
      • Well-foundedness
    • terms
      • Relations
      • Binary relation
      • Relations
      • _finitary-rel
      • Relations: Overview
      • Relations
      • Index of relations
      • Binary relations
      • Composition of relations
      • Equivalence class
      • Notation
      • Relation
      • Relations
      • Sets: Summary
      • Aggregation: Sets, Relations, Functions
  • Order theory
    • Order theory
    • List of order structures in mathematics
    • List of order theory topics
    • Order theory
      • Hasse diagram
      • Order theory
      • ordered-set
      • Partial order
      • Partially ordered set
      • Total order
  • Function Theory
    • Function Theory: GLOSSARY
    • Function Theory: HIERARCHY
    • Function Theory: LINKS
    • Function Theory: TERMS
    • Function Theory: TOPIC
    • Function Theory: WIKI
    • _articles
      • about-functions
      • Function
      • Formal definition
      • Definition
      • constant
      • Introduction
      • Types of functions
      • Functions: Summary of Notations
      • Functions: Overview
      • Properties of functions
      • Function properties
      • Functions: Summary
      • Function
    • Abjections
      • Bijective function
      • Function (abjections)
      • Injective function
      • Surjective function
    • topics
      • Function: TERMS
      • Codomain
      • Composition of functions
      • Currying
      • Division of functions
      • Domain
      • Function fixed points
      • Function cardinality
      • Function definition
      • Elements of a function
      • Function in mathematics
      • Function notion
      • Function operations
      • Function properties
      • Functional statements
      • Functions in programing languages
      • Image and Preimage
      • Image
      • Inverse function
      • Notion of functions
      • Number and types of functions between two sets
      • Operation
      • Range
      • Successor function
      • Time complexity classes
  • debrief-name: math section-code: 280 section-name: domain-theory section-desc:
    • Domain theory: LINKS
    • Domain theory
  • Logic
    • Logic: CHRONO TERMS
    • Logic: CLUSTERS
    • lo.GLOSSARY
    • Logic: Wiki links
    • 305-basic-concepts
      • Introduction to Logic
      • Argumentation
      • Logic: Basic terminology
      • Logic: Terminology
      • Truth function
      • Truth function
    • README
      • Mathematical Logic
      • Types of Logic
      • BHK interpretation
      • FOL
      • Index of Logic Forms
      • History of logic
      • Logic Indices
      • Interpretation of symbols in logic and math
      • logic-systems
      • Mathematical Logic: People and Events
      • Index of logical fallacies
      • Logical symbols
      • Mathematical conjecture
      • Mathematical induction
      • Mathematical lemma
      • Mathematical Logic
      • Mathematical proof
      • Mathematical theorem
      • Mathematical theory
      • Monotonicity of entailment
      • Satisfiability Modulo Theories
      • Sequent Calculus
      • Sequent
      • Tableaux
      • Truth tables
    • 360-propositional-logic
      • Propositional Logic
      • Propositional Logic
    • 370-predicate-logic
      • Predicate Logic
      • First-order logic
      • Predicate calculus
      • Examples of predicate formulae
    • 380-proof-theory
      • Argument-deduction-proof distinctions
      • Direct proof
      • Mathematical induction
      • Mathematical induction
      • Mathematical proof
      • Natural deduction
      • Natural deduction
      • Proof by induction
      • Proof by induction
      • proof-calculus
      • Proof Theory
      • Structural induction
      • System L
      • Proof theory
    • Logic: Indices
      • GΓΆdel's Incompleteness Theorem
      • The History of Mathematical Logic
      • forallx
      • Logic for CS
      • Lectures in Logic and Set Theory
      • _logicomix
    • Logic
      • Logical connectives
      • Logical equivalence
    • Rules of Inference
      • WIKI
      • Conjunction elimination
      • Conjunction introduction
      • Cut rule
      • Disjunction elimination
      • Disjunction introduction
      • Disjunctive syllogism
      • Exportation
      • implication-elimination
      • implication-introduction
      • Rules of Inference: Index
      • Rules of inference
      • Rules of Inference for Natural Deduction
      • Logical Inference
      • Reiteration
      • Rule of inference
      • Structural rules
      • substitution
    • Logic
      • The principle of bivalence
      • The principle of explosion
      • The Law of Identity (ID)
      • Laws of thought
      • Properties of logic systems
      • List of laws in logic
      • The law of non-contradiction
    • Logic
      • Logic systems: LINKS
      • Logic system
      • logic-systems
      • logic-typ
      • logics-by-purpose
      • _logics
      • Affine logic
      • Algebraic logic
      • Bunched logic
      • Classical logic
      • Traditional first-order logic
      • Hoare logic
      • Linear logic
      • Modal logic
      • Non-monotonic logic
      • Syntax
      • Predicate logic
      • Propositional Logic
      • Relevance logic
      • Separation logic
      • Substructural logics
      • Syllogistic logic
    • Logic: Sections: Elementary
    • Logic: Topics
      • Pages in Logic
      • Logic ❱ Terms ❱ List
      • Logic ❱ Terms ❱ Definitions
      • Absoluteness
      • Assumption
      • Automated theorem proving
      • Canonical normal form
      • Categorical proposition
      • Classical linear logic
      • Consequence
      • Decidability
      • Deduction systems
      • deduction-theorem
      • Deductive reasoning
      • Diagonal lemma
      • Fallacy
      • Fitch notation
      • Formal language
      • formal-system
      • Formalism
      • Formula
      • functionally complete
      • Hilbert system
      • Hoare logic
      • horn-clause
      • Mathematical induction
      • Induction
      • Inductive Reasoning
      • Intuitionistic logic
      • Intuitionistic logic
      • Intuitionistic logic
      • Judgement
      • Judgments
      • Linear logic
      • Logic in computer science
      • Logic
      • Logical connective
      • Logical consequence
      • Logical constant
      • Logical form
      • axioms-sets
      • Logical reasoning
      • Ludics
      • Non-logical symbol
      • Predicate
      • Premise
      • Quantification
      • Realizability
      • Boolean satisfiability problem
      • DPLL algorithm
      • Satisfiability
      • Semantics of logic
      • Skolemization
      • SAT and SMT
      • Syntax
      • Tautology
      • Term
      • Unification
      • Validity
  • 510 Lambda Calculi
    • Lambda Calculus: GLOSSARY
    • Lambda calculi: LINKS
    • Lambda Calculus: OUTLINE
    • Lambda Calculus: Basic concepts
      • Introduction
      • Lambda expressions
      • Free variables
    • Lambda Calculi
      • Lambda calculus: LINKS
      • Lambda calculus combinators in Haskell
      • Lambda calculus: Combinators
      • Combinators
      • combos-all.js
      • combos-bird.js
      • combos-birds-list.js
      • combos-birds.js
      • Fixed-point combinator
      • Fixpoint operator
      • Lambda calculus: Fixpoint
    • combinatory-logic
      • algebraic-structures
      • Combinatory logic
      • Combinatory logic
      • relation-classification
      • 04-definition
    • Lambda calculus encoding schemes
      • bohm-berarducci-encoding
      • Index of Church encodings
      • Church encodings
      • Church Numerals
      • Encoding data structures
      • Encoding schemes in lambda calculi
      • Lambda encoding
      • Mogensen-Scott encoding
      • Parigot encoding
      • encodings
        • Encoding data structures
        • Encoding of Data Types in the Ξ»-calculus
        • church-booleans
        • Church data structures
        • Church encoding
        • Church Numerals: Church encoding of natural numbers
        • Lambda Calculus: Church encoding
        • Lambda Calculus: Church encoding
        • church-numerals
        • Lambda Calculus: Church encoding: Numerals
        • Church pair
        • Pair
        • Lambda Calculus: Church encoding
        • Alternative encodings
        • Encoding schemes
        • Encoding schemes
        • Encodings in Untyped Lambda Calculus
        • Lambda calculus
        • Scott encoding
        • Lambda calculus: Scott encoding
    • lambda-calculus-evaluation
      • Call-by-name
      • Call-by-need
      • Call-by-value
    • lambda-calculus-forms
      • Beta normal form
      • Lambda terms
      • Fixity of lambda-terms
    • lambda-calculus-reductions
      • Alpha conversion
      • Beta reduction
      • Delta reduction
      • Eta conversion
      • Eta conversion
      • Lambda calculus: Ξ·-conversion
    • lambda-calculus
      • Alonzo Church
      • Inference rules for lambda calculus
      • Lambda Calculus: Introduction
      • Lambda abstraction
      • Lambda application
      • Lambda Calculus: Definition
      • About Ξ»-calculus
      • Type inference
      • Lambda Calculus
      • Lambda Calculus: Introduction
      • Introduction to Ξ»-calculus
      • Lambda calculus
      • Definition of Lambda Calculus
      • Functions in lambda calculus
      • History of Lambda Calculus
      • Using the Lambda Calculus
      • Name capturing
      • Variable occurrences
      • Variables
    • Lambda Calculus
      • Church-Rosser theorem
      • Curry's paradox
      • De Bruijn index
      • de Bruijn notation
      • Deductive lambda calculus
      • Kleene-Rosser paradox
      • Aspects of the lambda calculus
      • Function Refactoring
      • Lambda lifting
      • Let expression
      • Reduction strategy
      • Substitution
    • typed-lambda-calculi
      • Lambda Cube
      • Simply typed lambda calculus
      • System F
      • Typed lambda calculi
  • Type theory
    • Type Theory: GLOSSARY
    • Type theorists
    • Type Theory: SUMMARY
    • TERMS: Type Theory
      • Types
      • History of type theory
      • History of Type Theory
    • curry-howard-correspondence
      • The Curry-Howard Correspondence in Haskell
      • Curry-Howard correspondence
      • Curry-Howard correspondence
      • Curry-Howard correspondence
      • Curry-Howard-Lambek correspondence - HaskellWiki
    • dependent-types
      • Dependent type
      • Dependent type
    • Hindley-Milner type-system
      • Hindley-Milner type system
      • Monomorphism vs polymorphism
      • Let-polymorphism
      • The Hindley-Milner type system
      • Algorithm W in Haskell
      • Hindley-Milner Type Inference: W Algorithm
      • hindley–milner-type-system
      • Hindley-Milner type system
      • HM inference examples
      • HM in ML
      • Type Inference
    • Homotopy type theory
      • Homotopy type theory
      • Univalent Type theory as the foundations of mathematics
    • Intuitionistic type theory
      • Inductive definition
      • Inductive type
      • Intuitionistic type theory
    • Type Theory
      • TTTools
      • Coinduction
      • Impredicativity
      • Lean
      • Subsumption
    • Type Theory : Topics
      • Type Theory : Terms
      • Recursion types
      • Recursive data type
      • Subtyping
      • Type Class
      • Type Equivalence
      • Type Inference
      • Type rule
      • Type system
      • Variance
    • type-theories
      • Calculus of Constructions
      • Constructive type theory
      • ramified-type-theory
      • simple-type-theory
      • Substructural type systems
    • type-theory-general
      • Linear types
      • History of Type Theory
      • Type Theory
      • Overview
      • Type Theory
  • Abstract Algebra
    • 410-group-theory
      • Abelian group
    • algebras
      • Associative Algebra
      • Field
      • Group-like algebraic structures
      • group
      • Lattice
      • Magma
      • monoid
      • Overview of Algebras
      • Quasigroup
      • Rack and quandle
      • Ring
      • Semigroup
      • Algebra of sets
      • Setoid
    • boolean-algebra
      • Boolean algebra
      • Axioms in Boolean Algebra
      • Boolean algebra
      • Boolean Algebra Laws
      • Boolean Algebra Laws
      • Two-element Boolean algebra
      • Boolean algebra
      • Boolean domain
    • terms
      • Algebra
      • Axioms of abstract algebra
      • Algebraic notation for algebraic data types
      • Algebraic structure
      • Algebraic structure
      • Field of sets
      • Homomorphism
      • Isomorphism
      • Algebraic structures
      • Mathematical structure
      • Polynomials
      • Relation algebra
  • Category Theory
    • CT GLOSSARY
    • Category Theory: OUTLINE
    • CT SUMMARY
    • A First Introduction to Categories (2009)
      • Sets, maps, composition
      • 02-history
      • axioms-logic
      • Bijection of functions
      • Commutative diagram
      • Directed graph
      • CT prerequisites
      • String diagram
      • Transitive closure
    • Category Theory Fundamentals
      • Introduction
      • Interpretation
      • Fundamental concepts
      • Category theory
      • Category
      • Category Theory: Definitions
    • Key concepts
      • Duality
      • Functor
      • Homeset
      • Initial Object
      • Morphism
      • Natural transformation
      • Object
      • Terminal Object
    • Categorical constructions
      • Categorical constructions
      • Coproduct
      • Diagram
      • Product
      • Universal construction
    • Types of categories
      • Concrete category
      • Discrete category
      • Functor category
      • Groupoid
      • Hask
      • Kleisli category
      • Locally small category
      • Monoid
      • monoidal-categories.md
      • Index of named categories
      • Opposite category
      • Ordered category
      • Set category
      • Small category
      • Subcategory
    • Types of Functors
      • Adjoint functor
      • relation-arity
      • Endofunctor
      • Faithful functor
      • Forgetful functor
      • Hom functor
      • Identity functor
      • Inverse functor
      • Monad
      • Powerset functor
    • Types of Morphisms
      • Anamorphism
      • Automorphism
      • Catamorphism
      • Endomorphism
      • Epimorphism
      • Homomorphism
      • Hylomorphism
      • Idempotent morphism
      • Identity morphism
      • Inverse morphism
      • Isomorphism
      • Metamorphism
      • monomorphism
      • Natural isomorphism
      • Split morphism
    • 20-advanced-concepts
      • Coalgebra
      • (Co)Inductive types
      • Recursion Schemes
    • Category Theory
      • Category Theory: TERMS
      • Algebraic Data Types
      • Category Theory
      • Category
      • Coproduct
      • Function type
      • Functoriality
      • Initial Object
      • Limits and Colimits
      • Natural Transformation
      • 5. Products
      • Terminal Object
    • Category Theory :: Contents
      • CT :: Links
      • Category Theory :: Terms
      • Category :: Definition
      • F-Algebra
      • Functor
      • Initial object
      • Monoid
      • Natural Transformation
      • Number of morphisms
      • Terminal object
      • Transitive closure
      • Types of morphisms
      • Categories by cardinality
      • Types of functors
  • Number Theory
    • Invariance and Monovariance Principle
    • 615-arithmetic
      • Addition
      • Aliquot sum
      • Arithmetic function
      • Laws
      • Arithmetic operations
      • Index of arithmetic operations
      • Arithmetic operations
      • Arithmetic
      • Divisibility rules
      • Divisibility
      • division
      • Divisor Function
      • Divisor Summatory Function
      • Divisor
      • Euclidean division
      • Hyperoperations
      • hyperops
      • Modular arithmetic
      • Multiplication
      • Number Theory: primer in numbers
      • Percentage
      • Rules of Divisibility
      • Subtraction
    • The fundamental sets of numbers
      • Algebraic numbers
      • Complex numbers
      • Fractions
      • Fundamental number sets
      • Imaginary numbers
      • Integers
      • Irrational numbers
      • Natural number
      • Rational numbers
      • Real numbers
      • Transcendental numbers
      • Ulam's spiral
      • The whole numbers
    • COUNTING THEORY
      • Counting Theory
      • counting
      • Fundamental Counting Rules
    • 630-combinatorics
      • Combinatorics
      • Combinations
      • Combinatorics
      • Counting theory
      • Counting theory
      • Enumerative combinatorics
      • Partition
      • Pascals triangle
      • Permutations
      • Twelvefold way
    • Probability theory
      • Statistics β€Ί Probability theory: Glossary
      • Statistics β€Ί Probability theory β€Ί Topics
      • Statistics β€Ί Probability theory β€Ί Wiki Links
      • Conditional Probability
      • Distribution
      • Probability theory
      • Probability
    • Number theory
      • euclids-lemma
      • gcd-lcm
      • Induction
      • Infinity
      • Numbers and numerals with interesting properties
      • Lagrange's four-square theorem
      • Matrix
      • Matrix
      • List of Number Systems
      • Number Theory
      • Number Theory with Glenn Olsen
      • Number
      • Arithmetic
      • Numbers
      • numeral-prefixes
      • Numeral system
      • Numeral
      • Ordinal numbers
      • Parity
      • Peano axioms
      • Polynomial
      • Polynomial
      • Positional notation
      • Probability
      • Symbol
      • Well Ordering Principle
    • topics
      • Coprimality
      • Facorization of composite numbers
      • Fundamental Theorem of Arithmetic
      • Prime factorisation
      • Prime number
      • Prime numbers
  • Theory of computation
    • Theory of computation: Abbreviations
    • Theory of computation: CHRONOLOGICAL TOPICS
    • Theory of computation: GLOSSARY
    • Theory of Computation: HIERARCHY
    • Theory of computation: LINKS
    • Theory of computation: TERMS
    • Theory of computation: TOPICS
    • Theory of computation: WIKI
    • Theory of Computation
      • _toc-more
      • Theory of Computation
    • 610-automata-theory
      • Abstract machine
      • Automata Theory
      • Automaton
      • Edit distance
      • Finite-state Machine
      • Automata Theory: WIKI
    • Formal systems
      • Abstract interpretation
      • Alphabet
      • Binary combinatory logic
      • Chomsky hierarchy
      • Epsilon calculus
      • Formal language
      • Iota and Jot
      • Regular expression
      • Regular Language
      • SKI combinator calculus
    • 621-grammar
      • Backus-Naur Form (BNF)
      • Context-free grammar
      • Context-sensitive grammar
      • Extended Backus–Naur Form (EBNF)
      • Regular Language
      • Terminal and nonterminal symbols
    • 622-syntax
      • Syntax
    • 624-semantics
      • Axiomatic semantics
      • Denotational Semantics: Summary
      • Denotational Semantics
      • Denotational Semantics
      • Denotational semantics
      • Formal semantics
      • Operational semantics
      • Semantics in CS
      • Semantics
    • 630-computability-theory
      • Computability (recursion) theory: TERMS
      • Computability (recursion) theory: TOPICS
      • Effective Computability
      • Church Thesis
      • Church-Turing Thesis
      • Computability theory
      • Computability
      • Computable function
      • Entscheidungsproblem
      • Halting problem
      • Machine that always halts
      • McCarthy Formalism
      • Super-recursive algorithm
      • Recursion theory
    • 632-recursive-function-theory
      • Recursion Theory
      • Ackermann function
      • General recursive function
      • Minimization operator
      • Partial functions
      • Recursion Function Theory
      • Sudan function
    • 634-primitive-recursive-functions
      • Primitive Recursive Function
      • Initial functions
      • The list of primitive recursive functions
      • Primitive combination
      • Primitive composition
      • Primitive recursion
      • Successor function
    • 640-models-of-computation
      • Models of computation: Summaries
      • Model of computation
    • 680-complexity-theory
      • Algorithmic Complexity
      • Complexity Theory
  • debrief-name: math section-code: 900 section-name: aggregations section-desc: Aggregations, indices,
    • Index of closures
    • List of mathematical entities
    • List of mathematical objects
    • Enumeration of mathematical structures
    • Math : Axioms as Formulae
    • 950-math-areas
      • Areas of mathematics
      • Areas of mathematics
    • 970-links
      • check
      • Math: Links
      • Math Debrief: Links
      • Math Primer: LINKS
      • Links
      • Math: LINKS: ncatlab
      • Math: LINKS
      • WIKI
      • WIKI
      • WIKI_ALL
      • Math: Wiki lists
      • Glossary of areas of mathematics
      • WIKI_collections
      • Mathematics for Computer Science
      • Mathematics Classification
      • math
      • Resources
      • Math on YouTubel Video Playlists
      • wiki resources
    • 980-hierarchy
      • HIERAR
      • Math: Hierarchy
      • Math HIERARCHY
      • classification
        • Mathematics
        • https://ncatlab.org/nlab/all_pages https://ncatlab.org/nlab/all_pages/reference https://ncatlab.org/
        • Math Classification and Topical Pages
        • Areas of mathematics
        • Areas of mathematics
        • Math Classification: CCS
        • Math hierarchy
        • Computational mathematics
        • Taxonomy: Mathematics
        • Areas of mathematics
        • Mathematics Subject Classification
        • Math fields
        • math-topics
        • Mathematics Subject Classification – MSC
        • MSC Classification Codes
        • mss-top-levels-filenames
        • MSC classification: Top Levels
        • Math classification
    • 990-appendix
      • Math glossary at ENCYCLOPΓ†DIA BRITANNICA
      • Bibliography
      • Math: Abbreviations
      • math.GLOSSARY
    • Math : Canon
      • Main branches of mathematics
      • Enumeration: Math paradigms
      • enum-math-symbols
      • List of mathematical theories
      • enum-algebras
        • Group-like algebraic structures
        • Group
        • Groupoid
        • magma
        • Monoid
        • Semigroup
      • enum-axioms-indices
        • 03-variants
        • axioms-relations
        • disjoint-sets
        • ordered-pair
      • enum-axioms
        • Axiom of Extensionality
        • Axioms
          • List of Axioms
          • List of Axioms
          • LINKS
          • Index of axioms
          • Index of axioms
          • List of Axioms
          • List of Axioms in Relations
          • _laws
          • Index of axioms
          • Index of properties
          • Axioms in Boolean Algebra
          • Axioms for the Real Numbers and Integers
          • Axioms for the Real Numbers and Integers
          • ZF Axioms
          • ZFC Axioms
          • Axioms in logic
          • Axioms in set theory
          • List of axioms in set theory
        • Axioms
          • Absorption
          • Annihilation
          • Associativity
          • Cancellation
          • Closure
          • Commutativity
          • Complement laws
          • Distributivity
          • Domination
          • Idempotency
          • identity
          • Invertibility
          • involution
          • Linearity
          • Monotonicity
          • Well-definedness
          • Well-formedness
          • Well-foundedness
          • Well-ordering
      • enum-inference-rules
        • Enumeration: Rules of Inference
        • Enumeration: Rules of Inference for Intuitionistic Natural Deduction
      • Math β€Ί Logic formulae
        • Logic formulas concerning functions
        • Logic formulas concerning orders
        • Logic formulas concerning relations
        • Logic formulas concerning sets
      • enum-logic-system-elements
        • Conjecture
      • enum-logic-system-properties
        • Completeness
        • Consistency
        • Decidability
      • enum-topical-hierarchies
        • Outline of category theory
    • Mathematical Lists and Indices
      • Index of algebraic structures
      • Math equations and formulas
      • The fundamental number sets
      • index-of-math-elements
      • Arity
      • List of binary relations
      • Pretty formulae
      • Index of integer sequences
      • List of conjectures
      • Mathematical objects
      • Theorems
      • List of mathematical theories
      • list-of-unsolved-problems
      • Lists of problems in math
      • People
      • list-of-quotes-and-phrases
    • Mathematical elements
      • Mathematical (elements): PAGES
      • Mathematical abstraction
      • Mathematical analysis
      • Mathematical argumentation
      • Mathematical axiom
      • Mathematical concept
      • Mathematical constant
      • Mathematical deduction
      • Mathematical definition
      • Mathematical element
      • Mathematical expression
      • Mathematical formula
      • Mathematical method
      • Mathematical model
      • Mathematical notation
      • Mathematical object
      • Mathematical primitive
      • Mathematical reasoning
      • Mathematical statement
      • Mathematical structure
      • Mathematical symbol
      • Mathematical synthesis
  • debrief-name: math section-code: 800 section-name: misc section-desc: Misc and unclassified mathemat
    • 810-statistics
      • STATISTICS: HIERARCHY
      • STATISTICS: TERMS
      • Statistics β€Ί Topics
      • Statistics WIKI LINKS
      • Mathematical Concepts
      • Linear Regression
    • 888-calculus
      • Calculus
      • Math β€Ί Calculus β€Ί TERMS
Powered by GitBook
On this page
  • Contents
  • TOC
  • 0. Introduction
  • 0.1 Methods for specifying semantics
  • 0.1.1 Operational semantics
  • 0.1.2 Denotational semantics
  • 0.1.3 Axiomatic semantics
  • 1. Syntax
  • 1.1 Abstract syntax definition
  • 1.2 Mathematical and structural induction
  • 2. Sets, Functions and Domains
  • 2.1 Sets
  • 2.2 Functions
  • 2.2.1 Representing Functions as Sets
  • 2.2.2 Representing Functions as Equations
  • 2.3 Semantic Domains
  • 2.3.1 Semantic Algebras
  • 3. Domain Theory I: Semantic Algebras

Was this helpful?

  1. Theory of computation
  2. 624-semantics

Denotational semantics

PreviousDenotational SemanticsNextFormal semantics

Last updated 3 years ago

Was this helpful?

"Denotational Semantics: A Methodology for Language Development" Book by David A. Schmidt, 1997

Contents

TOC

  1. Introduction 0.1 Methods for specifying semantics 0.1.1 Operational semantics 0.1.2 Denotational semantics 0.1.3 Axiomatic semantics

  2. Syntax 1.1 Abstract syntax definition 1.2 Mathematical and structural induction

  3. Sets, Functions and Domains 2.1 Sets 2.1.1 Constructions on Sets 2.2 Functions 2.2.1 Representing Functions as Sets 2.2.2 Representing Functions as Equations 2.3 Semantic Domains 2.3.1 Semantic Algebras

  4. Domain Theory I: Semantic Algebras

0. Introduction

Any notation for issuing instructions to a computer is a programming language.

Arithmetic notation is a programming language, and so is Pascal. The input data format for an applications program is also a programming language. The person who uses a program thinks of its input commands as a language, just like the program's author thought of Pascal when she used it to implement the program. The person who wrote the Pascal compiler had a similar view about the assembly language he used for writing the compiler. This series of languages and viewpoints terminates at the physical machine, where code is converted into machine instructions.

A PL has 3 main characteristics:

  1. Syntax: appearance and structure of PL sentences.

  2. Semantics: assignment of meaning to the sentences.

  3. Pragmatics: usability of the language.

Pragmatics includes the areas of application, the ease of implementation and use, and a PL's success in fulfilling its goals.

Syntax, semantics, and pragmatics are features of every computer program. Considering an application, it is a processor for its input language, and it has 2 main parts: the input checker module (parser) reads the input and verifies that it has the proper syntax; the evaluation module evaluates the input to its corresponding output, and in doing so, defines the input's semantics. How the system is implemented and used are pragmatical concerns.

These characteristics also apply to a general purpose language like Pascal. An interpreter for Pascal also has a parser and an evaluation module. An issue of pragmatics may be that the interpretation is slow, so we prefer a compiler instead. A Pascal's compiler transforms its input program into a fast-running, equivalent version in machine code.

The compiler presents some deeper semantic questions. In the case of an interpreter, the semantics of a program is defined entirely by the interpreter. But a compiler does not define the meaning, instead, compiler preserves the meaning of a program when it translates it into the machine code. The semantics of Pascal is an issue independent of any particular compiler or computer. The case in point are Pascal compilers on two different machines; the two different compilers still preserve the same semantics of Pascal.

Rigorous definitions of the syntax and semantics of Pascal are required to verify that a compiler is correctly implemented. The area of syntax specification has been thoroughly studied, and Backus-Naur form (BNF) is widely used for specifying syntax. One of reasons this area is so well developed is the close correspondence between a PL's BNF definition and its parser: the definition dictates how to build the parser. A parser generator maps a BNF definition to a guaranteed correct parser. In addition, a BNF definition provides valuable documentation.

Semantics definition methods are also valuable to implementors and programmers, for they provide:

  • A precise standard for a computer implementation. The standard guarantees that the language is implemented exactly the same on all machines.

  • Useful user documentation.

  • A tool for design and analysis. Typically, systems are implemented before their designers study pragmatics. This is because few tools exist for testing and analyzing a language. Just as syntax definitions can be modified and made error-free so that fast parsers result, semantic definitions can be written and tuned to suggest efficient, elegant implementations.

  1. Input to a compiler generator. A compiler generator maps a semantics definition to a guaranteed correct implementation for the language. The generator reduces systems development to systems specification.

Unfortunately, the semantics area is not as well developed as the syntax area. This is for two reasons: first, semantic features are much more difficult to define and describe. (In fact, BNF's utility is enhanced because those syntactic aspects that it cannot describe are pushed into the semantics area. The dividing line between the two areas is not fixed); second, a standard method for writing semantics is still evolving.

0.1 Methods for specifying semantics

Programmers naturally take the meaning of a program to be the actions that a machine takes upon it. The first versions of PL semantics used machines and their actions as the foundation.

0.1.1 Operational semantics

The operational semantics method uses an interpreter to define a language. The meaning of a program in the language is the evaluation history that the interpreter produces when it interprets the program. The evaluation history is a sequence of internal interpreter configurations. One of the disadvantages of an operational definition is that a language can be understood only in terms of interpreter configurations: no machine-independent definition exists. Another problem is the interpreter itself: it is represented as an algorithm. If the algorithm is simple and written in an elegant notation, the interpreter can give insight into the language. Unfortunately, interpreters for nontrivial languages are large and complex, and the notation used to write them is often as complex as the language being defined. Operational definitions are still worthy of study because one need only implement the interpreter to implement the language.

0.1.2 Denotational semantics

The denotational semantics method maps a program directly to its meaning, called its denotation, using a valuation function. The denotation is usually a mathematical value, such as a number or a function. No interpreters are used in a denotational definition; it is more abstract than an operational definition, since it doesn't specify computation steps. Its high-level, modular structure means the individual parts of a PL can be studied without examining the entire definition. On the other hand, the implementor of a PL has more work to do. The numbers and functions must be represented as objects in a physical machine, and the valuation function must be implemented as the processor.

0.1.3 Axiomatic semantics

With the axiomatic semantics method, the meaning of a program is not explicitly given at all. Instead, properties about language constructs are defined. These properties are expressed with axioms and inference rules from symbolic logic. A property about a program is deduced by using the axioms and rules to construct a formal proof of the property. The character of an axiomatic definition is determined by the kind of properties that can be proved. For example, a very simple system may only allow proofs that one program is equal to another, whatever meanings they might have. More complex systems allow proofs about a program's input and output properties. Axiomatic definitions are more abstract than denotational and operational ones, and the properties proved about a program may not be enough to completely determine the program's meaning. The format is best used to provide preliminary specs for a language or to document properties that are of interest to the users.

∎

Each of the three methods of formal semantics definition has a different area of application, and together the three provide a set of tools for language development.

Designing a new programming system might proceed by first supplying a list of properties a PL should have. Since users interacts with it via an input language, an axiomatic definition is constructed first, defining the input language and how it achieves the desired properties. Next, a denotational semantics is defined to give the meaning of the language. A formal proof is constructed to show that the semantics contains the properties that the axiomatic definition specifies. The denotational definition is a model of the axiomatic system. Finally, the denotational definition is implemented using an operational definition. These complementary semantic definitions of a language support systematic design, development, and implementation.

Of the three semantics description methods, denotational semantics is the best format for precisely defining the meaning of a programming language. Possible implementation strategies can be derived from the definition as well. The study of denotational semantics provides a good foundation for understanding many of the research areas in semantics and PLT.

1. Syntax

A PL consists of syntax, semantics, and pragmatics. We formalize syntax first, because only syntactically correct programs have semantics. A syntax definition of a language lists the symbols for building words, the word structure, the structure of well formed phrases, and the sentence structure.

The Backus-Naur form notation is used to precisely specify the internal structure of a PL. A BNF definition consists of a set of equations. The lhs of an equation is called a nonterminal and gives the name to a structural type in the language. The rhs lists the forms which belong to the structural type. These forms are built from terminal symbols and other nonterminals.

The BNF definition gives a complete and precise description of the syntax. An expression derived from the language is called a derivation tree; it clearly exposes the internal structure. However, it may happend that a BNF definition results in two valid derivation trees for the same expression. When this happens, the syntax definition is said to be ambiguous. Ambiguous BNF definitions can usually be rewritten into an unambiguous form, at the cost of introducing some artificial levels of structure.

We consider the derivation trees are the real sentences of a language, and strings of symbols are just abbreviations for the trees. Thus, the string 4 Γ— 2 + 1 is an ambiguous abbreviation. A BNF definition is adequate for specifying the structure of sentences (trees) of arithmetic, but it is not designed for assigning a unique derivation tree to a string purporting to be a sentence.

In practice, we use two BNF definitions: one to determine the derivation tree that a string abbreviates, called the concrete syntax definition; and one to analyze the tree's structure and determine its semantics, called the abstract syntax definition.

A formal relationship exists between a concrete and abstract syntax definitions: the tree generated for a string by a concrete definition identifies a derivation tree for the string in the abstract definition.

Concrete syntax definitions are used to handle parsing problems; this isn't a concern of semantics, and we'll work with derivation trees, not strings. The concrete syntax definition is derived from the abstract one. The abstract syntax definition is the true definition of the structure of a PL.

1.1 Abstract syntax definition

Abstract syntax definitions describe structure. Terminal symbols disappear entirely if we study abstract syntax at the word level. The building blocks (words) of abstract syntax are called tokens, rather than terminal symbols. This relates syntax to semantics more closely, for meanings are assigned to entire words (tokens), not to individual symbols.

Set theory gives us an even more abstract view of abstract syntax. Each nonterminal in a BNF definition names the set of those language phrases that have the structure specified by the nonterminal's BNF rule. However, the rules can be discarded by introducing syntax builder operations; one for each form on the right-hand side of the rule.

Set-theoretic formulation of the syntax of arithmetic:

Sets
  Op
  Expr
  Numeral

Operations
  mkExprFromNumeral : Numeral -> Expr
  mkCompoundExpr    : Expr β¨― Op β¨― Expr -> Expr
  mkBracketedExpr   : Expr -> Expr

  plus  : Op
  minus : Op
  mult  : Op
  div   : Op

  zero  : Numeral
  one   : Numeral
  two   : Numeral
  …
  hundred : Numeral
  …

The language consists of 3 sets of values: expressions, arithmetic operators, and numerals.

The members of the Numeral set are exactly those values built by the "operations" (which are really constants): zero, one, two, etc. The Operator set contains just the 4 values denoted by the constants plus, minus, mult, and div. Members of the expression set, Expr, are built with the 3 operations, mk*.

Consider mkExprFromNumeral: it converts a value from the Numeral set into a value in the Expr set, thereby reflecting the idea that any known numeral can be used as an expression. Similarly, mkCompoundExpr combines two known members of the Expr set with a member of the Operation set to build a member of the Expr set. Note that mkBracketedExpr does not need parenthesis tokens to complete its mapping; the parentheses were just "window dressing". For example, the expression 4 + 12 is repr by mkCompoundExpr(mkExprFromNumeral(four), plus, mkExprFromNumeral(twelve)).

The set-theoretic abstract syntax is due to C. Strachey. When we work with the set-theoretic formulation of abstract syntax, we forget about words and derivation trees and work only in the world of sets and operations. The set-theoretic approach reinforces the view that syntax is not tied to symbols; it's a matter of structure. Syntax domain specifies a collection of values with a common syntactic structure (e.g. arithmetic has 3 syntax domains).

We specify a language's syntax by listing its syntax domains and its BNF rules. The syntax of a block-structured PL in this format:

Abstract syntax:
  P ∈ Program
  B ∈ Block
  D ∈ Declaration
  C ∈ Command
  E ∈ Expression
  O ∈ Operator
  I ∈ Identifier
  N ∈ Numeral

P := B.
B := D;C
D := var I | procedure I; C | D1; D2
C := I = E | if E then C | while E do C | C1;C2 | begin B end
E := I | N | E1 O E2 | (E)
O := + | βˆ’ | * | div

For example, the phrase B ∈ Block indicates that Block is a syntax domain and that B is the nonterminal that represents an arbitrary member of the domain. The structure of blocks is given by the BNF rule B := D;C which says that any block must consist of a declaration (repr by D) and a command (C). The structures of programs, declarations, commands, expressions, and operators are similarly specified. Identifier and Numeral have no BNF rules since they are collections of tokens.

1.2 Mathematical and structural induction

We must often show that all the members of a syntax domain have some property in common - the proof technique used on syntax domains is structural induction.

A specific case of structural induction is the mathematical induction, which is a proof strategy for showing that all members of β„• possess a property P.

  1. Show that P(0) holds

  2. Assuming that P(n) holds for an arbitrary n ∈ β„• (induction hypothesis), show that P(n+1) holds as well, P(n) -> P(S n)

When both steps are proved then it follows that the property holds for all the numbers in β„•. This is because any number k in β„• is either 0, for which the proof that P(0) holds was already given in (1), or k is S n, that is, k = 1 = S(0), or k = 2 = S (S 0), or k = S (… S 0); in other words, k is always of the form P(S(n)), which we have already proved in (2). In the usual notation: any number k ∈ β„• has the form (… ((0 + 1) + 1) + … + 1), as 1 added k times.

The mathematical induction principle is simple because the natural numbers have a simple structure: a number is either 0 or a successor of some number. This structure can be formalized as a BNF rule: N := 0 | N + 1.

Any natural number is just a derivation tree. The mathematical induction principle is a proof strategy for showing that all the trees built by the rule for N possess a property P.

Step 1 says to show that the tree of depth zero, the leaf 0, has P. Step 2 says to use the fact that a tree t has property P to prove that the tree t+1 has P.

The mathematical induction principle, generalized to work upon any syntax domain defined by a BNF rule, is structural induction. Treating the members of a syntax domain D as trees, we show that all trees in D have property P inductively:

  1. Show that all trees of depth zero (d = 0) have P

  2. Assuming that all trees of depth d or less have P (where d >= 0), show that a tree of depth m + 1 has P as well.

The structural induction strategy is easily adapted to operate directly upon the BNF rule that generates the trees.

[Definition] The structural induction principle: for the syntax domain D and its BNF rule:

d := Option₁ | Optionβ‚‚ | … | Optionβ‚™

all members of D have a property P if the following holds for each Optionα΅’ (where 1 <= i <= n): assuming that every occurrence of d in Optionα΅’ has P (inductive hypothesis), then Optionα΅’ has P.

The method appears circular because it is necessary to assume that trees in D have P to prove that the D-tree built using Optionα΅’ has P, but the tree being built must have a depth greater than the subtrees used to build it, so steps 1 and 2 apply.

The structural induction principle generalizes to operate over a number of domains simultaneously. We can prove properties of two or more domains that are defined in terms of one another.

2. Sets, Functions and Domains

Functions are fundamental to denotational semantics. We introduce functions through set theory. The concepts of set theory form a foundation for the theory of semantic domains, the value spaces used for giving meaning to languages. We examine the basic principles of sets, functions and domains.

2.1 Sets

  • principle of intensionality

    • internal view of sets

    • intensional equality of sets

  • principle of extensionality

    • external view of sets

    • extensional equality of sets

  • set product

    • n-ary product

  • ordered pair (2-tuple)

    • n-tuple

  • union

    • n-ary union

    • disjoint union

  • intersection

    • n-ary intersection

The internal structure of a set is exposed when sets are specified using a rooster notation. An external view treats sets as abstract objects, allowing us to only ask yes/no questions about membership of an element in some set; that way the internal structure of sets isn't even important, as long as membership questions can be answered.

To tie the internal and external views together, set theory has the principle of extensionality, also called extensional equality of sets: a set R is equal to a set S iff they give the same answer to all the membership queries:

R = S <=> (βˆ€x.(x ∈ R <=> x ∈ S))

The extensionality principle implies the two elementary properties of sets: set is an unordered collection without duplicated elements; because the questions about an element's membership can only ask whether some element is in some set or not; not questions about its order or multiplicity.

2.1.1 Constructions on Sets

Union and intersection are commutative and associative.

R = S <=> (βˆ€x. x ∈ R <=> x ∈ S)
R βŠ† S <=> (βˆ€x. x ∈ R --> x ∈ S)
R = S <=> (R βŠ† S β‹€ S βŠ† R)

βˆ€x. x ∈ (R ⋃ S) -> (x ∈ R ⋁ x ∈ S)
βˆ€x. x ∈ (R β‹‚ S) -> (x ∈ R β‹€ x ∈ S)

β„€ = ⋃ [i = 0 ..] {i, -i}

An ordered pair is an element of the product of two sets, e.g.

𝔹 β¨― β„• = { (b, n) | βˆ€b.b ∈ 𝔹. βˆ€n. n ∈ β„• }

A form of union construction on sets that keeps the members of the respective sets R and S separate is called disjoint union (or sum):

R + S = { (0,x) | x ∈ R } ⋃ { (1,y) | y ∈ S } = { (0,x), (1,y) }

The ordered pair construction is used to tag elements of R and S such that it's always possible to determine an element's origin (even if R and S are the same set).

The tags are elements of an arbitrary set that is called an indexing set when used in this role; those elements of the indexing set that are used for indexing are called indices.

Most of the time, the set β„• is used as the indexing set, but in the case of the binary disjoint union, it is customery to use the Boolean set, 𝔹, for indexing. Above, the elements originating from R are tagged by pairing them with the Boolean false value (0, x) as the first pair component.

The ordered pair will also need operations for assembling and disassembling its components, inR and inS, which behave as follows:

  • if x is in R then it is tagged with a F (false) x ∈ R. inR(x) = (F,x)

  • if y is in S then it is tagged with a T (true) y ∈ S. inS(y) = (T,y)

R + S = inR(x) + inS(y)

To remove the tag from an element m ∈ R + S, we could simply say snd(m), but instead we'll use a structured operation called case analysis. For any m ∈ R + S, the value of m can be deduced by

case m of
  isR(a) -> … a (here we know that the value came from R)
  isS(a) -> … a (here we know that the value came from S)
end

// for example:
f(m) = case m of
  isL(a : β„•) = a + 1
  isR(a : 𝔹) = 0
end

// if m is a value whose tag is L and whose value is a, then it is 'a'
// if m is a value whose tag is R and whose value is a, then it is 'a'
data Sum x y = L x | R y

m1 :: Sum Int Bool
m1 = L 42

m2 :: Sum Int Bool
m2 = R True

m :: Sum Int Bool
m = (unkown value)

case m of
  L a -> a is Int
  R a -> a is Bool

2.2 Functions

A function cannot be taken apart and its internals examined; it is like a black box that accepts an object as its input and then transforms it in some way to produce another object as its output. We must use the external view to understand functions.

For two sets R and S, f is a function from R to S, written f : R β†’ S, if to each member of R, f associates exactly one member of S.

  • the expression R β†’ S is called the arity or functionality of f

  • R is the domain and S is the codomain of f

  • if x ∈ R, and the element paired to x by f is y, we write f(x)=y

  • presenting an arg a to f is called application and is written f(a)

We don't know how f transforms the input to output, but we accept that somehow it does; the results are what matter. This viewpoint is similar to that taken by a user of an computer program: unaware of the workings of a computer and its software, the user treats the program as a function, as he is only concerned with its input-output properties.

An extensionality principle also applies to functions: for functions f: R β†’ S and g: R β†’ S, f is equal to g, written f = g, iff for all x ∈ R, f(x) = g(x).

Composition, g ∘ f = (g ∘ f) x = g(f(x))

Functions can be classified by their mappings, a function f : A -> B

  • βˆ€a ∈ A. βˆƒb ∈ B. f(a) = b is a function

  • βˆ€b ∈ B. βˆƒa ∈ A. f(a) = b is a surjuction (in terms of B)

  • βˆ€aa' ∈ A. f(a) = f(a') <=> a = a' is an injection (in terms of A)

  • βˆ€a ∈ A. f(a) = a is the identity function on A

  • and a function f⁻¹ : B -> A where is the inverse of f βˆ€b ∈ B. βˆƒa ∈ A. f⁻¹(b) = a <=> f(a) = b

  1. injective (one-one)

  • βˆ€x ∈ R.βˆ€y ∈ R. f(x) = f(y) <=> x = y

  • f : R β†’ S is injective iff f(x) = f(y) implies x = y

  1. surjective (onto)

  • f : R β†’ S is onto iff S = { y | βˆƒx ∈ R. f(x) = y }

  • βˆ€y ∈ S. βˆƒx ∈ R. f(x) = y

  • βˆ€x ∈ R. βˆ€y ∈ S. f(x) = y

  1. identity:

  • f : R β†’ R is the identity function on R iff forall x ∈ R, f(x) = x

  • f : A β†’ A is identity iff βˆ€a ∈ A. f(a) = a

  1. bijection, inverse: if f : R β†’ S is injective and surjective, then the function g : S β†’ R, defined as g(y) = x iff f(x) = y is called the inverse function of f. Function g, i.e. theinverse of f is denoted by f⁻¹

2.2.1 Representing Functions as Sets

…

2.2.2 Representing Functions as Equations

…

2.3 Semantic Domains

Sets that are used as value spaces in PL semantics are called semantic domains.

We will make use of primitive domains (𝔹, β„•, β„€, etc.) and the following four types of compound domains, built from existing domains A and B:

  1. Product domains A Γ— B

  2. Sum domains A + B

  3. Function domains A β†’ B

  4. Lifted domains Aβ«  where Aβ«  = A ⋃ { ⟘ }

The 4th construction adds a special value ⟘ (bottom) that denotes nontermination or the absence of value.

Since we are interested in modelling computing-related situations, there is a possibility that a function f applied to an arg a ∈ A may yield no answer at all, f(a) may stand for a nonterminating computation. In such situations, we say that f has functionality A β†’ Bβ«  and f(a) = b | ⟘.

The use of the codomain Bβ«  instead of B stands as a kind of warning: in the process of computing a value, nontermination may occur.

Including ⟘ as a value is an alternative to using a theory of partial functions (partial function is not defined for all domain values).

A function f that is undefined at argument a has the property f(a) = ⟘.

In addition to dealing with undefinedness as a real value, we can also use ⟘ to state what happens when a function receives a nonterminating value as an argument, f : Aβ«  β†’ Bβ« , we write f = Ξ»!x.Ξ± (Ξ»! is the strict Ξ») to denote the mapping:

-- definition
f : Aβ«  -> Bβ« 
f = Ξ»!.Ξ±

-- application
f ⟘ = ⟘
f a = [a/x]α   for a ∈ A

The Ξ»! denotes a strict function, so f cannot recovered from a nonterminating situation. For example

-- f is strict:
f : β„•β«  β†’ β„•β« 
f = Ξ»! n . 0

f = \ n -> 0
f !n = 0

f(⟘) = ⟘

-- g is lazy
g : β„•β«  β†’ β„•β« 
g = Ξ» n . 0

g(⟘) = 0

2.3.1 Semantic Algebras

Now that the tools for building domains and functions have been specified, we introduce a format for presenting semantic domains. The format is called a semantic algebra because (like the algebras studied in universal algebra) it is the grouping of a set with the fundamental operations on that set.

We choose the algebra format because

  1. Clearly states the structure of a domain and how its elements are used by the functions.

  2. Encourages the development of standard algebra "modules" or "kits" that can be used in a variety of semantic definitions.

  3. Makes it easier to analyze a semantic definition concept by concept.

  4. Makes it straightforward to alter a semantic definition by replacing one semantic algebra with another.

We use pairs of integers to simulate the rational numbers. Operations for creating, adding, and multiplying rational numbers are specified. The example also introduces a function that we will use often: the expression e1 β†’ e2 β–― e3 is the choice function, which has the value e2 if e1 = true, or e3 if e1 = false, i.e. e1 ? e2 : e3, or if e1 then e2 else e3.

Example:
  Simulating the rational numbers

Domain:
  Rat = (β„€ Γ— β„€)β« 

Operations:
  makerat :: β„€ -> (β„€ -> Rat)
  makerat= λp. λq. if q = 0 then ⟘ else (p,q)

  addrat :: Rat -> (Rat -> Rat)
  addrat= Ξ» !(p1,q1). Ξ» !(p2,q2). (p1 * q2 + p2 * q1 , q1 * q2)

  multrat :: Rat -> (Rat -> Rat)
  multrat= Ξ» !(p1,q1). Ξ» !(p2,q2). (p1 * p2, q1 * q2)

Since the possibility of an undefined Rat exists, addrat and mulrat are strict: they must checks both args for definedness (with a bang binding) before performing the operation.

3. Domain Theory I: Semantic Algebras

Contents
TOC
0. Introduction
0.1 Methods for specifying semantics
0.1.1 Operational semantics
0.1.2 Denotational semantics
0.1.3 Axiomatic semantics
1. Syntax
1.1 Abstract syntax definition
1.2 Mathematical and structural induction
2. Sets, Functions and Domains
2.1 Sets
2.1.1 Constructions on Sets
2.2 Functions
2.2.1 Representing Functions as Sets
2.2.2 Representing Functions as Equations
2.3 Semantic Domains
2.3.1 Semantic Algebras