On Using org-ref

This is another brief post, but I wanted to talk about a tool that I’ve been appreciating a lot lately: org-ref.

The long and short of it is that this is a library that works with org-mode to help you manage citations and your bibliography. You can read the installation instructions at the org-ref github page linked above, but the basic idea is that you can insert references into your org-mode text like

cite:2009arXiv0903.0340B

and you’ll get out the actual citation properly connected to your bibliography when you export the file. You can insert citations with a key binding, mine is C-c ], and it will give you a nice little menu based on the bibtex file you have that will let you choose which reference to include. There’s also a number of helper functions that allow you to build up your bibtex file and download pdfs just from the doi or the arXiv id.

This is all cute and something I appreciate, but in some ways what I really like is that if you open the link (with C-c C-o or by clicking on it) then you also open up the associated pdf, if it exists, and open notes on that paper. Maybe it’s silly, but I was really happy about the notes because for the link above I get, in my designated notes file, something that looks like

** TODO 2009 - {Physics, Topology, Logic and Computation: A Rosetta Stone}
 :PROPERTIES:
  :Custom_ID: 2009arXiv0903.0340B
  :AUTHOR: {Baez}, J.~C. and {Stay}, M.
  :JOURNAL: ArXiv e-prints
  :YEAR: 2009
  :VOLUME: 
  :PAGES: 
  :DOI: 
  :URL: 
 :END:
