Rubrication

I just spent a couple of very cold weeks in Anchorage Alaska. I went out with a bunch of friends to a bar on the night prior to leaving, where I met up with an old friend (and listened to two other friends play music). I started describing the lambda calculus to him since it is related to my work and he was curious what I was up to. In any case I found myself unable to produce addition of the church numerals off the top of my head, which I found pretty disturbing since it shows that I probably didn’t quite understand it in the first place. Therefor I sat down this morning to see if I couldn’t reconstruct it from first principles.

It turns out that it is relatively easy. First, let us start with a bit of notation, and a description of the lambda calculus. Since wikipedia describes the lambda calculus in detail, I’ll just show how one procedes with calculations. As examples let us start with the church numerals.

1 = (λf x.f x)
2 = (λf x.f f x)
3 = (λf x.f f f x)
…
n = (λf x.fⁿ x)

where fⁿ means “f f … f” n times.

The idea is that each numeral is represented by a lambda term. The lambda term describes the arguments (f and x in this case) and the “body” in which we substitute the arguments when the are passed in. An example of an “application” of a lambda term to an argument would be:

1 g = (λf x . f x) g => (λx . g x)

We pass in g, and replace every occurance of f in the body with g, and delete f from the list of variables. we can continue to apply this term to another term

(λx . g x) y => g y

Which leads us to conclude that

1 g y => g y

Ok, so now that you’ve seen a few calculations, let us try to construct addition. The first thing I tried to do is to construct the function +1. Clearly, we want +1 n => (n+1). n+1 is (λf x. f⁽ⁿ⁺¹⁾ x) which is also (λf x. f fⁿ x). Since n = (λf x. fⁿ x) we need to somehow add another f. The trick is to get the arguments to use the same symbols, and to remove the lambda abstraction. We can do this by applying the church numeral to the symbols we want to use, in this case f and x.

(λf x. fⁿ x) f x => fⁿ x

So now we know how to get rid of the lambda abstraction. Now we can add an f on the front, which will get us closer to n+1.

f (λf x. fⁿ x) f x => f fⁿ x

We are almost there. Now we need to have the λf x part at the beggining so that we look like a church numeral.

(λf x. f (λf x. fⁿ x) f x) => (λf x. f fⁿ x) = (λf x. f⁽ⁿ⁺¹⁾ x)

Looking great so far! Now we just need to be able to take the whole (λf x. fⁿ x) form as an argument. This turns out to be really easy, we just put a variable in it’s place and add it to the front of the list of lambda arguments.

(λa f x. f a f x) (λf x . fⁿ x) => (λf x. f (λf x. fⁿ x) f x) => (λf x. f fⁿ x)

This shows that (λa f x. f a f x) is the +1 function!

+1 = (λa f x. f a f x)

Ok, so now that we have +1 can we get a function that takes an n and returns +n? This would get us a long way towards addition. We can call this function n->+n.

Ok, so we can guess what +n will look like easily. It’s going to look just like +1 except with n leading f’s.

+n = (λa f x. fⁿ a f x)

So we should try to figure out how to take the fⁿ out of a church numeral, and place it there. Well, we should apply the same trick of applying the church numeral to f and x so that we can extract the body.

(λf x . fⁿ x) f x => fⁿ x

ok, but really we want a to follow, based on +n, so instead of using x, let us apply the form to a.

(λf x . fⁿ x) f a => fⁿ a

Great! Look how close we are. now we just need to abstract the a,f,x and place f x following it.
(λa f x. (λf x . fⁿ x) f a f x) => (λa f x. fⁿ a f x)

Ok, so now that we know how to take an n, and able to take the entire church numeral n as an a beta reduce it to n+1, let us abstract the n as an argument

(λb a f x. b f a f x)

Let us verify quickly that this function works.

(λb a f x. b f a f x) n =>
(λa f x. n f a f x) =>
(λa f x. (λf x. fⁿ x) f a f x) =>
(λa f x. fⁿ a f x)

