Computer Science ∩ Mathematics (Type Theory) - Computerphile
Вставка
- Опубліковано 10 січ 2017
- As computers are used more and more to confirm proofs, is it time to take computer science's contribution to mathematics further? Dr Thorsten Altenkirch discusses Type Theory vs Set Theory.
A Longer version of this interview can be found here: • CS ∩ Mathematics : LO...
EXTRA BITS: • EXTRA BITS: Computer S...
/ computerphile
/ computer_phile
This video was filmed and edited by Sean Riley.
Computer Science at the University of Nottingham: bit.ly/nottscomputer
Computerphile is a sister project to Brady Haran's Numberphile. More at www.bradyharan.com
I'm starting realize that just because I come here, it doesn't mean I'm smart.
Ксения Ковалевская lolz...
You're wandering into the trolls' dungeon, you might find yourself getting too much attention from those who are smart.
It's just learning the terminology. You are smart.
Zod 'kneel before Zod.' You were awesome.
***** I wish it applied to me in class. I'm horrible at math.
The guy Gérard Huet behind Coq also wrote some data structure he called The Zipper. Apparently he said in conference during a demonstration: "Now I'm gonna open the Zipper and show you my Coq".
Source: someone at INRIA who knew Huet told me.
Terrence Zimmermann Now that you can't make up.
Kevin Pacheco I didn't. I assume the guy wasn't trying to troll us when he told the story during a dinner (with mainly scientists and engineers), because well, he wasn't the trolling type. And you can check that Huet actually invented the Zipper (a kind of tree data structure).
Of course, what I said doesn't constitute a proof, but that's all I have.
A Huet Zipper isn't necessarily a tree-like structure, but you can make a Huet Zipper of a tree. A zipper is more or less a structure that gives the notion of a cursor on an underlying structure such that there's O(1) operations on whatever's underneath the cursor, and it has several operations for moving that cursor around said structure.
If you want to see some trolling, try out McBridge's presentation to the Haskell Implementors Meeting, '09 about the Haskell Preprocessor.
+Foagik Thanks a lot for the info, I am undoubtedly uninformed about that kind of structure as I never needed to use one. That seems quite powerful, I've downloaded Huet's paper for further understanding.
Conor McBride, right? I don't seem able to find this presentation, is it on yt?
I've worked with people at the INRIA and that's totally the kind of humour they have! I have no problem believing this story!
Drink a shot every time he says "ja".
HGich.T - Tutenchamun, he is clearly a fan ;D
Thank you for the advice I'm still laughing!
ja-ger
I cannot unread your comment....
"Das ich soll!"
Didn't know Thor was into maths
Hehehehe...get it? Because his name is Thorsten
lol red
Thors stone...
math*
it's maths, not math, stop omitting words
Mathematicians should wear robes and pointy hats and be interviewed in front of some copper plated bubbling apparatuses (apparati?). Then replace "theorem" by "curse", objects by "demons", and demonstrations by "invocation". "First evoke a local Riemann-integrable demon. the Fundamental Curse of Analysis allows you make sure you can restore that demon when you observe its growth." Cedric Vilani is the headmaster of the Lyon School of Wizardry and professor of Implicit Demons Taming.
Antonin Caors haha, yeah 😌 Master of Demon Invocations
Amandeep Kumar Come now, there's not even any DnD references yet! 😅
what? they are. wait where do you guys live?
New name for mathematics: demons taming
this sounds just so cool.
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.
As a unsuccessful student of mathematics who went to computer science I think, it's because computer scientists care much more about the style of notation and are better trying to find the right language which describes their current problems.
Wow, this is soo true.
But you can also tail call optimize at the compiler level.
John McCarthy, the father of LI
SP, relates how he tried to suggest to mathematicians that functional LI
"A function which doesn't function shouldn't be called a function"
Real-life James Bond Villain - 2017
I will die a happy man when the producers of James Bond finally hire this man to be their evil genius.
The jist of the curry-howard correspondence is:
In a well-typed programming language (such as Coq, Agda, Idris etc.)
Types correspond to theorems
Programs correspond to proofs.
You write the type, then you prove it by writing a body to that function.
I think this would have been more clear if we had examples of some useful types that propositions and their proofs could take.
I could provide some really simple examples in Idris or Agda, if you're still interested, but it takes a bit of knowledge Haskell-like syntax.
This was more like a history lesson than an explanatory video
Still this is very interesting stuff
@@Bratjuuc are u still willing to provide examples in agda? I'm currently studying this subject and the lack of examples is killing me
@@ivanpiri8982 Oof, that was pretty long ago. I forgot what I wanted to provide as examples back then.
I'm going to need some time revising, but I'm still willing to provide examples. I would prefer to provide them in Idris purely for syntax reasons.
So far I can illustrate the following:
*) Boolean logic.
*) maybe Existential quantifications
I'll probably update the list in a short amount of time.
Mathematical Poofs! I love this guy
He uses the coq system for his poofs!
Shubham Bhushan is this about Alan Touring :D ?
*Alan Giedrojc*
"...Alan Turing"
@@GilesBathgate bun
War is Peace - Freedom is Slavery - Ignorance is Strength.
More vids on Haskell and functional programming would be great!
That was really fascinating. I have heard of type theory but didn't know much more that it resembles types in programming. He contrasts it to set theory which helps a lot and makes sense. What we seem to have here, as he is saying, a potential, qualitative (of course partial) transformation of a field, mathematics, because new tools, computers, bring new paradigms. Fascinating, thank you so much. I would be happy to see some more of this, and maybe some examples from this style of math.
I'm pretty sure the only people who understood what he was saying already understood everything beforehand.
Gordon Chin roughly
I had to rewatch it but I think I got it down. Abstract math isn't exactly my forte though.
I think if you have a first year discrete math class or even maybe a high school computer engineering class under your belt, you should be able to follow along
First year Discrete Math couse is enough
Having a degree in CS should be enough to understand what he's saying
So it seems our galactic president Beeblebrox is into type theory.
BTW, great video! Love this more theoretical approach to Computerphile!
He must have painted his seond head Pink, too
Yeah totally agree! Altough I wish he would have written down something
Proof theorems ja. samsing wrong wis se pruuf.
Ja?
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.
I recently signed up for CS in school, and math class is doing set notation. A youtube title has never been so relatable.
UA-cam is great at suggesting videos. I am starting college and covering set theory, and I realized that there are multiple encodings for natural numbers and that implementation details were being exposed. And then I find this video which mentions the same thing. Amazing.
Need a proof? Bring on the COQ.
cringe
"coq could upset english speakers" LOL
and they say Germans dont have a sense of humor
cofi 41 French*
i think he meant the speaker, but isnt he like dutch or something?
@@steliostoulis1875 I think that was intentional
I think the guy behind this saw us complain about the 404 video and is now giving us some meatier content. I'm happy. :)
Ja
ja
great video hope to see more abstract discussions like this for more computerphile videos! or at least a numberphile video on this but more from the other guys' perspective.
I was surprised that he managed to talked about set, type and homotopy theory, abstract mathematics and new foundations of mathematics without mentioning category theory.
Calle Silver-Granhall I think because category theory is more difficult to explain to a general audience than the other three. Also, previous videos have alluded to type theory and set theory.
There is some on the whiteboard on its back...
I doubt it.
Category Theory isn't hard.
Literally every thing he mentioned would have been way easier if he did a quick recap of category theory and what it is. I mean basically everything he talked about was under category theory.
This is exciting.
Just finished Group Theory and this seems like something I can learn from a text book now.
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.
I know I'm late but props to the one(s) who made the subtitles. Very creative with using the relevant symbols.
Excellent video on a relatively new field of study with a real future!
Man, this dude is so intelligent. He just pulls all this theory history out of his head; its awesome.
I like listening to Dr Thor here
But I'm gonna be honest, I got lost about 5 minutes in :(
DeoMachina I was lost in his "ja"s.
His name is Dr. Altenkirch. He's not nordic either.
Mark, that's because the implementation and representation don't matter. As Dr Thor said, you have 1+1+... or binary or decimal... It also doesn't matter what shape the symbols are.
I was surprised to find out that the Predators use decimal system the same way as we do, just that symbols for 0, 1, ..., 9 are those funny patterns.
haha "Dr Thor", really like it, esecially when i read its an abbeviation of his real name..
gotta love the category theory diagrams on the back
I think of mathematical proofs as a mechanism for problem-solving and gaining understanding while producing useful outcomes. Consider machine learning vs. algorithms. Machine learning can develop a function based on a training set that we can use to predict results from other inputs. That's great, but it doesn't necessarily lead to expanding our understanding of the underlying principles, things that we can use to help solve other more general problems.
This is awesome, my mind is blown and I feel much better
I like to think that I know quite a lot about both mathematics and computer science, but this goes way over my head
This guy takes no.3 spot after the Klien bottle and Japanese guy.
No way. Matt and James come before him by a long shot.
Patrick Wienhöft but they are over on numberphile ;)
Patrick Wienhöft
I'm talking on the "looks like science/math" scale. Although I think James could compete with this guy. Oh I forgot the Chemistry guy too!
I was going to say, no one looks more like science than Prof. Sir Martyn Poliakoff.
Well, then Tadashi shouldn't be there. He just looks like an ordinary Japanses.
The chemistry guy obviously belongs in there then, yes ^^
Eyyy funny stuff, I just used Coq a month ago for researching a class project. I was writing a paper on using recurrent neural nets to automatically write proofs in a Coq-like language. I was not successful - turns out it's pretty hard to do, lol
Ok, the comments have spoken: "Dr. Thor" it is
Edit: very interesting! Thanks for doing these!
this is really awesome and interesting, I will check out set and type theories!
It will be interesting to see if a type theory is developed in which univalence is a theorem rather than an axiom
Check out the cubical system made at Chalmers university.
10:49 he is onto something imo
Aesthetics and genres and psychology and visual mediums paired with endless user data
For those who don't know, "coq" means "rooster" in french.
COQ magic :D
Can't be misinterpreted at all, eh?
The Gathering?
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've always struggled with gaining intuition in abstract mathematical theories because of the set theoretic foundations, (set theoretic definition of topology, for instance)
Please do video on backpropagation algorithm in neural networks
or linzer computerphile, don't be afraid to get a bit technical!
or linzer 3blue1brown did that video recently
More videos of this guy please. I have no idea what he's talking about but... more videos please.
Really informative and 'enlightening'. My thanks.
Surprising as this may seem, Mathematicians seldom bother with sets in practice. In fact they already use mathematical constructions pretty much exactly like how it is described with types.
For example the natural numbers N, defined as a set together with a preferred element 0 and a function s:N ->N that gives the successor (programmers would call it next) which is "universal" with this property (in the precise technical sense below), is enough to define N unique up to _unique_ isomorphism (= bijection), and that is perfectly good enough to work with it and ignore any implementation details and it nicely avoids asking silly questions like whether 2 \in 3 because they are not preserved under these isomorphisms.
Here a set of natural numbers (N, 0 , s) is _universal_ if it has the following property: for any set X, element x \in X and any function T:X->X, there is a unique function f: N->X such that f(0) = x and f(s(n)) = Tf(n) (from which it easily flows: f(n) = T^n(x)). Of course one now has to prove that such a set exists (surprise surprise, it does).
This is still an implementation detail. Type theory and category theory abstract away all of this and just have the type N.
What you're describing is a declarative but iterative way of describing a set, which really isn't any better from my perspective than set builder notation, which is also declarative and how the highest abstraction of iteration is expressed in functional languages.
In fact what you're describing is two levels of abstraction lower than set builder notation which is considered implicit iteration while the iterator you're describing here is external iteration
I have been studying formal mathematics for my Computer Science thesis for a little while now. And looking back on it, I think Set Theory has its priority backwards. Set Theory tries to take two Sets of elements, and tries to evaluate whether a function definition exists as a pathway between these two sets. Type Theory takes a set and a function definition, and uses it to generate elements of another set, which can be used as proofs for the other set.
How I understand it is that: Set Theory is like a funky subset of Type Theory because Set Theory deals with concrete definitions generated from abstract ideas, whereas Type Theory works the other way around. In a way, this is more useful and powerful than Set Theory because you can easily create various definitions of a set of elements that would otherwise be hard to do using Set Theory. It's not impossible. It's just hard...
I super enjoyed this video
could we have a second video perhaps going more into detail of type theory maybe xsome examples of its uses. pls
For me, it always been that the sign ∩ was turned 90 degrees anticlockwise in this statement. :)
6:43 or as Mr. Numberphile would call it: The Parker Function.
can you make videos explaining type theory and how math ideas can be proven with it?
I actually once used 2 (element) 3 in a Discrete Maths homework where we couldn't use
Could you talk about the Haskell type system?
Not as rich as COQ, Agda or Idris ones
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.
Wow. Brady's really bringing in the big bucks. He brought in the scientist from Independence Day.
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.
I didn't mean "logical equivalence" but logical equivalence is a special case. Indeed all operations on propositions in type theory are "truth functional". I don't understand your counterexample in particular I don't know what the principle of transposition is. I have no idea how you justify the step form (1) to (2).
It turns out I made a mistake in the proof. I found out that I had used a universal specification rule on a negated universal statement. Because it was negated it was existentially quantified and the rule couldn't be used. Sorry about that. (Thanks for the reply though)
Alex Armstrong no problem. And cheers to you for experimenting and dis overnight your own flaw.
This video is really abstract to me compared to the other. In some videos the most basic concepts (to me) are explained but this one is really hard to follow, so much stuff is considered to be known and there doesn't seem to be much concrete stuff to relate to. It would have helped if it had been a bit more scripted, may be with examples or something. It's quite hard to get into Dr Thorsten Altenkirch's head for this topic!
The entire topic is abstract and you'd basically be learning math from scratch to understand it.
Set theory has the concept of universal set on which a choice function to extract a particular set can be applied....
Like moving from from everything towards being specific.
Does universal set include everything that might be constructed?
such a great thumbnail
Top 10 programming languages to learn in 2020: 1. Type theory 2. Type theory 3. (wait for it) Type theory ...
I was watching with subtitle, and i saw he was gonna have to pronounce Coq, and couldnt wait to hear that.
I just watched this video and to my understanding using HOTT you would be able to show that in fact two different proofs have the same outcome and thus are the same.
So you would be able to first create a proof and then verify that in fact it is an improvement (more elegant, easier, whatever) to an already existing older proof... ?
Or, the other way around, you would be able to show that a proof is really different from another proof...?
A function that does not function should not be called a "function". Makes sense on so many levels!
This makes me feel guilty about not having read TAPL for two weeks...
This guy looks like the scientist from Independence Day!!!
he's my lecturer! top top guy
Nice explantions but I doubt many will understand, I learned Measure Theory and thus can understand the general outline but those unfamiliar will be lost.
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.
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.
ja?....ja?....ja?
Marcelo Souza what does that mean?
@marcelo ja
@saber it means "ya"
So this may be way off, but is SFINAE (in C++ templates) for type deduction basically using the same relationship to encode logical statements?
2 as an element of 3 doesn't seem silly to me.
Thanks! Very interesting.
More of this!
Could this be used to assist with the verification of the proof to the ABC conjecture?
this guy is my spirit animal
11:32
"It's true that 2 is an element of 3, doesn't really make any sense, right?"
I mean, isn't 3 basically == | | |
And 2 == | |
so there indeed is a *| |* inside 3.
So 2 is indeed an element of the set called 3
If it is unable to distinguish between different representations of numbers, is it impossible to do boolean algebra? Is it possible to calculate the result of 42 AND 69 for instance without representing the numbers in binary?
I'm a Swedish mathematician as well.
6:43 "Dysfunctional function". LOL
ja
I will die a happy man when the producers of James Bond finally hire this man to be their evil genius.
Spelling out a rational plan that works in the end :)
We are talking about a type of logic that has to be necessarily less expressive than First Order Logic (that is used for mathematical proofs) otherwise computers cannot help that much.
insidioso The trick is that constructive mathematics works well with the termination requirements for programs and physical computation. To derive equivalence, you simply have to inhabit the type representing the equivalence. The first order logic is derivable from the theory, which is something set theory cannot do.
No, ZFC itself can be modeled inside Homotopy TT, for example.
Is it wrong that I love the sound of this man's voice more than what he's talking about?
Moooooore from this guy please :)
The biggest problem will be when dealing with infinities, other than memory constraints some of the concepts become quite abstract.
It's not actually that much of a problem since we can use codata. Consider, for example, if we wanted to represent an infinite sequence of binary digits. We can do this by defining a function from the natural numbers onto the booleans, so that if we want the nth digit, we just issue it into the function defining the sequence. Since the function's algorithm is finite, we can represent the full infinite sequence using finite data.
Generally speaking, so long as we can define something in finite terms (which is everything we can define in practice, including the concept of infinity itself), we can represent it on a computer using those exact terms.
So would Type Theory make it possible to compile abstract math into executable code? I ask because that is basically what I dream about.
Yes.
Cool!
Kind of... although in general when you compile type theory it's more along the lines of interpreting it. For example, for a Coq proof to be "proven," all you have to do is compile it and there's nothing left to execute. So in a sense, executing the abstract math happens as your proof gets verified. As a result, it doesn't feature many tools for writing executable code (although it does allow you to "extract" the code into another language that can provide the tools for writing useful programs). You can also use some other languages to compile type theory programs into executable programs (Idris and ATS, for example).
no. you would have to create a proof to have a program (proofs are programs). and proving in Coq is much harder than conventional programming
isn't Formal Programming a way of proofing mathematical theorems?
This should be on numberphile
Did I get this correctly?
- Set theory is like a declarative programming language and a set may not be enumerable or infinite (termination problem);
- Type theory is more constructive much like an imperative programming language.
No, if anything, it's the opposite, as type theories tend to be functional languages.
Set theory isn't like programming at all. It's a completely static logical system which, by default, has no computational interpretation.
Type theory exists so that a computer can internalize the semantics of what a program is meant to do. If you want a program to sort a list, you can use type theory to define what it means to sort a list, then a type checker verifies that the program meets that specification within that type. What's significant is that, at the extreme ends of expressiveness, this is sufficient to act as a foundation for mathematics.
Type vs set transcends "has a" and "is a" (in no particular order but maybe I'm off target..?)
Can anybody relate this with typescript, babel and how types(shapes) are identified and are considered to be interpreted into another types. Like replacing a type instance with another equivalent instance which do the work.
I did not find the other part of the video on numberphile maybe someone can pass me the link
"A function that does not function should not be called a function" -- Made me laugh, but has a very concrete truth to it.
amazing that we have evolved to be able to realize such abstract concepts
can someone explain what this math on the whiteboard behind him is about?
It's about his research for formalizing type theory inside type theory. Basically, if lots of math can be expressed in TT, why not try TT itself as well? Since proofs in TT are executable programs, modeling TT inside TT is also a way of doing metaprogramming and proving properties of metaprograms in the same system.
Until a latter day Gödel arrives. (this is a reply to András Kovács's comment below).
How would you check the infinitude of number of primes via computing??
"That is getting abstract."
lol ikr how you gonna say this when already talking about type theory xD
That was interesting and difficult to keep up with.