Thursday, November 01, 2007

Today Dr Sabry mentioned the Oral Qualifiers to me - maybe I should start putting together a reading list and selecting a committee. I thought I should put down a first list based on what comes to mind first without caring too much about what people really want to deal with. So this list will have to undergo many alterations - I thought it would be nice to preserve it. I don't know how large or small PhD Orals reading lists are - maybe I should ask around. Maybe this one is too small.

Oral Qualifiers
===============

Computational/Process Calculi
-----------------------------
Functions as Processes, Pi calculus - Milner
Join Calculus, Reflexive CHAM - Gonthier, Fournet
STM - Tim Harris, Simon PJ, Herlihy

Foundations: Logic and Mathematics
----------------------------------
Basic Category Theory - Pierce
Basic Mathematical Logic - ?
Natural Deduction and Sequent Calculus - Dag Prawitz
B*, K* logics, Linear/Affine type systems - Dunn, Walker
Lattices, Gaggle theory - Dunn, Bimbo

Types & Semantics
-----------------
Lambda Cube (Fw, Dep. types) - Barendegt, Aspinwall, Hofman
Typed Operational Reasoning, Equational Correspondence - Sabry, Harper, Felleisen
Something about Pure Type Systems - ?
Basic Model Theory, Scott Models, Denotational Semantics - ?
Calculus of Constructions - Coquand
Lambda~ mu mu~ Calculus, CBV CBN duality - Curien, Herberlin, Wadler
Type theory behind Control operators - Makarov, Sabry, Danvy, Filinski, Kiselyov, Felleisen
Theory of Objects - Cardelli, Abadi

As I look at this list I wonder, what can I possibly do in the *real* world after I get out of here? Maybe I should be writing a web server or some such thing. That way when I am out of here maybe someone will say "He knows all this Category theory nonsense. Really! I looked it up on Wikipedia, it really is called the generalized-abstract-nonsense. But he's also written a web server, maybe we should interview him?"

 

If you are wondering what PhD Oral Quals are like, maybe these serve as a good explanation -

More...

Thursday, November 01, 2007 12:06:29 AM (Eastern Standard Time, UTC-05:00)  #    Comments [3]  | 
 Wednesday, October 31, 2007

Aziz has released his shiny new Ikarus Scheme compiler. This is the first compiler specifically targeted at  R6RS Scheme. R6RS is the latest Scheme standard - as a matter of fact it is so new that the standard itself is still under development. Ikarus implements almost all of the interesting parts of the standard. It is supports a superset of R5RS, the current standing Scheme spec.

Ikarus is also a fast optimizing compiler that generates x86 opcode as of today and it runs on Windows, Mac and Linux systems. Ikarus has its own unicode engine, garbage collector, loader, linker, cross platform binary format, stack management, etc etc. Pretty much all of the things you would expect to find in a JVM or a .Net. All the of the compiler is written by Aziz, and a lot of it is based on the work of his advisor, Kent Dybvig, on the Chez Scheme  system.

http://www.cs.indiana.edu/~aghuloum/ikarus/index.html:

Ikarus is a free optimizing incremental native-code compiler for R6RS Scheme.

Ikarus is free to download, to distribute, to modify, and to redistribute. The complete source is available according to the GNU General Public License (GPL3).

Ikarus is an optimizing compiler, so your Scheme code will run fast without the need to port hot spots to C "for performance". With an incremental compiler, you don't need a separate compilation step to make your program run fast. The best part is that the compiler itself is fast, capable of compiling thousands of lines of code per second.

Finally, Ikarus is an R6RS compiler. R6RS is the latest revision of the Scheme standard. The preliminary release of Ikarus supports over 80% of the most important features R6RS, and later releases will bring Ikarus closer to full R6RS conformance. R6RS libraries, scripts, record types, condition system, exception handling, unicode strings, bytevectors, hashtable, and enumerations are among the supported features.

Ikarus is probably also useful as a target language for compiling experimental functional languages as opposed to targeting C or going through the pain of compiling to ASM, .Net or JVM yourself.

