PaperlayerView exact revision on arXiv

Source-linked AI summary

Interaction Trees: Representing Recursive and Impure Programs in Coq

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic

arXiv:1906.00046v2cs.PL

TL;DR

Existing approaches to interactive, effectful, and potentially nonterminating computations can be difficult to compose, reason about, and execute. The paper introduces coinductive interaction trees and a Coq library with event handlers, equational reasoning, and extraction support, then demonstrates the approach through trace correspondence and a verified compiler. The resulting compiler proof establishes termination-sensitive bisimulation using structural induction and equational reasoning, while the library hides most coinductive proof details from users.

  • Problem

    Interactive, effectful, and potentially nonterminating computations need representations that support compositional reasoning and executable formal models.

  • Method

    The paper develops coinductive interaction trees as a Coq library with monadic event handlers, weak-bisimulation theory, recursion abstractions, and extraction support.

  • Results

    The Imp-to-Asm case study proves compiler correctness as a termination-sensitive bisimulation, while ITrees are shown weakly bisimilar exactly when their event-trace sets coincide.

  • Takeaways & Limitations

    ITrees provide an executable denotational foundation for formal verification of interactive systems, with library abstractions that let clients reason without explicit coinduction tactics.

  • Takeaways & Limitations

    Adapting the library to other proof assistants may require substantial work because some systems lack coinductive types or higher-order types.

Abstract

from arXiv · show

"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from "event handlers", which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification. We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq's coinduction tactics. To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.

1 INTRODUCTION

Interaction trees (ITrees) provide a Coq library and denotational framework for modeling interactive, effectful, recursive, and potentially nonterminating computations while remaining executable and compositionally reasoned about. The paper demonstrates this approach through event interpretation, equational reasoning, extracted code, trace correspondence, and a termination-sensitive compiler-correctness proof.

  • Core contribution: ITrees model interactive, effectful, and potentially nonterminating computations in Coq while supporting program extraction.They provide denotational semantics despite Gallina’s purity and termination constraints, and extracted code can link to external libraries for execution, testing, and implementation.
  • Core contribution: The coinductive structure and silent Tau effect represent nontermination, silently diverging computations, and weak bisimulation without step-indexed fuel.Weak bisimulation can quotient away silent steps while remaining termination sensitive.
  • Core contribution: The authors mechanize iteration results and use ITrees to define semantics for mutually recursive interactive components compositionally.The paper presents this as a practical consequence of the theory of iteration.
  • Core contribution: The library provides monadic event handlers and equational reasoning principles for compositionally interpreting events and structuring recursive definitions.It develops ITrees as a monad, supports KTrees and event handlers, and hides brittle coinductive reasoning behind library abstractions.
  • Case study: The verified Imp-to-Asm compiler case study proves a termination-sensitive bisimulation by structural induction and equational reasoning over ITree denotations.The proof hides the coinductive nature of the result and relates the semantics of both languages after interpreting events into state monads.
  • Connections and implementation: ITrees connect executable denotational developments with trace-based and operational models because weak bisimilarity coincides with equality of event-trace sets.This correspondence supports formal connections to non-executable small-step semantics and related formalisms.

2 INTERACTION TREES

Interaction trees represent interactive computations as coinductive trees that can return, perform silent steps, expose events, or diverge. Their monadic composition, weak bisimulation, KTree abstractions, and equational laws support structured construction and reasoning about recursive effectful programs.

  • ITree structure: ITrees represent computations that interact with an environment through visible events, may return values, or may diverge without producing visible events.The event interface E determines interactions, while R is the result type returned if computation halts.
  • ITree structure: The constructors Ret, Tau, and Vis encode immediate termination, silent internal computation, and an event with a response-dependent continuation.Vis carries an external event and a continuation that produces the rest of the computation for each environment response.
  • ITree structure: Coinductive definitions and explicit Tau steps let ITrees represent potentially infinite interactions and silent divergence without relying on step-indexed fuel.The library uses the recommended negative coinductive form in its implementation, although the displayed historical definition uses positive coinduction.
  • Composing ITree computations: For any event type E, itree E forms a monad: bind replaces each Ret r with k r, while ret injects a value into Ret.The monadic interface supports sequencing and treats events as uninterpreted effects related to free-monad operations.
  • ITree equivalences: Weak bisimulation identifies trees with the same terminal and visible behavior while permitting finite Tau differences, but it remains termination-sensitive to infinite Tau behavior.The library also proves that weak bisimulation is an equivalence relation and that strong bisimulation implies it.
  • KTrees: KTrees represent functions returning ITrees in point-free form, and their composition forms the Kleisli category with associative composition and identity ret.The library also exposes cocartesian structure and derives operations such as bimap and swap from sum-type combinators.

