A formal language for cyclic operads

TL;DR

This paper introduces the $ ext{-}syntax$, a formal language inspired by lambda calculus, to represent cyclic operads and demonstrates its effectiveness through rewriting methods and equivalence proofs.

Contribution

It presents a novel formal language for cyclic operads and provides a complete rewriting-based proof of their unbiased and biased definition equivalence.

Findings

The $ ext{-}syntax$ effectively models cyclic operad structures.

Rewriting methods establish the equivalence between different cyclic operad definitions.

The formalism simplifies reasoning about cyclic operads.

Abstract

We propose a $\lambda$-calculus-style formal language, called the $\mu$-syntax, as a lightweight representation of the structure of cyclic operads. We illustrate the rewriting methods behind the formalism by giving a complete step-by-step proof of the equivalence between the unbiased and biased definitions of cyclic operads.