Friday, April 11, 2008

I came across this old paper by Milner, apparently one of the seminal ones about LCF:

ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/73/332/CS-TR-73-332.pdf

I was surprised by (1) how readable the early parts of the paper are and more importantly (2) how all this didn’t happen so long back. When it comes to denotational semantics, LCF and such I somehow had unfounded feeling that its all ancient and set in stone. Plotkin’s foundational work that revealed huge gaps in the denotational world view happened in my lifetime (well almost)… and the computer science community has studied it and has (mostly) moved on. That’s a really fast pace!

This was originally linked from LTU.

Friday, April 11, 2008 12:48:06 AM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Sunday, April 06, 2008

I was speaking with a friend the other day and we were talking about the interaction of effects and how to explain them.

One informal way to explain some additions to languages are that they are scale down localized structured versions of features that were largely available for the whole program. Let me explain: Did you start programming with an imperative language with global variables? (There is one called C that affected the minds of many people.) When you switch to an object oriented language, someone might have explained to you that there is no longer any need for real global variables. You may make these wannabe globals members of a class. You can turn methods that need the globals into members of that class as well. So they are global as far as the methods in question go, but they are not truly global.

In much the same way, we can explain yield. Programming languages have always had input and output operators - scanf-printf, gets-puts etc. However these operators are global with respect to your program. When you execute a printf, it is the output of the whole program, not of any one part of it. Yield on the other hand can be thought of as a localized input output operator. You can yield values from one part of the program to another part of the program. You get input from one part of the program. A method that yields is a packaged up opaque entity, a little sub-program, that communicates using yield with its consuming-context, the rest of the program.

We can explain exceptions in this way as well. In the absence of exceptions when there was a fault, the whole program would come down. It would core dump, modulo global error handlers. The whole machine does not come down, just the program that faults does. The environment that hosts the program may realize that there is a fault and do something about it. Its much the same with exceptions, but with the difference that only a part of the program "core dumps". Its a localized failure of the program that the environment (the rest of the program) can handle (or not handle, thereby making it a global failure).

So can you play this game or any other global program features, turning them into powerful localized structured operators?

Sunday, April 06, 2008 9:55:25 AM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Saturday, March 01, 2008

I have started liking groups so much, that I think its worth spending some time drawing out these beautiful things with some care. These mathematical abstractions have some really nice corresponding pictures.

 

image

This is the dihedral group D3, produced by
s^3 = i
(st)^2 = i

 

image   image

The quaternion group.

Quaternions are a generalization of complex numbers. I am a little fascinated with the above group because a long time back before I had known of Group theory I had constructed the above diagram in my attempt to understand quaternions and multi-dimensional geometry.

The discovery of quaternions is credited to the great mathematician Hamilton. Story has it that Hamilton had been pondering the issue for a quite a while and fundamental equation of quaternions came to him when he was taking a walk with his wife. It is said he carved the equation into bridge where he was at that time. The bridge, now has a plaque to this effect. So here is the fundamental equation:

ijk = -1

From this we can also derive i^2 = j^2 = k^2 = -1

 

image

The group produced by
s^3 = i
(-s)ts = t^2

where "-s" is to be read as "s inverse".

Here is a slightly different rendition of the same group:

image

 

Here is a different group:

image

This is the group generated by:
s^4 = i
(-s)ts = t^2
t^15 = i

 

image

This is the group generated by a variation of the above equations:
s^4 = i
(-s)ts = t^2
t^5 = i

Saturday, March 01, 2008 3:21:05 PM (Eastern Standard Time, UTC-05:00)  #    Comments [3]  | 
 Friday, February 08, 2008

Today I was trying to draw the Cayley diagram for symmetry groups of a regular tetrahedron. (A tetrahedron is a like a pyramid, but with a triangular base.) What I ended up with, surprised me. I had started with the idea that I would end up with something that was tetrahedron like - or atleast suggestive of the fact that it started from a tetrahedron.

 Cayley diagram for a symmetry group of the tetrahedron.

Cayley diagram for a symmetry group of the tetrahedron.

Now, this is not the only group one can generate from a tetrahedron. And even for this group, this certainly not the only Cayley diagram as well. We can visualize the above diagram as a 3d object If I were to redraw this slightly, we get -

image

And now if I imagine this as 3d object, I get something looks like this.

image image

front and back respectively.

It is as if each triangle has triangle facing in the opposite direction behind it. And there are 4 such perspectives, each corresponding to a vertex of the tetrahedron. Cute. I wonder if I can make choices for a different set of rotations such that the triangles are not inverted? 

