Patent reduction redux

In my last post I presented a translation of a patent into Haskell. This post went up on Hacker News and Slashdot, and I got over 25,000 page views plus a lot of comments. There are too many comments to respond to individually, and many of them cover similar ground. So here is a more general response to the main issues raised.

Its trivial

Well, yes, in the computer science sense it is. We all know that any algorithm can be written in any turing-complete language, and the Lambda Calculus is turing-complete. QED.

However when I read court judgements related to patentability this never gets mentioned, not because judges are too stupid to understand the point, but because as far as I can tell no lawyer has ever tried to put it in front of a judge. I'm not sure exactly why this is, but I suspect that it is a combination of the general squishiness of the law (see below) and the fact that you want to base your case on a tried-and-tested legal theory rather than building something completely new. From a lawyer's point of view an obscure mathematical theorem (most lawyers have never heard of Turing) looks like a very shaky foundation for a legal argument.

So it seemed to me that if I could convert this abstract theoretical point about turing-complete languages into a practical demonstration that directly addressed a key point of law then it might make a big difference. Sure its a small step for computer science, but it could be a giant leap for legal thinking.

The law is squishier than that

Eben Moglen has said

... the hacker belief that laws are form of code [creates] a particular frame of analysis for legal questions. [...] one thing which lawyers around the world all share is an awareness of the squishiness of law, it is by no means the hard arthropod carapace for internal soft organs that non-lawyers have a tendency to assume it is

Moglen is undoubtedly correct, and when I look at legal judgements I often seem to discern a judge trying to construe the facts and law in a way that will deliver what s/he believes to be justice in the wider human sense as well as in the strict legal sense.

But judges are still constrained by the law; however much they might want to, they cannot look at evidence conclusively showing fact X plus a law saying "if X then Y", and then deliver a judgement of "not Y". The trick is to provide incontrovertible evidence for X. To extend Moglen's metaphor, the law may not have an arthropod carapace, but inside the squishy flesh it still has a rigid skeleton of of laws that judges cannot bend at will.

The law / lawmakers are too corrupt; they'll just legislate around this.

I don't believe the application of the law in the US is anything like corrupt enough for this to be an issue. The worst one can say about the application of American law is that effective legal representation can be bankruptingly expensive for the little guy. But that's not a problem here.

Lawmakers are an issue; the leadership of America is routinely for sale to any sufficiently large campaign contribution. But the limits on patentability are long-standing and fundamental, and until the State Street decision in 1998 it was generally understood that computer software and other information-processing algorithms were not patentable. For the US legislature to change this basic principle of patent law seems unlikely.

Everything in the patent is prior art anyway.

Prior art is one of the most misunderstood things in patent law. Each claim in a patent is an entire invention; there may well be things in the invention that are prior art, but unless you can show that everything in the whole claim existed in a single entity previous to the patent priority date then you don't have prior art.

So the fact that hash tables and linked lists were well known before this patent is irrelevant. Of course if anyone can show actual prior art that includes everything in one of the claims then I imagine that the Red Hat lawyers would like to hear of it.

But all patents can be reduced to a formula / number, so this argument would abolish all patents.

This misunderstands patent law.

USC 35 II 10 defines a patentable invention as

... any new and useful process, machine, manufacture, or composition of matter, or any new and useful improvement thereof ...

This definition excludes mathematical formulae and physical facts from patentability. Leaving aside the fact that it is also well known, the quadratic formula is not patentable because it is not a useful process, machine etc.

The patent covers the physical realisation of the idea, not the idea itself. So publication of the patented material in any form is fine in theory; that is the whole point of the patent system. What you can't do is make and sell the patented invention. (An exception has been carved out here for ready-to-run implementations of software patents on the grounds that they contribute to infringement by the users, which is bad law but not part of this argument).

The 120 patent recites a computer running the algorithms to create a useful improvement in performance, so that makes it patentable.

