### 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…

### Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language.

In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure.

And so we arrive at our story. In Coq, equality is som…