I’m the teaching assistant for MATH116 this semester and the office hours I originally chose didn’t suit most of my students. To remedy this, I set up a doodle poll asking them which times they could do. I downloaded their responses as an Excel table and exported it .csv (comma-separated values).
Then I wrote a script to “parse” the .csv and figure out which 3 hours to choose in order to minimise the number of people who can’t come to any of them. Works pretty well!
I’ve been working with derivatives recently and once again found that the definition of the total derivative doesn’t make too much sense.
A function is differentiable at iff there exists a linear map such that .
The supposedly intuitive explanation is that is the best linear approximation of at :
The problem with this definition is that I couldn’t find a meaning for the word “best” to match the equation. Suggesting that the derivative is the solution to an optimisation problem is somewhat ironic given the fundamentality of differentiation in continuous optimisation.
Here’s an explanation that I found more intuitive: a function is differentiable at if when you plot it and zoom in closer and closer at the point then it will look more and more like a line (or hyperplane in general). We shall call this being locally linear and try to formalise it.
But first, let’s look at an example (no audio):
I have never felt this certain that addition of natural numbers is commutative! I proved it myself from scratch (including annoying steps using symmetry of equality). But more importantly it was my first proof in Agda.
So far it seems that Agda is a bit horrible to read (will probably improve once I start using optional params) and write (which should also improve once I set up agda-mode), and it took me hours to prove this theorem, but the feeling of my proof being checked and knowing that it’s correct is just spectacular!
Quite often when I hand in solutions to a problem sheet, there will be questions that I’ll be very confident about having answered well. I hand in my answers to have them marked, but I’m not expecting any corrections, I’m basically certain about my proof working. But Agda gives me a whole new level of certainty which is very exciting! Sadly it takes an enormous amount of time to translate from paper to agda but hopefully I will get better at this over time.
Many sources, including Wikipedia claim that the Yoneda lemma is a generalisation of Cayley’s theorem. I was quite puzzled by this fact, and was unhappy with some of the explanations on the internet, so I decided to prove it for myself:
First, something I call Haskell-notation: I if are functors then the set of natural transformations between them is denoted: . I also write for .
Using this notation we state (the contravariant version of) the Yoneda lemma:
For any functor we have
where the isomorphism is given by
Now let be a group, that is a category with only one object and where all arrows are isomorphisms, and set
is a natural transformation from to that has only one component (). We define a functor by
A quick glance at the definition of assures us that this is indeed a functor and we can see that is injective on arrows (as was an isomorphism).
This allows us to view it as an injective monoid homomorphism from our group to (or in very formal notation).
As functors preserve isomorphisms, it is clear that the image of is contained in , the symmetric group on the underlying set of our group.
From this we may conclude that is indeed isomorphic to a subgroup of a symmetric group.
The proof is finished, but there are some observations to be made. Firstly, most of the power of the Yoneda lemma was not used: we didn’t need the fact that was natural or that was natural.
What was crucial however is to see how our group which was born a category could be turned into a group in , using the functor.
It is also worth noting that is naturally isomorphic to so it doesn’t matter which version of the Yoneda lemma we use.
I have (more or less) successfully finished my 3rd year at Oxford and it’s time to go through my exam results, and say a few words about the subjects!
Lambda Calculus and Types – 90%
One of my favourite subjects, but as it was my last exam, I didn’t have a lot of time to revise it. In the end however I was well-prepared having proved every little lemma in the notes and redone all the problem sheets up to types. I didn’t have much time for ‘Types’, which I learned on the morning of the exam and sure enough, I chose to answer a question on them! I am happy with my result, good subject overall.
Lectures attended: none.
Read the rest of this entry »
There’s less than two weeks left before exams, trials more difficult than anything I’ve ever had to face. I find myself in a destructive loop of procrastination and anxiety. Today was a pleasant day spent revising Principles of Programming Languages. Well, it was spent coding something that was more exciting than preparing for exams.
My creation is a bounded version of the programming language IND found in Harel’s book on Dynamic Logic. The idea is that rather than assigning a fixed value to a variable we assign a list of possible/necessary variables.
This is essentially a generalisation of non-deterministic programming to something quite similar to Alternating Turing Machines.
The most interesting part of writing this code was that when I wanted to quickly copy-paste some of my old parsers I came across Counter, the first programming language I implemented.
It had remarkable similarities to the code I wrote today and made me realise how little progress I’ve made in this direction
It also reminded me of the seemingly unending inspiration I had back in those times. It appears to me that regaining this inspiration could be the most important step towards a successful academic career.
My girlfriend’s father enjoys a casual game of Bubble Breaker, he even got into the top 100 players on the website he frequents. Trying to impress/troll him lead me to the following challenge: become the Bubble Breaker champion.
Rules: pop a connected set [blob] of bubbles () to make them disappear and be replaced by bubbles above. When a row is emptied, it will be removed.
Goal: remove rows and columns
- popping a blob of size :
- removing columns in a single move:
Termination: the game ends when the goal is reached or when there are no blobs of size
Well, as I didn’t want to spend a lot of my time playing Bubble Breaker there was an obvious plan: write a program that plays it for me. To make things a lot easier I asked a more experienced programmer, exFalso to help.
Sensor: a scraper that runs the java applet and collects the data necessary for the controller
Controller: a (limited) depth-first search in the graph of game states armed with awesome heuristics
Actuator: play the game (in the applet) according to the „best” sequence of moves found by the actuator
As for heuristics we planned introduce a number of variables regarding the game state and see how they correlated with high scores.
This required exFalso to decompile the applet. The result was shocking: the decompiled code had sensible variable names and was well-formatted. After writing a Swing container for the applet exFalso realised something that would change everything: despite the fact that the applet interacted with the server on each move, it was possible to send an arbitrary high score without playing.
A note on premature optimisation
Prior to discovering that we could “print our own money” we spent a lot of time arguing about the controller: I thought it should be written in Haskell (rather unsurprisingly) and he pushed C++. His argument was that depth-first search was inherently stateful (as well as the whole algorithm) and that mutable linked lists are part of the obvious solution. Even after I convinced myself that this was rubbish, I still spent a lot of time thinking about the difference between using immutable arrays or lists of lists for the representation of the grid.
I think this is a rather striking example of premature optimisation: when you optimise code that won’t even be used in the final “product”.
Finally I’d like to thank Alex and Pete for their advice.