### A Theory of Science

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...

### Managing state in Prolog monadically, using DCGs.

Prolog is a beautiful language which makes a lot of irritating rudimentary rule application and search easy. I have found it is particularly nice when trying to deal with compilers which involve rule based transformation from a source language L to a target language L'.

However, the management of these rules generally requires keeping track of a context, and this context has to be explicitly threaded through the entire application, which involves a lot of irritating and error prone sequence variables. This often leads to your code looking something a bit like this:

compile(seq(a,b),(ResultA,ResultB),S0,S2) :- compile(a,ResultA,S0,S1), compile(b,ResultB,S1,S2).
While not the worst thing, I've found it irritating and ugly, and I've made a lot of mistakes with incorrectly sequenced variables. It's much easier to see sequence made explicitly textually in the code.

While they were not designed for this task, but rather for parsing, DCGs turn out to be a convenient …

### Generating etags automatically when needed

Have you ever wanted M-. (the emacs command which finds the definition of the term under the cursor) to just "do the right thing" and go to the most current definition site, but were in a language that didn't have an inferior process set-up to query about source locations correctly (as is done in lisp, ocaml and some other languages with sophisticated emacs interfaces)?

Well, fret no more. Here is an approach that will let you save the appropriate files and regenerate your TAGS file automatically when things change assuring that M-. takes you to the appropriate place.

You will have to reset the tags-table-list or set it when you first use M-. and you'll want to change the language given to find and etags in the 'create-prolog-tags function (as you're probably not using prolog), but otherwise it shouldn't require much customisation.

And finally, you will need to run etags once manually, or run 'M-x create-prolog-tags' in order to get the initia…

### Formalisation of Tables in a Dependent Language

I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of…