Introduction to Bisimulation and Coinduction

Introduction to Bisimulation and Coinduction
Davide Sangorgi
Cambridge University Press, 2012

Bisimulation is a natural notion of equivalence for process algebras, and arises naturally in modal logic, graph theory and other settings.  Suppose we have a labeled transition system $(X,\stackrel{a}{\to})$, then a bisimulation $R$ is a relation satisfying:

• for all $x~R~y$, if $x \stackrel{a}{\to} x'$ then there exists $y'$ such that $y \stackrel{a}{\to} y'$
• for all $x~R~y$, if $y \stackrel{a}{\to} y'$ then there exists $x'$ such that $x \stackrel{a}{\to} x'$

Then bisimilarity is defined as the largest relation $\approx$ that contains every bisimulation.  Equivalently, the largest relation closed under the above two rules.

Bisimulation is defined coinductively, that is, in terms of the greatest fixed point of a monotone operator, in contrast to inductive definitions (least fixed-points) that are more familiar to computer scientists.  Bisimulation and coinduction are general concepts, but they have generally been covered in the context of process calculi such as CCS or the $\pi$-calculus, or for reasoning about infinite streams or other infinite behaviors in functional programming.  This book provides an accessible treatment of both topics in their own right, rather than as a secondary matter arising in the study of process calculus or streams.
Read more »

Programming with Higher-Order Logic

Programming with Higher-Order Logic
Dale Miller and Gopalan Nadathur
Cambridge University Press 2013

Church's higher-order logic, based on the typed $\lambda$-calculus, is a foundation of mathematics and computer science.  It underpins a number of other influential logics and type theories, including systems for formalized mathematics such as LF, HOL and Coq, which in turn have led to interesting developments relevant to mainstream mathematics such as formal proofs of the Four-Color Theorem and Feit-Thompson Theorem in Coq, as well as the Homotopy Type Theory program initiated by Voevodsky.  This book is about higher-order logic viewed in a different light, as a foundation for programming, specifically following the computation-as-deduction approach taken in logic programming languages such as Prolog.  Higher-order logic programming builds on higher-order unification, and generalizes Horn clauses over first-order terms in Prolog to hereditary Harrop formulas over higher-order terms in languages such as $\lambda$Prolog. One might view (higher-order) logic programming as a tool deserving a place in a logician's toolbox analogous to numerical or symbolic tools for analysis: not a replacement for mathematical reasoning, but a framework for experimentation and automation.

Read more »