Now, we can verify that this works on m, to obtain n+m as the +n function should:

(λa f x. fⁿ a f x) m =>
(λf x. fⁿ (λf x. f^m x) f x) =>
(λf x. fⁿ f^m x) = (λf x. f^(n+m) x) = n+m

Hooray! Not only did we find n->+n, but we have obtained the function “addition” for free. Since, once we have the +n function we can apply it to m. So we now have the function:

add = (λb a f x. b f a f x)

I haven’t tried multiplication and exponentiation yet, but you are welcome to try!

Probably one of the best papers I’ve read on the relationship between CBN, CBV and the Curry-Howard correspondance is the paper Call-by-value is dual to call-by-name by Wadler. The calculus he develops for describing the relationship shows an obvious schematic duality that is very visually appealing.

After reading the paper that I mentioned earlier on Socially Responsive, Environmentally Friendly Logic (which shall henceforth be called SREF Logic), it struck me that it would be interesting to see what a CPS (Continuation-passing Style) like construction looks like in SREF logic, so I went back to the Wadler paper to see if I could figure out how to mimic the technique for multi-player logic. It looks like the formulation by Wadler comes out directly by thinking about logic as a two player game! I’m excited to see what happens with n-player logic.

This has been a big diversion from what I’m actually suppose to be working on but I didn’t want to forget about it :).

Once again the internet comes to the rescue with a Systematic Search for Lambda Expressions. This is the answer to yesterdays question of whether we can iterate over isomorphic proofs exhaustively in order to extract all programs of a specification which in this case is realised as a “type”. Hooray for computer science!

I have a bunch of ideas that I don’t have time to follow up on but I’d like to retain in some fashion so here goes.

1.

A long time ago I had a question about the shortest assembly program (parameterised by the instruction set of course!) that could encode the generators of the quaternions under multiplication. It is a very easy thing to program this, but as I was doing it, I found myself being highly doubtful that I was choosing the “right” encoding. In fact I almost certainly wasn’t. Would there not be some very tight encoding in terms of “normal” assembly language operators? This has been a persistent question in my mind that comes up frequently in different and often more general forms. If you want to make a fast compiler, how do you know what instructions to output? If you have a highlevel specification, how can you avoid the ridiculously high overhead usually associated with extremely high level languages?

Today I found this fabulous paper (from 1987!) that deals with some of the basic issues involved in finding the shortest program for a given problem. It’s called “Superoptimizer — A look at the smallest program”. I’d link to it, but I got it off ACM so if you are one of the few people that has a subscription you’ll know where to find it and otherwise I don’t want to give the money grubbers the link-love.

Some other thoughts that are in this region of my thought-space. Can you take a given specification with a proof and systematically transform it to enumerate the space of satisfying programs? If not, why not? Even if you can’t, might it not be interesting to just perform large searches of this space? Are there methods of using the transformation operators such that programs are only decreasing or minimally increasing? If so then perhaps we can call the search good at some size threshold since very large programs are unlikely to be good because of locality issues. Also Automatic Design of Algorithms Through Evolution is in a very similar vein.

2.

Concurrency is a nasty problem. It doesn’t have a nice formalism that everyone in the CS world can agree on. There must be like 500 different formalisms. All of them better (easier, not neccessarily faster) than the ones that we actually use (locking, threads, condition variables) but none of them stand out as “the right thing”.

I recently found a paper called:
Socially Responsive and Environmentally Friendly Logic. I love the title But aside from that, the formalism is very nice. It is something that I’ve contemplated a bit but never had the drive to actually try to work out formally. The basic idea comes from the knowledge that Classical Logic and Intuisionistic Logic can be viewed as 2 player games. This game is pretty simple. If I have a proof phi then to win I have to prove it. If I have a proof ¬φ, then to win my oponent has to fail to prove it. If I have φ ∧ ψ then my partern gets to pick a formula and I have to prove it. If I have ∀x then my oponent gets to pick any stand-in for x that he would like. You can probably guess the rest (or look it up). This alternate logic breaks the essential two person nature of the logic. One interesting practical feature of negation in the traditional logics, is that they give rise to Continuations in the Curry-Howard Correspondance. So what does this give rise to in the N-player games defined by Abramsky? I’m not sure, but I suspect it might give process migration! Something worth looking in to.

