  After surveying classical results, we introduce a generalized notion of
inference system to support structural recursion on non-well-founded data
types. Besides axioms and inference rules with the usual meaning, a generalized
inference system allows coaxioms, which are, intuitively, axioms which can only
be applied "at infinite depth" in a proof tree. This notion nicely subsumes
standard inference systems and their inductive and coinductive interpretation,
while providing more flexibility. Indeed, the classical results can be extended
to our generalized framework, interpreting recursive definitions as fixed
points which are not necessarily the least, nor the greatest one. This allows
formal reasoning in cases where the inductive and coinductive interpretation do
not provide the intended meaning, or are mixed together.
