Computer Science ∩ Mathematics (Type Theory) – Computerphile


There’s a new way to do Mathematics. which has a number of advantages and this new way of doing mathematics is basically very close to just using a programming language. [Computer Science ∩ Mathematics] In Mathematics, people prove theorems I mean that’s the productivity of mathematicians and there’s a problem: Sometimes theorems turn out to be wrong! so it’s very embarassing: I mean people publish something and provide a proof but then there’s something wrong with the proof. That happens lots of times. And now we have a new opportunity, using Computer Science technology We have something called Interactive Proof Assistants and what you can do with those is, basically, dialogue with a computer you produce a proof – a mathematical proof. which can be stored like a computer program And it can be checked by this or another program to make sure that you haven’t cheated. So that’s… Very cool. And there is increasing use of this: There are actually some conferences where you can submit an artifact which is this formal proof. like, computer code which actually proofs the theorem. and then people can check and you can be very, very sure, that your proof is correct. People are getting lazy these days, you know? You get all these referee requests: “I can’t read this proof, this is too much! I don’t have the time!” But now we have these computer systems, one of them is called Coq it’s a French system. I think they called it that to upset English speakers. We could just do mathematics as it has been done using Set Theory and we’d learn about Sets and Elements and that sort of thing and just formalize it that way but I think if we would do this, we really miss an opportunity: This Coq system, for example, is actually based on a programming language called Type Theory. So this Type Theory is at the same time a programming language and logic, so you can do logical reasoning and it’s a replacement for this language Mathematicians use, called Set theory. It’s a more recent development going back to the 70s: By the Swedish Mathematician and Philosopher
Per Martin-Löf He wanted to capture what it called Constructive Mathematics By Constructive Mathematics we mean that we can actually always obtain a result. that we don’t just claim, for example, if you have a function, you may have no way to calculate the answer In constructive mathematics there is always a way to obtain an answer. If you say there exists a number of some property, in classical mathematics you may not know the number. In constructive Mathematics you can only make this claim if you can actually provide a concrete number. and Per Martin-Löf, he had nothing to do with computer science, he was really a Philosopher and Mathematician a very interesting guy “but then people thought: ok, this idea of always getting an answer:” “doesn’t this correspond to, like, writing a computer program?” And he said: “Yeah, this is like a computer program.” And this has been made more precise and has been used, so people started basically to implement this Type Theory on a computer. Type Theory uses the Types we have in Programming language, like for example the type of booleans, the type of Integers… or the type of functions from Integers to Booleans.
Int → Bool Input an Integer and output a Boolean
Int → Bool and so on. These are types. And a very important observation is, that we can use types in order to model logical reasoning. To model logical propositions. So if you have a proposition, a logical expression, For example, “There are infinitely many ℙrime Numbers”
∀p∈ℙ : ∃q∈ℙ | q>p is a proposition or, for every two ℕatural Numbers, one is less than, equal to or greater than the other
∀a,b∈ℕ: ab These are propositions. And the observation is that, for every proposition, we can associate a type. And that’s the type of evidence or proof for this proposition. This is called the Curry-Howard Equivalence So whenever you have a proposition you find a Type such that , if there is a program of its corresponding type, then you know this proposition holds. Sean: So this is computing getting its elbows in and getting stuck into some mathematics Yes and I would say, ok, using type theory is very natural to do on a computer where as Set Theory seems to be rather alien to use on computers. In Set Theory, for example, there is the notion of a function, but it’s a derived concept: You have a set of pairs with certain properties
{p|p=(a,b), *certain properties hold*} There is not this idea like in Type Theory That a function is something where you put something in and get something out
f : a → b Which corresponds to how we think in Computer Science So a function in Type Theory is something we can actually compute with, Where as a function in Mathematics and Set Theory is something like the set of all pairs of inputs with corresponding outputs but a function in Mathematics may be something you cannot compute So I’m always saying “This is not a good name, to call it `function` because a function which doesn’t function shouldn’t be called a function” Sean: dysfunctional functions
Thorsten: Yeah dysfunctional functions Type Theory has got some other interesting features, which have been discovered or made explicit more recently and this is work which was started by a mathematician, actually: He’s called Vladimir Voevodskij and he’s a Fields medalist at the Institute for Advanced Study in Princeton He is doing something called Homotopy Theory So Homotopy Theory is a quite abstract area of Mathematics where we try to understand geometric objects, a very abstract geometric objects. and you can identify geometric objects which you can transform like plastic… or play dough where you can transform one into the other in continuous transformations and first of all that doesn’t seem to have anything to do with the Type Theory I mentioned but, Vladimir Voevodskij observed, that there actually is a close connection between Type Theory and Homotopy Theory which leads to this new idea called Homotopy Type Theory (HoTT) and the idea here is, that when, in Type Theory, you have a proof that two things are equal, this is like surfaces where you have a path between them and then you can also ask yourself: “Are two equalities equal?” – “Is there a path between paths?” A continuous transformation of paths Ok. That’s
Sean: It’s getting quite abstract Thorsten: It’s getting very abstract
Sean: Is this like a Sean: -These play dough objects are a bit like a way of visualizing these ideas? Is that what he has discovered? Thorsten: No, it’s not really. It’s rather surprising. Because we started with something that is called Type Theory which is a programming language and a logic as I have explained. And then there is this Homotopy Theory which has completely different rules in what is called, Algebraic Topology Which is like, I mean, topology is an idea of describing continuous phenomena like ℝeal numbers and and surfaces and so on, which are important in physics and so on And then, in Homotopy Theory, people do this more and more abstractly. They try to distill the essence of these objects. They are infinitely dimensional – no really good intuition for what’s going on. But then, the surprising thing, and this one of the surprising reuses of mathematics: You go completely abstract in one direction and you come out somewhere completely different And this is a relation between Type Theory and Homotopy Theory, ok? So it’s not very direct; it’s not like we have a type and then we have a picture which corresponds to this type It’s not like this. It’s much more indirect but the mathematical principles underlying this Homotopy Theory and Type Theory are matched up Surprisingly well. Maybe one question is “What is the pay-off?”, I mean, what does this buy us? And I think there are some very exciting opportunities now, where Type Theory shows its superiorirty over Set Theory And this has to do with abstraction: If you want to build large mathematical libaries you have to climb a ladder of abstract reasoning You don’t want to do everything on a concrete level, you have to do things abstractly. That’s the power of Mathematics. Type Theory, and especially Homotopy Type Theory, in its very structure is designed in a way, that you cannot talk about the details of how things are actually implemented so for example, ℕatural Numbers: In Set Theory, ℕatural Numbers are Sets. That’s maybe surprising. But in Set Theory, Everything is a Set. And there is a particular Encoding of ℕatural Numbers using Sets using {curly brackets} but there is more than one! So you can use Sets to encode ℕatural Numbers in various ways. so for example, in the standard encoding in Set Theory, there is a very strange artifact for example, one number is element of a bigger number of ℕatural Numbers, Counting Numbers It’s true that 2 is an element of 3
0∈1∈2∈3∈4∈… doesn’t really make any sense, right? It’s just the way it’s set up. Which means, when you work in Set Theory, you can see the implementation details. How numbers are actually represented using {curly brackets}. Now that’s something that doesn’t really matter when you think about numbers: 2∈3 is silly. But you can’t hide this In Type Theory, when you introduce ℕatural Numbers in Type Theory, you cannot talk about the encoding – how they are actually represented – So for example, numbers are often represented following an idea of an Italian mathematician callead Peano, who said: 0 is a ℕatural Number
0∈ℕ and every other ℕatural Number is a previous number +1
∀n∈ℕ : succ(n)∈ℕ (where succ(n) is n+1) is also a ℕatural Number
∀n∈ℕ : succ(n)∈ℕ (where succ(n) is n+1) and that’s a way we can build all ℕatural Numbers. But there are other ways to do this, right? When you write numbers in this system they become very long. Because you write +1 + 1 +1 +1; that’s not a very good system. So what we rather like to do is using binary encoding of numbers Using 0 and 1. That’s much shorter. I mean still longer than decimal, but It’s much shorter than this +1+1+1 And this are two ways of encoding the ℕatural Numbers. Now in Type Theory, you cannot express the difference between these two encodings. Because they are actually in a way the same:
They exhibit the same concept. So you automatically hide implementation details, like, that’s what we wanted to do in Computer Science. We want to hide implementation details because, like, if you want to change one implementation for another, we don’t want to go all the way up so everything which uses this has to be rewritten. We want to say “Ok I’ll just plug something else in and it works.” So you want to be able to plug in, if we use the Peano Numbers and say “that’s too cumbersome” “and I’ll plug in my binary numbers” and nothing should change.” And that’s how Type Theory is designed. And from this Homotopy Type Theory comes a very important principle which is called the Univalence Principle
(=)≅(≅) And it basically says that two things which are equivalent (≅), like the binary and Peano numbers, then they are equal (=) We cannot, not just, we cannot talk about implementation details but because we cannot talk about implementation details, two things which behave the same from outside (≅) are actually considered to be the same (=) Sean: Is this changing massively the way that people think about things in other areas, then? Thorsten: Yes, so let’s see:
It has the potential of doing this. So Homotopy Type Theory has been suggested as a new Foundation of Mathematics. People can just move into it, they can learn logical reasoning and abstract mathematics just coming from this programming angle. So I think there is an exciting opportunity. And I think, looking back to Set Theory, we have these new tools of Proof Assistants to do interactive proofs And in a way it would be a shame if we used this new technology to formalize the mathematics of the 20s and 30s, the mathematics of, let’s say, yesterday. But there is an exciting new opportunity here, to really use new mathematical ideas, new foundations when we formalize mathematics. …we got a value here at x1 and we are going between x0 and x1 and the value of y, at this position… …in Type Theory means you can proof the Excluded Middle for this particular predicate, You can proof, for all numbers, either prime(n) or not prime(n)…

