Rubrication

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.

I was thinking about cut elimination on my way back from work today due in large part to a post on the cut rule made by sigfpe on A Neighborhood of Infinity.

It occured to me that the fact that cut-free proofs can be so tremendously much larger than the cut-full ones and that directly constructing cut-full proofs is so difficult is a bit strange. It seems somehow unfair.

As I was thinking about this I realised that one could find cut-free proofs automatically and then reduce them with reverse cut-elimination to produce extremely cutfull proofs. These proofs should be very economical computationally. If one keeps the terms that correspond with the proofs along side, one should be able to obtain a source to source translation that might have performance benefits.

Another totally far-out idea came to me as well. Mathematicians often use lemmas repeatedly. Perhaps the process of finding cuts is generally useful. Specifically, if a lemma is useful in simplifying one proof, maybe it is more likely to be useful in simplifying other proofs. There should be statistical measures over random syntactically valid sentences that one could come up with to see if such lemmas exist.

As you might know, I like logics. Notice that logic is in the plural. This might seem a bit strange to you. It certainly seems a bit strange to me. How can it be that there is more than one?

There are quite a number of logics at this point. We pretty much started out with Aristotelian logic, ie. the logic of syllogism which you were probably forced to study in school. Aristotelian logic was formalised and generalised during the early part of last century and this formalism has come to be called Classical Logic or often just CL.

This formalisation caused some to view with suspicion the outcome of various formal arguments. It gave rise to a more conservative ‘constructive’ logic which we will call Intuisionistic (or IL) whose informal interpretation is known as the Brouwer-Heyting-Kalmagorov interpretation or BHK.

Basically in Classical logic you can make proofs about things for which you can not provide examples. This also happens however in Intuisionistic logic for arguments that use the ∀ quantifier. It doesn’t seem so onerous in those cases however as you can see by playing with it a bit.

We can even make things more restrictive and get Minimal Logic (or ML). Minimal logic rejects the provability of arbitrary things from Falsum. The rule is often called ‘ex falso sequitur quodlibet,’ or ‘ex falso.’

Since then there has been a real explosion of the types of logic. There are Substructural Logics, Quantum Logic (QL), Linear Logic (LL, a pretty big fish than can even swallow CL) and a host of others.

From this the question naturally arises in my mind. Which is the right logic? As someone who writes programming languages I have a natural sympathy for IL as it leads naturally to a term calculus meaning that terms can be given back to the user that exemplify proofs. It is a natural logic to look at for the purposes of a database query language. There are however problems with it in regards to this. It is not “resource sensitive”. Things change in data stores and none of the above mentioned logics provide the appropriate tools to deal with this. Linear Logic comes closest but fails to deal with sharing or ordering. Many new resource logics have been invented to deal with this but I have yet to come across something that looks to me like a suitable answer (which doesn’t mean it isn’t already out there!).

In science the problem may be even worse. People use some form of quasi-classical reasoning to make arguments. It seems that this might not even be the appropriate tool to use when reasoning about Quantum Mechanics. Quantum Logic has been proposed as the appropriate way to deal with Quantum quandries in some (fairly fringe) circles. So far Quantum Logic looks to me to be too anemic. Something closer to a theory that has a curry howard isomorphism with quantum computation would be more satisfying.

So what is it that makes a good logic? My personal feeling is this. A logic is a constraint framework from whence you can show various programs that are the “proofs” of the constraint apparatus are acceptable. An appropriate constraint framework is one in which constraints that apply to your system can be expressed simply with minimal work. I believe that the Classical Logic for Propositions arose as a sort of logic of the natural sciences because it was in fact a type of physics. It is a calculus in which we can present common sense notions of real things in a simple way. When we extended the apparatus to classical logic we may have gotten something that strays so far from common sense it is no longer useful (this of course is debatable, and I’m not sure how much I believe it).

Now that we have a quantum world with physics that does not function in ways that our common sense would dictate, it seems perfectly reasonable to reject the notion of classical logic in this regime. In favor of what? I think the jury is still out on this one.

As for as how to quantify what a good logic is, I’ll make a couple of guesses. You want to be able to express constraint systems that apply to your realm with parsimony. You want to be able to verify and extract programs from proofs. If those two conditions are met more often for one logic than another for a particular problem, then I would deem it superior.

Of course this doesn’t even go into notions of logic in ethics…

Thanks to my brother I got a really cool book on proof theory called “Basic Proof Theory”. It has a bunch of nice features including a from the ground up presentation of proof theory that should be relatively accesible to anyone with a background in mathematics. It demonstrates some of the connections provided by the Curry-Howard correspondance (which is my favourite part of the book) . It also describe Second order logic, which is great because I’ve had very little formal exposure to this. Second order logic is really beautiful since you can define all the connectives in terms of ∀, ∀² and →. If you pun ∀ and ∀² you have a really compact notation.