In the State Street case the Court decided that a mathematical formula could form part of an invention, as long as the whole thing was a new and useful process, machine etc. This was a radical departure from previous US decisions, but it matches current European law (I don't know which came first) where mathematical formulae and computer programs cannot be patented "as such", but can be patented as part of an invention that achieves a "technical effect" (which seems to mean the same as "new and useful improvement" in the US).

However Bilski has now blown all that out of the water. The Court in Bilski specifically declined to endorse anything in State Street, and instead decided that patentability should be decided in line with three other cases. For more details see my post on this, but in essence it means that while a mathematical formula or algorithm can form part of a patented invention, it doesn't contribute anything to the novelty of that invention. Even if the formula or algorithm is completely new, for the purposes of the patent it is treated as "well known". Hence in the Diehr case (the rubber curing method) the invention was the use of a calculation to tell the mould when to open rather than a predetermined time interval. The formula to do this was part of the patent, but the invention was its use in a new kind of machine; one that opened based on temperature readings rather than a timer. On the other hand in the Flook and Benson cases the only novelty was in the formula; everything else was held to be already known, so the patents were disallowed.

In Bilski the central component of the invention was a formula for hedging bets in energy markets. All else was well known, so the patent was disallowed. The Supreme Court said:

Claims 1 and 4 explain the basic concept of hedging and reduce that concept to a mathematical formula. This is an unpatentable abstract idea, just like the algorithms at issue in Benson and Flook.

In this case the patent application itself contained the reduction of the concept to a mathematical formula. But clearly if the claims had left the formula unstated and merely listed an equivalent series of steps or assemblage of "means" (e.g. "a multiplication means connected to an addition means") then this would have merely been a change in the drafting, and it is well established that you can't make something patentable just by changing the words in the claims. So this leads to the following conclusion: any element of a patent claim that can be reduced to a mathematical formula is not patentable material, and the subsequent Section 102 analysis (to determine if the invention is new and non-obvious) must ignore it.

So in the case of the 120 Patent, all the claims come down to "a general purpose digital computer running software that implements a bunch of mathematical formulae". Running software on a computer is prior art, so there is no new invention here.

Patent 5,893,120 reduced to mathematical formulae

I have previously argued that the Bilski ruling renders all software unpatentable in the US because any method of manipulating information (i.e an algorithm) can be translated into a Haskell program, every Haskell function is a formula in the Typed Lambda Calculus, and all the variants of the Lambda Calculus are part of mathematics. Hence any algorithm can be reduced to a mathematical formula, which US patent law states is not patentable subject matter.

The computer science community has tried to explain this to the patent industry, but these explanations have fallen on deaf ears. So I thought I would try a different tack.

Google has just been ordered to pay $5M for infringing patent 5,893,120 (hereafter "Patent 120"). This patent covers a very simple data structure and the algorithms for manipulating it. In fact much of the text of the patent is a pseudo-code implementation in a Pascal-like language. So I thought I would provide a practical demonstration of what has, until now, been a theoretical proposition; the reduction of a software patent to set of mathematical formulae. The result is below, and is also posted here (although I believe that the paste-bin will eventually expire).

I chose this patent partly because it is comparatively simple (there are 95 lines of Haskell source code in the file), but also because it is potentially important; Google's "infringement" consisted of using Linux, which uses this algorithm. Hence anyone using Linux is a potential target.

Red Hat is reportedly seeking a declarative judgement that this patent is invalid, and Google is expected to appeal, so this is not over yet. If anyone knows how I can contact their lawyers to draw these formulae to their attention, I'd be grateful.

Edit 1:A brief overview of the relationship between Haskell and the Lambda Calculus can be found here.

Edit 2:Of course a judge isn't going to know the Lambda Calculus from a lump of rock, but that is what expert witnesses are for. Get a professor of mathematics from an internationally recognised university to testify that these are formulae in the Lambda Calculus, and that the Lambda Calculus is part of mathematics, and you have a sound legal proof. The only thing the patent holders could do is find another professor to testify differently.

Edit 3:Sorry about the broken formatting. If you want to review the code you can either look at this colourised version or copy and paste it into your favourite editor.

Edit 4: This post has been slashdotted. Rather than try to respond to all the various comments individually I have posted a general response to the common themes.

In the meantime, here are the formulae:

{- |

The claims of United States Patent 5,893,120 may be reduced to a set
of mathematical formulae expressed in the Typed Lambda Calculus, also
known as System F.  This file contains these formulae.  The language
used is Haskell, which is a version of System F with extra "syntactic
sugar" to make it useful for practical purposes.

It happens that formulae expressed in Haskell can also be transated by
a Haskell compiler into executable computer programs.  However that
does not make a Haskell function any less of a mathematical formula.
Otherwise the quadratic formula

>    x = (-b +/- sqrt (b^2 - 4ac))/2a

would be rendered patentable subject material by the same argument.

-}


module Patent120 where

import Data.Char (ord)

-- The "ord" function defines a bijection between text characters and
-- numbers.

import Data.Map (Map)
import qualified Data.Map as M

-- The Data.Map module is a standard module defined entirely as a set
-- of Haskell formulae, in the same way as this module.  The "import"
-- means that these formulae are incorporated with the formulae given
-- here.

{-
Claim 1. An information storage and retrieval system, the system
comprising:

  a linked list to store and provide access to records stored in a
  memory of the system, at least some of the records automatically
  expiring,

  a record search means utilizing a search key to access the linked
  list,

  the record search means including a means for identifying and removing
  at least some of the expired ones of the records from the linked list
  when the linked list is accessed, and

  means, utilizing the record search means, for accessing the linked
  list and, at the same time, removing at least some of the expired ones
  of the records in the linked list.
-}

-- | A record with Birth value below some threshold is considered "expired".
type Birth = Integer 


-- | Records in the list have their birth recorded, and also contain
-- a key and a value.
data Record k a = Record Birth k a

-- | True iff the record is older than the threshold argument.
expired t (Record b _ _)  =  b < t   -- | True iff the record matches the key. matches k (Record _ k1 _) = k == k1   -- | The value stored in a record. value (Record _ _ v) = v   -- | Records are stored in a linked list in the system memory. type Storage k a = [Record k a]   -- | The "search1" function includes a threshold age parameter. -- It returns both the items that match the key and the linked list -- with the expired items removed. --  -- The recitation of "means" cannot be used to disguise the formula -- given here.  Otherwise any mathematical formula could be patented -- by reciting e.g. "addition means" and "multiplication means" that are -- mechanically derived from the formula. search1 :: (Eq k) => Birth -> k -> Storage k a -> (Storage k a, [a])
search1 t k records = foldr nextItem ([], []) records
  where
     nextItem r@(Record b k2 v) (retained,found) =
        (if b > t then r:retained else retained,
         if k == k2 then v:found else found)


{-
Claim 2. The information storage and retrieval system according to
claim 1 further including means for dynamically determining maximum
number for the record search means to remove in the accessed linked
list of records.
-}

-- | Similar to "search1", but with an added parameter for the maximum
-- number of records to remove.
search2 :: (Eq k) => Int -> Birth -> k -> Storage k a -> (Storage k a, [a])
search2 n t k = (\(_,x,y) -> (x,y)) . foldr nextItem (n,[],[])
  where
     nextItem r@(Record b k2 v) (n2,retained,found) =
        (n2-1,
         if b > t || n2 == 0 then r:retained else retained,
         if k == k2 then v:found else found)


{-
Claim 3. A method for storing and retrieving information records using
a linked list to store and provide access to the records, at least
some of the records automatically expiring, the method comprising the
steps of:

  accessing the linked list of records,

  identifying at least some of the automatically expired ones of the
  records, and

  removing at least some of the automatically expired records from the
  linked list when the linked list is accessed.

Claim 4. The method according to claim 3 further including the step of
dynamically determining maximum number of expired ones of the records
to remove when the linked list is accessed.
-}


-- | Claim 3 can be reduced to the same formula as Claim 1.  The use of
-- a sequence of steps cannot disguise the fact that this represents
-- a mathematical formula.  Otherwise it would be possible to patent
-- any mathematical formula simply by reciting the steps in evaluating
-- it. e.g. "step 3: the addition of the results of step 1 and step 2"
search3 :: (Eq k) => Birth -> k -> Storage k a -> (Storage k a, [a])
search3 = search1

-- | Likewise Claim 4 can be reduced to the same formula as Claim 2.
search4 :: (Eq k) => Int -> Birth -> k -> Storage k a -> (Storage k a, [a])
search4 = search2

{-
Claim 5. An information storage and retrieval system, the system
comprising:

  a hashing means to provide access to records stored in a memory of the
  system and using an external chaining technique to store the records
  with same hash address, at least some of the records automatically
  expiring,

  a record search means utilizing a search key to access a linked list
  of records having the same hash address,

  the record search means including means for identifying and removing
  at least some expired ones of the records from the linked list of
  records when the linked list is accessed, and

  meals, utilizing the record search means, for inserting, retrieving,
  and deleting records from the system and, at the same time, removing
  at least some expired ones of the records in the accessed linked list
  of records.
-}


-- | Every key has a hash code.  Strings of characters may be used as
-- keys.
class (Eq k) => Hashable k where
  hash :: k -> Int  -- Every key has a hash code.

instance Hashable Char where hash = ord

instance (Hashable a) => Hashable [a]  where
  hash = foldr (\x h -> ((hash x + h) * 53 + 1) `mod` 1733) 0

type HashedStore k a = Map Int [Record k a]


-- | Access a hashed store with a function that returns the modified list of records.
hashAccess5 :: (Hashable k) =>
  (Storage k a -> (Storage k a, [a])) -> Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
hashAccess5 f t k store = (M.insert h retained store, result)
  where
     h = hash k
     (retained, result) = case M.lookup h store of
                             Just records -> f $ filter (expired t) records
                             Nothing      -> ([], [])


-- | Search using hashAccess.
search5 :: (Hashable k) => Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
search5 t k = hashAccess5 srch t k
  where srch store = (store, map value $ filter (matches k) store)

-- | Insert using hashAccess.
insert5 :: (Hashable k) => Birth
                             -- ^ Expiry threshold for old entries.
                          -> Birth
                             -- ^ Birth date for new entry.
                          -> k -> a -> HashedStore k a -> HashedStore k a
insert5 t b k v = fst . hashAccess5 (\store -> (Record b k v : store, [])) t k


-- | Delete using hashAccess
delete5 :: (Hashable k) => Birth -> k -> HashedStore k a -> HashedStore k a
delete5 t k = fst . hashAccess5 (\store -> (filter (not . deleted) store, [])) t k
  where deleted (Record _ k1 _) = (k == k1)


{-
Claim 6. The information storage and retrieval system according to
claim 5 further including means for dynamically determining maximum
number for the record search means to remove in the accessed linked
list of records.
-}


-- | Access a hashed store with a function that returns the modified list of records.  The "Int"
-- argument is the maxiumum number of expired records to remove.
hashAccess6 :: (Hashable k) =>
  Int -> (Storage k a -> (Storage k a, [a])) -> Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
hashAccess6 n f t k store = (M.insert h retained store, result)
  where
     h = hash k
     (retained, result) = case M.lookup h store of
                             Just records -> f $ filterN n (expired t) records
                             Nothing      -> ([], [])
     filterN _ _ [] = []
     filterN n1 p (x:xs) = if n1 <= 0 || p x then x : filterN n1 p xs else filterN (n1-1) p xs    -- | Search using hashAccess. search6 :: (Hashable k) => Int -> Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
search6 n t k = hashAccess6 n srch t k
  where srch store = (store, map value $ filter (matches k) store)

-- | Insert using hashAccess.
insert6 :: (Hashable k) => Int
                          -> Birth
                             -- ^ Expiry threshold for old entries.
                          -> Birth
                             -- ^ Birth date for new entry.
                          -> k -> a -> HashedStore k a -> HashedStore k a
insert6 n t b k v = fst . hashAccess6 n (\store -> (Record b k v : store, [])) t k


-- | Delete using hashAccess
delete6 :: (Hashable k) => Int -> Birth -> k -> HashedStore k a -> HashedStore k a
delete6 n t k = fst . hashAccess6 n (\store -> (filter (not . deleted) store, [])) t k
  where deleted (Record _ k1 _) = (k == k1)


{-
Claim 7. A method for storing and retrieving information records using
a hashing technique to provide access to the records and using an
external chaining technique to store the records with same hash
address, at least some of the records automatically expiring, the
method comprising the steps of:

  accessing a linked list of records having same hash address,

  identifying at least some of the automatically expired ones of the records,

  removing at least some of the automatically expired records from the
  linked list when the linked list is accessed, and

  inserting, retrieving or deleting one of the records from the system
  following the step of removing.

Claim 8. The method according to claim 7 further including the step of
dynamically determining maximum number of expired ones of the records
to remove when the linked list is accessed. 
-}

-- | As with Claim 3 vs Claim 1, the formulae for Claim 7 are the same as for Claim 5
hashAccess7 :: (Hashable k) =>
  (Storage k a -> (Storage k a, [a])) -> Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
hashAccess7 = hashAccess5

search7 :: (Hashable k) => Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
search7 = search5

insert7 :: (Hashable k) => Birth
                             -- ^ Expiry threshold for old entries.
                          -> Birth
                             -- ^ Birth date for new entry.
                          -> k -> a -> HashedStore k a -> HashedStore k a
insert7 = insert5

delete7 :: (Hashable k) => Birth -> k -> HashedStore k a -> HashedStore k a
delete7 = delete5


-- | And the formulae for Claim 8 are the same as for Claim 6
hashAccess8 :: (Hashable k) =>
  Int -> (Storage k a -> (Storage k a, [a])) -> Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
hashAccess8 = hashAccess6


search8 :: (Hashable k) => Int -> Birth -> k -> HashedStore k a -> (HashedStore k a, [a])
search8 = search6

insert8 :: (Hashable k) => Int
                          -> Birth
                             -- ^ Expiry threshold for old entries.
                          -> Birth
                             -- ^ Birth date for new entry.
                          -> k -> a -> HashedStore k a -> HashedStore k a
insert8 = insert6

delete8 :: (Hashable k) => Int -> Birth -> k -> HashedStore k a -> HashedStore k a
delete8 = delete6

Why I am voting Yes to Alternative Vote

On May 5th the UK votes whether to change its electoral system from "first past the post" (FPTP) to "alternative vote" (AV). In FPTP you put an X next to the name of one candidate, and the candidate with the biggest number of Xs wins. In AV the first preferences are counted as for FPTP, but then the candidate with the lowest number of votes is eliminated and the second preferences of their voters are then counted towards the other candidates. This process carries on until someone has more than 50% of the vote.

When I was at University the Students Union used AV, and one year a man stood for the post of Womens' Officer under the name of "Captain Kirk". Against him were two more conventional candidates standing on the Conservative and Labour platforms.

When the votes were counted Captain Kirk got 49% of the first preference votes, with the Conservative getting 26% and Labour 25%. Under FPTP Kirk would have won, but now the Labour candidate was eliminated and it turned out that all of the people who voted for her first had voted for the other woman as second preference. So now the Conservative candidate had 26%+25%=51% of the vote, and Kirk was defeated.

I'm well aware of the Arrow Impossibility Theorem, which shows that given an election with three or more candidates and three or more voters it is impossible to have a voting system that always delivers the right result, but it seems to me that this is rather like the fact that any programming language is logically equivalent to a Turing Machine; its true, but it doesn't mean that all (voting systems | programming languages) are equally good. FPTP seems particularly prone to perverse outcomes, such as the election of a male Womens' Officer when the majority of the electorate wants a female. Pretty much every election in the UK is a 2-horse-1-pony race, with the Liberal Democrats as the pony, and every election pundits discuss the impact of "tactical voting" as people who would like to elect the Lib Dems instead vote Labour for fear of otherwise "letting the Conservatives in". Under AV they can simply vote Lib Dem first and Labour second.

The anti-AV campaign's arguments seem to come down to:

• It will create more hung parliaments. Possibly. I don't see this as a bad thing. The current coalition seems to be doing OK, and a coalition means that more of the electorate's views get represented in government. Having a government elected by 40% of the people get 100% of the power seems to me rather undemocratic.
• It will empower the National Front. For those who don't know, the National Front (NF) is an extreme right wing racist party, which occasionally does well in poor inner-city areas where the "immigrants are taking your jobs and houses" line gets a sympathetic hearing. But equally, if most people object to the NF on principle then AV makes it much easier to vote against them; just put the NF at the bottom of your list. That ensures that no matter how other people vote, your vote will count against the NF.
• The most popular person doesn't always win. Well yes, if you define "most popular" as "winner under FPTP" then this is true; if AV didn't give a different result sometimes then there wouldn't be any difference. The point about AV is that the candidates with the broadest support tend to win much more often, whereas FPTP is prone to producing winners who most of the electorate actively dislike.

So for these reasons I'm going to be voting YES to AV.

Why I am not buying an ebook reader

Being the kind of person with a lot of bookshelves and still not enough room to keep all my books, I wondered about moving to ebooks. There is a lot to like in the concept; the idea of being able to take a significant chunk of my library with me when I am away from home is very attractive, as is being able to back up the whole lot somewhere off site. With a waterproof cover for my ebook reader I could take it into the bath or just read when outdoors on a rainy day without worrying about the wet. And of course you don't have to wait for days for a book to be delivered by Amazon.

So I started looking for answers to the following questions:

1: What books are available in ebook format? And for how much?

I picked a selection from the books I have around me now. Terry Pratchett's books are on the Kindle for around £4.50 each, although "I Shall Wear Midnight" is £9.24. Hang on a minute, the paperback of ISWM is only £3.49. So for almost three times the price I get to save the book industry the cost of printing and shipping me a physical product? I don't think so. Even the older Pratchett books still cost more for the Kindle than in paperback.

Looking elsewhere, the first four Google hits are for pirate torrents and Usenet indexers. Then there is "Fictionwise", which seems to be Barnes & Noble in the US selling stuff on it's Nook. Despite getting a hit in the Google search it seems that B&N don't actually sell any Pratchett. Finally the Diesel e-book store has them for around $8 each, with ISWM for $10. At the moment a dollar is about £0.61 although doing it through a credit card company is going to cost more.

OK, what about some other books? Robert Heinlein: there are four Kindle e-books out of the 32 novels and 59 short stories written by Heinlein. Diesel does better, with 8 Heinlein books. Baen also have some more Heinlein books.

"Contact" by Carl Sagan is not available for Kindle. Googling for "contact sagan ebook" turns up pages of pirate copies but nothing legitimate.

Lois McMaster Bujold's Vorkosigan saga I already have in ebook format because Baen included the entire opus on a CD with the latest volume. Not only does it not have DRM, but it is licensed for free redistribution. Kudos to Baen, and I hope the experiment works for them.

The Matthew Shardlake stories by C.J. Sansom are all available for Kindle, for about the same price as the paperbacks. They are also available in other ebook formats from Diesel for $13 each, which seems a bit steep even by ebook standards.

"Next Stop Execution" by Oleg Gordievsky is not available on the Kindle or on Diesel.

Some of Matt Ridley's books, including "The Red Queen", "Genome", and his latest "The Rational Optimist" are available on the Kindle, but "The Origin of Virtue" is not, which seems odd. Diesel only has "The Rational Optimist".

So my conclusion is that I can buy most of my existing library in ebook format, but not all. Even then its going to be an expensive business to do it legally; we probably have around 1,000 books in our house (never actually counted), and the cost of getting just half of them in ebook format is going to be in the thousands of pounds. Ouch!

2: What about Digital Restrictions Management

The attitude of most publishers here is best summed up by Barnes & Noble. Its "LendMe(TM) technology" lets you lend a book to someone else for a maximum of two weeks exactly once. Amazingly this is sold as a feature! What planet are these people living on? My wife and I both enjoyed C.J. Sansom's series of historical novels. If we used ebook readers then we would both have to buy our own copies. And our son is now starting to read my Terry Pratchett books, so make that three copies in some instances.

And then there is the limit on transfers to new devices. It seems from reports on the Web that ebooks can only be transferred to new devices a finite number of times. After that, your books are stuck on your old devices. So as I upgrade and replace my ebook readers over the years, as I am sure I will, eventually I will start having to keep my old readers around or else purchase their content yet again. Also these transfers have to be mediated by the website you bought the ebook from; if they go out of business then your content is stuck.

Of course I could resort to the pirate copies around the Net. It seems like pretty much anything that is available in a DRM version is available unlocked for free. As a test I downloaded a copy of "The Moon is a Harsh Mistress" from one such site, and sure enough I got an unencrypted PDF (which I could read on my Linux box as an added bonus). I don't feel morally obligated to buy a whole new book just to shift formats: I've already paid the author for the words when I bought the dead-tree version. (Or have I? Some of my books were purchased second-hand. Interesting conundrum there.) But such "solutions" are inherently unreliable. I also worry that I will be sucked into a life of copyright infringement; a little demon on my shoulder is asking me, if I'm going to the trouble of locating and downloading a pirate copy to escape the DRM, why bother buying a legitimate copy that I'm never actually going to look at?

The list of things I can't do with a DRM'd ebook grows the more I think about it. As our son grows out of books we have donated the old ones to his school library. I've lent technical books to colleagues. I've bought out-of-print books second hand. I've borrowed books from libraries. My parents read some of our books when they visit. None of these things are possible with ebooks.

So despite all the advantages, I think I'll pass for now. Maybe in a few years the publishing industry will learn the same lessons that the music industry is learning about the futility of DRM and how to price electronic material, and more old books will be digitised. Then I'll get an ebook reader. But not now.

Is this an Arrow II: The Type System Strikes Back!

In my last post I asked about my EventStream and RTSP types, and asked if RTSP could be an arrow and what the behaviour of "&&&" should be. You can see the first post with the type definitions here. Jason Hart Priestley replied suggesting that "&&&" should be thought of as a join of two computations, which made a lot of sense. So I went with that.

Returning now to the definition of "first", consider:

first ((*2) >>> dup 5)

where "dup 5" emits two copies of every input event, the second one delayed by 5 seconds. So if the input event was [Event t (3, 3)] you would want the output to be [Event t (6, 3), Event (t+5) (6, 3)]".

But suppose that the input had two events like this: [Event t (3,3), Event (t+1) (4,4)]. What should the output be now?

It seems to me that the output of the argument to "first" should be paired with the second value of the events that "caused" those outputs. So the result should be:

[Event t (3,6),
 Event (t+1) (4,8),
 Event (t+5) (3,6),
 Event (t+6) (4,8)]

However to get this you need to have every arrow track the "cause" of every output and tag the event with that information. So you get

type TagEvent t a = (t, Event a)

data EventStream t b c =
   Emit {esEmit :: TagEvent t c, esFuture :: EventStream t b c, esHandle :: RTSP t b c}
   | Wait {esHandle :: RTSP t b c} deriving Show

newtype RTSP t b c = RTSP {runRTSP :: TagEvent t b →  EventStream t b c}

The type "t" indicates the type of the tag for this kind of event. Whenever an arrow emits an event in response to an input then it puts the tag from the input on the output. In the case of "dup" the EventStream it returns from handling a new event will contain both the pending outputs (with the tags from previous input events) and the two new events with tags from the latest input.

So now I can define two functions:

esFirst :: EventStream (d, t) b c → EventStream t (b, d) (c, d)
esFirst (Emit (Event t va, (vb, tag)) es k) =
      Emit (Event t (va, vb), tag) (esFirst es) (rtspFirst k)
esFirst (Wait k) = Wait $ rtspFirst k 

rtspFirst :: RTSP (d, t) b c →  RTSP t (b, d) (c, d)
rtspFirst (RTSP r) = RTSP $ λ(Event t (va,vb), tag) ->
      esFirst $ r (Event t va, (vb, tag))

The second item in the pair (of type "d") gets tacked on to the tag for the whole arrow and re-appended at the end. Problem solved? No.

instance Arrow (RTSP t) where
   arr f = RTSP $ λ(e, tag) →  Emit (fmap f e, tag) (Wait $ arr f) (arr f)
   first = rtspFirst

GHC complains about the infinite type "t = (d, t)". The problem is that the argument to rtspFirst has the type "RTSP (d, t) b c" but it needs to have the type "RTSP t b c". So this version of RTSP isn't an arrow. I have get rid of the type tag "t", but still have some way of having an arrow match causes with effects. Is there some kind of type hackery that will do this?

Is this an Arrow?

I've been thinking about what a native Haskell middleware would look like for a while. One thing seemed obvious: it was going to have to be event-based. So I started thinking about event
streams.

 data Event a = Event  {
    eventTime :: UTCTime
    eventValue :: a
 } deriving (Show, Eq)

 instance Functor Event where
 fmap f (Event t v) = Event t (f v)

 -- | True if the first event occurs strictly before the second.
 isBefore :: Event a →  Event b →  Bool
 isBefore ev1 ev2 = eventTime ev1 

The simplest representation of a stream of events is just an infinite list, so you can define an event processor as a function from one stream to another:

 type EventProcessor a = [Event a] -> [Event a]

Unfortunately this won't work. Suppose that your program is going to emit an event e1 at time t1, but an incoming event before t1 would make your program do something else. In order to decide whether the next item in the output list is e1 you need to look at the time of the next input event. But since that event hasn't happened yet you have to wait for it. If it arrives after t1 then you have missed the deadline.

What is needed is a way to reify the two possibilities here: either the next input event is before t1 or it is after it. This leads to the following data structures:

   data EventStream b c =
    Emit {esEmit :: Event c, esFuture :: EventStream b c, esHandle :: RTSP b c}
    | Wait {esHandle :: RTSP b c} deriving Show
  
 newtype RTSP b c = RTSP {runRTSP :: Event b →  EventStream b c}

The "Emit" case embodies these two possibilities. An interpreter function will process this as follows:

1. If no input event intervenes then it will emit the event esEmit and call
   itself on esFuture.


2. On the other hand if an input event arrives before esEmit then the function
   in esHandle gets called instead, generating a replacement EventStream
   representing a different future.


3. Finally the Wait case allows the event stream to do nothing until an event
   arrives.

The RTSP stands for "Real Time Stream Processor". It also handles the problem of what an event stream is supposed to do before the first event arrives.

Interestingly, both EventStream and RTSP are Categories. The composition operator for EventStream is simple in principle, although in
practice all the different combinations of value and timings make it rather fiddly. Here it is,along with a block comment that explains the logic if you are really interested.

  {-
  The (.) operator for EventStream has to deal with several scenarios:
  
  1: (Wait k2)∘(Wait k1).  This is simple because the only possible event
     is an input that is piped through the two RTSPs.
  
  2: (Wait k2)∘es1@(Emit e1 es1a k1).  In this case there are three timelines:
     a) e1   : (k2 e1)∘es1a      -- Event e1 is passed to k2 and the result composed with es1a.
     b) ev e1: (Wait k2)∘(k1 ev) -- e1 never happens.  Instead the input is passed to k1, which
        generates a new event stream to be composed with k2.
  
     The code for case b is the "k" value in the "let" clause.
  
  3: es2@(Emit e2 es2a k2) es1@(Emit e1 es1a k1).  The logic here is similar to scenario
     2, except that the timing of e2 has to be taken into account as well.  There are five basic
     timelines. Let ev = the next input event and es2b = runRTSP k2 e1
  
     a) e2 e1    : Emit e2 (es2a∘es1a) (k2∘k1)
     b) e1 e2    : k2 e1 ∘ es1a    -- e2 never happens because it is overridden by e1
     c) ev ...   : es2∘(k1 ev)    -- ev overrides e1, and the new output is fed to es2.
     d) e1 ev e2 : esProcess (es2b∘es1a) ev  -- e1 overrides e2, giving es1a and es2b to process ev.
     e) e2 ev e1 : Emit e2 (es2a∘(k1 ev)) -- e2 is emitted, then ev overrides e1.
  -}
  instance Category EventStream where
     -- id :: EventStream b c
     id = Wait $ RTSP $ λe →  Emit e id id
  
     -- (.) :: EventStream  c d →  EventStream b c →  EventStream b d
     (Wait k2)∘(Wait k1) =
        Wait $ k2∘k1
     es2@(Wait k2)∘es1@(Emit e1 es1a k1) =
        let es = (runRTSP k2 e1)∘es1a
            k = RTSP $ λev ->
               if ev `isBefore` e1
                  then es2 ∘ runRTSP k1 ev        -- Timeline 2b
                  else runRTSP (esProcess es) ev  -- Timeline 2a
        in case es of
           Emit e2 es2b _ →  Emit e2 es2b k
           Wait _         →  Wait k
     es2@(Emit e2 es2a k2)∘es1@(Wait k1) =
        Emit e2 (es2a∘es1) (RTSP $ λev →  es2∘runRTSP k1 ev)
     es2@(Emit e2 es2a k2)∘es1@(Emit e1 es1a k1) =
        let k = RTSP $ λev ->
               if ev `isBefore` e1
                  then es2∘runRTSP k1 ev          -- Timeline 3c
                  else runRTSP (esProcess es) ev  -- Timeline 3d
            es = (runRTSP k2 e1)∘es1a
        in if e1 `isBefore` e2
           then   -- Timelines 3b, 3c and 3d.  e2 never happens.
              case es of
                 Emit e3 es3 _ →  Emit e3 es3 k
                 Wait _ →  Wait k
           else   -- Timelines 3a, 3c and 3e.
              Emit e2 (es2a∘es1) (esProcess es2∘k1)
            
  -- | Given a new input event to an existing event stream, this returns the
  -- modified event stream.
  esProcess :: EventStream b c →  RTSP b c
  esProcess (Wait k) = k
  esProcess (Emit eOut rest k) = RTSP $ λeIn ->
     if eIn `isBefore` eOut
        then runRTSP k eIn
        else Emit eOut (runRTSP (esProcess rest) eIn) k

