Graphs enter as structures via mathlib's $SimpleGraph.structure$. The target structures of a graph transduction are therefore honest graph structures — symmetric and irreflexive — so the interpreting formula must define the output adjacency exactly. This matches the common convention of interpreting by an arbitrary formula $φ$ and keeping the pairs $u ≠ v$ with $φ(u,v) ∧ φ(v,u)$: that symmetrized condition is itself a formula, so both conventions define the same transduces relation on graph classes.