News aggregator
Proposal: Syntax for explicitly marking impossible cases in pattern matches
ANNOUNCE: brick 0.1 released (deprecates vtyui)
Dominic Steinitz: Stochastic Integration
Suppose we wish to model a process described by a differential equation and initial condition
But we wish to do this in the presence of noise. It’s not clear how do to this but maybe we can model the process discretely, add noise and somehow take limits.
Let be a partition of then we can discretise the above, allow the state to be random and add in some noise which we model as samples of Brownian motion at the selected times multiplied by so that we can vary the amount noise depending on the state. We change the notation from to to indicate that the variable is now random over some probability space.
We can suppress explicit mention of and use subscripts to avoid clutter.
We can make this depend continuously on time specifying that
and then telescoping to obtain
In the limit, the second term on the right looks like an ordinary integral with respect to time albeit the integrand is stochastic but what are we to make of the the third term? We know that Brownian motion is nowhere differentiable so it would seem the task is impossible. However, let us see what progress we can make with socalled simple proceses.
Simple ProcessesLet
where is measurable. We call such a process simple. We can then define
So if we can produce a sequence of simple processes, that converge in some norm to then we can define
Of course we need to put some conditions of the particular class of stochastic processes for which this is possible and check that the limit exists and is unique.
We consider the , the space of square integrable functions with respect to the product measure where is Lesbegue measure on and is some given probability measure. We further restrict ourselves to progressively measurable functions. More explicitly, we consider the latter class of stochastic processes such that
Less Simple Processes Bounded, Almost Surely Continuous and Progressively Adapted
Let be a bounded, almost surely continuous and progressively measurable process which is (almost surely) for for some positive constant . Define
These processes are cleary progressively measurable and by bounded convergence ( is bounded by hypothesis and is uniformly bounded by the same bound).
Bounded and Progressively Measurable
Let be a bounded and progressively measurable process which is (almost surely) for for some positive constant . Define
Then is bounded, continuous and progressively measurable and it is well known that as . Again by bounded convergence
Progressively Measurable
Firstly, let be a progressively measurable process which is (almost surely) for for some positive constant . Define . Then is bounded and by dominated convergence
Finally let be a progressively measurable process. Define
Clearly
The Itô Isometry
Let be a simple process such that
then
Now suppose that is a Cauchy sequence of progressively measurable simple functions in then since the difference of two simple processes is again a simple process we can apply the Itô Isometry to deduce that
In other words, is also Cauchy in and since this is complete, we can conclude that
exists (in ). Uniqueness follows using the triangle inequality and the Itô isometry.
Notes
We defer proving the definition also makes sense almost surely to another blog post.

This approach seems fairly standard see for example Handel (2007) and Mörters et al. (2010).

Rogers and Williams (2000) takes a more general approach.

Protter (2004) takes a different approach by defining stochastic processes which are good integrators, a more abstract motivation than the one we give here.