Yay! I think I will be moving away from Petite Chez Scheme and start using Ikarus as my primary Scheme system (despite the fact that its under the non-free unethical GNU license which does actual material harm to the society). If functional languages and Scheme are your cup of tea, try out Ikarus!

Wednesday, October 31, 2007 8:21:50 PM (Eastern Standard Time, UTC-05:00)  #    Comments [4]  | 
 Tuesday, October 30, 2007

I have been thinking about what it means to understand something. In computer science we tend to claim that we understand something, often in a way that is truly confusing. That is because often in CS one can can get by with little knowledge of something, without developing a truly deep understanding of the nature of what we are dealing with. This is probably true of real life as well and hence this blog entry.

I think it was several years into programming with C++, and other similar languages, when it struck me that I truly don't understand object orientation and OO programming. Knowing the syntax of the class construct or writing some programs that use classes does not mean that the program is written in an OO style. What my understanding lacked here was a good enough insight to use the philosophy of OO design to write my programs as communicating objects.

Sometimes, however, the level of non-understanding is much shallower than this. Very often we use a name or a pronoun as an explanation. I was reading Richard Feynman the other day, in one of this articles he talks about his childhood and his father:

He had taught me to notice things and one day when I was playing with what we call an express wagon, which is a little wagon which has a railing around it for children to play with that they can pull around. It had a ball in it -- I remember this -- it had a ball in it, and I pulled the wagon and I noticed something about the way the ball moved, so I went to my father and I said, "Say, Pop, I noticed something: When I pull the wagon the ball rolls to the back of the wagon, and when I'm pulling it along and I suddenly stop, the ball rolls to the front of the wagon," and I says, "why is that?" And he said, "That nobody knows," he said. "The general principle is that things that are moving try to keep on moving and things that are standing still tend to stand still unless you push on them hard." And he says, "This tendency is called inertia but nobody knows why it's true." Now that's a deep understanding -- he doesn't give me a name, he knew the difference between knowing the name of something and knowing something, which I learnt very early. ... So that's the way I was educated by my father, with those kinds of examples and discussions, no pressure, just lovely interesting discussions.

I myself had developed wariness of pronoun-explanations early on, and hence my mis-explanation-beasts wear a more convincing sheep-skin. I have been reading about type systems this weekend. A couple of brilliant talks given by Kyle Ross and Michael Adams got me seriously thinking about the magnitude of my ignorance. I had a working knowledge of type systems, I knew enough tricks to impress people at juggling tricks and mimicry with respect to types, but I never truly understood them. Today I was commenting to someone that my understanding of existential quantification is just a bunch of random properties about what it stands for.  I know how to look at existentials as abstract data type encodings or as modules or such - but all those explanations seem like different ways to looking at it without actually taking the bull-by-the-horns.

My understanding of existentials reminds me of an old story about blind men seeing and elephant. Back in India, I think everyone has heard this tale at some point or the other. In the US most people don't seem to get the reference to the blind men seeing the elephant. This is an interesting and fairly good allegory for explaining  a limited or half-baked understanding.

http://www.kheper.net/topics/blind_men_and_elephant/Buddhist.html

http://en.wikipedia.org/wiki/Blind_Men_and_an_Elephant :

In various versions of the tale, a group of blind men (or men in the dark) touch an elephant to learn what it is like. Each one touches a different part, but only one part, such as the side or the tusk. They then compare notes on what they felt, and learn they are in complete disagreement. The story is used to indicate that reality may be viewed differently depending upon one's perspective, showing how absolute truths may be relative; the deceptive world of half-truths.

Coming back to computer science, the other day I was talking to my advisor, Prof Amr Sabry. We were talking about macro systems and staged evaluation and such. I believe we were talking about the KFFD algorithm or so when the topic came up. We had some algorithm that sort of works but was cluttered with a lot of details. Sometimes I tend to be a little lax about how I look at things and say, "If I can implement it, I understand it". This seemed to be a good measure of the understanding - if I can build it myself from scratch, I "understand" it.

At this point he said "Let me show you the difference between understanding something and knowing it well enough to be able to implement it. Consider the following encoding:

encoding

