Design: returning dynamical computations, resumptions, and their FreeM/ITree semantics

[quangvdao]

@dtumad This issue records a design tension exposed while reviewing the new dynamical-system stack and proposes a canonical separation between stateful realizations, state-free behavior, finite programs, and interaction trees.

This is deliberately a design issue rather than an implementation PR: the central proposal seems strong, but the names, universe-polymorphic surface, and exact migration boundaries should be reviewed before cutting over downstream users.

Repository state this issue describes

This issue is anchored to main at commit f1a4c4c2e8bbd3308cecc869a20f6ddefaff4e38, the squash merge of #31 (“adopt upstream cslib free monad definitions”), on 2026-07-13.

At that commit:

• PFunctor.FreeM is the upstream cslib inductive free monad, with PolyFun retaining its polynomial-specific maps, handlers, paths, displayed families, and roll bounds.
• PFunctor.DynSystem S p is definitionally Lens (selfMonomial S) p, equivalently the coalgebra S → p.Obj S.
• DynSystem.behavior : S → PFunctor.M p gives the unique terminal-coalgebra behavior tree.
• ITree p β is the M-type with Ret, Tau, and Vis nodes.
• DynSystem.toITree currently embeds a non-returning dynamical system as an all-query ITree p PEmpty.
• PointedMachine p α β still stores State, expose, update, init, and a separate output : State → Option β.
• feat(dynamical): PointedMachine.Implements — machine-implements-program relation #29 is the only remaining open PR. It adds PointedMachine.Implements and its simulation proof method, but is still phrased against the current representation and the pre-refactor(pfunctor): adopt upstream cslib free monad definitions #31 branch tip. Its proof ideas should be preserved and restacked after this design is settled.

No existing open issue covers this proposal.

The current tension

The current definition is:

structure PointedMachine (p : PFunctor) (α β : Type) where
  State  : Type
  expose : State → p.A
  update : (s : State) → p.B (expose s) → State
  init   : α → State
  output : State → Option β

Operationally, a state with output s = some b has returned and the runner stops. Structurally, however, that state must still expose a p-position and provide updates for all its directions.

This causes several concrete problems.

1. Returned states contain unreachable interface data

An already-returned computation still needs expose and update. The clearest symptom is:

PointedMachine.pureAt :
  Point p → (α → β) → PointedMachine p α β

A pure computation needs an arbitrary Point p solely to populate an interface position that execution will never inspect. If p.A is empty, the current representation cannot express a pure returned machine at all.

2. Termination lives outside the dynamical interface

The dynamical system is over p, while termination is a second observation interpreted specially by toComp and runWith. In the polynomial account, a terminal result should instead be an interface position with no directions.

Niu–Spivak’s halting automata use exactly this construction: active positions have the ordinary input directions, while a halting position has no directions. See §4.2, especially Example 4.21, of Polynomial Functors: A Mathematical Theory of Interaction.

3. The current representation contains terminal junk

There is a canonical lossy normalization:

current PointedMachine
    → initialized DynSystem State (C β + p)

by sending:

output s = some b  ↦ return b
output s = none    ↦ query (expose s) (update s)

This discards expose and update at returned states, because they are observationally irrelevant.

The reverse direction is not canonical: to reconstruct the old structure at a returned state, one must fabricate a p-position and update map. This is precisely the arbitrary Point p required by pureAt.

Thus the proposed representation is not merely a cosmetic rearrangement. It quotients away data that the current operational semantics already treats as unreachable.

4. We have finite approximants but no canonical returning behavior

PointedMachine.toComp k : State → FreeM p (Option β) is a useful depth-k approximation:

• some b is a real result;
• none marks an unresolved cutoff;
• ResolvesIn k says the cutoff contains no none leaves;
• fuel counts visible p-queries exactly.

What is missing is the coinductive object being approximated: the possibly infinite tree that either returns a β or makes a p-query and continues.

5. Semantic correctness and bounds are currently coupled

#29 proposes:

Implements M z k :=
  ∀ x, M.toComp k (M.init x) = some <$> z x

This is a good bounded operational theorem, but it simultaneously states:

• behavioral correctness with respect to z;
• resolution/termination;
• a uniform natural-number query bound.