So after a bit of research it turns out that the big reason that we don’t have a meta-compiler compiler generator project because sophisticated partial evaluators are pretty much never self applicable. As far as I can tell from the literature the Futamura projections in the context of logic programming have only ever been applied in practice on “off-line” partial evaluators. Off-line partial evaluators tend to be much less sophisticated since they do most of their reasoning “off-line”, that is, without attempting to unfold.

Apparently part of the reason for this is the use of extra-logical features in the sophisticated partial evaluators, in order to make them fast enough that they can reasonably be applied. It is hard to make performant prolog without using cut. Once cut is used however, all bets are off, since it is nearly impossible to reason about effectively.

I started writing my meta-compiler without using cut, but restricting myself to soft-cut, because of the purely declarative reading that can be given to soft-cut. If I’m careful perhaps this will allow me to make my meta-compiler self-applicable. Since I don’t really understand all of the details of why on-line partial evaluators are not generally self applicable, we’ll have to see.

Legend has it that a million years ago Plotkin was talking to his professor Popplestone, who said that unification (finding the most general unifier or the MGU) might have an interesting dual, and that Plotkin should find it. It turns out that the dual *is* interesting and it is known as the Least General Generalisation (LGG). Plotkin apparently described both the LGG for terms, and for clauses. I say apparently because I can’t find his paper on-line. The LGG for clauses is more complicated so we’ll get back to it after we look at the LGG of terms.

We can see how the MGU is related to the LGG by looking at a couple of examples and the above image. We use the prolog convention that function symbols start with lower case, and variables start with uppercase. The image above is organised as a DAG (Directed Acyclic Graph). DAGs are a very important structure in mathematics since DAGs are lattices. Essentially what we have done is drawn an (incomplete) Hasse diagram for the lattice defined.

Each of the arrows in our diagram represents a possible substitution. For instance ‘p(X)’ can have X substituted for either ’s’ or ‘g(r,Y)’. Anything that can be reached from a series of downward traversals is “unifiable” and the substitution of the unification is the aggregate composition of substitutions we encountered on the path. So for instance ‘p(X)’ will unify with ‘p(g(r,s))’ under the substitution X=g(r,Y) and Y=s. Any two terms which are not connected by a path are not unifiable.

The least general generalisation is also apparent in our picture. Any two terms will have a common parent in the Hasse diagram. The least, (in the sense of distance from the top) parent of any two terms in our diagram is the LGG. So actually the connection between the two is fairly straightforward (using 20/20 hindsight).

Code transformation or meta-compilation as it is sometimes called (which is the general notion of techniques including Partial Evaluation, Supercompilation, Deforestation, or my advisors Distillation), is a powerful technique in computer programming. The benefits (and drawbacks) are almost certainly not sufficiently studied.

I was just conversing with my room-mate Tom about meta-compilation and I made the supposition that Meta-compilers are somewhat like the technology of the lathe. There are a huge number of technologies that require a lathe in order to be produced effeciently. A lathe can be viewed as a major nexis in the dependency graph of machining technology. A lathe is an almost a completely fixed precondition for the mill. The Mill is the crux of modern machining. It allows you to construct almost any currently available machined part. Without the mill we really wouldn’t have the industrial age at all. Do such things exist in computer programming?

