Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.


The theme here is Automatic Differentiation. Consider the following (theoretical) data type:

class adouble2 {

double data;

adouble value;

adouble derivative;


It's my alternative to the classical:

class adouble {

double value;

double derivative;


that would (hopefully) enable fully functional autodiff on functions like

$f(x) = sin(x) + \dot{g}(e^{x^2})$,

where there are derivatives of other known functions in the body of the main function, nested to arbitrary depth.

I would like to perform math on these objects in order to prove that they can do the job, but I haven't found a proper structure to do so. So my question would be:

What algebraic structure is suitable for representing self-referential data types? and why!

For example, I know a ring wouldn't be suitable, because I would have to define a set

$\mathbb{A} = \{ (a, x, \dot{x}) : a\in\mathbb{R}; x, \dot{x}\in\mathbb{A} \}$

with the sum

$++ : \mathbb{A}\times\mathbb{A}\to\mathbb{A}$ where $(a, x, \dot{x}) ++ (b, y, \dot{y}) := (a+b, x++y, \dot{x}++\dot{y})$

And the problem with this is that neither the set $A$ is well-defined nor I can prove $++$ is closed in $A$, nor I can define a product or do anything at all.

From the research I have done so far, I am under the slight impression that coalgebras might do, but I wouldn't like to dive

into something that complicated unless strictly necessary. If that would be the case, then a second question arises: how exactly a coalgebra can represent an object like adouble2 ?

As background info I shall add that this research project has just been assigned to me (an undergraduate) so it is barely starting.

Please excuse my English, and thanks for reading!

share|cite|improve this question
Try (co)inductive types, for example in Coq:… - but is this a programming question, a question on (co)inductive types or something else? –  David Roberts Feb 20 '13 at 6:59
This question should be at –  Neil Toronto Feb 20 '13 at 15:15
My interest is purely mathematical. I am not willing to implement anything at all, just to prove! Already bagan to look for (co)inductive types though, thanks! –  A. Arredondo Feb 20 '13 at 18:41

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.