After some playing around with it, I got this. I realized that following any sequence of red-blue-red-blue arrows always leads back to the starting point. If I were to compose every pair of red-blue arrows into a single arrow, lets color this green, then we get a different diagram. This diagram is indeed suggestive of the shape of the tetrahedron. The same shape would result if we were to include the blue arrows instead of the red ones.

Cayley diagram for a symmetry group of the tetrahedron

Cayley diagram for a symmetry group of the tetrahedron

This shape is interesting because you can imagine that looks almost like a large green tetrahedron with the each tip sliced of to reveal a small red triangle. Here is a picture I found on the web:

truncated_tetrahedron_un[1]

This diagram also lets itself to a nice explanation - each triangle at a vertex corresponds to the sub-group for rotation about that vertex.

Friday, February 08, 2008 9:15:15 PM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Wednesday, January 23, 2008

Here is a rather pleasant introduction to the philosophical point of view underlying Category Theory.

When is one thing equal to some other thing-

One of the templates of modern mathematics, category theory, offers its own formulation of equivalence as opposed to equality; the spirit of category theory allows us to be content to determine a mathematical object, as one says in the language of that theory, up to canonical isomorphism. The categorical viewpoint is, however, more than merely “content” with the inevitability that any particular mathematical object tends to come to us along with the contingent scaffolding of the specific way in which it is presented to us, but has this inevitability built in to its very vocabulary,and in an elegant way, makes profound use of this. It will allow itself the further flexibility of viewing any mathematical object “as” a representation of the theory in which the object is contained to the proto-theory of modern mathematics, namely,to set theory.

I have been spending some amount of time looking into Category theory and it is truly something elegant. A small selection of topics from Category theory have made their way into my reading list for my Oral Qualifiers. Hence, interested reinforced by need.

One of the strange things about category theory, and probably the most elegant thing about it as well is that category theory really has nothing much to do with objects in the way that Set theory does. Set theory and I think most things deal with objects, collections of objects and such. Category theory on the other hand is a theory about relationships, rather than the objects they relate. This shift, to me, is reminiscent of the Leibniz-Clarke viewpoints on the notion of space.

Wednesday, January 23, 2008 12:22:51 AM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Saturday, January 12, 2008

These are beginner level references for Category theory, ones that can be read by students of Computer Science. I haven't had a chance to look at all of this material myself. Ones that I have looked at have been marked with a star. Things that I think are better beginner material have more stars. At the time of this writing I am an absolute beginner in category theory and to most of abstract mathematics (with possible exception of Set theory), hence take my opinions here as just that - beginner level opinions. Finally, material that has been recommended to me by some of my professors has been marked with a +.

Categories
by T S Blyth (amazon) **

An Introduction to Categories in Computing
by Barry Jay (PS file)

Category Theory for Computing Science
by Michael Barr and Charles Wells (homepage of Charles Wells) (PS file of lecture notes) ++

Categories, Types and Structures: Category Theory for the working computer scientist
by Andrea Asperti and Giuseppe Longo (PS book) +

Category Theory for Beginners
by Steve Easterbrook (PDF slides)

Elements of Basic Category Theory
by Alfio Martini (citeseer)

Computational Category Theory
by D.E. Rydeheard and R.M. Burstall (PDF)

A Categorical Manifesto
by Joseph A. Goguen (citeseer)

Basic Category Theory for Computer Scientists
by Benjamin Pierce (amazon) *+

Saturday, January 12, 2008 12:13:27 AM (Eastern Standard Time, UTC-05:00)  #    Comments [2]  | 
 Saturday, January 05, 2008

I am very moved by "Uncle Petros and the Goldbach Conjecture" by Apostolos Doxiadis. It's a work of fiction that makes several references to real people and real mathematics. It seems the author has done a fair bit of research to write this book. The book is about a mathematician "Uncle Petros" who spends his entire life trying to prove the Goldbach Conjecture.

In the course of the book, Doxiadis touches on the lives of G H Hardy, S. Ramanujan, Cantor, Kurt Godel and much of the pain, isolation, failure and achievement that is involved in doing research. The book is a fascinating read and is in many ways very true to life though the main characters are fictious.

The Goldbach Conjecture simply states that every even number greater than 2 can be expressed as the sum of two primes. Wikipedia has some more detail. The conjecture has been known for about 250 years now. There is still no proof, though the fact has been verified for very large numbers. It is a conjecture and not a theorem because it has no proof. Work still continues on this. Dare to try solve it? You may also enjoy looking at the Goldbach weave.