The book also forced me to learn some things I hadn’t wrapped my head around. One of those was Gentzen style sequent calculus. This really turns out to be pretty easy when you have a good book describing it. I’ve even wrote a little sequent solver (in lisp) since I found the proofs so much fun. The first order intuisionistic sequent solver is really not terribly difficult to write. Basically I treat the proofs as goal directed starting with a sequent of the form:

⇒ F

And try to arive at leaves of the tree that all have the form:

A ⇒ A

I have already proven that ‘F ⇒ F’ for compound formulas F from ‘A ⇒ A’ so I didn’t figure it was neccessary to make the solver do it. The solver currently only works with propositional formula (it solves a type theory where types are not parameteric.) but I’m interested in limited extensions though I haven’t thought much about that. I imagine I quickly get something undecidable if I’m not careful.

Anyhow working with the sequent calculus got me thinking about → In the book they present the rule for R→ as such

This is a bit weird since there is nothing that goes the other direction. ie. for non of: Minimal, Intuisionistic or Classical logic do you find a rule in which you introduce a connective in the left from formulas in the right. I started looking around for something that does this and I ran into Basic Logic. I haven’t read the paper yet so I can’t really comment on it. I’ll let you know after I’m done with it.

Ok, so last time we left off with a very informal discussion about Venn diagrams and how they relate to Boolean Logic.

First let us do a little set theory and then we’ll start drawing connections with the previous post to make it a bit more rigorous. We will stick with completely finite sets, so keep that in mind.

A set is basically a collection of distinguishable objects. Sets have no notion of the number of times an object is in them. They simply contain an object or they do not. A set (if it is finite) can be writen in terms of its elements, for instance: S = {a,b,c} is the set S with elements a,b and c.

A map can be thought of as arrows that leave from one set (the domain) and arive at another (the codomain).

We will also introduce a special set 2^S which is an exponential or a “homset” called hom(S,2). S will be jus t a collection of elements as above, and 2 will be a collection of the elements {0,1}. We can think of a homset as a collection of all maps from the elements of S into the elements of 2. In this particular case the map has some special properties because of 2. A map will either map an element to 0 or it maps it to 1. This means that we can fully describe a map from S to 2 by simply naming either the set that goes to 1 or the set that goes to 0. See the illustration below.

Since S is finite 2^S will also be finite. In fact if we use the naming trick above, where we associate the set of elements that goes to 1 with the map, the set of all maps can then be described as the set of all subsets of S. Try it out on paper with S={a,b,c}, 2^S = {{},{a},{b},{c},{a,b},{b,c},{b,a},{a,b,c}}.

Ok, so there are a couple of operations on sets that we will be interested in. One is ∩ which is pronounced “intersection” and ∪ which is pronounced “union”. The intersection of two sets is simply all elements that occur in both sets. So if we let A={a,b,c,d} and B={c,d,e,f} then A∩B={c,d}. The union of two sets is just every element that is in both of the sets. so A∪B={a,b,c,d,e,f}.

Ok now as it turns out we want to talk about another structure called a topology. A topology is a set, in our case S together with a set of subsets of S. We will write it as the tuple <S ,T>.

Now let us go back to Boolean Algebras momentarily. We had a Boolean Algebra B being a tuple <B ,∧,∨,0,1>. Now let us identify B with 2^S, ∧ with ∩ and ∨ with ∪. By doing this we have recovered a Boolean algebra simply by looking at the topology of all S together with all its subsets and the intersection and union operations!

Ok, that is great, but it doesn’t stop there. Topologies are not restricted to <s ,2^S> We can look at other subsets of S. And then it might be interesting to ask whether we will get something like a Boolean algebra. It turns out of course that you don’t get Boolean algebras with just any set of subsets, but you do get some kind of algebra. The thing that you always get is called a lattice.

As it turns out Quantum Mechanics also forms a kind of logic if we start with Hilbert space and use the idea of associating the spaces with a logic. Its more than just the union and intersection of sets however, we also need the concept of an algebraic closure operator (an operator having as properties X ⊂ C(X), C(C(X)) = C(X), and X ⊂ Y → C(X) ⊂ C(Y) ) since the join of hilbert spaces is a superset of the union. This is actually the source of “entanglement” in quantum mechanics which leads to so much confusion. The algebraic closure in the case of Hilbert spaces is the space spanned by the basis vectors of both sets. From this we can then look at the lattice structure and come to find that it isn’t much like a Boolean Algebra at all, but is something called an “Orthomodular Lattice” a bounded lattice that is also an ortho lattice (has a complementation operation) and satisfies the modularity condition. We can write the algebra as the tuple <S,∧,∨,’,0,1 >