And here is the matching RTSP instance:

  {-
  The (.) operator for RTSP has to deal with a similar range of scenarios to that of EventStream.
  The event that fires off the composed stream is e0.  This is passed to r1, giving es1, and the
  first event from es1 is passed to r2, giving es2.  Hence these events must occur in order.  However
  ev is a second input event that can arrive at any time after e0.
  
  The possible timelines are therefore:
  
     1: e0 e1 e2 ev: Emit e2 (es2a∘es1a) _  -- The basic case.  ev is passed to (es2a∘es1a)
     2: e0 e1 ev e2: es2∘es1a               -- e1 has happened, but ev occurs before e2 is emitted.
     3: e0 ev e1 e2: r2∘esProcess es1       -- e1 is overriden by ev.
  -}
  instance Category RTSP where
     -- id :: RTSP b c
     id = RTSP $ λev →  Emit ev id id
     -- (.) :: RTSP c d →  RTSP b c →  RTSP b d
     r2∘r1 = RTSP $ λe0 ->
        let es1 = runRTSP r1 e0
        in case es1 of
           Emit e1 es1a k1a ->
              let es2 = runRTSP r2 e1
                  k = RTSP $ λev ->
                     runRTSP (if ev `isBefore` e1 then r2∘k1a else r2∘esProcess es1) ev
              in case es2 of
                    Emit e2 es2a k2a ->
                       Emit e2 (es2a∘es1a) k
                    Wait k2a ->
                       Wait k
           Wait k1a ->
              Wait (r2∘k1a)