The requirement of progressive measurability can be relaxed.
Handel, Ramon von. 2007. “Stochastic Calculus, Filtering, and Stochastic Control (Lecture Notes).”
Mörters, P, Y Peres, O Schramm, and W Werner. 2010. Brownian motion. Cambridge Series on Statistical and Probabilistic Mathematics. Cambridge University Press. http://books.google.co.uk/books?id=eTbAdSrzYC.
Protter, P.E. 2004. Stochastic Integration and Differential Equations: Version 2.1. Applications of Mathematics. Springer. http://books.google.co.uk/books?id=mJkFuqwr5xgC.
Rogers, L.C.G., and D. Williams. 2000. Diffusions, Markov Processes and Martingales: Volume 2, Itô Calculus. Cambridge Mathematical Library. Cambridge University Press. https://books.google.co.uk/books?id=bDQyzoHWfcC.
Final call for papers for IFL 2015
Final call for papers for IFL 2015
Guide/Tutorial for Template Haskell?
Type level programming and Template Haskell seem like the magickal realms of Haskell. Type level programming is starting to get more and more blog posts and tutorials for, but I haven't really seen anything that details how to use Template Haskell or when it's a great idea to use. Could anyone point to some guides, tutorials, or other learning resources for this?
submitted by ephrion[link] [5 comments]
Guide/Tutorial for Template Haskell?
Type level programming and Template Haskell seem like the magickal realms of Haskell. Type level programming is starting to get more and more blog posts and tutorials for, but I haven't really seen anything that details how to use Template Haskell or when it's a great idea to use. Could anyone point to some guides, tutorials, or other learning resources for this?
submitted by ephrion[link] [5 comments]
What Math topics I must know to understand the inner workings of Haskell?
I really want to understand the mathematical underpinnings of Haskell and functional programming in general. I am basically a developer and I have coded in many other languages before coming to Haskell. With regards to Haskell, I consider myself an advanced beginner because I do understand Functors, Monads, Applicatives and some advanced Haskell concepts, but from a programmer's perspective.
I do not have a formal CS or Math background. I learned first order predicate logic by myself. Where should I go from here? What topics from CS theory should I study? What topics from Maths should I study?
submitted by wbaig[link] [10 comments]
Brent Yorgey: Catsters guide is complete!
About a year and a half ago I announced that I had started creating a guide to the excellent series of category theory YouTube videos by the Catsters (aka Eugenia Cheng and Simon Willerton). I am happy to report that as of today, the guide is finally complete!
As far as possible, I have tried to arrange the order so that each video only depends on concepts from earlier ones. (If you have any suggestions for improving the ordering, I would love to hear them!) Along with each video you can also find my cryptic notes; I make no guarantee that they will be useful to anyone (even me!), but hopefully they will at least give you an idea of what is in each video.
If and when they post any new videos (pretty please?) I will try to keep it updated.
Default implementation for <*>
Hello all
I was wondering why Applicative doesn't have a default implementation for (<*>). The following should be correct for any possible Applicative (since an Applicative is a Functor):
a <*> b = fmap (flip fmap b) aIs there any reason this isn't done that I'm not thinking of? This should give close to the same code one would write by hand anyway, and you can always override for your class if you care to.
submitted by nicheComicsProject[link] [1 comment]
Mark Jason Dominus: Reordering git commits with gitcommittree
I know, you want to say “Why didn't you just use gitrebase?” Because gitrebase wouldn't work here, that's why. Let me back up.
Say I have commit A, in which feature X does not exist yet. Then in commit C, I implement feature X.
But I realize what I really wanted was to have A, then B, in which feature X was implemented but disabled, and then C in which feature X was enabled. The C I want is just like the C that I have, but I don't have the intervening B.
I have:
no X X on A  CI want:
no X X off X on A  B  COne way to do this is to use gitrebase in edit mode to split C into B and C. To do this I would pause while rebasing C, edit C to disable feature X, commit the result, which is B, then undo the previous edits to reenable X, and continue the rebase, creating C. That's two sets of edits. I could backup the files before the first edit and then copy them back for the second edit, but that's the SVN way, so I'm not going to do that.
Now someone wants me to use gitrebase to “reorder the commits”. Their idea is: I have C. Edit C to disable feature X and commit the result as B':
no X X on X off A  C  B'Now use interactive gitrebase to reorder B and C. But this will not work. gitrebase will construct a patch for turning C into B' and will try to apply it to A. This will fail completely, because a patch for turning C into B' is a patch for turning off feature X once it is implemented. Feature X is not in A and you can't turn something off that isn't there. So the rebase will fail to apply the patch.
What I did instead was rather bizarre, using a plumbing command, but worked well. I wrote the code to disable X, and committed it as B, obtaining this:
no X X on X off A  C  BNow B and C have the files I want in them, but their parents are wrong. That is, the history is in the wrong order, but if the parent of C was B and the parent of B was A, eveything would be perfect.
But we can't just change the parents; we have to create a new commit, say B', which has the same files as B but whose parent is A instead of C, and we have to create a new commit C' which has the same files as C but whose parent is B' instead of A.
This is what gitcommittree does. You give it a tree object containing the files you want, a list of parents, and a commit message, and it creates the commit you asked for and prints its SHA1.
When we use gitcommit, it first turns the index into a tree, with gitwritetree, then creates the commit, with gitcommittree, and then moves the current head ref up to the new commit. Here we will use gitcommittree directly.
So I did:
% git checkout b XX A Switched to a new branch 'XX' % git committree p HEAD B^{tree} 10ddf433039fd3cbc5bec0c64970a45add15482e % git reset hard 10ddf433039fd3cbc5bec0c64970a45add15482e % git committree p HEAD C^{tree} ce46beb90d4aa4e2c9fe0e2e3d22eea256edceac % git reset hard ce46beb90d4aa4e2c9fe0e2e3d22eea256edceacThe first gitcommittree
% git committree p HEAD B^{tree}says to make a commit whose tree is the same as B's, and whose parent is the current HEAD, which is A. (B^{tree} is a special notation that means to get the tree from commit B.) Git pauses here to read the commit message from standard input (not shown), and prints the SHA of the new commit on the terminal. I then use gitreset to move the current head ref, XX, up to the new commit. Normally gitcommit would do this for us, but we're not using gitcommit today.
Then I do the same thing with C:
% git committree p HEAD C^{tree}makes a new commit whose tree is the same as C's, and whose parent is the current head, which looks just like B. Again it reads a commit message from standard input, and prints the SHA of the new commit on the terminal, and again I use gitreset to move XX up to the new commit.
Now I have what I want and I only had to edit the files once. To complete the task I just reset the head of my working branch to wherever XX is now, discarding the old ACB branch in favor of the new ABC branch. If there's an easier way to do this, I don't know it.
It seems to me that there have been a number of times in the past when I wanted to do something like reordering commits, and gitrebase did not do what I wanted because it reorders patches and not commits. I should keep my eyes open, and see if this comes up again, and if it is worth automating.
[ Thanks to Jeremy Leader for suggesting I write this up and to Jeremy Leader and Rik Signes for advance editing. ]
[ Adendum 20150813: a followup article ]