Permutation group algorithms are indispensable in the proofs of many deep results, including the construction and study of sporadic finite simple groups. This work describes the theory behind permutation group algorithms, up to the most recent developments based on the classification of finite simple groups. Rigorous complexity estimates, implementation hints, and advanced exercises are included throughout. The central theme is the description of nearly linear time algorithms, which are extremely fast both in terms of asymptotic analysis and of practical running time. The book fills a significant gap in the symbolic computation literature for readers interested in using computers in group theory.

Term rewriting systems, which developed out of mathematical logic, consist of sequences of discrete steps where one term is replaced with another. Their many applications range from automatic theorem proving systems to computer algebra. This book begins with several examples, followed by a chapter on basic notions that provides a foundation for the rest of the work. First-order and higher-order theories are presented, with much of the latter material appearing for the first time in book form. Subjects treated include orthogonality, termination, lambda calculus and term graph rewriting. There is also a chapter detailing the required mathematical background.

This two-volume work bridges the gap between introductory expositions of logic (or set theory) and the research literature. It can be used as a text in an advanced undergraduate or beginning graduate course in mathematics, computer science, or philosophy. The volumes are written in a user-friendly lecture style that makes them equally effective for self-study or class use. Volume I includes formal proof techniques, applications of compactness (including nonstandard analysis), computability and its relation to the completeness phenonmenon, and the first presentation of a complete proof of Godel's 2nd incompleteness since Hilbert and Bernay's Grundlagen.

Knowledge management and knowledge-based intelligence are areas of importance in today's economy and society, and their exploitation requires representation via the development of a declarative interface whose input language is based on logic. Chitta Baral demonstrates how to write programs that behave intelligently by giving them the ability to express knowledge and reason about it. He presents a language, AnsProlog*, for both knowledge representation and reasoning, and declarative problem solving. Many of the results have never appeared before in book form but are organized here for those wishing to learn more about the subject, either in courses or through self-study.

This two-volume set on Mathematical Principles of the Internet provides a comprehensive overview of the mathematical principles of Internet engineering. The books do not aim to provide all of the mathematical foundations upon which the Internet is based. Instead, they cover a partial panorama and the key principles. Volume 1 explores Internet engineering, while the supporting mathematics is covered in Volume 2. The chapters on mathematics complement those on the engineering episodes, and an effort has been made to make this work succinct, yet self-contained. Elements of information theory, algebraic coding theory, cryptography, Internet traffic, dynamics and control of Internet congestion, and queueing theory are discussed. In addition, stochastic networks, graph-theoretic algorithms, application of game theory to the Internet, Internet economics, data mining and knowledge discovery, and quantum computation, communication, and cryptography are also discussed. In order to study the structure and function of the Internet, only a basic knowledge of number theory, abstract algebra, matrices and determinants, graph theory, geometry, analysis, optimization theory, probability theory, and stochastic processes, is required. These mathematical disciplines are defined and developed in the books to the extent that is needed to develop and justify their application to Internet engineering.

This two-volume set on Mathematical Principles of the Internet provides a comprehensive overview of the mathematical principles of Internet engineering. The books do not aim to provide all of the mathematical foundations upon which the Internet is based. Instead, they cover a partial panorama and the key principles. Volume 1 explores Internet engineering, while the supporting mathematics is covered in Volume 2. The chapters on mathematics complement those on the engineering episodes, and an effort has been made to make this work succinct, yet self-contained. Elements of information theory, algebraic coding theory, cryptography, Internet traffic, dynamics and control of Internet congestion, and queueing theory are discussed. In addition, stochastic networks, graph-theoretic algorithms, application of game theory to the Internet, Internet economics, data mining and knowledge discovery, and quantum computation, communication, and cryptography are also discussed. In order to study the structure and function of the Internet, only a basic knowledge of number theory, abstract algebra, matrices and determinants, graph theory, geometry, analysis, optimization theory, probability theory, and stochastic processes, is required. These mathematical disciplines are defined and developed in the books to the extent that is needed to develop and justify their application to Internet engineering.

Probalistic reasoning with graphical models, also known as Bayesian networks or belief networks, has become an active field of research and practice in artifical intelligence, operations research and statistics in the last two decades. The success of this technique in modeling intelligent decision support systems under the centralized and single-agent paradim has been striking. In this book, the author extends graphical dependence models to the distributed and multi-agent paradigm. He identifies the major technical challenges involved in such an endeavor and presents the results gleaned from a decade's research.