In the early 90's a long standing famous problem, Fermat's Last Theorem was proved by Andrew Wiles. It took him 7 years of exclusive work to prove the theorem. The theorem has been know since 1637! And has escaped all these centuries without proof despite many many mathematicians working on it. One of the things that made Fermat's last theorem famous is that Fermat has scribbled in the margin of his notebook a comment to the effect that he knew a proof but that the margin is not wide enough to note it. (Wikipedia) Wiles's proof is 150 pages and uses mathematics discovered in the 20th century - this is most likely not the proof that Fermat had in mind, if indeed he had a correct proof.

The interesting things about proofs like these are not just that they confirm the truth of statements that we always suspected to be true, but that they advance the state of mathematics. In the course of chasing hard problems, often new theories and new approaches to proof theory are discovered.

Saturday, January 05, 2008 6:06:04 PM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Wednesday, November 28, 2007

An odd idea from a few days ago:

I watched this video a while back, this is Richard Feynman giving a lecture about discovering laws in physics -

He is talking about laws in physics. (the underlying Philosophy of Science that Feynman describes here is due to Karl Popper)

What Feynman is describing seems fundamentally different from what we do in the formal sciences like math/logic/cs. In the later we usually choose an axiom set that we believe to be right, based on our aesthetics, and then go on to prove other things that are right wrt our axioms.  Only things that are provable are taken to right and things that are right are irrefutably so. The system is inconsistent if we deduce False from the rules that we have. Inconsistent systems are not interesting. All formal methods work like this, in spirit - they keep track of what is right.

In what Feynman is describing, they don’t have a formal notion of right. They have a notion of what is wrong and as long as something cannot be constructively (by experiment) shown to be wrong, they can temporarily accept it to be not-wrong. If you look at this as a formal system, this is one where “what is not wrong yet” is known instead of what is right. Something is not wrong because 1) We don’t know a proof by which we can construct F from it or 2) Given our current inference rules there is no proof for it. But, we may add a new inference rule to the system in the future which may invalidate the belief that something is not wrong. It’s a feels like the opposite of what we do with logics.

Imagine a formal system or a model of computation based on notion like this. We are, in a fundamental sense, giving up the notion of consistency and completeness when we do this. I wonder if there exists a computational model that corresponds to such a “co-logic” of the sort they use in the *real* sciences. Such a system, in spirit, might be able to deal with partially correct data, incorrect assumptions etc. in a natural way. Absolutely correct data (or properties about the data) would be the exception.

(I wonder what this implies for the incompleteness theorem and such. I have been told that the "co-logic" I refer to here is actually co-induction. I see some similarities there, but I am not sure if its exactly that. )

A Tutorial on (Co)Algebras and (Co)Induction - Jacobs, Rutten

A Tutorial on Co-induction and Functional Programming

Wednesday, November 28, 2007 12:03:05 AM (Eastern Standard Time, UTC-05:00)  #    Comments [1]  | 
 Sunday, November 18, 2007

Being at Indiana University, which is an old time Scheme hub, every now and then I am exposed to some of the turmoil in Scheme community over the new Scheme standard, R6RS. Essentially the community is having a hard time agreeing on what should be in the new standard. There are some very smart, very accomplished, very opinionated people who belong to this community and the language spec is a bit of a battle ground, from what I hear. (As are all language specs... some battles, I suspect, lack the intellectual quality of this one)

I am not very much of a Schemer myself, I sometimes indulge the language on a need basis. I hear from some my more intensely-Scheme-happy friends about some of the latest news at Scheme-spec land. One of the names that was mentioned in recent times is that of Will Clinger. Apparently, Will Clinger set into motion some of the discussion that formed the origins of the new standard, called R6RS (that is short for Revision-6 of the Report on Scheme - or something approximately like that). Over the years the formalization of R6RS has had its ups and downs. Of the many differences of opinion on the standard, some resulted in the formation of a group that decided to create an alternate standard. This group is called SchemePunks, apparently headed by Will Clinger himself (*). While this is mostly hearsay, it seemed amusing none the less. I also, sort of, like Scheme - so I listen in when one of these conversations come up.

Today I was searching for something and I came across the SchemePunks webpage/wiki. I didn't realize they had a webpage. Better yet no one told me that it written in excellent Hitchiker style! I read this and burst out laughing - what a way to motivate a language standard! I don't know any of the design decisions they have made, but the introduction here is sheer genius. Despite not being a Schemer, I am almost tempted to join in. :)

