Friday 28 November 2014

Why We Need a Proof Assistant in Law and Finance.

Generalising the "Proof Assistant" for Understanding the Models of Law and Finance.

With oh so many subjects available to study & so many amalgamations going on at both the subject and institutional level, maybe we ought  to think about what's "worth doing" and "why".  There is a trend at the higher-end of mathematics to build "proof assistants" (see Voevosky's videos at his website at the Institute of Advance Studies),  It's clear to him that building a communication tool to computers so that proofs can be checked WILL eventually be the way mathematics will be taught in the general culture someday.  This is absolutely determined, because how else can the mathematical space be explored with such complex proofs, NOBODY can be certain if they are true?  A machine-based (including a quantum machine-based) tool that does most of the mechanical "checking" quickly would help ensure that complex proofs are true and accurate.  Most complex proofs after all have no way of being checked to 100% accuracy by mere humans.

Apply this same idea to much more difficult subjects such as law and finance [Remember Von Neumann's comment? "Anyone who thinks mathematics is difficult, has not yet experienced real life."], and the concept of a "law and finance 'proof assistant'" becomes both theoretically and practically interesting.

Now, imagine the irony if building that sort of machine were really, really difficult?  Voevosky states that the only computer language that could take on the formalities of his Homotopy Type Theory (HOTT) is Coq.  So everybody and his mother is now writing in Coq to get to a universal proof assistant.

But Gross, Chlipala & Spivak (http://adam.chlipala.net/papers/CategoryITP14/CategoryITP14.pdf) say that doing rather easy category theory in Coq is pretty hard!  So they've written some short-cuts to make the use of Coq less burdensome.

This brings me to my point that category theory which was invented [see Eilenberg & Mac Lane 1945) so that we could compare complex theories in mathematics could be made to be extremely useful for COMPARATIVE LAW and a genuine understanding of how COMPLEX FINANCIAL INSTRUMENTS actually work.  In effect, the hinge is that legal systems are models and in the extreme are isomorphic categories which can be compared using functors.  Same can be said about financial instruments. From a legal and financial perspective, the MOST COMPLICATED instrument in the financial universe is the MORTGAGE because it has centuries of legal strata embedded within it (legal-historical interpretations are about 2000 years) and its current re-interpretation via ASSET-BACKED SECURITIES REGULATIONS as an underlying asset of pass-through or senior-subordinated note structures has been further complexified with CREDIT RISK RETENTION REGULATIONS.  All of these legal-financial rules are complex models that need to be re-arranged into MODEL-TYPES than can be formally compared.  Otherwise, really, just as Voevosky says about complex proofs, we have no chance at all in understanding how these instruments actually work in the real world.

For a way to get started in this approach, I recommend reading David Spivak's (2013/2014) A Category Theory for Scientists.  There's an old version freely available on the web and the MIT edition is also quite convenient.  

No comments:

Post a Comment