So now we have shown that these two things are both Categories, can we make them Arrows? The Arrow class requires a definition of first with the following types:

  first :: EventStream b c -> EventStream (b, d) (c, d)  
  first :: RTSP b c →  RTSP (b, d) (c, d)

This is where I run into problems. EventStream can't be an Arrow because the first argument might emit a value before any input is received. At this point first is supposed to pair up the output with some other value of type d, but no such value exists. So EventStream can't be an Arrow.




RTSP doesn't have this problem because some value of type d must have been passed in at the start, so this lets us define first. However from a semantic point of view it is not clear how this should deal with delays and subsequent events.

Its easy to write a delay arrow: it simply echoes every incoming event with a fixed delay added to the event time. Other variations on the theme are possible, such as a dup arrow that echoes every input immediately and then again after a fixed delay, or an arrow that echoes every input as a Right value, but also emits a Left timeout value if no input is received after a defined delay. There is clearly a whole family of combinators waiting to be written here. But first things first.

What should first do if its argument is delay 1? Intuitively, first puts the first item of the pair through its argument, but the second argument bypasses this processing. However this would mean emitting one part of the result before the
second. What should it do with dup 1? And what do the answers imply for this
expression?

  delay 4 &&& delay 5

I don't have any good answers. Maybe RTSP isn't an arrow, but that is a real nuisance. Any ideas?

