Chemical Abstract Machine

Origin. Gérard Berry and Gérard Boudol, "The chemical abstract machine" (POPL 1990; journal version in Theoretical Computer Science 96, 1992), building on the Gamma multiset-rewriting formalism of Banâtre and Le Métayer. The aim was a presentation of operational semantics for concurrency in which no syntactic ordering has to be undone before a step can be taken. Milner's reaction-based presentation of the π-calculus adopted the chemical style, and Fournet and Gonthier's reflexive CHAM (1996) is the join calculus.

Models. Computation as chemical reaction. A state is a solution, a multiset of molecules; because a multiset has no order, no structural rule is needed to bring two reactants together. Membranes delimit scope. Two kinds of rule are distinguished: heating and cooling rearrange a solution reversibly without computing, while reaction rules consume molecules and produce new ones. Concurrency is built in — independent reactions occur without an interleaving rule — and nondeterminism is the choice of which reaction fires.

Formalism.

Solution: S = M₁, M₂, ..., Mₙ (multiset) Molecules separated by comma. Order irrelevant (commutative).

Membrane: ⟨S⟩: solution in membrane. Scope delimiter.

Structural equivalence (heating/cooling): M, ⟨S⟩ ⇌ ⟨M, S⟩ (molecule crosses membrane) Airlock law.

Reaction rule: M₁, ..., Mₙ → M'₁, ..., M'ₘ Consumes left, produces right.

Chemical law: If S → S' and S ≡ T, T' ≡ S': Then T → T' Reactions work modulo heating/cooling.

Example (λ-calculus): (λx.M), N → M[N/x] Application as reaction.

Concurrency: Multiple reactions can fire simultaneously. Independent molecules react in parallel. Non-determinism: choice of reaction.

Four rule classes: Heating/cooling (structural, reversible). Reaction (irreversible, the computation). Airlock (membrane crossing). Chemical law (reaction closed under structural equivalence).

Join patterns (Join calculus): x⟨v⟩, y⟨w⟩ → P Synchronization via multi-way join. The reflexive CHAM adds rules that create rules.

Presentations given by Berry and Boudol: TCCS and CCS, the fragment of Milner's π-calculus used to encode the λ-calculus, and a sketched higher-order concurrent λ-calculus. Each chemical presentation replaces a set of SOS congruence rules.

Symbols.

Symbol	Unicode	Name	Meaning
,	—	Comma	Multiset union
⟨⟩	—	Membrane	Scope
→	U+2192	Reaction	Computation
⇌	U+21CC	Heating	Structural equiv
≡	U+2261	Identical to	Structural equivalence, the closure of ⇌
S	—	Solution	Multiset of molecules
M	—	Molecule	Term in solution

Metatheory. The essential move is the chemical law: reaction is closed under structural equivalence, so a reduction relation is defined on solutions modulo ≡ rather than on syntax trees. This is the format Milner adopted for the π-calculus, where reduction up to structural congruence replaces the congruence rules of a structural operational semantics; the same content is expressed with a much smaller rule set. Heating and cooling are inverse, so they generate an equivalence and no computation, and progress is made only by reaction rules. Berry and Boudol gave chemical presentations of TCCS, CCS, and the fragment of Milner's π-calculus used to encode the λ-calculus, and showed each induces the standard reduction relation, so the machine is a reformulation rather than a new semantics. The model is Turing complete, since the λ-calculus is among the encodings. The fragment whose molecules are atomic and whose reaction rules are fixed is exactly multiset rewriting, which is a place/transition Petri net: solutions are markings and reactions are transitions.

Applies to. Concurrent programming. Process calculi. Biological modeling. Distributed systems. Chemical computing.

Limitations. The machine is a presentation format, not a theory: it supplies no behavioural equivalence, no proof system and no compositional reasoning principle, so bisimulation, congruence and full-abstraction results must be imported from whatever calculus is being presented. The solution is flat, meaning any two molecules can meet, which is exactly the global-rendezvous assumption that has no distributed implementation — the join calculus exists because of it. Heating is reversible, so a machine can cycle through structural steps indefinitely without reacting, and termination arguments have to be conducted modulo ≡ rather than on the raw transition relation. Which reactions occur, as opposed to may occur, is left to an unspecified scheduler, so fairness and liveness properties are not expressible. Firing a rule requires finding a matching sub-multiset, a search the notation hides.