Metacompiler technology is incredibly powerful. It is a technique that usually is concidered to be a superset of a partial-evaluator. It is a compiler technique that starts in the source language and ends in the source language rather than some target language as does a standard compiler. While this might at first sound trivial or irrelevant a few examples can convince one that it actually a very useful tool. (2*2) can be coded in most languages, but really it is just the literal 4. Partial-evaluation will reduce this computation at compile-time elminating the cost from the final executable. The power doesn’t stop there though. One particularly convincing example that I found was the partial evaluation of fairly simple grammar recogniser (parser) which reduced a problem directly from an NDFA to a DFA. Which is basically the compilation process used for regexps.

The Futamura projections give us some idea of just how powerful the technique is. If we have a metacompiler, we can metacompile an intepreter with respect to a program writen in the source language of the interpreter to arive at an executable in the language of the metacompiler. In fact, if we metacompile the metacompiler with respect to the interpreter and we can generate a compiler!

So I have a *lot* of questions about metacompilation. It sounds almost too good to be true (but there are good reasons to believe that it isn’t). Some of them are very technical which I will probably save for tomorrow’s post. The following question though is more philosophical, and practical (can those two happen at the same time?)

Why aren’t supercompilers/partial evaluators used as general compilation systems? If you can write a supercompiler in some high level, nice language like OCaml and then all you have to do is write an interpreter for your language of choice in order to produce a compiler, then why isn’t this done?

This seems like the holy grail of leveraging, or code re-use. You could write one really good compiler for a good language for specifying languages (Which ML was originally designed for, and of which OCaml is a decendant). One really good metacompiler. At this point every other language (front end, in the terminology of GCC) is simply the act of writing an interpreter. Writing an interpreter is *radically* simpler than making a sophisticated compiler. It is basically equivelent to a specification for the language. The process of language design can hardly be facilitated more than this since interpreters are pretty much the minimal requirement for specifing the operational semantics of a language!

My question is why isn’t this general procedure really carried out in practice? Are metacompilers not good enough in practice to produce high quality performant programs? Has it just not been tried? If not, I’d like to see some effort expended on this, since it seems like a crutial technology that could really be leveraged far more than any of the “shared VM” projects like C# with minimal cost to language implementors.

It has often been said that Irish is a language with little use, and no place in the new Ireland and should no longer be a cumpulsory subject taught in schools. This notion needs to be unclothed as a complicated psychological condition and not a well reasoned argument.

School is cumpulsory. Numerous subjects in school are cumpulsory. English is cumpulsory. Maths are cumpulsory. While it is clearly desirable to have students who are enthusiastically engaged with subjects such that they study them even in their spare time, it is unreasonble to assume that that state should support a public school curriculum in which no subjects are cumpulsory and a basic level of knowledge is unecessary in any subject. I’m sure that most reasonable people will agree that some cumpulsory subjects are necessary and
desirable for the education of the public.

This naturally leads as to ask which cumpulsory subjects these should
be? Bilingualism has enormous cognitive benefits as has been demonstrated by numerous studies. It is hard to overstate the pedagogic value of bilingualism. The positive effects bleed into other subjects including performance in mathematics, critical thinking and of course learning subsequent languages.

The indirect socialogical benefits are also numerous. Nothing can unmask subjectivity and perspective like the study of another language. Additional languages provide access to conversations that could never have been had otherwise. If the language has a literary tradition (as does Irish) they also give access to a body of literature that might otherwise be inaccessable.

While the strong Sapir-Whorf hypothesis is not widely believed, it would be hard to suggest that some form of the weak Sapir-Whorf hypothesis is untrue even for universalists (I’ll have to make this a whole other post sometime).

Bilingualism should be considered a minimal basic requirement of education. What should this baseline be? I contend that Irish is the natural choice.

Irish is already fairly well known by most people in Ireland. While competency in speaking the language is low, people I have met tend to know quite a lot more than a ‘copla focal’. It would require very little effort for many Irish to gain speaking competency.

It is often claimed, half in jest, that either Polish or Mandarin should be the cumpulsory language since more people in Ireland use them daily then use the Irish language. For true bilingualism to occur it is neccessary that at least one of the additional languages taught, be taught universally. It is imperative to expect that one can use the langauge, at least at a basic level, and be understood. It is unreasonable to think that the language that will have these qualities is either Mandarin or Polish. It can’t be possible to make either of
them the single baseline cumpulsory language in school.