From the SchemePunks webpage:

On 29 August 2007, the Revised Revised Revised Revised Revised Revised Report on Scheme was ratified by the Steering Committee. This has made a lot of people quite angry and has been widely regarded as a bad move.

Many programmers believe that it was created by some sort of community process, though the Jatravartid people of Viltvodle VI believe that the entire Standard was in fact sneezed out of the nose of a being called the Great Green Arkleseizure. This theory is not widely accepted outside Viltvodle VI, and so, standards being the puzzling documents that they are, other standards are being designed. And this wiki, which is called SchemePunks, is definitely not part of the Scheme Underground, even if it is, which it isn't.

Which is very odd, because without that fairly simple piece of knowledge, nothing that is written on here could possibly make the slightest bit of sense. We hope to develop an alternative specification for the Family of Programming Languages known as Scheme. Watch this space.

Being somewhat bowled over, I had to look for the man - William Clinger, Professor of Computer Science, Northeastern U.
http://www.ccs.neu.edu/home/will/Personal/western1.jpg

:)

I wish more languages where designed in H2G2 spirit. Aah!

From his webpage:
http://www.ccs.neu.edu/home/will/R6RS/essay.txt

More than twenty years have passed since I wrote this [1]:

Programming languages should be designed not by piling feature on top of feature, but by removing the weaknesses and restrictions that make additional features appear necessary. Scheme demonstrates that a very small number of rules for forming expressions, with no restrictions on how they are composed, suffice to form a practical and efficient programming language that is flexible enough to support most of the major programming paradigms in use today.

I have to say, I am compelled to agree, though I wonder how of it applies to the Scheme of today. The essay is worth a read, even if you are not a Schemer. You can skip over the Scheme specific parts and just look at the language design philosophy.

Sunday, November 18, 2007 11:11:35 PM (Eastern Standard Time, UTC-05:00)  #    Comments [0]  | 
 Saturday, November 03, 2007

I get irritated because too many people in the "computing" business don't understand the word "lambda". Its just irritating because at the heart of it, its just a simple fundamental idea, like the notion of natural numbers or counting. So just spend a few minutes, understand what it means and stay educated. In a few years (if not already), almost every language is going to expose something like a lambda to its programmers. So just pick up the idea ok?

This is a working description, it wont make you an expert on the Lambda Calculus. It might give you some intuitions about it though. Lets get started.

So assuming you are familiar with a C-like language, how do you write a function that takes an integer and returns it?

int foo(int x) {
    return x;
}

Now lets look at what this is saying, it says there is a function called foo, it takes an int which it names x and it returns an int. the body of the function has a single statement called return x. Great! Now, this function is a very famous one and is called the identity function (usually goes by the nick-name id). Also when we talk about functional programming we dont really care very much for the C-style types. So let's rename the function and drop the types.

id(x) {
      return x;
}

Don't worry too much about the types. Typed functional languages usually have a different notion of types from the C like languages. The types will come back, but in a bigger and better form. We however wont discuss any type theory in this article.

So now, what it is saying? It says here is a function called id, it takes some value that it calls x and it returns x. Ok, now lets take a look at this closely. In the syntax that we have here, the name of the function is part of the syntax. We would like to say - here is a function and then assign it the name id. So that we are able to look at the function and its name as two different things. Lets do that by introducing the keyword called "function". Javascript, for example, has such a keyword.

id = function(x) {
      return x;
}

Ok. Now lets make one more simplification. Lets say that the language is a little like Ruby or so where that last statement in a functions body is its return value. Did you get that? That means that we no longer need the keyword return. We can simply make the last statement x and by that we know that the return value from the function will be x.

id = function(x) {
      x;
}

Great, lets rewrite this a bit:

id = function(x) { x; }

Now for one more simplification (really C like languages are so complex!) - lets assume that we can write only one statement inside each function. Just one. If that's the case it can be much like a if with just one statement - we don't need the curly braces anymore. We also don't really need the semicolon.

id = function(x) x

Great! Congratulations ladies an gentlemen, you are looking at a lambda. Simply rename the keyword function and call it lambda and we are all set.

id = lambda(x) x

If we drop the name assignment and look at it we have:

lambda(x) x

This is a function that has no name. It take one argument and return it. Various functional languages use slightly different syntax for writing out their lambdas. The lambda calculus, the underlying calculus of these systems, usually uses a \ instead of the verbose name lambda. It also uses a dot to separate the arguments from the body of the function. A little like this:

\x.x

The functional language Haskell uses an arrow to separate the body from the arguments.