Bilski says software is not patentable

The US Supreme Court's decision In re Bilski doesn't say much, but I think it says more than perhaps Justice Kennedy intended. In particular I think it is possible to argue that software is not a patentable subject matter.

The Court rejected the "machine or transformation" test as being too narrow; it would seem to exclude things, including business methods, that are "processes" or "methods" under the usual English meanings of those words. But the Court also refers to precedents in Benson, Flook and Diehr (three previous cases), and states that these were used to decide Bilski. It follows that the principles in those precedents are the ones that should generally be applied. Crucially the Court also declined to endorse anything in the State Street decision that originally opened the floodgates to software patents.

The Benson case involved a patent for converting BCD into pure binary. It was held to be an unpatentable abstract idea because the method in the patent was derived from a formula, and so a patent on the method was in effect a patent on the formula.

The Flook case was for a patent on setting alarm thresholds based on a "mathematical algorithm". Again the patent was overturned. In this case a key principle made in the decision was that any mathematical algorithm must be assumed to be "well known". This is a crucial point; a patent can include things that were already known, provided it combines them in a novel way, or with some novel element. The invention has to be considered as a whole, but adding a "trivial post-solution activity" such as setting an alarm wasn't considered to be inventive enough if the formula used was considered to be part of prior art. This means that any "mathematical algorithm" you might come up with is considered as "well known" even if you are the first person to invent it. It can go into a patent, but it doesn't add to the novelty.