[[cite:2009arXiv0903.0340B]] [[file:~/Dropbox/Papers//2009arXiv0903.0340B.pdf][pdf]]

which really simplifies my whole system of trying to link up papers, notes, pdfs and all of that because I used to link all of those things together manually with each paper and it was a headache. I feel like this is going to make it easier for me to write blog posts too, since I can export citations to HTML as well.

So, yeah, it’s not like you couldn’t have done all of this with elbow grease and plain bibtex, but as someone who needs a lot of organization to keep my thoughts in order this is a bit of a godsend.

The Recompiler

Today I wanted to make a brief post plugging The Recompiler, which is a new quarterly hacker magazine being launched this summer.

The way Audrey advertised the magazine to me was essentially that it was intended to be an accessible, educational, technical publication with a feminist core and I immediately asked for the opportunity to write for it.

So you might see me writing an intro to theoretical computer science piece in the near future, but regardless of that submissions are open until the end of the month, so if you think you have a topic to contribute you should absolutely submit.

Subscriptions are going to be open starting a week from today, April 21st.

Still Alive

It’s been quite awhile since I was updating regularly. A large part of that was the typical “I’ve removed the immediate emergency stressors so now my body is going to crash” thing that I think a lot of people are pretty familiar with. I was seriously ill for over a month straight starting in mid-january and since then I’ve just been chronically exhausted.

I am still alive and kicking though! This is just the massive crash that I’ve been delaying for two or three years now. I’ve started to be able to think more clearly again, the panic attacks are coming less often, and even in the middle of panic it’s getting easier to push it aside and get work done.

I’ve been doing a lot of reading, largely in trying to get caught up with the entire transcendental syntax/ludics/geometry of interaction program that I didn’t know much about until recently. They’re not the incomprehensible papers I’ve seen some (jokingly?) claim they are, but they’re dense and build on themselves. I’ve been bouncing around between Locus Solum and some of Girard’s more recent papers.

Is there some research goal that I have in mind for this reading binge of the last few weeks? Not particularly. Indeed, I’ve been trying to remind myself that I’m allowed to read things that are not within my speciality or have a clear goal to them. Sometimes it’s nice just to learn things for the sake of learning them, and the fact that it’s a topic that I find interesting and that’s making me think harder about my assumptions on logic-as-a-field is just a bonus.

Other than reading and walking so much that I’ve destroyed yet another pair of boots, I’ve still been picking away at the intro to computer science book that I’ve mentioned previously. It’s going to be in Python because that’s what my university has more-or-less standardized on, but when I asked on twitter about people’s suggestions for first programming languages I was surprised that the most common answer I got was Racket! I hadn’t really considered it as a teaching language before, despite the existence of How To Design Programs. The rest of the answers were interesting as well. More than one person suggested teaching some form of assembly language, which I’d also never considered but I can see the reasoning behind it: giving a low-level picture of how computers see computation is definitely useful. On the other hand, I seriously worry that assembly first might obscure the fundamentally algebraic character of computation. That’s my bias showing, of course, since I’m always going to lean towards understanding computation mathematically rather than as things are implemented.

So that’s basically where I am at the moment. Coming out of a long stretch of just being sick and exhausted, and getting back into the swing of things. I’m going to try and turn my beeminder goal for the blog back up again and see if we can get an honest-to-goodness posting schedule again, so we’ll see what happens!

On Scheduling or Lack Thereof

So the past couple of weeks, since my term ended, I’ve been trying to heavily schedule my days so that I don’t end up idleing or wasting my time during this leave. Yes, this was partly a medical leave which means I should be resting, but I’m not sure how easy that will ever be for me.

What I’m realizing, though, is that trying to schedule out my days in advance just really doesn’t work. I started doing it because, as I’ve written about before, I have a hard time keeping continuity in my ideas over time and making sure I don’t drop threads. I try to schedule out, a week or so in advance, all the tasks on all the various pieces of ideas that I want to keep alive. The biggest problem I’ve been having is that I can’t really predict, on any given day, what I’m going to be capable of accomplishing. This means that on most days I wake up, check my org agenda and then have to postpone most of the 12 hours of work I end up scheduling myself each day. That’s rather disheartening at first blush, but then I started thinking harder about the problem after reading Sacha Chua’s post on having a relaxed routine.

I think the real issue is not of laziness that I’ve been making a few major mistakes on trying to schedule things:

  • I’ve been pretending that there’s a way to know in advance what mental disability will allow each day
  • I’ve been overscheduling by a factor of two or three
  • I’ve had my tasks be huge things rather than small steps, e.g. “read this 120 page article on game semantics for PCF” as a single task

So I’m thinking that I need to follow something a bit more akin to the Zen To Done style of picking three important things to work on each day (or two…or one on the really bad days) and just do them. I already have all of my ideas and proposed tasks in my .org notes and a custom org-agenda view that brings up any headline starting with the keyword NEXT. That means it should be pretty easy to bring up an agenda view each morning that will let me pick a couple of things to work on each day.

When I’ve accomplished those few things, then I can take stock of how much I have left in me for the rest of the day and, if I’m all tapped out, then rest knowing that I’m still making progress. That’s one of the problems I’ve been having a lot of trouble with. At the end of the day I’m just thinking about all the things I’d hoped to do yesterday and it’s hard to just stop and take a deep breath.

Goals for the New Year

It’s probably a bit cliche to write blog posts about the new year on New Year’s Day, but it’s a ritual that I kinda like.

So I’ve already talked about the intro to programming book I want to write this year, and there’s all the drafts of papers that I was picking away at last term, so I want to get all of those things done this year but that’s not really all.

I want to do a lot more reading than I have been, both technical and non-technical. I’ve read so little fiction in the past year because I’ve barely had the energy to focus on anything when I haven’t been teaching. It’s a shame because I live in a city with one of the best library systems in the nation. I also want to read a lot more philosophy than I have. I think I’m missing a lot of the background from the more philosophic side of logic and the ways that trying to understand human reasoning inspires work in logic. I’ll be honest that I’m not entirely sure where I should begin, so if anyone has any recommendations I’ll be more than happy to take them!

I also want to sharpen my programming skills a bit since, well, I’m a good programmer and fluent in multiple languages I’m not really a master at any language in the sense of knowing the ins-and-outs of every advanced feature, trick, or technique. To that end, I really want to improve my mastery of

  • Agda
  • Idris
  • All the modern ghc-implemented Haskell extensions, since I’m mostly comfortable with Haskell 98 + multi-parameter type classes
  • C
  • Maybe OCaml and ML so I can understand the implementations of Coq and Isabelle respectively
  • Emacs lisp

Note I’m saying that I want to improve my skills in all these things, but I’m trying to be vaguely realistic about the fact that all of that plus my writing goals, a number of other research related goals, and ~1000 pages of papers to read (half of which is a couple of dissertations I want to work through) on top of this is being a medical leave means that I probably can’t accomplish everything I want in this year.

That’s a horrifying concept, really. In this time I’ve taken off to rest and heal, the idea of actually letting myself rest makes me feel sick.

So how do I figure out the real balance? I don’t know. Maybe that’s going to be a big part of what I learn this year.

Teaching Intro to Programming

So I’m on leave now, officially, but that doesn’t mean I won’t be working. I’m probably going to start teaching the intro to programming courses at my institution and, me being me, I’ve already started planning for how to do that. Why? Because even before I decided to go on leave I’d started writing my own book for the subject. I worry that seems arrogant, but I’ve looked at a number of intro to programming books and I don’t really like most of them? Basically, I want to emphasize the fundamental algebraic nature of programming and teach not just a particular language but also explain how to learn programming languages in general by way of understanding both syntax and semantics. I’m probably going to take an approach of explaining small step operational semantics without ever actually saying that’s what I’m doing. I want to emphasize that with any program you can in principle evaluate it all by hand. Now, that’s not exactly feasible for anything non-trivial but it’s a perspective that can help when learning to program. When I was first learning to code, I felt like most introductory resources made programming feel like a form of incantation. You appease the Divine Computation by using particular patterns of supplication to get the kinds of results you want and, if your prayers don’t work, you really don’t have the skills to figure out why.

I really want to try and explain, in a principled way, how every syntactic construct can be evaluated by hand and thus how to predict accurately what any piece of code is doing. I’m planning to do all of this in Python since, despite my PL-nerd ways, I want to pick a language that has a lot of local traction and, thus, community and job opportunities. Since Python isn’t referentially transparent it’s a little harder to explain how to think in terms of an operational semantics, but I have this whole approach that I used over this past summer of having the students draw out a table of values based on

  • all the variables in scope
  • the line number

and filling it out as you attempt to evaluate the program. We can introduce iterative constructs through loop unrolling forms, give functions by substitution, etc. I know that Python doesn’t have a formal semantics, but we can at least give something close enough for intuition.

Of course, that’s not all I want to try and explain in a three quarter intro sequence. I really want to explain how to read code, how to write code by figuring out the invariants that should hold and how to classify the types of variables even in an untyped language, and how to test and debug code. One of the skills that I think is important to learn is how to read a library’s, often sparse, documentation, look at the code, and thus learn how it works.

It’s going to take a couple of months to pull together a rough draft of this, but I’m planning on making it extremely example and exercise driven and I’m hoping to get a chance to refine it by having students use it once I’m back from leave.

Incremental Progress and Organizing

Another short post today, just to start getting myself into the habit of writing again. My leave is all official and taken care of now, I’ve turned in my grades for the term, and now I’m not going to have obligations to my university for awhile.

Of course, I’ve been working on research related things everyday. I’m organizing my notes, I’m going to send my advisor another draft of this massive tome in the next couple of weeks, and I’ve got a stack of papers a mile high that I’m working through.

My biggest problem seems to be making sure that I don’t push myself too hard. I have to keep reminding myself that the reason why I’m going on leave is that my mental illness has been bad enough that I need time to rest and heal and just let myself be crazy in that way that is a short term hardship, but a long term good. It’s like resetting a bone. It hurts more and feels worse at first but eventually means the healing can be done.

I’ve started using effort estimates in org-mode to plan my day. It was a little shocking when I tried to schedule out this week and discovered that I was planning out 10-12 hour work days every day. That’s probably not a great plan if I’m supposed to rest, so I’m trying to instead plan for maybe 6-7 hour days at least in the first few weeks of my break.

I tend to get this panic where I need to do All The Things as fast as possible because I get convinced that I’m running out of time on some fundamental level. I’m in my early 30s now and I had expected that I’d be able to be done with a PhD years ago. I didn’t expect that I’d have to get started on this as late as I did and that mental disability would make everything take so much effort. It may sound silly, but in undergrad I always heard variants “no mathematician is worth their salt over 25” or that if you hadn’t done important work by 30 then you never would etc. and those ideas really wormed into my head. I don’t really believe any of that, at least not when it comes to anyone else, but I look at myself being 32 and 5 years into a PhD and I think “wow, I must be a total loser”.

The problem, though, is that pushing myself to work as fast as possible doesn’t actually get anything quickly. It just burns me out faster. On the other hand, in this past year I’ve started making incremental progress on a number of things and it’s actually starting to build up. I have a number of research projects that are starting to get mature enough to share with others, I’m working towards a draft of my thesis proposal, I’ve written up significant notes and learning materials for the theory course I teach, I’ve even managed to write more for this blog than I’ve ever written for any other attempt at a technical blog over the years. I’ve written almost 150k words since March of this year, not all of it towards my doctorate, but it’s still an order of magnitude more than what I’ve managed to produce any other year.

I’m trying to convince myself that incremental progress is going to add up if I can keep my notes going and keep continuity of my ideas and to that end I know I need to not burn myself out.

Allowing Myself To Rest

It’s been some time since I’ve posted here. The past couple of months have been very difficult and, well, after talking some with the disability resource center at my university and doing a lot of thinking in the past two weeks I’ve decided to take a leave of absence from my department for awhile.

I’m taking pretty much all of 2015 off, which is intimidating because it feels like I’m admitting defeat somehow, but in the end I think this is going to be a good idea. I’m not planning to leave my research alone during this time off, quite the opposite actually. I’m probably going to be more productive with my writing once I get a chance to let myself really rest for a bit.

I’ve needed this break ever since the sexual assault two years ago, but I didn’t even know it was an option. I didn’t think it’d be possible for me to pull off financially or professionally but, after having some bad scares with ideation in the past month, I decided to ask today and my department chair was completely understanding and has already approved my leave.

I’m still a bit in shock that it was that easy and I’m aware of the level of luck and privilege that is allowing me to take time off from working in this way, where I’ll have a guaranteed job once I’m back. It’s no small thing to have this opportunity, given the general lack of support for people with disabilities in the U.S.

So, I guess we’ll see what happens during this next year. I’ll probably be a lot more active on this blog again! No matter what, though, I think this break was overdue for a very long time.

Domain Theory and Semantics: III

Well, it’s been awhile since our last post on domain theory, but where we left off last time we’d talked a little bit more rigorously about what it means to be a CPO, the existence of fixed points in pointed domains, and about algebraic CPOs. Now we want to get to actually describing the D_{\infty} construction that provides an explicit model of the untyped lambda calculus. It’s going to require a little bit of category theory, but it’s not going to be that bad, I promise.

First, though, I want to go back to compact elements and all that. So I was reading chapter 5 of Gunter’s semantics book, the chapter on notions of finite approximation and finite element, when it finally hit me what’s useful about the definition about compactness for elements and why it encompasses a notion of finiteness. As a reminder, an element x is compact when for any chain Y such that x \sqsubseteq \bigsqcup_i Y_i then there is some element y in the chain such that x \sqsubseteq y. Now, if we consider a chain where every element is less than x whose least-upper-bound is x then this condition means that we’ll have some element of the chain, y, that is simultaneously y \sqsubseteq x and x \sqsubseteq y which means that it’s actually equal to x. In simple words, it means that if you have a chain of approximations of a compact element then there can only be finitely many steps to the approximation before you reach the compact element. This is the sense in which compact elements are finite, in that they are reachable through finite steps of “computation” for some very abstract notion of computation as process.

Alright with that epiphany out of the way, we’ll start actually describing the D_{\infty} construction. We’ll follow the approach in Tennent’s semantics book, because I think it does a really good, clear job of outling the pieces of the approach and showing how constructing models for the untyped lambda calculus is a special example of general solution of domain equations.

Here’s the basic outline of the argument. First, that we want to let our domain equations, such as D = D \to D, to be defined as the least-fix points of some kind of functor so that the equality in our domain equations is “really” just isomorphism. We also want to define a special kind of category of CPOs for two reasons. The first is that we want to have the arrows in the this category represent a notion of embedding, where an arrow D \to E exists iff D is somehow a subdomain of E, so that we can have a notion of infinite sequences of embeddable domains and show that such sequences have colimits. Now why is this important? Because such an infinite sequence represents all the finite approximations of some domain such as, I don’t know, a domain we’re trying to define as the least fixed point of a functor. Once we know such colimits exist, then we just need to show that our domain-building functor preserves colimits so that it’s action on the colimit is, again, a colimit of the sequence of finite approximations. What do we know about two colimits for the same diagram, girls and boys? That’s right! They’re isomorphic!

Wait, you might ask, how is this the least fixed point. That’s because this is a colimit in the category of CPOs and embeddings. To be more specific, assume that our sequence of domains is D_i, our colimit of the sequence is D_{\infty} and that E is another domain that all of the D_i can be embedded into consistently, i.e. it’s a cone over the diagram given by the sequence D_i. The property of being a colimit means that there is an embedding h : D_{\infty} \to E such that all the embeddings into E from D_i must factor through h. In words, this means that D_{\infty} is the smallest domain that contains all the finite approximations in the sequence D_i.

So that’s the basic idea. We’re going to

  • define our notion of embedding
  • show that sequences of embedded domains have a colimit
  • show that the (diagonalization of the) exponential functor ( \to ) is colimit preserving

then, we will have shown how to create a model of the untyped lambda calculus as well as a number of other calculi.

Let’s start on step one. The notion of embedding we’ll use is that of “embedding-projection pairs”, often abbreviated as ep-pairs, and in some literature such as Amadio and Curien they’re called “injection-projection pairs”. An ep-pair between domains D and E, symbolically represented as D \triangleleft E, is a pair of continuous functions f : D \to E and g : E \to D such that

  • g \cdot f = id_{D}
  • f \cdot g \sqsubseteq id_{E}

or, in words, that f is a 1-1 continuous injection of D into E and g is a continuous surjection that takes elements of E to their best approximants in D.

We’ll skip the details showing that for any category of domains that we want to use, such as CPO, that the corresponding category of domains that have embeddings as arrows truly is a category. It’s pretty simple to show, though, that identity arrows exist and that you can define an appropriately associative composition.

Instead, let’s go to showing that any sequence of domains D_i and embeddings (f_i : D_i \to D_{i+1}, f_i^P : D_{i+1} \to D_i) has a colimit. The definition of the colimit is fairly simple: it’s the set of partially-defined sequences s : \mathbb{N} \to \bigcup_i D_i such that

  1. there is some j such that s_j exists
  2. for any s_j that exists, then s_j : D_j
  3. if either s_j or f_i^P (s_{j+1}) exists then both exist and s_j = f_j^P(s_{j+1})

and D_{\infty} is given a domain structure pointwise, so both comparisons and LUBs are defined by their action at each “slot” in the sequence. Since these are sequences of CPOs, we know that the pointwise LUBs must exist.

In order to show that this is a colimit, we first need to give arrows \eta_i : D_i \triangleleft D_{\infty} that commute with the f_i : D_i \triangleleft D_{i+1}. In more categorical language, we need to define the cone over the graph. Since such an embedding takes an element of D_i to a sequence of elements in D_{\infty}, we’ll basically use the pairs (f_j,f_j^P) in order to generate a sequence from a given element, projecting it forward with repeated applications of the f-s if i \le j and projecting it backwards with applications of f^P-s if i > j. Slightly more formally, we have that the sequence \eta_i(d) has elements given by \eta_i(d)(j) = (f_{j-1} \cdot f_{j-2} \cdot \ldots f_i)(d) if i \le j and if instead i > j then we project “down” with \eta_i(d)(j) = (f_{j}^P \cdot \ldots f_{i-1}^P)(d). The projection is even simpler, as \eta_i^P(s) = s_i, or in other words the projection from a sequence down to the i-th individual domain is just given by taking the i-th element of the sequence. The nice thing is that the commutivity requirement we want follows immediately from the definition of the embedding and projection.

So now we’ve defined the cone, but we have to show it has the colimit property that says any other cone must be able to be factored through D_{\infty}. Basically, the idea is that if we have another cone with base point a domain E and embeddings \psi_i : D_i \triangleleft E then we’ll define our factoring map h : D_{\infty} \triangleleft E such that for all i then \psi_i = h \cdot \eta_i. First, we note a couple of things: first that if we take \psi_i \cdot \eta_i^P then this composition creates a monotone sequence where psi_i \cdot \eta_i^P \sqsubseteq psi_{i+1} \sqsubseteq \eta_{i+1}^P. The reason for this is that composition is monotone and by the nature of embeddings we have that both \psi_i \sqsubseteq \psi_{i+1} and \eta_i^P \sqsubseteq \eta_{i+1}^P, from this we can conclude that in the continuous function space we then have that the LUB \bigsqcup_i \psi_i \cdot \eta_i^P is well-defined. This will play the injection part of our embedding h and then h^P will be the “dual” defined as $\bigsqcup_i eta_i ⋅ psi_i^P. Noting, without proof, that \bigsqcup_i \eta_i \cdot \eta_i^P = id_{D_{infty}} then we can rather easily prove that h^P \cdot h = id_{D_{infty}} and that h \cdot h^P \sqsubseteq id_{D_{infty}}, so this is a properly defined embedding. We still need to show that this embedding gives us the factoring that we want and that any other such embedding must be equal to h.

Since this post has already gotten to be much longer than I intended, I think maybe I’ll leave things here for now and just write a part 4 sometime soon. I mostly just want to post something right now given that it’s been I think over a month since my last post and that’s far too long.

Looking To Teaching This Term

It’s the start of a new term this week and with it a lot of challenges in trying to balance teaching and research. The problem I often have is that there’s an unlimited amount of time one can put into teaching. Your lectures can always use more tweaking, you can always spend more time doing sketching out even more example or rehearsing your delivery. Last year, I really got sucked into the work of teaching and barely had time to do any research.

Since last year, I’ve figured out a lot about how I work, how to deal with my mental disability, and now I also have a lot more experience in teaching this undergraduate course and I’ve got most of my materials set up in advance! Seriously, I’ve got quite a bit here at my github repo for the class. I’ve got my syllabus, I’ve got my homeworks, I’ve got my rough lecture notes, I’ve got the first four weeks of in-class worksheets. I’m feeling pretty prepared at this point, though I still need to finish preparing my homework solutions for the course but that won’t be super hard.

My researchy goals for this coming term are mostly to finish clearing out my backlog of ideas. The idea hasn’t gotten any less anxiety inducing, but it needs to be done. I’ve done a decent amount of work over the past couple of years and it should probably be seen by someone other than me before it’s judged to be unredeemable trash. If I can get all my ducks in a row on this, well, like four papers I’m sitting on at the moment then my career is going to be looking a lot prettier in the near future and maybe, just maybe, I can start believing that I can actually finish this.