\x->x

The language(s) ML, OCaml, SML, (maybe F#) etc. use the name fun to stand for lambda.

fun x -> x

The language Scheme uses the name lambda and lots of parenthesis.

(lambda (x) x)

Ruby lets you write something very similar to a lambda like this:

lambda {|x| x}

Most of these languages give you some mechanism by which you can give a name to your lambdas (otherwise most of the time you are a little hard pressed to refer to them).

Haskell

id = \x -> x

ML

let id = fun x -> x

Scheme

(define id (lambda (x) x))

There are some alternate syntaxes for writing named lambdas in most languages:

Haskell

id x = x

ML

let id x = x

Scheme

(define (id x) x)

So what is a lambda? It is usually a name used to define a function. The function is a value that can be assigned to a variable name. Just like any other value in your language.

A lambda is an abstraction form. Normally in a program you can read the value of a variable to which you have not assigned a value. In other words is you write (x + 1), it does not have any meaning if x has not been assigned a value already. One way to look at what lambda says is that it abstracts the value of the x. So \x.(x+1) means - give me a value for x and then I will give you the value for x+1. The value of x is abstracted in the body of the lambda. This description comes very close to our informal notion of a function in a C like language.

The lambda calculus usually allows only for lambdas that take one argument. Hence to write functions that take multiple arguments we nest lambdas. We write \x.(\y.(x+y)) for a function that adds two numbers. Most functional languages support multi-argument lambdas. In Haskell this would be \x y -> (x+y).

So what's the big deal? Nothing much and quiet a lot. Nothing much because the notion of functional abstraction is something we learn from high-school math which we port over to programming languages. This is an old and familiar notion.

That said, in the functional programming community, it has long been realized (it is a large community with varying beliefs, secret cults, traditions and practices) that lambdas are the only abstraction form required for a lot of things.  One can do away with loops and conditionals (if, switch) and assignments and numbers and object oriented programming and pretty much everything you can think of (and some things you cant) - they can all be encoded using lambdas. Hence lambdas form a sort of foundational building block for a large number of programming paradigms. At the heart of all of this is the notion of a function - hence the name functional programming.

Saturday, November 03, 2007 6:03:52 PM (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]  | 
 Wednesday, October 03, 2007

One of the things I have a hard time truly internalising is the difference between existentials and universals (written sometimes as exists and forall). They have a very strange relationship and its hard to maintain the intuitions about what each of them mean, other than in the most obvious of interpretations. I remember Prof Mike Dunn, who is a renovned logician and was the Dean of the School of Informatics, in his classes on Galois logics would say that he keeps mixing them up because they are duals of each other.

One area where these crop up and innevitably confuses me is in type theory, especially when looking at the types of continuations. Its at times like this Prof Sabry would saying something mystical sounding, in true sufi style, which will leave me with a little flashlight to use in the darkness.

So some intuitions. What is a universal? Consider the function "head" that takes a list and returns the first element of the list. The function does not concern itself with the types of the quantities in the list, it only cares about the list itself.

So "head" has the type: forall x. List x -> x

(Functions like this may show up when programming with generics (or templates) in some languages. You are free to make these connections, I wont make them here.)

What is the type of head saying? It says that it doesnt care about the underlying type of elements in the list. It only cares about the fact that these elements are in a list. So when head is invoked with a list of integers, "List Int", it returns an integer, "Int". When called with "List String", it returns "String". When called with "List (List Int)" it returns "List String". You get the idea. The "idea" should have two parts (1) "head" is concerned about the fact that it gets an abstract List. (2) There is nothing, no code, inside "head" that depends in anyway on the type of the contents of the list. If head is called with a "List Int" it cannot return an integer that it had hidden off in a variable. It can produce an "Int" only by looking into the List. Why? Beacuse head did not know that its argument would be a list of "Int".

In other words the "forall" says that "head" is truly independant of the type "x". It can manipulate the List, but it can't manipulate the "x". Its is "pure" with respect to "x". The "x" in the List is abstracted away from it. Having a function that is forall quantified is different from having several functions, one for each datatype that you have in your system, because of two reasons (1) There can be an infinite number of data types, which means you will have to have an infinite number of such functions (2) Each such function is for a specific type, "List Int -> Int", and hence knows that it need not ever look into the List but can return any Int to you to satisfy its type; in other words each such function is not "pure" wrt the type of the elements of the list.

Wednesday, October 03, 2007 5:37:27 PM (Eastern Standard Time, UTC-05:00)  #    Comments [1]  |