Once canonical coinductive behavior exists, these can be stated and composed separately.

6. “Pointed” describes only part of the data

Coalgebraically, “pointed” normally means one distinguished state 1 → State. Here init : α → State is an α-indexed family of entry states, and the terminal β-result is at least as important as initialization. The term has legitimate ancestry, but it does not expose the true computational boundary.

Proposed canonical layout

The key polynomial is:

C β + p

Its extension is, up to the evident equivalence:

(C β + p).Obj X ≃ β ⊕ p.Obj X

A node therefore either returns a β with no children, or exposes a p-query whose directions select continuation states.

The order C β + p is chosen to match the standard equation β + F X; p + C β is equivalent by the coproduct symmetry.

State-free behavior: Resumption

abbrev PFunctor.Resumption (p : PFunctor) (β : Type) :=
  PFunctor.M (PFunctor.C β + p)

Mathematically:

Resumption p β = ν X. β ⊕ p.Obj X

An element is a possibly infinite, tau-free interaction tree:

return b
query a (fun d => continuation d)

Every infinite branch performs infinitely many visible p-interactions. Silent divergence is intentionally absent.

This should be an abbreviation over the canonical M-type, not a parallel structure duplicating it.

Stateful realization: DynComputation

Schematic definition:

structure PFunctor.DynComputation
    (p : PFunctor) (α : Type) (β : Type) where
  State       : Type
  toDynSystem : DynSystem State (PFunctor.C β + p)
  init        : α → State

This is a hidden-state realization of an α-indexed family of returning computations. Computational accessors should expose the coalgebraic view ergonomically, e.g.:

DynComputation.view :
  M.State → β ⊕ p.Obj M.State

The canonical state-free semantics is:

DynComputation.denote :
  DynComputation p α β → α → Resumption p β

M.denote x := M.toDynSystem.behavior (M.init x)

Different state spaces may realize the same behavior. Raw DynComputation structures are therefore intensional presentations; equality of denotations is the canonical observational equivalence.

Conversely, any f : α → Resumption p β has the canonical realization whose states are residual resumptions, whose initialization is f, and whose transition is M.dest. Thus, morally:

DynComputation p α β / behavioral equivalence
  ≃
α → Resumption p β

Finite state-free programs: FreeM

FreeM p β = μ X. β ⊕ p.Obj X

This is the initial-algebra/well-founded counterpart of Resumption:

FreeM p β       finite/well-founded p-trees with β-leaves
Resumption p β  possibly infinite p-trees with β-leaves

There should be a canonical embedding:

FreeM.toResumption :
  FreeM p β → Resumption p β

with the expected equations and laws:

toResumption (pure b) = Resumption.pure b
toResumption (liftBind a k) =
  Resumption.query a (fun d => toResumption (k d))

toResumption (x >>= f) =
  toResumption x >>= fun b => toResumption (f b)

It should be injective: a well-founded tree does not lose information when regarded as a possibly infinite tree.

Interaction trees

Up to a polynomial equivalence, the current ITree definition is:

ITree p β = ν X. β ⊕ X ⊕ p.Obj X

corresponding to:

Ret β | Tau X | Vis (p.Obj X)

By contrast:

Resumption p β = ν X. β ⊕ p.Obj X

Therefore Resumption p β is the tau-free fragment of ITree p β.

Required bridge:

Resumption.toITree :
  Resumption p β → ITree p β

preserving pure, query, map, and bind.

A later precise characterization should be:

Resumption p β ≃ {t : ITree p β // t.TauFree}

where TauFree is formulated in the coinductively appropriate way.

There cannot be a total constructive inverse ITree p β → Resumption p β: erasing tau would need to decide whether an unbounded silent prefix eventually reaches Ret/Vis or diverges silently.

This is the semantic role of Tau, not just a representation detail. The current DynComputation proposal remains tau-free because its state advances only through visible p-directions, matching the current PointedMachine model.

The complete object matrix

FreeM p β
  = μ X. β ⊕ p.Obj X
  finite/well-founded programs

Resumption p β
  = ν X. β ⊕ p.Obj X
  possibly infinite visible behavior

ITree p β
  = ν X. β ⊕ X ⊕ p.Obj X
  visible behavior plus silent steps/divergence

DynComputation p α β
  = State + init + a coalgebra State → β ⊕ p.Obj State
  an intensional state-space realization of α → Resumption p β

Stateful presentations of FreeM

The stateful counterpart of FreeM should not initially be another foundational structure. It is a DynComputation together with well-foundedness.

A qualitative predicate should express that every query continuation eventually returns:

inductive DynComputation.TerminatesFrom
    (M : DynComputation p α β) : M.State → Prop where
  | return ...
  | query ...
      (children : ∀ d, M.TerminatesFrom (next d))

Recursion on this proof produces:

DynComputation.toFreeMFrom :
  M.TerminatesFrom st → FreeM p β

DynComputation.toFreeM :
  (∀ x, M.TerminatesFrom (M.init x)) → α → FreeM p β

This is more general than ResolvesIn k. With infinitely many possible query answers, every branch may be finite while their depths are not uniformly bounded by any k : ℕ.

The intended hierarchy is:

TerminatesFrom
  qualitative well-foundedness

ResolvesIn k
  uniform visible-query bound

ImplementsWithin k
  semantic agreement plus a uniform bound

A bundled WellFoundedDynComputation should be added only if real consumers repeatedly need to pass the computation and proof together.

No new with-tau FreeM by default

The inductive type

μ X. β ⊕ X ⊕ p.Obj X

can already be represented by something equivalent to FreeM (X + p) β. Because it is inductive, every branch contains only finitely many tau nodes, and they can be erased structurally. Finite tau adds no denotational expressivity.

If internal steps must be counted or observed, they should be an explicit event such as Tick, Yield, or InternalStep, not a semantically invisible tau.

Tau becomes essential in the coinductive setting, where it supports guarded internal recursion and silent divergence. We should therefore keep:

• FreeM tau-free;
• Resumption tau-free;
• full ITree with tau;
• no tau-aware stateful computation until an operational-semantics consumer needs it.

Canonical operations and laws

On Resumption

We should expose:

• pure / return;
• query;
• dest / one-step view;
• corec;
• map;
• universe-polymorphic bind;
• same-universe Functor/Monad instances where Lean’s classes permit them;
• bisimulation/finality principles inherited from PFunctor.M;
• transport along an interface lens.

The implementation must preserve the current universe generality. PFunctor.M itself supports independent position/direction universes, while the existing ITree surface currently aligns its universes. The Resumption core should not unnecessarily inherit that restriction; the ITree bridge may state whatever alignment it genuinely requires.

On DynComputation

Migrate or provide:

• pure : (α → β) → DynComputation p α β, with no Point p;
• contramapInput;
• mapResult (preferred over “output” to distinguish terminal results from dynamical positions);
• dimap;
• interface transport/wrapping;
• sequential composition;
• finite truncation toComp;
• run, runWith, and handler-parametric finite execution;
• ResolvesIn;
• behavioral equivalence through denote.

Sequential composition

Stateful composition may continue to use:

M₁.State ⊕ M₂.State

as a private two-phase realization. Its defining semantic theorem should be:

denote_seqComp :
  (M₁.seqComp M₂).denote x =
    M₁.denote x >>= M₂.denote

This makes behavioral associativity and identity laws consequences of the resumption monad, independent of state-sum association.

The existing fuelled sequencing theorems should then be finite-approximation/bound corollaries rather than the primary statement of correctness.

Truncation

toComp k : State → FreeM p (Option β) remains useful. It should be characterized as the depth-k truncation of denote:

• a return becomes some b;
• each visible query consumes one unit;
• an unresolved continuation at the cutoff becomes none.

This should connect:

Resumption behavior
    ↓ truncate k
FreeM p (Option β)
    ↓ no-none / ResolvesIn k
FreeM p β

Handlers

A possibly infinite Resumption cannot in general be interpreted into an arbitrary Monad: the target needs suitable iteration/domain structure, or the computation needs a termination proof.

Therefore:

• fuelled runWith into any lawful monad remains valid;
• a terminating computation can first convert to FreeM, then use the existing universal handler;
• genuinely infinite execution requires a complete Elgot/ωCPO/other appropriate semantic target and should not be smuggled into the base Monad API.

Restating “implements”

After this foundation lands, split semantic correctness from quantitative bounds.

Proposed shape:

def DynComputation.Implements
    (M : DynComputation p α β)
    (z : α → FreeM p β) : Prop :=
  ∀ x, M.denote x = (z x).toResumption

def DynComputation.ImplementsWithin
    (M : DynComputation p α β)
    (z : α → FreeM p β)
    (k : ℕ) : Prop :=
  ∀ x, M.toComp k (M.init x) = some <$> z x

We should prove the precise relationship between them, expected to be semantic implementation plus an appropriate total-roll/query bound.

The simulation machinery from #29 should be ported, but its clauses can become more canonical: a machine state and a FreeM residue should have matching return/query one-step shapes and related continuations. Separate output_pure, output_roll, and expose_eq fields are artifacts of the current split representation.

Proposed migration sequence

1. refactor(pfunctor): adopt upstream cslib free monad definitions #31: done. Treat f1a4c4c as the foundation; all new work uses upstream cslib FreeM.
2. Add Resumption without breaking current code. Define the M-type abbreviation, constructors/destructor, corecursor, map/bind, monad laws, and FreeM.toResumption.
3. Add the Resumption–ITree bridge. Implement toITree, prove constructor/map/bind compatibility, and document/formalize its tau-free image.
4. Cut over PointedMachine to DynComputation. Replace the separate output representation by DynSystem State (C β + p); migrate the operational API with no compatibility layer; replace pureAt by interface-polymorphic pure.
5. Make denote_seqComp the central sequencing theorem. Retain state-sum composition as one realization and derive behavioral laws from resumption bind.
6. Restack feat(dynamical): PointedMachine.Implements — machine-implements-program relation #29. Preserve its simulation and handler proof work, but split Implements from ImplementsWithin and state correctness through denote.
7. Add qualitative well-foundedness. Define TerminatesFrom, toFreeM, and bridges to ResolvesIn/total roll bounds.
8. Adapt VCVio. Make OracleMachine a thin specialization over DynComputation; keep concrete handlers, audited definitions, computability, and polynomial-time content downstream.

The additive Resumption and ITree PRs should land before the breaking machine cutover so the new semantic target exists before the old representation is removed.

Questions to settle during implementation

• Is DynComputation the best stateful name, or should it live under a DynSystem namespace? The mathematical boundary matters more than the final spelling.
• Should the structure store toDynSystem directly, or store a coalgebraic view : State → β ⊕ p.Obj State and derive the lens? The former maximizes reuse; the latter may be more ergonomic for constructors.
• What is the best coinductive formulation of ITree.TauFree in Lean, and should the subtype equivalence block the first bridge PR?
• Which Resumption operations can remain fully universe-polymorphic, and where do Lean’s Monad classes force aligned universes?
• Should semantic correctness be named Implements, Realizes, or Denotes? It should not silently include a resource bound.
• Do future Iris-style consumers require silent state transitions? If so, that should be a later explicit tau-aware layer rather than complicating the default cryptographic computation model.

Proposed acceptance criteria

The design is realized when:

• pure returning computations no longer require Point p;
• terminal states carry no unreachable p-interaction data;
• every DynComputation has canonical Resumption semantics;
• FreeM embeds into Resumption, which embeds into tau-free ITree;
• sequential composition denotes resumption bind;
• finite unrolling is proved to be truncation of coinductive behavior;
• qualitative termination and quantitative query bounds are distinct;
• feat(dynamical): PointedMachine.Implements — machine-implements-program relation #29’s simulation method is preserved against the new definitions;
• downstream oracle-machine theory can specialize the PolyFun abstraction rather than duplicate it.

Terminology references

• Niu–Spivak, Polynomial Functors: A Mathematical Theory of Interaction: dependent dynamical systems as lenses, halting automata via directionless terminal positions, and terminal coalgebras as polynomial trees.
• Xia et al., Interaction Trees: Representing Recursive and Impure Programs in Coq: Ret/Tau/Vis coinductive computations and weak equivalence up to silent steps.
• Uustalu et al., The Coinductive Resumption Monad: coalgebraic resumptions as potentially non-well-founded effectful computations.
• Goncharov–Milius–Rauch, Complete Elgot Monads and Coalgebraic Resumptions: the relationship between iteration and coalgebraic resumption monads.