3 SEMANTICS OF EVENTS AND MONADIC INTERPRETERS

ITree event handlers assign monadic meanings to events, and interpreters fold those handlers over trees while preserving monadic structure. The section develops state interpretation, compositional event algebra, and event-type inclusion mechanisms.

  • Event handlers and interpreters: Event handlers map events into monadic operations, while interpreters fold those handlers over ITrees.A valid interpretation respects the ITree monad’s ret and bind operations.
  • State interpretation: State handlers interpret Get and Put events as state-monad operations over an input state.The handler computes an output state and result in stateT S (itree E).
  • State interpretation: The state interpreter satisfies monad-morphism laws and yields the expected equations for reading, writing, and eliminating redundant reads.It maps get to the unchanged state and put s' to the updated state with unit.
  • General interpretation: A general interp operator works for any monad equipped with iter by interpreting each tree constructor and continuing with the resulting tree state.Its core laws preserve monadic structure and interpret trigger e by applying the handler to e.
  • Event composition: The library supports combining event types and automatically lifting computations across structural subevent inclusions.The E -< F typeclass synthesizes inclusions such as IO into X +' IO +' Y.
  • Event-handler algebra: Handlers compose through event interpretation, forming a cocartesian category with trigger as identity and case_, inl_, and inr_ as structural operations.These operations support compositional translation between event types.

4 ITERATION AND RECURSION

The library provides iteration and recursion combinators that make recursive ITrees compositional and hide Coq’s coinductive proof complexity. These abstractions support general recursion, mutual recursion through events, and equational reasoning.

  • Recursion abstractions: Corecursive definitions are exposed through abstractions that avoid Coq’s brittle, non-compositional coinduction mechanisms.Library users generally need only typecheck recursive definitions, including those with divergent behavior.
  • Iteration and recursion combinators: The library exports iter and loop for iteration, plus mrec for mutually recursive event handlers.The three constructs are mutually inter-derivable but support distinct recursive-definition styles.
  • Iteration: iter repeatedly applies a body that returns either a next state or a final result, without assuming a particular loop-body shape.Its implementation avoids the intensional guardedness check required by cofix.
  • Iteration: The equations for iter establish fixed-point, parameter, composition, and codiagonal identities, giving continuation trees an iterative-category structure.The proofs use weak-bisimulation coinduction, while the resulting equations hide that complexity from library users.
  • Iteration: MonadIter generalizes iteration beyond ITrees, with instances for ITrees, the predicate monad, and lifted monad transformers such as stateT S M.Implementations must satisfy the iterative laws.
  • Mutual recursion: mrec represents recursive calls as events and recursively handles those events while preserving other effects.It is characterized by an unfolding equation and satisfies the same iterative equations as iter for event handlers.

5 CASE STUDY: VERIFIED COMPILATION OF IMP TO ASM

The case study defines ITree-based denotational semantics for Imp and Asm, then proves compiler correctness as a termination-sensitive bisimulation using structural induction and equational rewriting.

  • Case study: The compiler translates a simple imperative language, Imp, into an assembly language, Asm, using ITree-based denotational semantics.The case study formalizes and verifies the compiler in Coq.
  • Imp semantics: Imp semantics map syntax to ITrees, using the iter combinator to represent While and event types for state operations.Expressions and statements produce itree E unit values, with GetVar and SetVar events representing variable accesses.
  • Imp semantics: Imp events are interpreted separately into state-transforming computations over a finite environment map.The two-stage design first gives syntax a behavioral meaning, then assigns concrete meanings to memory events.
  • Asm semantics: Asm represents computations as linked control-flow subgraphs whose denotations separate control flow from register and memory events.Its semantics use basic blocks, labels, KTrees, and event handlers for state effects.
  • Compiler correctness: The correctness theorem states that each Imp program and its compiled Asm program are equivalent through a termination-sensitive bisimulation.The bisimulation compares executions up to Tau and relates terminating states through a simulation relation.
  • Compiler correctness: The proof is purely equational and proceeds by structural induction, with coinductive reasoning hidden behind the ITree library.The proof relies on equations for KTree and linking combinators such as app_asm_correct and seq_asm_correct.

6 EXTRACTING ITREES