While the teaching (and speaking) of these two languages should be encouraged they can not be a replacement for Irish. Irish itself is the language with the greatest likelyhood of generating the socialogical consesus necessary to be a universally spoken language on the Island.

Irish, with its poetic character and its extensive and historically important literature should be seen as one of the pillars of pedagogy in public education in Ireland.

I, as an immigrant, have little comprehension of the complex emotional relationship that natives of the island have with the Irish language, besides the obvious understanding that it is indeed very complex. I have witnessed more than once, the same person in the same conversation both arguing for, and against, the importance of saving the Irish language. With such internal conflict amoung many Irish people, it is no wonder that there is a public conflict concerning the language.

There are a couple of vectors that I think that may have contributed to this complicated situation. One of which the cumpulsory teaching of the Irish language. The fact that after 12 years of study of the language in school, only a tiny percentage of people are able to speak the language with any fluency has to have had a negative effect. I’ve often heard people say that the language is impossible to learn. This is far from true, but it may indeed seem that way due to the tremendously poor methods employed in the teaching of the language.

I have heard from many sources that Irish is taught as a dead language; without a focus on conversation, and forcing memorization without teaching rules of grammar. This is a confluence of the absolute *WORST* ways to teach a language. Is it any wonder that people who take 4 years of French in the Irish school system feel far more comfortable in French? There is a large body of study on the proper methodology for teaching languages to obtain fluency. These methods need to be employed and the old techniques should be removed IMMEDIATELY before they can inflict psychological damage on yet another generation.

The Irish government is currently cash rich, and of all possible uses of money, nothing has a greater benefit for society and the long term economic health of a country than proper education. It has a nearly incalculable benefit. With this in mind my program for obtaining true bilingualism on the island would be the following.

Money should be made available to all teachers and child minders to spend signifcant periods in the Gaeltacht in the interest in assuring a high standard of fluency for those that are responsible for the education of our children.

Money should be made available to entirely subsize child care given through the Irish language. This would remove the hurdle for those who are usually at the greatest economic disadvantage in obtaining the Irish language. The money spent on child care would serve the dual perpose of education and social welfare while not increasing costs to the state significantly for either goal.

Money should be made available for adult education in the language. It is more expensive to obtain Irish language instruction in the Republic than it is in Northern Ireland. RTE should give their Irish language materials away for free (charging only for the cost of media). The BBC has better free language learning materials for Irish than does any entity in the Republic. I find this a highly embarassing situation, and I hope that others do as well.

The teaching of Irish in school should be modernised with a two pronged approach focusing both on conversational Irish, and on grammar and the study of literature.

I think that if these policies were to be put in place we could see wide spread fluency in the langnuage and most importantly a bilingual island within a generation.

I don’t intend that the Irish people be forced to give up their characteristic melange of national pride and self deprecation. I would never suggest such a thing. However, this should not keep us from implementing the most effective education system that we can.

I’ve been hacking away at my program to test a theory I have about machine translation. I wrote a bit about it in a previous post but I was fairly vague. I thought I’d describe in more detail exactly how the technique would work (I’m still in phase 1).

The idea is simple. The first phase is to take a corpus in a language. Take each sentence of the source (or some other sized chunk, currently I’m limited by computational tractability to a single sentence) and recombine each element of the sentence into every possible string of n-grams. If you play with it a bit you’ll realise that there are 2^(N-1) of these for a string of size N. One way to think about it is that there are N-1 indexes into the spaces between words in the string. You can then think of each sentence as being a collection of indexes at which we combine words. This is obviously the power set of the set of indexes {1,2,3…N-1} and hence there are 2^(N-1). It turns out however that it is nice to have a special word meaning “beggining of sentence” and another for “end of sentence”, so we end up starting with N+2 words, and getting 2^(N+1). That can be a big number!

