A lot of people have been asking me what I’m going to be doing this summer, and I have been very vague, for the excellent reason that until today, I didn’t know either. I’ve been spouting buzzwords like functional programming and nlp and machine learning in every direction.
I will be working with Prof Siddhartha Gadgil from the IISc Math Department.
The overarching idea is to take mathematics as it is done today and rest it on the foundation of homotopy type theory (which is more scalable, so this is not as crazy as trying to do the same with set theory). This requires several steps:
Step 1: Convert mathematics as written in papers to something controlled.
Step 2: Translate the controlled language to HoTT
Step 2 requires a lot of knowledge of homotopy type theory, so I’ll be working on step 1
Step 1 has two parts
Step 1A : Parse latex source (the typesetting languge math papers are written in – you thought they’re written in English?) and convert it into a dependency tree, which is mostly the same words, but tagged with their part of speech, and what other words they refer to.
Fortunately there exist parsers, such as the StanfordParser, which can mostly do this for us. As Mohan Ganesalingam pointed out, mathematics is a lot easier to parse than english in general. There will be issues, of course, especially with latex formulae, but we’ll figure things out. (I hope.)
Step 1B : Convert the dependency tree to the Controlled Language (Gadgil calls it the Naproche-like CNL, but naproche looks like English, while this stuff sure doesn’t, so I prefer to just call it Controlled Language
The plan is to do this via a recursive functorial framework in Scala
The framework exists, but not most of the translation rules, so my job will be to come up with these rules.
So now I have to quickly learn a bunch of skills
How to program in Scala
How to run stuff, build packages etc
Understand what functors and monads are.
How to use Github (I’m really embarrassed I don’t know this yet)
How to parse English
How to identify and describe patterns in mathematical argument.