Diehr was concerned with a patent for curing rubber. The patent described a machine that measured the mould temperature continuously, pushed the temperature readings through a "mathematical formula" (which was in fact very well known in practice as well as in the narrow legal sense), and opened the mould when the output reached a certain value. The patent was upheld because the novelty lay in the use of continuous measurements to control mould opening, rather than a precomputed delay as had previously been the practice. The fact that a formula was embedded in a computer program as part of the invention did not change this.

So where does this leave software patents? The Court followed the reasoning in the precedents to conclude that since the concept of "hedging" in the Bilski patent was reduced to a mathematical formula in Claim 4, that formula could not be considered a novel contribution. Nothing else in the patent was novel, so they rejected it.

Following this reasoning, it would seem that anything that can be reduced to a "mathematical formula" or "mathematical algorithm" is not patentable. It is possible that Justice Kennedy made a layman's error in his thinking here by assuming that all "mathematical formulae" are concerned with real numbers, as were all the formulae considered in Bilski and the precedents listed.

But of course any computer scientist or mathematician will tell you that this is not true. The whole of discrete mathematics is concerned with mathematical formulae and algorithms that are not related to real numbers.

So it would seem that formulae and algorithms related to discrete mathematics would fall under this rule as well. The Court uses the term "algorithm" and "formula" as synonyms, as indeed they are. To see this, consider the QuickSort algorithm:

