Term Graph Syntax for Multi-Algebras

Multi-algebras allow to model nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results. Starting from a functorial presentation of multi-algebras based on "gs-monoidal theories" we argue that specifications for multi-algebras should be based on the notion of term graphs instead of on standard terms. We consider the simplest case of (term graph) equational specification, showing that it enjoys an unrestricted form of substitutivity. We discuss the expressive power of equational specification for multi-algebras, and we sketch possible extensions of the calculus.