2
$\begingroup$

Hi,

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!

$\endgroup$
3
  • $\begingroup$ Try (co)inductive types, for example in Coq: google.com.au/… - but is this a programming question, a question on (co)inductive types or something else? $\endgroup$
    – David Roberts
    Feb 20, 2013 at 6:59
  • $\begingroup$ This question should be at cstheory.stackexchange.com. $\endgroup$ Feb 20, 2013 at 15:15
  • $\begingroup$ 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! $\endgroup$ Feb 20, 2013 at 18:41

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.