So now that we have our n-grams for each sentence we want to look at transition probabilities between n-grams. The reason for this is that various parts of a sentence have unpredictable size. In the absense of a full NL parsing system there is no way to figure out what a syntactic unit (a noun phrase for instance) will be. This process completely obviates the need for an NL parser. This in itself is a huge win since NL parsing is at least difficult and probably impossible to do correctly because of idioms and variations in dialect. With the n-grams in hand we can now look at transition frequencies amoung the various n-grams in each of the different patterns in which they were combined. At this point we enter the information into a database which stores the transition probability between every two n-grams. Let us assume that we ignore sentences larger than 12 words. This means that we have 2¹³ or 8192 words for a large sentence. This gives us 67,000,000 entries in our transition frequency matrix. O.K. So this is looking fairly intractable. If we decided that we will only look at correlations between neighbors and next neighbors however, we are back in the realm of possibility. This limitation has a certain justification beyond making things computationally feasible in that every element of the sentence will be a next nearest neighbor with an element of one of the n-gram sentences therby relating every possible syntactic unit. It should even be possible given this information to “guess” a parse based on our frequencies given a large enough corpus.

Stage 2 revolves around extracting information from a parallel corpus. We will simply perform a nearly identical procedure between two parallel corpuses.

When stage 1 and stage 2 are completed, we can use the probabilities of co-occurance from the parallel corpus in conjunction with the intra-language transition frequencies to generate “most probable” sentences.

We’ll see how it goes.

If there is one aspect of modern society that I positively can’t stand it has to be cars.

If we could stand back and look at transportation objectively, cars would just look completely ridiculous. Let us contemplate cars as transportation for a moment.

Large steel objects are hurtled towards each other at a sum relative velocity of something like 160km/h whilst carrying only one person each. They use enormous amounts of energy. They use up huge tracts of land for their storage and for the infrastructure needed to carry them. Because they have no systematic routing, they end up with lower *average* velocities during rush-hour than bicycling. They spew enormous amounts of toxic fumes. A person is killed because of one every 240 minutes in our tiny island. Cars drive demand for energy much above what it should be resulting in increased desirability of oil which serves to create pathological political instability in the middle east. They lower quality of life as they are expensive to own and care for.

In sum total, they are not only wasteful, inefficient, toxic and deadly. They are also completely unecessary. We can affect travel in much better ways. The DART is a fabulous transportation system. If we could cover the island with a system like this, it would take up far less space, use less energy, and it would be faster for the purpose of travel than cars ever could.

I often hear the various parties (including the Greens!) saying that the trafic problem should be solved that with more and bigger roads to solve the traffic problem. One need only look at LA to see the complete futility and absurdity of trying to solve the problem by throwing roads at it. LA had faster average cross town transit speeds in 1920 when trolleys were common. It would be and environmental and aesthetic disaster if we were to turn Ireland into an LA-like twisted mass of freeways.

Where I grew up, in Anchorage Alaska, there really was nothing for it but to own a car. The city center was 12 km from my home, and winter temperatures could reach as low as -40C. There was no public transportation that could be used reliably. The most frequent bus routes were served once every 45 minutes. The buses were frequently late, or even worse early, and they sometimes didn’t come at all. The transit center where all bus transfers took place was at the *edge* of town. The poor were at a terrible disadvantage. A car was necessary to hold a job. The poor also spent a disproportionate amount of income on their cars since the weather causes more repairs to be necessary than in a more moderate climate and cheap cars would break down frequently.

Things are certainly never going to be that terrible in Ireland. The public transit system is great relative to the US, even if it is terrible relative to most of Europe. I am however frightened by the lack of support for a comprehensive public transportation plan and the talk of increased roads. If anything, all public roads should be toll roads. Using cars should be discouraged, and the money could be used to provide real alternatives. Poor decisions should not be rewarded with subsidies from the state. Building roads and road maintainance are a subsidy of a poor tranportation choice.