How to Compute Fibonacci Numbers?
Some inductive proofs and some light program derivation about Fibonacci numbers. If you think the fastest way to compute Fibonacci numbers is by a closed-form formula, you should read on!
Research Blog
Adjoint Functors Induce Monads and Comonads
It is folklore knowledge that a pair of adjoint functors induces a monad and a comonad. Due to my recent work, I had to load relevant information into my brain cache. However, it turned out to be hard for me to find all the pieces of information I need in one place. Therefore, I am going to summarise here what I know and need, hoping it will be helpful for someone like me.
Deriving Monadic Programs
I started to take an interest in reasoning and derivation of monadic programs around 2016-17. Several years having passed, I collaborated with many nice people, managed to get some results published, failed to publish some stuffs I personally like, and am still working on some interesting tiny problems. This post summaries what was done, and what remains to be done.
Proving the Church-Rosser Theorem Using a Locally Nameless Representation
Around 2 years ago, for an earlier project of mine (which has not seen its light yet!) in which I had to build a language with variables and prove its properties, I surveyed a number of ways to handle binders. For some background, people have noticed that, when proving properties about a language with bound …
Proving the Church-Rosser Theorem Using a Locally Nameless Representation Read More »
Calculating Programs from Galois Connections
One is often amazed that, once two functions are identified as a Galois connection, a long list of nice and often useful properties follow from one concise, elegant defining equation. But how does one construct a program from a specification given as a Galois connection?
Evaluating Simple Polynomials
I had a chance to show the students, in 25 minutes, what functional program calculation is about. The student have just been exposed to functional programming a week ago in a three-hour course, and I have talked to them about maximum segment sum way too many times.
Sum of Squares of Differences
Given an array of integers having at least two elements, compute the sum of squares of the difference between all pairs of elements. It is not hard to quickly write up a O(N²) program using nested loops, which, I have to confess, is what I would do before reading Kaldewaij’s book and realised that it is possible to do the task in linear time using one loop.
An Exercise Utilising Galois Connections
In the recent work of Sharon and me on maximally dense segments we needed quite a number of functions to be monotonic, idempotent, etc. It only occurred to me after submitting the paper: could they be defined as Galois connections?
Finding Maximally Dense Segments
Sharon and I have finally concluded, for now, our work on the maximally dense segment problem (download the draft here), on which we have been working on and off for the past two years. Considering the algorithm itself and its derivation/proofs, I am quite happy with what we have achieved. The algorithm is rather complex, however, and it is a challenge presenting it in an accessible way. Sharon has done a great job polishing the paper, and I do hope more people would be interested in reading it and it would, eventually, inspire more work on interesting program derivations.
The Maximum Segment Sum Problem: Its Origin, and a Derivation
In a previous paper of mine, regrettably, I wrongly attributed the origin of the maximum segment sum problem to Dijkstra and Feijen’s Een methode van programmeren. In fact, the story behind the problem was told very well in Jon Bentley’s Programming Pearls.
I learned the function derivation of the maximum segment sum problem from one of Jeremy’s papers and was very amazed. It was perhaps one of the early incident that inspired my interest in program calculation.