This text is ideal for advanced undergraduate or beginning graduate students. The author first develops the necessary background in probability theory and Markov chains before using it to study a range of randomized algorithms with important applications in optimization and other problems in computing. The book will appeal not only to mathematicians, but to students of computer science who will discover much useful material. This clear and concise introduction to the subject has numerous exercises that will help students to deepen their understanding.

The discrepancy method has produced the most fruitful line of attack on a pivotal computer science question: What is the computational power of random bits? It has also played a major role in recent developments in complexity theory. This book tells the story of the discrepancy method in a few succinct independent vignettes. The chapters explore such topics as communication complexity, pseudo-randomness, rapidly mixing Markov chains, points on a sphere, derandomization, convex hulls and Voronoi diagrams, linear programming, geometric sampling and VC-dimension theory, minimum spanning trees, circuit complexity, and multidimensional searching. The mathematical treatment is thorough and self-contained, with minimal prerequisites. More information can be found on the book's home page at http://www.cs.princeton.edu/~chazelle/book.html.

Covering both theory and progressive experiments, Quantum Computing: From Linear Algebra to Physical Realizations explains how and why superposition and entanglement provide the enormous computational power in quantum computing. This self-contained, classroom-tested book is divided into two sections, with the first devoted to the theoretical aspects of quantum computing and the second focused on several candidates of a working quantum computer, evaluating them according to the DiVincenzo criteria. Topics in Part I Linear algebra Principles of quantum mechanics Qubit and the first application of quantum information processing-quantum key distribution Quantum gates Simple yet elucidating examples of quantum algorithms Quantum circuits that implement integral transforms Practical quantum algorithms, including Grover's database search algorithm and Shor's factorization algorithm The disturbing issue of decoherence Important examples of quantum error-correcting codes (QECC) Topics in Part II DiVincenzo criteria, which are the standards a physical system must satisfy to be a candidate as a working quantum computer Liquid state NMR, one of the well-understood physical systems Ionic and atomic qubits Several types of Josephson junction qubits The quantum dots realization of qubits Looking at the ways in which quantum computing can become reality, this book delves into enough theoretical background and experimental research to support a thorough understanding of this promising field.

This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to noncompositional methods, whose presentation culminates in an exposition of the communication-closed-layers (CCL) paradigm for verifying network protocols. Compositional concurrency verification methods reduce the verification of a concurrent program to the independent verification of its parts. If those parts are tightly coupled, one additionally needs verification methods based on the causal order between events. These are presented using CCL. The semantic approach followed here allows a systematic presentation of all these concepts in a unified framework which highlights essential concepts. The book is self-contained, guiding the reader from advanced undergraduate level to the state-of-the-art. Every method is illustrated by examples, and a picture gallery of some of the subject's key figures complements the text.

C++ is capable of tackling a whole range of programming tasks. The purpose of this book is to give breadth and depth to C++ programmers’ existing experience of the language by representing a large number of algorithms, most of them implemented as ready-to-run (and standalone) programs. The programs are as readable as possible without sacrificing too great a degree of efficiency, generality, portability and robustness. Both the classes and programs are designed to demonstrate major programming principles. There is coverage of two key language features - templates and exception handling - apart from which the reader is assumed to have working knowledge of C++. Besides traditional subjects, such as quicksort and binary trees, this book also covers some less well-known topics, including multi-precision arithmetic, route planning and external sorting. Demonstration programs for these and many other exciting applications are based on C++ classes which you can also use in programs of your own.