Now suppose I tell you that my phone number is 855-3127, can you convert it into the encoding? Well, sure you can. Can you implement it? Yes you can. You can write a little table and look up the values and such. But do you understand it?"

"You understand stand it when you are able to see this."

This put me back on my toes with respect to what I think I understand. A bit of much needed sharpening of the old intellectual-honesty-knife.

Tuesday, October 30, 2007 1:50:07 AM (Eastern Standard Time, UTC-05:00)  #    Comments [1]  | 
 Sunday, October 28, 2007

This is a great slide deck from Benjamin Pierce, Professor Computer Science at UPenn, that shows what the world of programming languages research is doing especially in the context of types.

http://www.cis.upenn.edu/~bcpierce/papers/tng-lics2003-slides.pdf

Also from Pierce is a really good introduction (the best I have found to date) about polymorphic lambda calculi and actually programming in some of those languages. This describes the hierarchy starting with the simply typed lambda calculus (F1) and describes F2, F3, etc and Fw (F-omega). He also talks about encodings of various sorts of types and a whole lot of neat stuff. All of that written in a very readable fashion. I spent my weekend on this and it was time well spent.

http://www.cis.upenn.edu/~bcpierce/papers/leap.pdf

(For some reason this pdf seems to be back to front, but its just fine when printed)

Pierce's webpage is a gold mine of information for the PL student, including neat things like a 'Great Works in Programming Languages' list. He is also a pretty good photographer. I did see him in person when I was at MSRC in summer of 2006. I believe he was visiting those days. I now regret not having walked up to him and saying hi.

Sunday, October 28, 2007 10:25:11 PM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Friday, October 26, 2007

I cannot help it if my paintings do not sell.
But the time will come when people realize that they are worth more than the cost of the paint.
     -- Vincent Van Gogh

 

Vincent
Don McLean,
1971

Starry Starry Night
Vincent Van Gogh
Saint-Rémy, France: June, 1889

 

Moonrise
Ansel Adams
Hernandez, NewMexico, 1941

Friday, October 26, 2007 9:06:48 PM (Eastern Standard Time, UTC-05:00)  #    Comments [1]  | 
 Wednesday, October 24, 2007
  Life... 

Lots of stuff happening in the past few days. No, real work though.

I saw Nagesh Kukunoor's Dor. Nice film. I believe Kukunoor is making the mistake of being creative in Bollywood, that might be an expensive mistake. So much so that people will have to keep talking about his work years later, while he pretty much nothing out of it while it matters. How wonderful. So Dor is a creative hindi movie, as far as conventional hindi movies go.

I found the storytelling weak and/or cliched in parts - had it not been for this, it would have been a fairly top class movie, maybe among my all time favorite hindi movies - this also means that it would have surely done worse at the box office. With these flaws added in it stops being a truly great film and instead becomes a nice film - certainly worth watching. The main characters all play their parts really well - especially Gul Panag and Ayesha Takia.

 

This weekend I got to listen to IU's philharmonic orchestra play Beethoven's 5th. Wow! The piece has a completely different power and energy when you hear it live. I was blown away. I was also much impressed by the attention to detail and the sheer wonderful complexity of something like a philharmonic orchestra. Lovely.

This isn't IU, but everything else matches.

 

On the music scene, this weekend, I also got listen to Bob Dylan. Live. No kidding. Dylan was playing at IU (for some reason). I had not known about this and it was hardly advertised. One of my students in my Operating Systems class mentioned it to me in passing. He is Iranian and we were talking about Firdaus and Khayyam when he mentions Dylan. The concert itself was a bit of a let down. We didn't get great seats, though they were rather good. IU's audio systems were a let down and so most of the time I couldn't catch the lyrics. This is also partly due to Dylan - if you think he sounded rough and raspy back in the day, you should listen to him now. Despite all this it was, in some sense, soul satisfying to see the man in person and listen to him sing, I doubted if I would ever really get a chance to, considering that he maynot be singing for a whole lot longer.

Here are some lovely videos from Dylan's early days, when he still used to "sing". These days most of his songs, even his present renditions of his classics have degenerated into a sort of chant, sometimes short coughed up statements with background music. But well, the magic of Dylan will always be just that, magic.