1. If there are only 0 or 1 items in the list to be sorted then stop.
   
2. Take the first item from the list of things to be sorted. Call this the "pivot".
3. Divide the rest of the items into two sublists; (a) those less than the pivot, and (b) the rest.
4. Apply this whole algorithm to each of the two sublists from step 3, thereby sorting the sublists.
5. Assemble the sorted list by taking the sorted sublist (a), appending the pivot, and then appending the sorted sublist (b).

This is clearly a method or process. It is also an algorithm. It can also be represented as a formula:

sort [] = []
sort [x] = [x]
sort (pivot:rest) = sort sublistA ++ [pivot] ++ sort sublistB
where (sublistA, sublistB) = partition (< pivot) rest


This is QuickSort written in Haskell. Every Haskell program has a well-defined translation to a formula in the Lambda Calculus, and the Lambda Calculus is part of mathematics. Haskell is turing-complete, which means that any process that can be written as a sequence of steps for manipulating information of any sort can also be written as a Haskell program. Therefore any such process can be reduced to a "mathematical formula". Since mathematical formulae are not patentable subject matter it follows that no process for manipulating information is patentable subject matter.

It might be argued that the use of the modifier "mathematical" by the Court is an attempt to distinguish mathematical formulae and algorithms from non-mathematical ones. But in reality there is no such distinction.

