Comments on A Neighborhood of Infinity: Finite Differences of Types

"I think this geometric analogy can be taken ...

2010-06-13T09:24:10.650-07:00

"I think this geometric analogy can be taken a lot further and that in fact a non-trivial piece of differential geometry can be made to work with types"

care to spill the beans on what you're thinking of? =)

Duncan, You could try here if you're not a Haskell programmer (yet). '+' is disjoint union. Another place is here.

I'm really new to this stuff, but I find it fa...

2009-11-03T23:46:01.233-08:00

I'm really new to this stuff, but I find it fascinating. I'm a bit confused however: what does it mean to add two types together? i.e. it makes sense to me that X^2 is (X,X), but I don't understand, for example, why a list of Xs has type L(X)=1+X L(X). Do we just think of + as a form of union? Could you recommend a reference on this stuff?

Thanks! Duncan

There's another version here.

Jon, Interesting! That looks remarkably like a si...

2009-09-29T11:07:25.685-07:00

Jon,

Interesting! That looks remarkably like a side project of mine. Unfortunately I can't read the web site right now because despite following lots of instructions I've never managed to make the fonts work for the n-category cafe under Linux. I'll see how it looks under MacOSX tonight.

See Differential Logic and refs therein.

leihaus, I just talked about the easy case of an ...

2009-09-28T15:38:25.058-07:00

leihaus,

I just talked about the easy case of an N-element array here. Otherwise it's all in Conor's papers.

Hey Dan, i forget did you already post on the zip...

2009-09-28T15:33:35.014-07:00

Hey Dan,

i forget did you already post on the zipper-comonad connection to spell out the connection between differentiation and comonads?

Best wishes,

--greg

Sjoerd, Sounds like you're trying to find a <...

2009-09-28T14:57:44.673-07:00

Sjoerd,

Sounds like you're trying to find a Faa di Bruno style formula. I think there may be a nice way of approaching that but I have no time right now...

I was specifically going for the second difference...

2009-09-28T10:12:42.120-07:00

I was specifically going for the second difference of function composition, i.e. the difference equivalent of (fg)''(x) = f''(g(x))g^2(x) + g''(x)f'(g(x))

The problem is that I'm not sure about what the formula of second order difference should be exactly.

But I agree that having the difference view makes things easier.

I derived the first difference by guessing what the difference equivalent of the chain rule would be, and confirming the result by filling in the difference formulas.

Conor will probably agree as well, as the C&J paper says: "Of course, what’s missing here is a more semantic characterisation of dissection, with respect to which the operational rules for /|\ p may be justified."

Sjoerd, there's no need for second differences...

2009-09-28T09:49:51.914-07:00

Sjoerd, there's no need for second differences in the chain rule. We want the first difference of the composition of two functions:

Informally:

Δ(F o G)(X,Y)
=(F(G(X))-F(G(Y)))/(X-Y)
=(F(G(X)-F(G(Y))/(G(X)-G(Y)) . (G(X)-G(Y))/(X-Y)
= ΔF(G(X),G(Y)) . ΔG(X,Y)

That can now be verified using Conor's definition of dissection. When Y=X we get the usual chain rule.

I think this would have been tricky to derive without seeing dissection as finite difference.

Still doesn't seem right. Can't get the ch...

2009-09-28T07:14:38.164-07:00

Still doesn't seem right. Can't get the chain rule to work. Looking at the holes it should be something like:

Δ^2(FG)(X,Y,Z) = Δ^2G(X,Y,Z)DF(G(X),G(Z)) + DG(X,Y)DG(Y,Z)Δ^2F(G(X),G(Y),G(Z))

(I.e. the 2 holes in the same part of F or in different parts of F)

Perhaps my question makes no sense, but what would...

2009-09-28T01:20:07.168-07:00

Perhaps my question makes no sense, but what would it mean to define the "exponential" type as the type that is equal to its own derivative?

Or, can you do "type" differential equations?

Ah, I forgot that you can choose which hole goes t...

2009-09-27T15:28:17.836-07:00

Ah, I forgot that you can choose which hole goes to F and which to G.
So: Δ^2(FG)(X,Y,Z) = F(X)Δ^2G(X,Y,Z) + 2ΔF(X,Y)ΔG(Y,Z) + Δ^2F(X,Y,Z)G(Z)

This can be derived from Δ^2(f)(x,y,z) = (f(x) - 2f(y) + f(z)) / (x - y) / (y - z)

What about second order dissectioning? F.e. Δ^2(FG...

2009-09-27T15:00:18.408-07:00

What about second order dissectioning?
F.e. Δ^2(FG)(X,Y,Z) = F(X)Δ^2G(X,Y,Z) + ΔF(X,Y)ΔG(Y,Z) + Δ^2F(X,Y,Z)G(Z)
(I.e. both holes in G, one hole in F and one in G or both holes in F.)

I couldn't manage to derive this from second order finite difference. But maybe I did something wrong.

You refer to X^N as the type of arrays of elements...

2009-09-27T13:36:34.077-07:00

You refer to X^N as the type of arrays of elements of X of length N, but shouldn't they be thought of instead as N-tuples? (I guess it's a minor difference in terminology, but I think of ‘array’ as specifically connoting extensibility, with some sort of push/pull operation.)

Creighton, No exponentials needed here as N is an...

2009-09-27T12:25:38.567-07:00

Creighton,

No exponentials needed here as N is an integer.

With a bit of trickery I did once sort of get exponentials going with derivatives. But I don't think anything similar will work for finite differences and exponentials.

I think that (f(x)g(x)-f(x)g(y)+f(x)g(y)-f(y)g(y)...

2009-09-27T12:17:30.006-07:00

I think that

(f(x)g(x)-f(x)g(y)+f(x)g(y)-f(y)g(y)/(x-y)

is missing a paren before the /.

(f(x)g(x)-f(x)g(y)+f(x)g(y)-f(y)g(y))/(x-y)

Permutations and combinations crossed my mind.

2009-09-27T12:16:54.899-07:00

Permutations and combinations crossed my mind.

Okay - so categorically this is requiring finite p...

2009-09-27T12:14:17.503-07:00

Okay - so categorically this is requiring finite products, finite sums (and exponentials for your X^N example)?

What I'd be very curious about is how well this generalizes to categories with less structure - monoidal instead of cartesian, for instance.

I just did the tree example to show it works even ...

2009-09-27T10:04:18.729-07:00

I just did the tree example to show it works even for algebraic functions like square root, not to show it's easier :-) But in general, I find thinking about dissection as finite differences does make it a lot easier.

I find finitely differentiating T(X)=X+T(X)^2 dire...

2009-09-27T09:48:51.795-07:00

I find finitely differentiating T(X)=X+T(X)^2 directly easier. It becomes ΔT(X,Y) = 1 + (T(X) + T(Y))ΔT(X,Y) which is obviously a list of (T(X) + T(Y)).

One typo: "That tells us that Δf(x,y) = 1/(f(x)f(y))." I think you got 2 formulas confused here.

You should investigate interval arithmetic and int...

2009-09-27T09:30:20.840-07:00

You should investigate interval arithmetic and interval constraints. Interval constraints are used to deal with the explosive ranges that accumulate with interval arithmetic. This is relevant to floating point numbers so you can have very accurate calculations (bounded by the smallest different floating numbers possible).

e.g. http://webhome.cs.uvic.ca/~bmoa/icsp.ppt