ITrees can be extracted to executable OCaml code and run with external event handlers, supporting debugging, testing, and executable interpreters for larger systems.

  • Extraction: ITree definitions extract to lazy OCaml datatypes whose evaluation is forced by observing the tree.The extracted echo example demonstrates executable interaction-tree representations.
  • Execution: A driver traverses an extracted ITree and handles visible events, interpreting Input and Output through OCaml operations.The example uses read_int for Input and print_int for Output.
  • Applications: ITree extraction supports executable interpreters for LLVM code and web-server specifications.The Vellvm interpreter tests small- to medium-sized LLVM samples, while web-server models support linking to C and property-based testing.
  • Applications: The extracted Vellvm interpreter handles LLVM features including recursion and loops and is reported to perform well enough for small- to medium-sized code samples.All but the outermost run driver are extracted from Coq.

7 RELATING ITREES AND TRACE SEMANTICS

The paper relates ITree traces to operational trace semantics by defining refinement and equivalence over possible traces, showing that trace equivalence coincides with weak bisimulation.

  • Operational semantics: Relational operational semantics quantify over environmental inputs, making their propositional encodings difficult to extract as executable programs.The universal quantification over responses prevents direct extraction of such semantics from Coq.
  • Trace semantics: ITrees instead directly denote sets of possible traces recording visible events, environment responses, termination, and partial execution.The trace datatype includes TEnd, TRet, TEventResponse, and TEventEnd cases.
  • Trace semantics: Trace refinement requires every trace of one ITree to be a trace of another, while trace equivalence requires refinement in both directions.These notions are defined using the is_trace_of predicate.
  • Equivalence: Trace equivalence coincides with weak bisimulation for ITrees.The paper states t1 ≈ t2 if and only if t1 ≡ t2.
  • Limitations and extensions: Trace refinement can treat silent divergence and finite Tau insertions or removals differently, while richer refinements can accommodate nondeterminism.The paper notes that finite traces cannot distinguish spin from bottom and discusses alternative refinement definitions.

8 RELATED WORK

The related work situates ITrees among monads, free monads, resumptions, algebraic effects, and dependent type theory. It emphasizes ITrees’ general-purpose Coq library, equational reasoning, compositional interpretation, and support for recursive interactive computations.

  • Monads and free monads: Unlike the directly coinductive free-monad formulation, ITrees expose continuations in Vis and satisfy Coq’s positivity requirements.The directly nested formulation can violate strict positivity for some event functors.
  • Monads and free monads: ITrees extend free-monad ideas with coinduction, enabling representations of nonterminating computations without fuel or step indexing.A silent Tau effect supports silent divergence and weak bisimulation.
  • Resumptions and Coq libraries: ITrees provide a general-purpose alternative to specialized coinductive semantics by combining functional denotational interpreters with extraction-compatible recursion operators.The comparison with prior Imp semantics highlights generality beyond global state and compatibility with executable artifacts.
  • Algebraic effects: The library connects event interfaces and handlers to algebraic effects, with handlers interpreting visible operations and continuations into monadic actions.ITree interpretation requires explicitly invoking handlers such as interp_state, unlike languages with native algebraic effects.
  • Effects in type theory: Compared with dependent type theories that prohibit silent steps, ITrees allow general recursion while retaining an equational theory for interpreters.Earlier approaches may support recursive computations through object encodings but do not study the general equational theory or interpreter implementation in the type theory.
  • Composition and approximation: ITrees support compositional environment reasoning, mutually recursive linking, and post-hoc approximation by trees or traces when step-indexed reasoning is useful.The related discussion connects these capabilities to environment properties and possible concurrent composition frameworks.

9 CONCLUSION

The paper concludes that ITrees provide a theoretical and practical basis for denotational semantics of impure, recursive computations in Coq. It also identifies portability and broader-effect support as remaining challenges.

  • Conclusion: ITrees offer a theoretical foundation, Coq realization, and verified compiler demonstration for impure and recursive computations.The demonstrated compiler example provides a practical use of the theory.
  • Limitations: Adapting the library to other proof assistants may require non-trivial work despite the theory being assistant-independent.The implementation choices made for the library are a source of transfer difficulty.
  • Limitations: The approach relies on extraction, coinductive types, and higher-order types, creating different portability obstacles across proof assistants.Lean lacks coinductive types, Isabelle/HOL lacks higher-order types, while Agda is described as suitable.
  • Future work: Nondeterminism and concurrency remain open directions requiring new simulations and reasoning principles.The authors also report accumulating empirical evidence that ITrees are expressive and convenient for formalization.

http://arxiv.org/ps/1906.00046v2

The supplied material identifies two figure files associated with the paper: kill9.jpeg and spin.jpeg.

  • Figures: The paper includes a figure file named kill9.jpeg.The supplied passage only identifies the file format and name.
  • Figures: Both listed figure files are available in JPEG format.No figure content or comparison is stated in the supplied passages.
  • Figures: The paper includes a figure file named spin.jpeg.The supplied passage only identifies the file format and name.
Loading 1906.00046v2…