The modularity condition is very interesting but visually producing spaces that exhibit it is a bit tricky. I’ll try to draw some nice pictures of spaces that display this behavior in an intuitive way in part IV.

P.S. I lied about getting to Heyting algebras didn’t I!

Ok, I’ll say something about it. When we talk about our typical notions of spaces as we learned them in high school we run into some differences with the boolean algebraic description. The topology that we provided for our boolean space 2^S has an unusual property. If we look at the dual of 2^S in the sense that we exchange 0 for 1 in our naming of sets for hom(S,2) nothing changes. If we have a complement operation in our topology, that is an operator ¬ such that ¬A = S⁄A where ⁄ produces a set with every element of S that is not also in A. The set of all complements of sets in 2^S is 2^S. We say in topology that the tuple <S ,T> is the tuple of a set S, and its open sets T. The complement of the open sets are the closed sets. In 2^S every thing is both closed and open! In fact the silly mathematicians even say that they are “clopen”.

When we took algebra we learned that [0,1] is not the same as (0,1). That is the set that includes its boundary is not the same as the one that does not. This leads us to a different topology in which we have a clear distinction between open and closed sets. In the standard description of space in high school Algebra (that is, the topology induced by the euclidean distance measure) there are only two sets that have the property of being clopen (can you guess what they are?).

So in a Heyting algebra we don’t even bother with the notion of complementation since it leads to complications. Instead we introduce a symbol → into our algebra. We then have the algebra <S,∧,∨,→>. The symbol → is pronounced “implies”.

I promise to tell you more later

I was checking my access logs and noticed that I was #1 on MSN for “logic of space” which is a bit embarassing since my last post had so little content, so I’ve decided to make it up to those who end up here.

We can start with Venn diagrams.

Venn diagrams are spatial representations of logic. They can be used to reason in boolean logic. A Boolean Algebra can be thought of as a tuple < S,∨,∧,¬,0,1 > where S is a set (a collection of elements), ∨,∧ are binary operators, ¬ is a unary operator, and 0,1 are nullary operators (if you don’t know what I’m talking about yet don’t worry). We can think of 0,1 as false and true respectively.

In the Diagram above S represents everything in the picture. A and B are subsets of S which we will write A<s meaning that A is a proper subset of S. White in our pictures will always represent things that are not in the set of interest.

When you look at these diagrams you can often make sense of them by replacing the letters A B and S with familiar heirarchical objects. For example take S as Animals, A as mammals and B as animals with legs. The statement A<S can be expressed as “All mammals are also animals”. Since it is < (proper subset) and not ≤ the statement also implies that there are animals which are not mammals.

The symbols ‘∨’ and ‘∧’ can be used to produce new sets from subsets of S. ‘∨’ is called ‘join’, but in our case it can be read as ‘or’. ‘∧’ is called ‘meet’ and can be read as ‘and’.

In the above image we see A∨B. This can be read A or B, as in “Animals with legs or Mammals”.

The above diagram in light of or Animals example would represent mamals with legs (which of course is just about all mammals excluding pinepeds).

Next we have the unary operator ¬ also called complementation or negation. In our case it gives us set complementation by which we mean ¬A represents all elements that are in the set S but not in the set A. With the animals example ¬A is any animal that is not a mammal which includes birds and reptiles.

With our Animals example we pictorially described the situation ‘Not a mammal or not an animal with legs’. This set (¬A)∧(¬B) would have such elements as whales and lizards but would not include dogs.

The DeMorgan’s law: ‘(¬A)∨(¬B)=¬(A∧B)’ is true for any A or B in S in a Boolean algebra (but also in other algebras including orthomodular algebras). This law is obeyed by our intuitive notion of inclusion with finite sets. Since ¬ is an involution in Boolean algebra (¬¬x=x; read ‘not not x’ is equivelent to ‘x’) we can also derive the dual formula: ‘(¬A)∧(¬B)=¬(A∨B)’.

Another important concept that will be more central in our next discussion, because complementation/negation is not a fundmental operation in Heyting algebras, is implication. In a Boolean Algebra we can define the symbol → as ‘A → B = (¬A) ∨ B’. At first this formula might be a bit difficult to interpret. It does however follow our intuitive notions of implication. If A is true then ¬A is false so B must be true.

All of this discussion so far has been very informal and has been meant as an introduction to the ideas I plan to present next. In the next post I’ll talk about the topology of boolean algebras and heyting algebras and how we can think of them pictorially.