3 ms·

(See the sibling comment with a "10." in it for context.) 6. The Growth of Univalent Foundations/ Homotopy Type Theory. This is the bastard offspring of (semi-

by gjm11 11y ago

(See the sibling comment with a "10." in it for context.) 6. The Growth of Univalent Foundations/ Homotopy Type Theory. This is the bastard offspring of (semi-)automatic proof checking, the "foundations of mathematics", and, of all things, topology. The connection between these may become less surprising if you are familiar with category theory, which has always been kinda foundational and kinda topological. I don't really know anything about this stuff, and unlike (e.g.) inter-universal Teichmueller theory or the Langlands program I can't really claim that that's because it's beyond human comprehension :-). I bet there are people here who know a lot more than I do about this, and I hope they'll correct my mistakes and fill in my gaps. Anyway, it goes something like this: Mathematicians have always liked building complicated things out of simple things, and in particular have always wanted to build the whole of pure mathematics on top of something nice and simple. The traditional nice-and-simple thing to use for this has been set theory; the study of collections of things. The usual path from raw sets to the mathematical objects we're familiar with -- which is not relevant to "univalent foundations", so skip this if you like -- goes like this. First, build a structure to serve as your non-negative integers. Zero will be the empty set; n+1 will be {0,...,n}. Define addition and multiplication "by induction". Next, ordered pairs: if a,b are sets then {{a},{a,b}} is a set from which you can work out what a,b were. Abbreviate that as (a,b). Now we can make the integers as follows: consider ordered pairs (a,b) where a,b are nonnegative integers, and interpret them as meaning a-b. We need to treat (a1,b1) and (a2,b2) as the same when a1-b1=a2-b2, which is the same as a1+b2=a2+b1, which is a statement only about nonnegative integers and addition. Now we can make rational numbers: take ordered pairs (a,b) where a,b are integers and b isn't zero, meaning a/b; again (a1,b1) and (a2,b2) are the same when a1/b1=a2/b2, which is the same as a1.b2=a2.b1, which is a statement only about integers and multiplication. Now make real numbers by "Dedekind cuts"; the real number x "is" the set of all rational numbers < x. Etc., etc., etc. There are some not-so-likeable things about basing mathematics on set theory. One is that the notion of "set", although it seems absolutely straightforward and transparent, turns out to be not so much so when you look more closely. E.g., you might think that for any proposition P with a single "free variable" x in it, there should be a set of "all x such that P". E.g., "all x such that x is a prime number". But that famously can't work in general; take P = "x is a set that doesn't have itself as a member" and you get a paradox. So you have to restrict your ability to form sets in this way, and there are a bunch of different ways of doing it, and none of them is perfectly satisfactory. (A certain amount of unsatisfactoriness is inevitable thanks to Goedel's incompleteness theorem. However you try to construct mathematics, either your system will just be broken or else there will be questions it can't resolve.) "Univalent foundations" is an entirely different approach. The idea is to build mathematics on something like the lambda calculus -- that is, roughly, you start with functions rather than objects. You can very very handwavily say that the relationship between u.f. and traditional set-theoretic foundations is a teeny little bit like that between Haskell and, say, C. One of the cute things about lambda calculus is a theorem that connects types with mathematical theorems, and expressions that compute a value of a given type with proofs of the corresponding theorems. This is at the heart of proof-checking systems like Coq and Agda. And one of the ideas behind univalent type theory is to find a type system rich enough that you can use this for talking about all of mathematics. I've not really got very far into talking about UTT but I'll stop here because (see above) I don't really know what I'm talking about and I'm sure other people on HN know it much better. The hope is to provide foundations for mathematics that (1) don't have so many layers of arbitrary construction between the foundations and the things mathematicians actually use, and (2) are amenable to automated checking. I think.

