Notation and Types

A few years ago I sat in a lecture from Thomas Hales on, among other things, his formal abstracts project. This project is aimed at turning paper abstracts and main results into machine-readable forms that could be interepreted by theorem provers, allowing many computational applications to the body of mathematical theory.

In order to get computers to understand the meaning of mathematical statements, it seems like type theory is an indispensable tool. I’m no expert in this stuff, but basically by assigning types to symbols or expressions, the theory ensures that combinations of these objects form coherent, meaningful statements by making sure that mismatched types don’t go together. This stuff has been around for years in theoretical computer science for the construction and study of programming languages, but it’s exciting to think of it becoming part of standard practice in mathematics.

As a fan of OEIS and StackExchange, I am excited about the improvements the formal abstracts project could bring to the experience of searching for math on the web. I’m sure many of us have the experience of typing strings of mathematical notation into search engines and having them return unrelated garbage. But if the parts of these searches were “tagged” as [G: finite group] or [I: two-sided ideal], the search interpreter could use this extra layer of meaning to get better results. Especially because sometimes it seems like adding these tags ad hoc seems to make search results frequently worse. If people have tricks, please help us all.

After all, much of what humans do when reading math is to make sure expressions are build of things of the right type. What business does a:X\to Y have mapping stuff if a is just a number? A lot of how we choose notation is meant to make this sort of checking easier for us. Certain letters, fonts, and symbols are reserved for certain contexts, and then inevitably evoke them when they appear elsewhere.

I think it’s kind of fun and interesting to catalog this tacit knowledge, so I’m working on the following picture of acceptable/frequently used notation. I respect the freedom of all to alter and reinvent notations, but there are some things that we seem to agree on and I think it’s to our mutual benefit that we do. Someday, the machines will agree too.