FM and the pi-calculus

Murdoch J. Gabbay

Abstract

It has historically been a problem to give inductive definitions of syntax-with-binding up to alpha-equivalence. Two examples of methodologies which do give such definitions are "de Bruijn indeces" and "weak Higher-Order Abstract Syntax". Datatypes of terms of the untyped lambda-calculus using the two approaches are
  • Lam_dB = Nat + Lam_dB * Lam_dB + Lam_dB

  • Lam_WH = Atm + Lam_WH * Lam_WH + Atm -> Lam_WH

    respectively, where here Nat is the set (object) of natural numbers and Atm is some set (object) of urelemente or *atoms*.

    FM techniques propose the following:

  • Lam_FM = Atm + Lam_FM * Lam_FM + [Atm] Lam_FM,

    where here [Atm]X is the *FM abstraction type*, which has properties of both a product Atm*X and a function space Atm -> X. This type does not exist in ordinary set theory (category of sets Sets), but in the closely related theory of FM sets (Schan, the Schanuel topos).

    It turns out that Schan admits a simple axiomatisation as a category of sets with an action by permutations (bijections) of Atm and a finiteness condition, which I shall give.

    The criteria for success for ``an account of syntax with binding'' are essentially those of a good programming language: can we build the datatypes we want, and define the functions on them, in a natural and intuitive way (in terms of categories, the issue is how well-behaved the arrows in Schan are). As a demonstration of FM's ability to fulfill these criteria, and subject to limits of time, I shall consider the theory of the pi-calculus. We model the transitions of the pi-calculus as elements of

  • \Pi * [Atm](Act * \Pi)

    instead of

  • \Pi * Act * \Pi .

    Thus fresh names extruded in transitions can be modelled using the bound name in $[Atm](Act * \Pi)$. Since $R$ a subset of $X * L * X$ is generally called an LTS (labelled transition system) I suggest we call R a subset of $X * [Atm](L * X)$ an LTSB (...with Binding). I will show how this simplifies the theory of the pi-calculus, and how this can all be programmed in FreshML---a dialect of ML based on a semantics in Schan---see pi-ltsb-1.fml to pi-ltsb-4.fml on my homepage.