This volume contains the proceedings of the 17th International SPIN Workshop on Model Checking Software (SPIN 2010). The workshop was organized by and held at the University of Twente, The Netherlands, on 27-29 September 2010. The workshop was co-located with the 5th International Conference on Graph Transformation (ICGT 2010) and several of its satellite workshops, and with the joint PDMC and HiBi workshops, on Parallel and Distributed Methods for veri?Cation and on High-performance computational systems Biology. The SPIN workshopis a forum for practitioners and researchersinterested in state-spaceanalysisofsoftware-intensivesystems.Thisisapplicableinparticular to concurrent and asynchronous systems, including protocols. The name of the workshop re?ects the SPIN model checking tool by Gerard J. Holzmann, which won the ACM System Software Award 2001, and is probably the most widely used industrial-strength model checker around. The focus of the workshop is on theoretical advances and extensions, al- rithmic improvements, and empirical evaluation studies of (mainly) state-based modelcheckingtechniques,asimplementedintheSPINmodelcheckerandother tools. The workshop encourages interaction and exchange of ideas with all - lated areas in software engineering. To this end, we co-located SPIN 2010 with the graph transformation, and high-performance analysis communities. This year, we received 33 submissions, divided between 29 regular and 4 tool papers.Eachpaperwasrigorouslyreviewedbyatleastfourreviewers,andjudged onitsqualityandits signi?canceandrelevanceforSPIN.Weaccepted13regular papers, and 2 tool papers for presentation and for publication in this volume.

Written for students in mathematics, computer science, operations research, statistics, and engineering, this text presents a concise lively survey of several fascinating non-calculus topics in modern applied mathematics. Sheldon Ross, noted textbook author and scientist, covers probability, mathematical finance, graphs, linear programming, statistics, computer science algorithms, and groups. He offers an abundance of interesting examples not normally found in standard finite mathematics courses: options pricing and arbitrage, tournaments, and counting formulas. The chapters assume a level of mathematical sophistication at the beginning calculus level, that is, a course in pre-calculus.

Modern scientific computational methods are undergoing a transformative change; big data and statistical learning methods now have the potential to outperform the classical first-principles modeling paradigm. This book bridges this transition, connecting the theory of probability, stochastic processes, functional analysis, numerical analysis, and differential geometry. It describes two classes of computational methods to leverage data for modeling dynamical systems. The first is concerned with data fitting algorithms to estimate parameters in parametric models that are postulated on the basis of physical or dynamical laws. The second is on operator estimation, which uses the data to nonparametrically approximate the operator generated by the transition function of the underlying dynamical systems. This self-contained book is suitable for graduate studies in applied mathematics, statistics, and engineering. Carefully chosen elementary examples with supplementary MATLAB (R) codes and appendices covering the relevant prerequisite materials are provided, making it suitable for self-study.

This textbook offers a unified, self-contained introduction to the field of term rewriting. Baader and Nipkow cover all the basic material--abstract reduction systems, termination, confluence, completion, and combination problems--but also some important and closely connected subjects: universal algebra, unification theory, Gröbner bases, and Buchberger's algorithm. They present the main algorithms both informally and as programs in the functional language Standard ML (An appendix contains a quick and easy introduction to ML). Key chapters cover crucial algorithms such as unification and congruence closure in more depth and develop efficient Pascal programs. The book contains many examples and over 170 exercises. This is also an ideal reference book for professional researchers: results spread over many conference and journal articles are collected here in a unified notation, detailed proofs of almost all theorems are provided, and each chapter closes with a guide to the literature.

The twin themes of computational complexity and information pervade this 1998 book. It starts with an introduction to the computational complexity of continuous mathematical models, that is, information-based complexity. This is then used to illustrate a variety of topics, including breaking the curse of dimensionality, complexity of path integration, solvability of ill-posed problems, the value of information in computation, assigning values to mathematical hypotheses, and new, improved methods for mathematical finance. The style is informal, and the goals are exposition, insight and motivation. A comprehensive bibliography is provided, to which readers are referred for precise statements of results and their proofs. As the first introductory book on the subject it will be invaluable as a guide to the area for the many students and researchers whose disciplines, ranging from physics to finance, are influenced by the computational complexity of continuous problems.

The goal of this book is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and the simulation methods used for proving its correctness. The authors concentrate in the first part on the general principles needed to prove data refinement correct. They begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The topics of Hoare Logic and the Refinement Calculus are introduced and a general theory of simulations is developed and related to them. Accessibility and comprehension are emphasized in order to guide newcomers to the area. The book's second part contains a detailed survey of important methods in this field, such as VDM, and the methods due to Abadi & Lamport, Hehner, Lynch and Reynolds, Back's refinement calculus and Z. All these methods are carefully analysed, and shown to be either imcomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all these methods can be described and analyzed in terms of two simple notions: forward and backward simulation. The book is self-contained, going from advanced undergraduate level and taking the reader to the state of the art in methods for proving simulation.

