interaction-trees.md

Interaction trees: state, ticks, and three ways to run

The complete, checked example is Examples/Tutorials/InteractionTrees.lean. Build it with lake build PolyFunExamples, then open it in your Lean editor.

Write the program

An interaction tree ITree E α is a possibly infinite tree of events from the signature E with α-leaves and explicit silent steps. Here the signature is a sum: state events on a natural number (StateE Nat, with get and put) plus one external event, a tick.

import PolyFun.ITree.Interp.State

open ITree

/-- One external event, a tick, acknowledged with no payload. -/
abbrev Tick : PFunctor.{0, 0} := ⟨Unit, fun _ => Unit⟩

/-- The program's signature: state events on a natural number, plus ticks. -/
abbrev Sig : PFunctor.{0, 0} := StateE Nat + Tick

/-- Read the counter, tick once, store the incremented value, and return the value read. -/
def bump : ITree Sig Nat := do
  let n : Nat ← lift (F := Sig) (.inl .get)
  let _ ← lift (F := Sig) (.inr ())
  let _ ← lift (F := Sig) (.inl (.put (n + 1)))
  ITree.pure n

lift a issues the event a and returns its answer; ITree.pure returns a value. The type annotation on the first line names the answer type of get, which the signature stores as a dependent fiber. As a tree, the do block is three query nodes in sequence, where query a k issues a and continues with k on the answer. bump_eq states this form, and the proofs below start from it.

Run with the state corecursor

runState bump s eliminates the state events directly, threading the state s through the tree. Each state operation becomes one silent step, the tick stays visible as a query, and the final state is returned first: runState_bump proves the result is step (query () fun _ => step (pure (s + 1, s))), by rewriting bump_eq and the exact computation rules of interpState.

Run through a handler

interp h t runs a tree in any iterative monad, answering each event through a handler h. StateE.stateHandler answers get and put in StateT Nat (ITree Tick) and leaves the tick in place. The result is not syntactically the corecursor's: it returns the pair in the other order and takes one silent step per node rather than per state operation. The library proves the two agree up to weak bisimulation and pair order (interpState_weakBisim_interp), and the file states that instance for bump.

Change the handler

The same program interprets into OptionT (ITree (StateE Nat)) through two handlers. Both pass state events on unchanged with liftHandler; on the tick, acknowledge answers and refuse fails. The file computes both runs exactly. run_interp_acknowledge_bump reads the counter, writes the incremented value, and returns some of the value read. run_interp_refuse_bump reads the counter and ends with none at the tick, so the write never happens. The proofs unfold the loop of interp once per node with iter_unfold, and the loop takes one silent step each time it moves on to the next node. Such steps are why runs are compared up to weak bisimulation: the bisimulation guide explains why silent steps must be hidden and how WeakBisim does it.

Keep exploring

• Interaction trees guide for the design, the iteration laws, and interpretation into monads.
• Computation models for when to use a tree, a resumption, or an explicit-state machine.
• Program logic for reasoning about loops with vcgen.