Archive for November, 2005

From High-school algebra to University algebra

Friday, November 25th, 2005 by Thorsten

An equation like $a \times (a+1) = a^2 \times a$ can be read as an equation over the natural numbers or as an isomorphism which hold in a category with the appropriate structure. The problem of solving equations over 1,+,x,^ in the natural numbers is called the High School Algebra problem and Tarski asked whether the equations we learn at school are complete. Roberto di Cosmo and others observed that this is closely related to isomorphisms in cartesian closed categories with + (I recommend Roberto’s very readable survey).

Wilkie showed that high school algebra is incomplete, the core of his counterexample is that we cannot show using the equations of High School Algebra that $A\times D = B\times C$ implies $(A^x + B^x)^y\times (C^y+D^y)^x = (A^y+B^y)^x\times (C^x+D^x)^y$. I observed that this isomorphism is derivable using dependent types and exploiting $A+B = \Sigma x:2.\mathrm{if}\,x\,\mathrm{then}\,A\,\mathrm{else}\,B$ and $A\to\Sigma x:B.C\,x = \Sigma f:A\to B.\Pi x:A.C\,(f\,x)$ . This observation leads to formulating what I call university algebra which generalizes high school algebra by using $\Sigma and $\Pi.

Here are some laws of university algebra:

  • \Pi a:A.\Sigma b:B\,a.C\,a\,b = \Sigma f:(\Pi a:A.B\,a).\Pi
                           a:A.C\,a\,(f\,a)
  • \Pi p:(\Sigma a:A.B\,a).C\,p = \Pi a:A.\Pi b:B\,a.C (a,b)
  • \Sigma a:A.\Sigma b:B\,a.C(a,b) = \Sigma p:(\Sigma a:A.B\,a).C\,p
  • 1\to A = A
  • 1\times A = A
  • \Pi a:A.B\,a = \Pi a:A.B\,(\phi\,a) where \phi:A = A is an isomorphism
  • \Sigma a:A.B\,a = \Sigma a:A.B\,(\phi\,a) where \phi:A = A is an isomorphism

When deriving isomorphisms we may use equalities of types which relies on equality of terms. We can read those as equations on natural numbers, every type corresponds to a number and
a : A can be read as $a < A$. I believe that unlike High School algebra, University Algebra is complete. Without 0 it may even be decidable, with 0 it isn’t because we can encode consistency of formulas of intuitionistic predicate logic in it.

Roll your own induction principles

Friday, November 18th, 2005 by James Chapman

The other day I tried to write division on natural numbers in epigram. This function is not obviously structurally recursive so we cannot use the standard justification ‘<=rec ‘ to justify our recursive calls and also leave our function looking like the one we wanted to write in the first place. We can exhibit a view to do a custom case analysis that does the necessary subtraction for us yielding patterns of arguments to ‘plus’ (this is the Compare view from VFL). We can then exhibit another view to justify the recursive call on an argument to ‘plus’. I found a likely candidate in Edwin Brady’s thesis and Conor informed me that it first saw the light of day in a talk by James McKinna in 2002. It’s called ‘PlusRec’ and I don’t understand it.

Using Proof to Reason about Errors in Ontology Construction

Thursday, November 17th, 2005 by Louise

I’ve written up the FP lunch stuff I spoke about 3? weeks ago as a Dream Group Blue Book note which I’ve also put on the web at Using Proof to Reason about Errors in Ontology Construction.

Two PhDs and some obfuscated code

Friday, November 4th, 2005 by Wouter

Having visited Utrecht a few weeks ago, I felt that it was my turn to stand up and save James’s bacon. I mentioned two new PhD theses that are worth looking into.

Bastiaan Heeren recently defended his thesis Top Quality Type Error Messages. There are some fairly compelling examples of strange type errors that GHC can give to relatively innocent programs. Rather than fixing the order of unification, Bastiaan argues that the type checker should first collect all the necessary constraints and subsequently try to solve them. Type errors become more precise and can be scripted by users. A lot of the ideas have been implemented in the Helium compiler, which is definitely worth checking out.

Atze Dijkstra will be defending his thesis in a few weeks. He wrote a large incrementally developed type system for a rather large subset of Haskell. During the process of coding, he implemented several interesting tools. The Ruler tool is essentially a domain specific language for describing type systems. It allows different views of typing rules and incremental specification of complex type systems. The ruler tool itself generates both an attribute grammar implementation and \LaTeX specification of the type rules. Although there are no soundness checks, the tool itself works nicely enough and has actually been used to describe rather large type systems.

As an encore, I outlined Ulf Norell’s winning submission to the succ-zero-th Obfuscated Haskell contest.