Homotopy Type Theory Discussed - Computerphile
Вставка
- Опубліковано 12 жов 2017
- Discussing Homotopy Type Theory with Professor Thorsten Altenkirch.
Main Vladimir Voevodsky Video: • Homotopy Type Theory: ...
/ 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
2:35 "Some stupid programmer exploited that this was implemented in a certain way." Story of my life...
Thorsten?! I've been in his lectures before! Nice to see Homotopy Type Theory again. :)
I guess it was kinda hard to do with Play-Doh but I wish you'd have done a demonstration of the different paths on a torus.
There are actually infinitely many different paths connecting any given point to itself.
The two most obvious ones are:
- Go along the big circle once.
- Go along the small circle (through the hole) once.
But actually you can also wind up paths. You won't be able to unwind them. So you can go through the hole twice or trice or n times... Each of those cannot be further simplified. That's what he was talking about.
Whereas on a sphere it really doesn't matter at all. No matter what you do, you *will* be able to shrink any given path to just a single point.
+Kram1032 I nearly posted an outtake of how hard it was just attempting the paths on the 'sphere' decided the torus a bit too hard. Have decided to try (again) to learn Blender instead! >Sean
to be honest, that actually sounds kinda hard-ish to do in Blender as well.
I mean, it's easy enough in that to get something like this to work at all. But to make it work well? Kinda fiddly to manipulate tiny paths like that.
Probably still easier than irl.
That being said, while the first path on the torus I described must be harder than a path on the sphere, all other paths ought to actually be easier. The torus itself would hold the path on it, right?
Anyway, should have gone for those outtakes :D Maybe in a blooper reel someday?
And there are infinitely many paths which dont connect them.
The important part is that there are only 3 homotopy equivalence classes on the torus, because the homotopy equivalence classes are the elements of the fundamental group, i.e. the first homotopy group. So, while there may be infinitely many loops based at any given point, all those loops are path homotopic to 1 of 3 classes of loops, that is to say, essentially the same.
They are? I assume you mean the paths:
- don't go around a circle at all (same as on sphere, can be contracted)
- go around one loop
- go around the other loop
But how can loops that you wind up more often be contracted into one of the later two?
The way this guy pronounces "theory" is so satisfying.
Is Homotopy theory just topology with paths? Everything he talked about sounded like it was just a different approach to topology.
Homotopy is an important tool in topology, yes.
_"Is Homotopy theory just topology with paths?"_
Kind of. A _homotopy_ is a perturbation between continuous maps. More concretely, if you have continuous maps
f, g: X -> Y
(maps taking X continuously into Y), then a homotopy from f to g is a map
F : X x [0,1] -> Y
such that F(x,0) = f(x) and F(x,1) = g(x) for all x in X. That is, at "time 0", F(-,0) is just f, and at "time 1", F(-,1) is just g, and you have to continuously morph from one to the other. Note that a "path" in a space is a map
p : [0,1] -> X,
a map from the unit interval into X. So a homotopy is just a "path" between maps.
An important perspective of topology is that you ditch some geometry (like distances), to be left with something more fundamental but still important. Homotopy theory goes further, by ignoring the difference between two maps which are homotopic. Usual topology kind of has too much "room" for boring differences between spaces/maps, but homotopy theory collapses a lot of useless details to get a theory which has a kind of more algebraic flavour. For example, there are tonnes of maps
f: S^1 -> S^1
(where S^1 is the unit circle), there's too much space to "wiggle", but up to homotopy you have just one for each integer, the "winding number" of the map (how many times your loop your first circle onto its target). That's an insightful and useful feature of the circle which you wouldn't see as clearly by having to think about all continuous maps.
As another basic example, take the unit disc D in the plane. There is a map
f : D -> *
to the one-point space * which collapses everything to that point. You can also go backwards:
g : * -> D
by including that point in the disc (say at the centre). Doing g then f is the identity on *. Doing f then g collapses the disc to its central point. That's not the identity, but it's homotopic to the identity (you can start with the identity, and as you vary the time variable t in [0,1], just collapse more and more until you collapse everything to the centre). So in the homotopy category, * and D are isomorphic. And, indeed, neither have interesting topological features, they're both "collapsible to point", a feature known as "contracatble" in topology. So in homotopy theory, all contractable spaces are isomorphic.
"just topology with paths" is a hilarious way to describe a baffling subject that many people have spent their lifetimes trying to unravel, and about which we still know little 😂. The homotopy groups of objects as simple as spheres, for example, are still very mysterious.
Homotopy theory is a subfield of topology, in the same sense that, e.g. graph theory is a subfield of combinatorics.
This is even better than the main video.
Also there is some improvement with this latest Thorsten topic, maybe I am becoming accustomed to his accent, his english is improving, or the recording is higher quality.
Bicycle tube. Because donuts don't exist in Europe.
Nathan Dehnel not like that they tend not to
I go on holiday to france every year, and I genuinely can't remember ever seeing a doughnut. They have their own patisserie.
Just watch Simpsons and youll end up knowing what "doh nuts" are.
I can't speak for the mainland, but ring doughnuts definitely exist in the UK, and so do bagels.
life belt
Could we get a video explaining the KRACK WPA2 vulnerability?
Interesting stuff!
Objects are typically defined in such a way as to juxtapose their environment. Between the two opposite topologies I just mentioned are the Klein Objects.
The connection to Computer science can be understood in reference to a quote by David Wheeler: "All problems in computer science can be solved by another level of indirection." What he refers to is none other than the definition of further distinction between new objects and their environments - that is to say in discovering new Klein Objects.
How does the time taken to execute a module fit in with homotopy theory? Or does it only consider the values used by and produced by the modules? How about other characteristics of a module, such as memory requirements, thread count, etc. These could be relied upon by an external program, which would then operate differently if a replacement module was used.
I think in this context we are only taking about the correctness of a program, not its space-time complexity.
This is much, much more abstract than a model that involves the time a computation takes. We aren't even really talking about computations at all, just about logic.
The "module and implementation" analogy was a very, very, very lose analogy. He's just trying to connect it to the channels' viewers as best he can. This subject is far more in the realm of abstract math than it is in computer science.
I'm completely ignorant about this, but how I see it is that two things can be equal/different under any criteria you want. When talking about time cost, two modules can be equal or not. But under correctness, they may also be equal or not. Or they may be equal or not regarding the size of file of the module. The point is that everything else besides the specific attributes is irrelevant to whether there is equality.
How does this compare to Category Theory?
Very, very closely related!
1. An infinity-category is (essentially) a category where you also have arrows between arrows, arrows between arrows between arrows, etc.
2. An infinity-groupoid is (essentially) an infinity-category where every arrow is invertable.
3. There is a very deep intuition (homotopy hypothesis) that infinity groupoids are the correct meaning of "spaces".
4. Homotopy Type Theory regards types as spaces, points as terms, and proofs two terms are equal as paths in a space.
So Homotopy Type Theory is a way of providing a type-theoretic syntax for infinity groupoids.
An aside: Voevodsky spent a large amount of his life working in higher category theory. As I understand it, he got frustrated that the structures were becoming too difficult to reason about without computer proof assistants, so he went to go find a foundation for mathematics which mirrored how mathemeticians think but also worked well with computers. So you can see he really met that challenge amazingly well.
To add to the other reply, we can generalize infinity-groupoids to general objects in a so-called "infinity-topos". Those infinity-topoi are really the objects of study in higher topos theory, one of the main research areas of higher category theory. It is conjectured that homotopy type theory has a canonical interpretation in any such infinity-topos. If that is confirmed, it would mean that one could reason about "every homotopy theory" (homotopy theory itself is essentially higher category theory) at the same time using a convenient language that is moreover easily computer-verifiable.
Precisely like this:
ncatlab.org/nlab/show/homotopy+level
edit: aka Category Theory is a directed homotopy 1-type.
@@shell_jump +1 most accurate answer
If I wanted to learn this, what would the prequisites be?
Bastian Kraft plenty on vids, but start with functional programming and how maths is done in software. (Mathematica et al )
Actually, I would say the only prerequisite is a good deal of mathematical maturity. The canonical reference for this is the HoTT book by the Univalent Foundations Program. Type theory is explained in enough detail in the first chapter, and only requires familiarity with basic logic. Then it builds on that, getting deeper into the theory. The second part of the book is all about using homotopy type theory to redo classical mathematics through examples so it can be skipped.
MichaelKingsfordGray - I’m admittedly a dinosaur but I don’t recall ever seeing Algebraic Topology or Category Theory even suggested in applied math programs. It seems like you’d have to do a bit of specialized curriculum tuning to prepare for learning about/working in this area.
Mathematicians might tell you things like "technically it only depends on an understanding of this or that..." but the truth is that it depends on a graduate education in math. This stuff gets really, really complicated, and really, really abstract. You'd need a graduate background in algebra (algebra that deals with category theory, some universities avoid teaching it that way), and topology. If you already have a strong undergrad higher math background (having taken algebra and analysis, at least), then I'd say it's at very least a year of full-time study before you're in a place when you could begin to chip away at this theory. I think that's very conservative, it would take most people longer before they could solve problems on their own.
What does he mean by implementation details in the context of mathematics? Axioms of models maybe?
Mathematicians often "identify" different objects "causally". An example is vectors in R^n: we often think of R^n as being attached at some point in the plane, like when we think of the velocity vector of a curve, or we often think of a vector in R^n representing a point in the plane, drawn from the origin.
These are technically two different objects defined in different ways: one is R^n, the other is the tangent space to R^n at a point p (it is often thought of as a kind of space of paths through the point p). We "identify" them, and don't distinguish between them when the math we're doing won't be affected by treating them as the same thing.
Once you get into curved spaces, the different tangent spaces aren't the same anymore, and it would be wrong to identify them. If you are looking at some objects you are considering "the same", their actually differences (which supposedly don't matter in your current context) are the implementation details. The "module" is an abstraction: it's "just the properties of these objects you actually need".
The important thing is to know whether what you're doing really is independent of the differences in these objects. Mathematicians are sometimes pretty cavalier about assuming this is true.
Another example comes from algebra: a "group" is an algebraic system (you can think of it as a collection of symbols) with a "times" operation such that each element has an inverse, there is an identity, and times is associative.
The following makes a group: take a rectangle. The elements of the group are transformations of the rectangle: you have the "do nothing" transformation (the identity), then a reflection across the y-axis, and a 90 degree rotation, and every combination of these. There turn out to only be 4 distinct ones.
Now, label the corners of the rectangle 1,2,3,4. Think of the rotation as a map between the integers 1 through 4 that moves each corner to carry out the transformation. It would map (1,2,3,4) -> (2,3,4,1). So, you can think of the same group as a collection of maps between sets of 4 integers, or as a set of transformations of the plane (that is, functions R^2 -> R^2). They are "equivalent" as groups, but not as sets; they are different mathematical objects. Each integer transformation has only 4 elements in its domain, whereas each transformation of the plane has infinitely many, for example.
Those differences are the "implementation details", but this particular abstract 4 element group is the "module". You want to know whether you can take some other collection of mathematical objects that interact in this same pattern, and swap them in for either of these examples, and still have your theorems be true. If your theorems only involve properties of groups, then it will work.
In research level math, the implementation details and types of objects at play get much more complicated, so it can be tough to know whether what you're doing really is independent of the details of the object you chose. That's what he's referring to. Type theory gives a framework to formalize when this works, and when it doesn't, instead of just having to sort of "think about it".
Me and my brain while listening to this:
Brain: what's that noise?
Me: what noise?
*whoosh*
Brain: there it is again!
Me: oh, i think i heard it. where's it coming from?
Brain: i think it's directly above us.
Me: *looks up*
Me: i don't see anything
*whoosh*
Brain: there it is again!
Me: whoa, what is that?
Brain: i guess it's called "Homotopy Type Theory"
RIP voevodsky
Computers can have donuts can they?
according to homotopic theoory apples cannot, windows can.
lol
3:13 We say it's isomorphic ;)
Yeah, he said that.. Is something wrong?
He was poking fun at his wink
that was great, moar
RIP
Bicycle different structures but elements which are equal in similar ways - suddenly bell rang!
It's only me that find very hard do understand Professor Thorsten Altenkirch accent? EN subtitles on his videos pls.
Thumbnail is wrong.
I like this guy, he studies one of the hardest shits ever created and he kind.of tell you it is useless for a software engineer.
why is it useless?
@@bibliusz777 Because it is not yet so applicable for an everyday use. It may become a great thing in the future.
Explain this theory interms of , If Photoshop and Paint are same?
What are the commercial applications of research into HTT?
Kurt Gödel Ultimately some problems will be easier to solve. With quantum computing, most problems are way harder. But some are orders of magnitude easier. Same with parallel computation, or functional programming. There will be groups of problems that "set theory" is not equipped to handle, but homotropic type theory handles with ease.
It's not really a commercial thing. It will help mathematicians to formalize their proofs. Eventually it will probably change the way we think about the theory of computer science, in an abstract way. Not everything people study is aimed at commercial applications. We do research because knowledge is a positive thing. Maybe some day 200 years from now, one of these concepts will end up being the key to something important, but we have no idea. It's still worth funding. Nobody knew higher-dimensional non-euclidean geometries would have applications, but we studied them, then it just so happened that relativity ending up needing them in a very central way. Einstein was able to travel and talk to the mathematicians that had been working on it. The theory would've ground to a halt if we hadn't already been studying the geometry for hundreds of years. It takes a really long time to come up with and improve these concepts.
Just use shortest encoded path.
k
Intriguing! Though the guy really doesn't make it easy to understand.
It's not easy to understand. He's already really, really stretching the reality of it to try to connect it to something down to earth.
The standard American Language inclusive of hyperPunctuation markers, upon standardization and legend-ing, should further the language-- the non-linear "linguistics", if you will, of t_pe theory and how We record (or recall rather), memorize assemblies of that manner of language\listing.
::
Intertranslation markers help One grapple with a non-linear language with principles, propositions\types, that may be applied in axioms to mathematics and geometry/chronometry.
I guess you could just compare the cardinality of the different types. If they are the same, they are equivalent.
genau so reden unsere Professoren auch wenn sie auf englisch ihre Vorlesung halten hahahaha
Last
Explanation starts at 5:13 , thank me later
how that guy can even talk without making a gap between his teeth?
When I think about reusability of code, Julia language comes to my mind.
first
Is the first equivalent to the last, as in there is a path from first to last.
+Jan Hoo
So?
Why does it matter to you to be 1st?
its just a little fun thing we do on the internet
these have gone so theoretical, i think basic concepts that day to day devs can relate to are so much more accessible and interesting
In a century this will be basic programmation
I think a mix is good. It's not like this has ever been a channel that aims to teach you practical skills, it's definitely more about interesting ideas.
UA-cam is filled the the pragmatic everyday programming stuff. One of the great things about Computerphile is that they also talk about theoretical computer science!
But day to day things aren't interesting.
There's not much interesting in day-to-day development. You have the tools, you write the implementation. What is there to talk about? (Obviously not everyone feels this way, but I do.)
I don't know how much more I can take of this guy, I like this channel. But if you keep spamming this mumble machine, I will free myself of the pain.
edit: I cant even turn caption on, This guy should not be leaving home without it.
editx2: I got 1/3 through, I just cant hear words, I hear moaning.