Tambourine Man, 1964:

Blowing in the Wind, 1963:

The Times they are a Changin, 1965:

More on the music front IU's opera series had Carlisle Floyd's Susannah this weekend. This was a far more moving presentation that IU's attempt at Rigolleto, from last month. As before the stage setup and costumes were excellent. For Susannah, they had several layers of translucent curtains covering the stage. When each scene starts the actors stand perfectly still giving the illusion that one is looking at a life size painting. The lights slowly brighten and the screen lift bringing the scene to life gradually and then the actors start to move. It was brilliant. The singing and performance, for the most part, was also very good. I would certainly recommend watching it - its playing again next weekend.

 

Moving on from  the music scene, last week there was talk by the famous logician and philosopher Saul Kripke. IU is getting a new president, Michael McRobbie, and Kripke's talk was one of the many functions related to the Presidential Inauguration events. President McRobbie, I am told, is also a logician of some renown and hence, Saul Kripke was speaking at IU.

I personally don't know much about Kripke's work except for the "Kripke Semantics" for intuitionistic logic. This (I like to believe) I understand, pretty much everything else starts to go downhill, especial all the modal stuff. My brief encounters with some of the related areas leads me to conclude that most of my own thinking is oriented more towards constructive mathematics than to classical mathematics. This was the official description of the talk.

Saul Kripke, distinguished professor of philosophy at the Graduate Center of the City University of New York, will deliver Indiana University’s inaugural Presidential Lecture in Alumni Hall of the Indiana Memorial Union. He intends to speak on “The Collapse of the Hilbert Program,” a philosophically significant topic with a technical result. Kripke received the Schock Prize for Logic and Philosophy in 2001 and is considered by some to be the world’s greatest living philosopher and logician.

Needless to say I didn't get much out of it. I think I understood what was said broadly, but didnt get any of the details. It was however rather nice to see Kripke himself. His talk started out with some details that I felt I understood and somewhere 5 mins in into it, it took a nose down dive and I had no idea of what he was saying. I remember trying to recollect details about the arithmetic heirarchy and Pi^0_2 systems and such. I felt this was pretty much the state for most of the audience. Disturbingly though, my advisor was with me and he seemed to be understand a lot of the details..

I remember this one point towards the end of the talk - in the front row sat one of the senior professors of the department, an emeritus, and very well known logician. Kripke was saying something was completely baffling to my intelligence and it seemed like the elderly professor was nodding. At this point, Kripke asks the professor, calling him by his first name (they knew each other), "Hey *, Are you nodding because you are understanding?" and he replies "oh, No". It was hard to suppress laughter. Enough said.

 

Today there was a talk at IU by Professor Neta Bahcall, the Eugene Higgins Professor of Astrophysics at Princeton University. Fascinating stuff, I haven't been to a good physics talk in ages. She was talking about "The Dark Side of the Universe". The discussion today was largely about "Dark Matter" and "Dark Energy" in the universe, the reasoning behind their existence and such. Makes me wish that I had never switch to CS and had stayed with physics somehow.

This is a two-part lecture. The session on Thu will talk about the  history of the universe in some approximate detail. Prof Bahcall's presence at IU is part of what we call the Patten lecture series. they get eminent speakers to come and talk about a variety of topics. Last year one the speakers was Amartya Sen who talked about the notion of identity.

 

Today I finally received my copy of "The Lightning Should Have Fallen on Ghalib", my second book on Ghalib's works. The first was Chirag-e-Dair which I picked up at Mumbai airport the last time I was flying out of India. Needless to say Ghalib is fascinating. He had me laughing and chuckling at his chutzpah in minutes.  This is a rather good quality English translation and contains verse in Devanagiri (Hindi) and Urdu script.

In paradise, as we know, God showed Adam the door.
When I have been shown your door, I feel a shame deeper than his.
                     -- Ghalib (as translated by Sunil Dutta)

 

Fall has come to Bloomington and rows of trees shine golden, orange and fiery red. Such beauty before the waste of winter. I have been enjoying taking pictures.

bloomington-fall-2007-1


There is more, I am too tired to write.

