A unified treatment of structural definitions on syntax for\n capture-avoiding substitution, context application, named substitution,\n partial differentiation, and so on

We introduce a category-theoreticabstraction of a syntax with auxiliary\nfunctions, called an admissiblemonad morphism. Relying on an abstract form of\nstructural recursion,we then design generic tools to construct admissible monad\nmorphismsfrom basic data. These tools automate ubiquitous standard patternslike\n(1) defining auxiliary functions in successive, potentiallydependent layers,\nand (2) proving properties of auxiliary functions byinduction on syntax. We\ncover significant examples from theliterature, including the standard\nlambda-calculus withcapture-avoiding substitution, a lambda-calculus with\nbindingevaluation contexts, the lambda-mu-calculus with named substitution,\nandthe differential lambda-calculus.\n