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

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.