Computer Science and Homotopy Theory - Vladimir Voevodsky

i guess the title was a computer science or something like that or computers and ah homotopia theory so i'll i'm not entirely sure what what part of my work i will be speaking about because i would also appreciate uh having questions being asked during the during the conversational part i mean during the during the talk um so i'll try to explain in think you're boring i'll try to explain a little bit what i'm working on right now so um so here is the story so there is um there is a in an area in theoretical computer science which is called uh type theory so let me try to um to explain what it is about it um developed as as in a sense as an alternative to classical logic as an alternative to classical logic which which is more convenient it's actually some kind of a combination of logic and set theory in a sense so it's something which can be used by computer scientists to describe um what computer programs should do so um i will uh it's probably a standard to consider it as a kind of alternative to to logical set theory so um in in logic we have uh the the units of um of expression are uh so in logic and in type theory so the unions of expression and logic are sentences so a typical logical sentence would uh would look something like that for all x let's say in the language of set theory for all x uh um i don't know what is a syntax to maybe i should put a point here it's not true that x is a member of x that would be a sentence of of set theory so set theory is a theory where where one can use the standard logical operations which would be for all exist no and or and let's see what else we have we have also implied which we can express through the others so this is common to any this is common to any what's called first order uh language in classical logic there are rules of of deduction and but but in order for this to to start working one also needs to um to have some kind of elementary properties of of uh entities so in uh in set theory there is only one expression which which can be used to build formulas and sentences and this expression is x belongs to y so so the the classical set series has only one uh as it's called um propositional symbol or or predicate which is something belongs to something and then all the standard ways of of operating with this with this expression so this is a logical statement and then i can make something like for all x for all y for all z uh probably should put some kind of dots here ax belongs to y implies y belongs to uh in place there exists t in z such that y belongs to t that would be a slightly more complicated statement quite quite typical one in in cermela frankel's theory uh so we were all told that tremelo frankel series somehow serious sets it's in fact not true i mean it it can pretend to be a theory of sets it can also pretend to be a theory of which can be used to create listings of products in the supermarket it can be used almost for anything but what it actually is uh it describes uh so so so so-called sets uh are in fact are in fact trees uh they're trees with certain properties because so as we know the uh the the way insurmelo frankel one approaches things is one starts with the empty set then there is an axiom which says that um for all x there exists a unique oh yeah i forgot i should have said it there is also a quality which is very important so there is equality and and and this sign for belongs so there is an action which says that for each x there exists a unique y such that for all z in y z equals x so that's the action which says that for each x there exists a unique new set y which has only one element namely x itself and it's typically denoted by uh by this so uh starting from there being an empty set which is an action which says it for all x uh which is an action which says that there exists the unique the fact that it's unique can be proved but x uh such that for all y it's true that y is not a member of x and that's the definition of uh of the empty set and so if you have an empty set and uh and then you have this then you can form this and and and this and and so on uh one can also do other things and but uh the point of the matter is that everything is being built out of uh empty set and in fact if i have a set in cermelofranco series so it has a bunch of elements but each element is a set by definition because there's nothing else but sets in in that so um so this uh one can draw it like this so this is my my main set which i'm trying to describe it consists of elements but each element is a set so it it consists of elements probably there are no elements here for example and then each element is again a set so it consists of elements and so on so in fact every object described in cermelo franco theory is naturally a tree and there are precisely two conditions which describe all the trees which can be obtained in this way and the first condition is that um so as an axiom of of set theory it's axiom that two sets are equal if and only if they have the same elements so it means that two sets must be distinguished distinguishable from from the tree structure of their elements so what it means it means that each tree has a property that uh it's a rooted tree and it has a property that uh all the branches are different non-isomorphic so uh all branches at the vertex are distinct not isomorphic um and the second property is that everything has to be build up in finite number of steps from uh from the empty set and that um relates to the fact that if i take any of the uh what are they called um any of the leaves of the tree then uh there is a finite the number of steps to go from from the leaf to the root is finite so for each leaf leave the depths of it is finite uh that doesn't mean that it's it's bounded uniformly for example one can have a initial numbers are represented by tree which looks like this and so uh oh wait no no well that's one way of doing it but we can do it another way also uh no this is not a way to do it because this would be not not permitted according to the first rule because we would have a tree where all these three branches are the same so that is not allowed so instead what one does to represent natural numbers is this then this then this this and so on so again each leaf has only finite depth but the depths are increasing so we have an infinitely many non-isomorphic uh graph sticking out of one point now one can do obvious things with this for example one can consider all subsets in here all sub graphs all of the sub graphs will be different and there will be uncountably many of them so this way one can represent an uncountable set um now that's that's a bit of a strange way my explanation is taking me but i think it's very important to understand so uh now how does one encode something like a group in in set theory so one one starts with doing the following one says let's define what is a pair so this is a definition x is a pair and now let me try to to invent it because i don't exactly remember it so the idea would be if i have two sets x and y and i want to form a pair out of them then i form a new set which consists of um let's see what i should do i think i should take the first uh just in case how about um it doesn't work very well if x equals y i if i take x but i still can get into trouble if if the set if x is the set which consists of only y because i do need no it's not ordered but but but the idea is that you have um maybe uh but this x and y is is going to degenerate into into x if x equals y so so in the case when x equals y this this this this will be x comma x in in and and x cannot be equal to 2x because uh because of this a set can be a an element of itself so okay so this called the pair so let's see what what it means actually for something to be a pair for something to be a pair it means i don't entirely remember the whole axiomatics it might be a an action or it might be a theorem uh so i don't really uh i don't really remember so let's see what has a pair then so a pair is a set z such that um there exists uh a in z there exists b in z such that for all c in z c equals a or c equals b that would be a definition of element of set with two elements and i and there exists uh how about a pair of x and y then it will be easier a little bit so uh if there exists b in z such that for all c in z c equals x or c equals b and uh there and uh and for all uh d in uh in b uh d equals x or d equals y i think that would be a definition of a pair if you really wanted to write it down as as a formal statement in in now you can ask what is a group so we know what is a group a group is a set together with a map and a bunch of other things so to encode it all in in set theory what one needs to do is to represent it as a as as a kind of uh embedded pairs so it will be a set and then the next so a map between sets is also a set so uh so a map from x to y uh what is the map from x to y it's probably a a triple which consists of a set x uh so so we don't have a triple so we'll need to work with pairs so it will be a pair which consists of set x together with a pair which consists of set y and and set z where set z is a subset in the product of x and y something like that now i i'm not trying to make fun of you i mean that is precisely how mathematics is supposed to be formally encoded in the set theory so a definition of a group would be an expression of this sword which is probably about two pages long and uh so computer scientists obviously needed to actually work with formal uh formalizations and and obviously it's impossible to work with this type of formalization so they invented something called type theory uh and what is now coming to so i have 20 minutes to speak right and then so what is now uh so type system is is totally different belongs totally different class of formal languages where i should so in logic elementary pieces are sentences in type theory elementary pieces are sentences in type zero elementary pieces are called sequence and they're typically written as follows x1 t1 x2 g2 x and now i'm underlying um i'm underlying letters which which denote expressions as opposed to letters x1 x2 and so on which denotes single variables so this uh this type of arm this thing is read as follows so we're assuming that x1 is a variable of type t1 where t1 is some kind of expression x2 is a variable of type t2 where t2 is a type some kind of expression and so on and under these assumptions this expression r of x 1 and the delta x n will have type capital r of x 1 and so on x i now one you need to consider some sort of examples but um the point so so now uh the way one works with those things is that there are rules which permit one to construct a new are syntactically legal uh sequence out of old ones for example so so this the first part of the of the sequence is called context and it's traditionally denoted by capital uh greek letters and the uh the part after the turnstile symbol is called the judgment so in this context this judgment holds and uh the typical typical construction would be the construction of dependent product for example if i have gamma uh rr actually i mean so suppose gamma consists of this and then i have this then i can form a new sequence for which context will be just gamma without this thing and the assertion will be that in the context gamma i can form a product over all x in t of the corresponding r of x's in r of x so that's one of the ways to to construct a new sequence from an old one uh now it turns out that logic as well as some kind of set zero can be expressed entirely inside this type of formalism so that this combines together both the deduction rules of the logic and the axons and that it's very convenient and actually can be quite efficiently used by uh by people who need to describe some concrete structures there is a big part of it which i'm not don't have time to go into there is the um the whole theory of how to do inductive types inductive definitions in general work with inductive arguments inside this uh this kind of approach uh which is very ingenious and once once one have this one can build all the uh all the same things as a sets here except uh except better so uh so typically so in in the simplest there's a simplest type theory it's called um type lambda calculus it was invented by church many many many years ago and i don't think he used this particular notation but in in his uh version one would have some generating types some symbols which which are just like letters in the alphabet i mean and then one would have uh the construction of dependent product uh well which will not be very dependent in that case of lambda so it's it's a branch of lambda calculus in a sense so there will be this lambda expression for i'll explain what lambda is so if i have gamma uh so i have the same thing as here to start with actually what did i write sorry that that would be the the rule for the formation of a dependent product and that would be the rule for the formation of of a member of dependent product so in that case i can write gamma lambda x c r and that will be a member of the product of x gr now it's hard to understand without without some semantics assigned to it and here where is where the second half of of of the title comes in so uh people have been looking for good semantics for type series especially for complex type series for for many many years and they've been there have been some very ingenious construction like uh dana scott construction with for um for non-type lambda calculus but basically for for the kind of languages which actually emerged in in the practice of computer science i mean these languages emerged as practical tools of describing programs uh no one knew any reasonable semantics so the semantics was where types are interpreted as sets and and members of types are interpreted as elements of the sets and it never worked very well and so what we've discovered recently about two years ago is that the kind of the correct semantics for this kind of languages one obtains if one considers types is to be homotopic types as opposed to as opposed to sets and then kind of a lot of rich syntax of of of this uh kind of series finds its reflection in in the structure of the homotopic category in in in in totally amazing ways and kind of the more we work on it the more we understand that this is the way to to approach things like foundation of mathematics for example and instead of going through the set theory and formalizing mathematics in this unseemly way one should one should go through type theory and then what one gets one gets a formalization a syntactic formalization of of the world of homotopy types suddenly and instead of just the word of sets so things like groupoids for example are independently have independent meaning you don't have to build a group without offsets in order for it to have a meaning there are types which are by by diverse group words so when one wants to say to speak about things like the the collection of all finite sets it makes little sense to think about it as a set because as i said it actually depends on on on on the choice of a model very strongly like you have a slightly bigger model there will be more one-point sets slightly smaller model will be fewer one-point sets if you think about or finite sets in general if you think about finite sets as a groupoid then it doesn't matter how how many actual members are there up to an equivalent so this group will always be the same and this type of things is extremely naturally expressed in in this type theoretical language and that's that's what i'm trying to to promote and work on um thank you

Channel: Institute for Advanced Study

Views: 14,177

Rating: 4.9128065 out of 5

Keywords:

Id: UvDeVqzcw4k

Length: 28min 57sec (1737 seconds)

Published: Thu Aug 25 2016