I haven't been getting much *real* work done, though I have been thinking about things. The other day, my advisor mentioned to me the importance of "doing the boring work", the context of writing this paper that I have been delaying for a while now. For over a year or so, I have been walking around with one or two publishable pieces of work and been not doing very much about it. He is very patient man, far more that I would have been in his place. I fear that I should do some "boring" work one of these days, or be disowned or something like this. :)

(Dear Microsoft Live Team, why does "Windows Live Writer" get slower with each new release? I will have to refuse to upgrade if this is a mandatory new feature each time. Please take out the Thread.Sleep()s.)

Wednesday, October 24, 2007 12:35:06 AM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Friday, October 19, 2007

"Can you recommend any C++ books?"
"I don't recommend C++."

Afterwards I reluctantly come up with some names. I beginning to notice that I eventually end up mentioning the Scott Meyers "Effective C++" books. The last time I did this I started to wonder why I say this?

When I first read "Effective C++" I was horrified. If I derived any pleasure out of it, it was comparable to the morbid curiosity of going to witness an execution (I probably would not do that though, if I ever got such a chance. I don't have the stomach for it). Back to C++ - Firstly there was no way I was going remember all of that. Secondly I felt deeply uncomfortable. In time I realized that the whole book was written in the style of demonstrating "effective" usages of C++, while what it truly was is a careful documentation of the flaws of the language. Every chapter in that book talks of a language flaw in excruciating detail and how to live with it. That book should have been called "Defective C++".

Then there was "More Effective C++" which essentially did more of the same.  Here is what the language does, here is what you think it would do, here is what you'd like it to do and you put these together and it blows up in your face. In time, my intellectual immune system kicked in and started erasing most of my memories about all this.

So why do I recommend the "Defective" and "More Defective" books? My first recommendation would be to get out of the situation, don't deal with the language if that's possible. If not, and you intend to get it to serve you (instead of the converse) you need to quickly understand that most of the abstractions it provides are leaky. There are hardly any non-leaky abstractions that C++-land provides. (Some people associate this behavior with some notion of "freedom" - I trust evolution will take of those folk.)

So if your abstractions are leaky, in that they are going to have strange interactions with each other under-the-hood, then you should quickly start developing an understanding of what happens under the abstractions you are given. Your effectiveness as a developer becomes proportional to your understanding of what happens under the surface. Hence the "defective" C++ books are a useful read.

Friday, October 19, 2007 12:05:29 PM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Tuesday, October 16, 2007

Today Aziz mailed me a build of his Ikarus compiler for Windows. Though I don't have much to do with software as such these days, I was excited. Ikarus is Aziz's Scheme Compiler. I use Petite Chez Scheme on my machine. Petite  is Kent Dybvig's Scheme interpreter, part of the Chez Scheme compiler system. I don't have Chez Scheme itself because it sells, I am told, for several thousands of dollars and hence I cant afford it. I expect Ikarus to be comparable to full Chez in many ways and surpass most other Scheme systems out there.

What Aziz sent me was a zip file that extracted to a 128k exe and 4mb "boot" file. He says the boot file says the same between windows, linux and mac. The bootstrap executable changes. This is amusing because the "boot" file is actually the compiler binary. It contains the compiled x86 code.  He able to get away with this because he only relies on the OS to load his little bootstrap exe. After that point he simply allocates memory pages from the OS and relies on the OS for almost nothing that he can do himself. So the exe loads the boot file into memory which then acts as its own loader, sets up its own stack, lays out its own code and data areas, does its own GC and such.

Of course, all of this is written in Scheme itself. There is probably a small C file somewhere that acts as the main() and the initial call into some ASM code that transfers control to Scheme. Fun fun.

I have talked to Aziz about many parts of this system and almost always the design has seemed to be of very high quality. His management of code objects, the runtime stack, continuations and on and on. The system has a large part of R6RS implemented and is already a superset of R5RS as far as I understand. Depending on how the development process stabilizes (after all, this is all one persons implementation), I might move over Ikarus altogether and maybe use it exclusively. 

Tuesday, October 16, 2007 10:49:16 PM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  |