Checking out the drawing program Milton. Got version 1.4.4 compiling and working, newer versions failed to link, but no time to debug it now. What I want to use it for is to have a whiteboard which I can easily share through VNC. But I will have to wait until I’m back at home where we have a drawing pad to test it properly.
Wrote about type theory on the mathematics page of my web-site. I also updated the deployment script for the web-site so that it uses rsync for copying to the server.
Went skating for the first time in about ten years. It was fun, and I had not completely forgotten how to move around on the ice. We were at a place called Охта Парк near Saint-Petersburg, and the skating course was actually structured as a collection of paths through the trees — making it more intersting than just skating around in a circle.
Back at the office, where my desk has been fixed. It is one of those where the push of a button makes it go up or down, but the controlbox was malfunctioning — causing the legs to misalign whevenver I adjusted it above the appropriate height for a kindergardener.
DnD night! Since two of the player characters walked through a portal to the Abyss last time, I have divided the group between this Wednesday and the next. This time Kava and Baern went exploring the Abyss, more specifically the Plane of Portals. To be honest, it was a lot easier for me as a dungeon master to manage a smaller group than usual.
Concluding a productive work week, where I have been trying to understand the connection between inductive-recursive definitions and higher-order rewrite systems. This is motivated by the concrete case of λ-calculus, which happens to be both a higher-order rewriting system and an inductive recursive type: Λ = μF.λX.X+F(X+1)+F(X)², where μ denotes the fixed-point operator for type transformations.
I have also made progress on the project from which the above is an abstraction, namely the investigation of systems with quoting operations.
Walking ouside today, I found myself smiling. After a moment’s contemplation I decided it was because of the sunlight penetrating a small opening in the clouds — a rare sight these days.
A new lamp over the kitchen table has brought more light inside as well. The lamp consists of an old, cheramic lamp screen we had at home when I was a child, a new lamp wire/bulb socket and a 2100 lumen, dimmable LED “bulb”.
Went for a walk today also, this time aiming for Smøråsfjellet. The weather was windy and cold, but the walk was nice none the less.
Tested the new thermos I got for Christmas. I really prefer its style of lids, where the combination of a narrowing inside the thermos and a rubber band at the bottom seals the thermos and a pair of channels on the lid allows for inflow of air and outflow of hot liquid when you slightly undscrew it. Other solutions I’ve seen have been overcomplicated, usually involving a button and resulting in having to clean carefully inside some hidden cavity.
Attendended a lecture on type theory by Marc Bezem at the institute for informationcs at UiB. The lecture was a short introduction to the theory, focussed on the intuions behind dependent type theory.
When it comes to dependent type theory there is a big gap between being able to use the notions (Π-types etc) informally and being able to correctly phrase the actual theory. The most carefully spelled-out type theories (notably by Per Martin-Löf), have to include a remarkable amount of structural rules to get the system working.
Working from home, which is good and relaxing1, but I realise I should find some good way to synchronise my bookmarks between home and work. But how do this without some middle-man getting their hands on my bookmarks?
Bookmarks are nice. I don’t want my browser remember every site I visit, since most sites I will not want to visit a second time. I therefore agressively bookmark and tag sites I think might be useful again. I also have no auto-completion on when searching in the titlebar, but Firefox searches my bookmarks while I type, which means that I can easily find stuff I myself thought would be useful for the future me.
My only complaint about Firefox’ way of handling bookmarks is that to browse them by tag you need to do a whole little mouse dance:
Excerpt from the Firefox documentation…
Using Tags to organize your Library
To access your tags in the Library:
- Click the library icon , then click Bookmarks. Scroll to the bottom and click Show all Bookmarks. Click the Bookmarks button Bookmarks and select Show All Bookmarks to open the Library window.
- On the left side of the Library window, click the arrow next to the Tags item. The list of tags will expand.
- Click on a tag to show what bookmarks are associated with it.
- Double click on a bookmark in the list to open it in Firefox.
Tonight is DnD night! Today we will be following Dalaran, Hyperion and Tirin, just after they have escaped the collapsing Orcus temple, which was hidden under their starting town.
Spent the workday undstanding the how simplicial sets and cubical sets are related. Marc suggested to look at the map Δop → □op induced by looking at the first as linearly ordered sets with distinct min. and max. and the other as strictly bipointed sets. This turned out to be a good idea, as it gives (at least) an adjunction between simp. and cub. sets. On the level of geometry, this constructs the cubes from simplices in a quite straight-forward way.
In the evening, Andreas came over for dinner and games. We played Black Stories (a game where you guess the details of some makabre story by asking yes/no question) and Pirate Fluxx with the dice exansion. I think Pirate Flux is the most competetive Fluxx variant.
Andreas and I are also planning to make a computer game together some time. We have lots of ideas for it, so I hope we will find time to do something about them.
Trying to recharge my batteries a bit today. Tomorrow my parents will visit and we will go looking for a new sofa. We left our previous one in Täby, and have been living without one for a few months now. We need one which can be used as a bed for guests, and we have decided we want one without a chaise longue.
Decided on a sofa. Black one, fake leather to be livened up with some colorful pillows. We also got hold of a mirror, a wall clock and various other things wich were need around the apartment.
Preparing for Dungeons & Dragons. For me that usually means one of the following activities:
And tonight I’m doing all three, while listening to Rolling Stones.
Met up with Andreas after work. We discussed game design and had fun emulating the look of old DOS dialogue interfaces using CSS. The result was not a pixel-perfect copy of the interface, but it definitely had the right feel — which is what we are aiming for.
Again time for Dungeons & Dragons. This time with Baern and Kava (played by John and Ingrid) continue their exploration of the Abyss.
The internet archive is an interesting place to spend your lunch break. Today I found an old website associated with Stockholm University called “Kunnskapsbanken”.
Kunnskapsbanken was a service where school students could pose a science related question and one of the researchers at SU would answer. The answers would then be stored in a searchable archive for future reference. The site seem to have died a slow death in the early 2000’s, despite a positive review by a university department (which also seems to have dissappeared) called Informationsenheten, suggesting further founding.
Today there are lots of websites to get answers for your mathematics and sicence questions online, especially if you are proficient in English. But this website highlighted the fact that there is a group of authorative experts, who speak your language, whose job is in part2 to help enlighten anyone interested in their area of expertise.
More monster-drawing today. Made a whole ensemble of a particular kind of monsters (not spoiling which, in case the players read my diary). Otherwise, the day was mostly cleaning and cooking. We are waiting eagerly for the arrving sofa (ETA: next Tuesday), which will hopefully make the livingroom a better place for the family to gather.
NRK reports, with positive remarks, that the roads in Norway will be lighted by means of LED in the future. While LED is certainly a great way to save electricity, one could wonder if we have sufficiently investigated the health effects this kind of light. The American Medical Association seems to think not.
Here is anothing thing one migth wonder about: Atiyah and Macdonald, in their 1969 “Introduction to Commutative Algebra”, take care to specify that application of functions is denoted in the book by “f(x)”, and not “(x)f”. Why do they choose to emphasise this? Was this a common dispute at the time? I would not think so: For instance, Bourbaki makes no remark about it. I recalled this oddity about A.—M. today when Marc Bezem mentioned that de Bruijn was an advocate of the notation (x)f. But apart from de Bruijn, I can find no early references to this way of denoting functions.
D&D night! Hyperion, Dalaran and Tirin are still on the material plane.
Just now listenig to «Faces – Three button hand-me-down», while figuring out some adjunctions between cubical and simplicial sets. Thanks to Eivind for recomending Faces to me back in 2008 — I’ve finally got around to listening some more to them ☺↩
Tredje uppgiften, “The third task”, is the obligation, by law, for universities in Sweden to spread knowledge about research to the rest of society.↩
Expecting a comment section? Feel free to e-mail me your comments, or otherwise contact me to discuss the content of this site. See my contact info. You can also write your opinion on your own website, and link back here! ☺