eli_gottlieb 11y ago
A fairly good summary, though more material on the Curry-Howard Isomorphism would have been nice. Summary for the layperson: The Curry-Howard Isomorphism is an exact syntactic correspondence between types for lambda calculi, propositions in intuitionistic logics, and objects in closed Cartesian categories. A lambda calculus is a very small programming language built only out of functions. You start assigning "types" so that you can talk about total functions, which will always return. Intuitionistic logic is just logic without the Law of the Excluded Middle (P \/ ~P), and in particular, it's a logic of constructive evidence in the form of proof. To assert X in intuitionistic logic, you must provide a proof which shows how to construct the object the proposition is about. If this sounds computational, it is: the Excluded Middle is false in intuitionistic logic because the Halting Problem is undecidable. For all computationally decidable problems, you can in fact prove the Excluded Middle for those problems by exhibiting the relevant decision algorithm. Closed Cartesian categories... well, I don't actually know enough category theory to describe them. Sorry. But anyway, what the Curry-Howard Isomorphism shows is that given any one of these things, I can turn it into all the others. A proof in intuitionistic logic can be turned into a program in typed lambda calculus, and the type of a lambda-calculus program can be turned into a proposition which that program proves. A program is also an arrow in a closed Cartesian category, and a type or proposition is an object. But anyway, what happened is that Martin-Loef's Intuitionist Type Theory has always been hard to work with, because you have to pull all kinds of funny definitional tricks with equality. In fact, to prove equality in ITT, you have to show that two things must be the same by definition, tautologically, trivially identical. Proving nontrivial equalities gets very difficult, as anyone fed up with trying to do so in Coq can tell you. What happened with Homotopy Type Theory? Well, they noticed that you could add another branch to the Isomorphism: programs are points, types are topological spaces. This isn't so surprising, because category theory has always been a bit topological. This gave them a notion of a formal system to work with, and they found a model for it (which proves the formal system is sound and consistent). They found that in this model, "equality is equivalent to equivalence" (Voevodsky's Univalence Axiom), or in other words, the kind of trivial equality one deals with in Coq is generalized as just a very low-dimensional instance of topological and categorical equivalence. They also found that equality could be defined as the existence of a path between two points -- two objects/proofs are equal precisely when they belong to the same "lump of rubber" in a topological space. Since paths can be nontrivial, "go around the hole in the donut" rather than just "go towards the other point in a straight line", this is a powerful tool -- homotopy theory becomes a part of the new foundational framework. Moreover, since topology and homotopy theory deal with continuous objects, and in fact the definition of continuity in general, from the get go, this meant that they would need a lot less nasty "plumbing" to define things like the real numbers, and thus most of common maths, in a "more topological" foundations. The fact that the new system has computational content and submits itself to computer proof-checking via the Curry-Howard Isomorphism is icing on the cake.

by gjm11 11y ago

eli_gottlieb 11y ago

A fairly good summary, though more material on the Curry-Howard Isomorphism would have been nice. Summary for the layperson: The Curry-Howard Isomorphism is an exact syntactic correspondence between types for lambda calculi, propositions in intuitionistic logics, and objects in closed Cartesian categories. A lambda calculus is a very small programming language built only out of functions. You start assigning "types" so that you can talk about total functions, which will always return. Intuitionistic logic is just logic without the Law of the Excluded Middle (P \/ ~P), and in particular, it's a logic of constructive evidence in the form of proof. To assert X in intuitionistic logic, you must provide a proof which shows how to construct the object the proposition is about. If this sounds computational, it is: the Excluded Middle is false in intuitionistic logic because the Halting Problem is undecidable. For all computationally decidable problems, you can in fact prove the Excluded Middle for those problems by exhibiting the relevant decision algorithm. Closed Cartesian categories... well, I don't actually know enough category theory to describe them. Sorry. But anyway, what the Curry-Howard Isomorphism shows is that given any one of these things, I can turn it into all the others. A proof in intuitionistic logic can be turned into a program in typed lambda calculus, and the type of a lambda-calculus program can be turned into a proposition which that program proves. A program is also an arrow in a closed Cartesian category, and a type or proposition is an object. But anyway, what happened is that Martin-Loef's Intuitionist Type Theory has always been hard to work with, because you have to pull all kinds of funny definitional tricks with equality. In fact, to prove equality in ITT, you have to show that two things must be the same by definition, tautologically, trivially identical. Proving nontrivial equalities gets very difficult, as anyone fed up with trying to do so in Coq can tell you. What happened with Homotopy Type Theory? Well, they noticed that you could add another branch to the Isomorphism: programs are points, types are topological spaces. This isn't so surprising, because category theory has always been a bit topological. This gave them a notion of a formal system to work with, and they found a model for it (which proves the formal system is sound and consistent). They found that in this model, "equality is equivalent to equivalence" (Voevodsky's Univalence Axiom), or in other words, the kind of trivial equality one deals with in Coq is generalized as just a very low-dimensional instance of topological and categorical equivalence. They also found that equality could be defined as the existence of a path between two points -- two objects/proofs are equal precisely when they belong to the same "lump of rubber" in a topological space. Since paths can be nontrivial, "go around the hole in the donut" rather than just "go towards the other point in a straight line", this is a powerful tool -- homotopy theory becomes a part of the new foundational framework. Moreover, since topology and homotopy theory deal with continuous objects, and in fact the definition of continuity in general, from the get go, this meant that they would need a lot less nasty "plumbing" to define things like the real numbers, and thus most of common maths, in a "more topological" foundations. The fact that the new system has computational content and submits itself to computer proof-checking via the Curry-Howard Isomorphism is icing on the cake.