All traditional implementation techniques for functional languages fail to avoid useless repetition of work. They are not "optimal" in their implementation of sharing, often causing a catastrophic, exponential explosion in reduction time. Optimal reduction is an innovative graph reduction technique for functional expressions, introduced by Lamping in 1990, that solves the sharing problem. This work, the first on the subject, is a comprehensive account by two of its leading exponents. Practical implementation aspects are fully covered as are the mathematical underpinnings of the subject. The relationship to the pioneering work of Lévy and to Girard's more recent "Geometry of Interaction" are explored; optimal reduction is thereby revealed as a prime example of how a beautiful mathematical theory can lead to practical benefit. The book is essentially self-contained, requiring no more than basic familiarity with functional languages. It will be welcomed by graduate students and research workers in lambda calculus, functional programming or linear logic.

This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological spaces that have proved of use in the modeling of various families of typed lambda calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is now known as Domain Theory, and was founded as a subject by Scott and Plotkin. One of the main concerns is to establish links between mathematical structures and more syntactic approaches to semantics, often referred to as operational semantics, which is also described. This dual approach has the double advantage of motivating computer scientists to do some mathematics and of interesting mathematicians in unfamiliar application areas from computer science.

Most object-oriented or functional languages are higher order languages, i.e. ones in which the means of manipulation (e.g. object or function) can itself be manipulated. This 1998 book contains a collection of original articles about recent developments in operational semantics for higher order programming languages by some of the leading researchers in the field. Operational techniques are important because they are closer to implementations and language definitions than more abstract mathematical techniques such as denotational semantics. One of the exciting developments reflected by the book is that mathematical structures and techniques used in denotational semantics (such as fixpoint induction) may be recovered from a purely operational starting point. The book surveys and introduces techniques such as contextual equivalence, applicative bisimulation, logical relations, improvement relations, explicit models of memory management, and labelling techniques for confluence properties. It treats a variety of higher order languages, based on functions, processes and objects, with and without side effects, typed and untyped.

The combinatorial theory of species, introduced by Joyal in 1980, provides a unified understanding of the use of generating functions for both labeled and unlabeled structures as well as a tool for the specification and analysis of these structures. This key reference presents the basic elements of the theory and gives a unified account of its developments and applications. The authors offer a modern introduction to the use of various generating functions, with applications to graphical enumeration, Polya Theory and analysis of data structures in computer science, and to other areas such as special functions, functional equations, asymptotic analysis, and differential equations.

Type theory is one of the most important tools in the design of higher-level programming languages, such as ML. This book introduces and teaches its techniques by focusing on one particularly neat system and studying it in detail. By concentrating on the principles that make the theory work in practice, the author covers all the key ideas without getting involved in the complications of more advanced systems. This book takes a type-assignment approach to type theory, and the system considered is the simplest polymorphic one. The author covers all the basic ideas, including the system's relation to propositional logic, and gives a careful treatment of the type-checking algorithm that lies at the heart of every such system. Also featured are two other interesting algorithms that until now have been buried in inaccessible technical literature. The mathematical presentation is rigorous but clear, making it the first book at this level that can be used as an introduction to type theory for computer scientists.

Information is a central topic in computer science, cognitive science, and philosophy. In spite of its importance in the "information age," there is no consensus on what information is, what makes it possible, and what it means for one medium to carry information about another. Drawing on ideas from mathematics, computer science, and philosophy, this book addresses the definition and place of information in society. The authors, observing that information flow is possible only within a connected distribution system, provide a mathematically rigorous, philosophically sound foundation for a science of information. They illustrate their theory by applying it to a wide range of phenomena, from file transfer to DNA, from quantum mechanics to speech act theory.

The automatic verification of large parts of mathematics has been an aim of many mathematicians from Leibniz to Hilbert. While Gödel's first incompleteness theorem showed that no computer program could automatically prove certain true theorems in mathematics, the advent of electronic computers and sophisticated software means in practice there are many quite effective systems for automated reasoning that can be used for checking mathematical proofs. This book describes the use of a computer program to check the proofs of several celebrated theorems in metamathematics including those of Gödel and Church-Rosser. The computer verification using the Boyer-Moore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology. The mechanization of metamathematics itself has important implications for automated reasoning, because metatheorems can be applied as labor-saving devices to simplify proof construction.