[FOM] 654: Theory Inspired by Automated Proving 1

[Lawrence Paulson]

It might be useful to try to be clear about different type systems that are in use and set up some basic terminology.

The basis of everything is Church’s 1940 simple theory of types. Here we have the types i of individuals and o of truth values and function types built over them. It’s too spartan to take seriously. HOL Light and similar proof assistants extend this by allowing user-defined types and crucially, polymorphism: this adds type variables to the calculus so that statements can be schematic in their types. Nobody could call this system complicated, but it’s not especially pleasant. John Harrison found an ingenious way to express the type R^n for n an arbitrary natural number. Simple type theory does not allow “dependent types” (in this case, types indexed by natural numbers), and the trick is that n is itself a type; its cardinality is the desired natural number and R^n is actually the function type n => R. Now it is possible to develop quite a lot of multivariate analysis for R^n, and one can even perform simple arithmetic on these exponents, using analogous type constructions. On the other hand, it is sometimes necessary to use R^1 instead of R, and to convert between these obviously equivalent types. And to bring the complex numbers into this scheme, it is necessary to identify C with R^2, so that we actually have 1 = (1,0) and i = (0,1) by definition.

The more elaborate type system that I described in previous messages extends that of HOL Light by incorporating axiomatic type classes. This allows the development of multivariate analysis in a much more abstract and natural way, as I alluded to previously. On the other hand, it is considerably more complicated theoretically than the HOL Light system.

Then there are the various dependent type theories, used in proof assistants such as Coq, PVS, Nuprl. There’s quite a lot of variation here, many of these theories are constructive in one way or another and not all of them are decidable. It’s richly ironic that the people most likely to be dogmatically attached to type theory will prefer one of these systems, where types take on more and more attributes of sets. But it’s not always obvious how to interpret such a type theory in set theory.

What really puzzles me are the remarks about John Harrison attached below. He is the architect of HOL Light, which uses the very strong type system that I’ve just described. There’s no other way to work. Either there is some misunderstanding here or he has done some very new work not using types.

Larry Paulson


> On 18 Feb 2016, at 01:08, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> But recent significant contact with John Harrison, who has a very
> different take, much closer to my instincts. Just look at the amazing
> continued success of John Harrison, and he certainly knows much more
> about involved type systems than I do, so it would be nice to hear
> from him about this issue.

> Secondly, and perhaps even more powerfully, John Harrison quite
> happily avoids relying on involved hard typing, and does not miss its
> absence. He seems to simply get very very very clear about the
> mathematics semiformally, and then breaks everything down in very
> natural ways, uniform throughout his corpus, and everything falls into
> place in record time - all as a part time "hobby".