100 comments

  • That was interesting and difficult to keep up with.

  • Oh, look where Jeffrey "The Dude" Lebowski ended up

  • Φοίβος Παναγόπουλος

    Underneath Type Theory there is a more foundational mathematical approach called Category Theory, which seems to unify all areas of mathematics. Unsuprisingly, Types form a Category. Just as there is a connection between Homotopy Theory and Type Theory, there is a connection between eg. Set Theory and Topology Theory via Category Theory and the theorems of one theory correspond to theorems of the other. I suggest you look into that.

  • This guy looks like Beard from Hotline Miami.

  • I have no clue what he was talking about… :'(

  • So skynet sent Arnold Schwarzenegger back to the past and used his twin brother professor Thor to create the robots??? Theirs speech and looks are uncanny

  • I'm a Swedish mathematician as well.

  • The biggest problem will be when dealing with infinities, other than memory constraints some of the concepts become quite abstract.

  • For me, it always been that the sign ∩ was turned 90 degrees anticlockwise in this statement. 🙂

  • I lost it at 1:31

    Damn french

  • Did he say Curly Howard?

  • There is a commute diagram over Dr Thorsten's head

  • This is very interesting, but a simple demo or at least example on white board would help a lot. After 15 minutes I'm still not sure what this really means.

    I found this intro to coq: https://coq.inria.fr/a-short-introduction-to-coq May be an idea for a future video @computerphile ? 🙂

  • Are there any programming languages that deal heavily with type theory?

  • Cooper & the Cash

    This is the fifth time I have a great idea only to find out it has existed years before I was born… Well, gotta come up with something even better yet again.

  • I can make my own version and call it Saci Patu. Why? Because it sounds like Ball Sack in French.

  • How would you check the infinitude of number of primes via computing??

  • Guy completely misses the point of mathematics and the arbitrary choice of names for mathematical objects. ("function" is something that "functions" is an invalid (recursive) definition. Please, don't make elementary logical errors whilst talking arrogantly about math. :/

  • Ja?

  • 12:23 abstract secrets from which originate powers of the S U C C

  • I love this guy! It's a brilliant idea – that math software Coq ( https- coq.inria.fr/download ).

    I believe I've understood what the software does… [Someone correct me if I'm wrong]

    My understanding:
    I believe this software is like a giant distributed virtual functional programming language in which mathematicians sit directly behind their own functions (proofs) which returns a True/False Boolean value indicating the completion of their proof. Their proofs are created by them in the form of algorithms which produce results until halted. Through linking, everyone's Proofs are connected together using a logical "AND" operator which forces them to all be true if depended upon (Leema).

    Does that sound about right? (that's my honest non-wikipedia answer)

  • I do this in my degree!

  • Is it wrong that I love the sound of this man's voice more than what he's talking about?

  • I'm sorry, but I don't like the idea of limiting math to what computers can do.

  • Computers along with there parts be it Monitors, Screens, Keyboards, Mouses, Remotes, Modems, Scanners, Printers, Floppy Discs, SD Cards, CPU's, and other devices can go hand in hand whether they are desktops, laptops, I pads, kindles, smart phones, cell phones, palm pilots, and other electronic devices and can serve well if they do not over heat or run out of storage space.

  • If the proof is wrong, then it isn't a proof. Does he have any common examples? I mean, from the intro, he made it sound like it happens all the time.

  • Upon the face of the Abyss

    pwoof

  • wtf is he talking about..

  • Accents take English from an "eh, its ok" sounding language to full on rad.

  • could we have a second video perhaps going more into detail of type theory maybe xsome examples of its uses. pls

  • We are happy to welcome you mathematicians into the programming world, but there is one thing you need to learn fast and constantly repeat to yourselves if necessary: Single character identifiers are not acceptable! Use full words and clear and consistent naming conventions. Learn it, live it, love it.

  • I was taught that it is never embarrassing if you prove something and it get established and afterwards someone else proves it to be wrong, because this is how the whole research process works. You prove with what knowledge is available to you; if it gets established that means smart brains in your time can't prove that wrong, they agree with it. And it is alright. 00:30

  • More of this!

  • It's Arnold's cousin, The Mathinator! ja? Don't be lazy! Use ze French Coq system!

  • More videos of this guy please. I have no idea what he's talking about but… more videos please.

  • he said coq. lol

  • reminds me of yellowism

  • don't show Yukon Cornelius this video, he'll go buck wild with the revolver.

  • My boxers have the same color and pattern as his shirt. I can't watch him without feeling … odd.

  • can you make videos explaining type theory and how math ideas can be proven with it?

  • OH! that moment when he said COQ. HAHA

  • Finally! I always hated how the mathematics they taught us in uni was so … 'clumsy' – and I always wanted it to be based on programming which is just way clearer, you cannot misinterpret it etc…

  • Man merkt einfach extrem, dass er deutsch ist. So wie er redet. 😀

  • This makes me feel guilty about not having read TAPL for two weeks…

  • I love coq. Come on, be mature.

    Ha ha ha ha ha ha…

  • Goa Goa MPU ja!

  • gotta love the category theory diagrams on the back

  • No such thing as computer science everything is math

  • Balu Vaithinathan

    Coq, secks theory… woah, this is an X rated computerphile vid.

  • at 6:42 he just knows he destroyed everyones brains and his grin proves it

  • Is this guy coping richars stallman style? 😛

  • Well that was clear as mud.

  • Im viewer 99,999

  • Some say you meet this man when you die

  • InSomnia DrEvil

    that was a really theoretical episode, a bit too theoretical for my liking tbh

  • George Labuschagne

    Could this be used to assist with the verification of the proof to the ABC conjecture?

  • Fernando Garibaldi

    I can listen to this guy talk about math and computer science theory forever or 1+ 1 + 1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1….

  • As a programmer, this makes so much sense. I was in a weird situation where i learned algebra first, and then learned programming (and algorithms and data structures), and then more maths, and i couldn't help but think how i could represent the concepts i learned in computer code, but the notation used in maths was set theory, which was slightly confusing some times. Then i noted to a lecturer that a definition he wrote of something could be expressed as a short recursive function, and turns out he knew (among other things) haskell and he agreed that the recursive notation was correct, but pointed out that you can solve some such functions which may be noted recursively using transformations that allow you to do it as one computation instead of a series of computations (iterative), which can dramatically impact the time they take to run, and he had done work on that. Using maths to speed up some heavy logic functions by transforming them.
    Anyways, my big take-away is i'm fairly decent at maths, but i'm a bad calculator, and i strongly prefer computer science notation over set theory notation. If i had been taught maths through programming the concepts, i would have done MUCH better, and it would also have allowed running the functions and (automatically through code) visualizing the output to gain a better "feel" for it.

  • Mathematicians have too much fun
    Coq upsets English speakers,Coq up Sets,its the Coq system

  • You're telling me I could have used this is in Analysis? And not had the most stressful 10 weeks of my life?

  • I love the palimpsest on the board behind him.

  • LIB3RTARIAN1337

    This is hardly a new development in Computer Science or Mathematics. Coq itself has been around for nearly 30 years. The foundations for this come from the Curry-Howard correspondence (completed by Howard in 1969) and Intuitionistic type theory (created in 1972), so in other words almost 50 years ago. The original type theory that was created by Russell was published all the way back in the 1910s in Principia (as a side note, his motivation were the paradoxes in naive set theory that he discovered).

    So proof assistants may be getting more use now due to recent developments such as the proof of the four colors theorem, but they have been around for what is considered an eternity in these fields (and pretty much every other field).

    Anyway, most mathematicians don't work with formalized set theory. An exception is those who are obsessed with mathematical foundations or working in areas closely related to it (mathematical logic, category theory). The rest just throw out the constructions that lead to paradoxes (ie, by defining collections or families of sets differently than sets), but they don't work with an axiomatic set theory like ZFC. There are even problems that can't be formalized in ZFC (or any other formalism using higher than first order logic thanks to Godel's incompleteness theorems).

    Edit: Well I just watched the rest of the video and I guess it turns out that Dr. Altenkirch pointed some of this stuff out himself. He has a very obscure definition of the phrase "new development"

    Edit 2: It is worth pointing out that the proofs these assistants help make do so by checking the type of the program, not running it. The correspondence is between the type of the program and a proposition in the logic. As such, it is static. Most efforts in Computer Science go towards what is useful at run time (and the type system is meant to aid in writing a program for the purpose of running it, not type checking it, it just helps out that we can reduce runtime errors by catching type errors before running the program). Most stuff in Computer Science cannot even be proven formally (this is actually true of math in general, but mathematicians aren't interested in those areas, whereas Computer Scientists are). In other words, Computer Scientists are studying computation, not static analysis (though that is an important part of theoretical CS, it is a small part handled by PLT). To be blunt, a program in Coq and a program in Idris, though similar in structure, have 100% orthogonal purposes. One is meant to be type checked and the other to be ran. I would go so far as to say that proof assistants are very marginally a part of Computer Science and mostly just pure math that got an implementation on a computer.

    Edit 3: It would be interesting to see what a functor between the category of types with functions as morphisms in (I'm assuming Intuitionistic) type theory and the category of surfaces with paths as morphisms (don't know if this is correct) in homotopy theory looks like. Perhaps that is what that mathematician discovered. In other words, category theory is awesome.

  • ja 😉

  • Computer Science ∩ Mathematics = Computer Science

  • Damn this dudes a party animal

  • Formal methods are getting more and more important as systems grow. For things like blockchain processing one approach to proving correctness is Hoare's Communicating Sequential Processes. Then there's Predicate Transformer Semantics etc.. It all gets very complicated.

  • So this may be way off, but is SFINAE (in C++ templates) for type deduction basically using the same relationship to encode logical statements?

  • I was watching with subtitle, and i saw he was gonna have to pronounce Coq, and couldnt wait to hear that.

  • After a few pints of IPA I can prove anything.

  • Primus Productions

    6:43 Parker Function

  • Dr Thorsten Altenkirch

    At 13:50, you talk about the Univalence Principal, where it is stated that if two things are equivalent, then they are equal.

    I have interpreted this as "If two things are logically equivalent, then they have the same properties.

    I shall show by example that this is not always the case:

    From the premises "forall x (Sx implies Px)", it can be proved that "Exists x (Sx & Px) iff Exists x(Sx)

    Using this example, I shall prove that if two logical expressions are equivalent, they don't necessarily have the same properties. In this example the property they don't have in common will be truth value.

    Take both Sx and Px to be "x=x". Substitution gives (1):

    "forall x (x=x implies x=x)"
    can prove
    "Exists x (x=x and x=x) iff Exists x (x=x)" (1)

    However, by the principal of transposition, it will also be true that (2):

    "forall x (not (x=x) implies (not x=x))"
    can prove
    "Exists x (not x=x) and (not x=x)) iff Exists x (not x=x)" (2)

    Example (1) has a truth value of true, however that of (2) is false. (x=x is always true, likewise (not x=x) is always false.)

    Thus if two statements are logically equivalent, they do not always have the same properties. Using transposition again, this means that if two statements have the same properties, they are not always the same statement.

  • The more I get deeper in my computer science degree the more scared I become ..I am gonna be working my butt off for this degree lmao

  • Amazing. I had thought that set theory was the best way to go. This has spurred me on to look at type theory. Can anyone tell me if it has been developed up to handle metric spaces?

  • This guy should have his own youtube channel

  • 1:42 ( ͡° ͜ʖ ͡°)

  • Seems weird not to mention that HTT is not a developed field and the idea of it functioning as a new foundation for mathematics is only a hypothesis, there are many theorems left to prove before one can conclude that the theory is powerful enough to be able to build all mathematics from it like one can do with set theory. Still a really fun prospect for research though.

  • I like to think that I know quite a lot about both mathematics and computer science, but this goes way over my head

  • This is exciting.
    Just finished Group Theory and this seems like something I can learn from a text book now.

  • please I need this accent. I'm sure i can ask confidently 6 figures salary with it.

  • He should be a character in Overwatch.

  • duck typing for the win

  • It seems the guy does not understand set theory, or algebraic topology, or homotopy type theory that well. Why are we bugging him about something above his pay grade? I mean he thinks type theory changes how functions work. That is pretty bad.

  • It's a strange feeling, I want to be like that guy and simultainously don't want to be like that guy.

  • "A function that does not function should not be called a function" — Made me laugh, but has a very concrete truth to it.

  • What about whitehead and russell? I guess they came up with such an idea way earlier…
    And the problem with a constructibility is that very important theorems couldn't be proven f.e. that every vectorspace has a basis or if you like non-standard analysis or even normal analysis you would loose many theorems that are quite crucial.

  • coq is a big thick piece of software, also veiny

  • as a mathematician, i'd like to say you are wrong

  • Top 10 programming languages to learn in 2020: 1. Type theory 2. Type theory 3. (wait for it) Type theory …

  • this guy is my spirit animal

  • Thorsten is a great explainer and talks about some really subjects – liked this video!

    You guys should also track down Kevin Buzzard. He's a great speaker, interesting guy, and he's recently been working on proof formalisation in a language called Lean. He and students have been writing up a whole bunch of definitions/theorems/proofs, and is planning to do his whole department's curriculum.

Leave a Reply

Your email address will not be published. Required fields are marked *