Merriam-Webster defines mathematics as:

the science of numbers and their operations, interrelations, combinations, generalizations, and abstractions and of space configurations and their structure, measurement, transformations, and generalizations

This is a poor definition, since it seems to ignore many topics that are conventionally considered part of mathematics even though they have no apparent relationship to numbers, such as graph theory and topology.
The Britannica is rather more useful, defining mathematics as:

[The] science of structure, order, and relation that has evolved from counting, measuring, and describing the shapes of objects.

It deals with logical reasoning and quantitative calculation. [...]

So is there a class of algorithms or formulae that is not "mathematical" in nature? Clearly not. If any algorithm can be recast as a formula. If such a formula is a product of logical reasoning then it falls under the ambit of mathematics. Even if we take the more limited definition of Merriam-Webster, Godel showed how any logical statement can be recast as a statement of number theory.

Another possible objection to my argument is that mathematics is "abstract" while a process is "concrete". But this is a distinction without a difference. It suggests that the algorithm for QuickSort, expressed as a series of steps, is somehow more concrete than the equivalent formulation in Lambda Calculus. Of course any formulation of QuickSort is going to be longer than the typical single line that non-mathematicians think of when presented with the phrase "mathematical formula", but this would imply that patentability is determined by length, which is clearly nonsense. A mathematical formula that takes a dozen pages to write down is still a mathematical formula.

So I have to conclude that anything capable of being expressed as a computer program is not patentable subject matter under US law.

This probably extends to business method patents as well. Since any business method is the manipulation of information, it follows that it can be written as a computer program (and in fact many Internet businesses have been built by doing exactly that). Even if the business method requires human judgement at some point, that judgement can be treated simply as another input to the program.

To return to where I started, the Supreme Court says that business methods are not a-priori unpatentable, since they are processes and methods. Bilski may not have had sufficient novelty once the formula was stripped out, but the Court wanted to allow for the possibility of a set of business methods that were sufficiently novel. However by following the court's own reasoning it is clear that this set is empty.