From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 11 Oct 2017 08:26:23 -0700 (PDT) From: "Daniel R. Grayson" To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: Vladimir Voevodsky MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_12629_1725708205.1507735583186" ------=_Part_12629_1725708205.1507735583186 Content-Type: multipart/alternative; boundary="----=_Part_12630_1502917587.1507735583187" ------=_Part_12630_1502917587.1507735583187 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Here is another old email from Vladimir to me. He reports that he has found a model for dependent type theory in simplicial sets and begun thinking about writing his own proof assistant. ----------------------------------------------------------------------------- From: Vladimir Voevodsky Date: May 1, 2006 9:26:06 PM EDT (CA) To: Vladimir Voevodsky Subject: Re: computers and math and education Dear Dan, sorry for a slow reply. I am in a kind of a transitional state in my work on all this proof related stuff and could not decide what is the best way to proceed. I think I still need a week or two to get to a point where I know myself what I want to do next. I remember what we talked about last time but do not remember anything about your code. What language are you using? What kind of formalism? Here is my story: I have come a long way since our last conversations. I have learned to some extend three existing "proof assistants" (well, "learned" is a bit too strong....) Mizar (based on ZF-theory), PVS (based on simple type theory) and Coq (based on a polymorphic, dependent type system called 'calculus of inductive constructions' which is not really described anywhere. See the e-mail from Carlos Simpson below.). I got convinced that dependent type systems is the best available framework for formalization of math. The first problem with these systems is that they lack(ed) "standard" model. I think I have invented such a model. It takes values in the homotopy category such that the model of the type of say groups is (equivalent to) the nerve of the groupoid of groups and isomorphisms. Having this new semantics I made some progress in modification of existing type systems to make them more complete for this "H- model". The homotopy lambda calculus which I gave some talks about is this modification. I am not entirely happy with the definition I have and keep thinking about how to make it better. I am also working on proving the existence of H-models for it and for some more basic type systems rigorously. This activity is basically a mixture of category theory and homotopy theory of simplicial sets with some basic type theory. Below is a copy of my message to Peter May with one of he questions related to this activity. Despite the fact that homotopy lambda calculus is far from being "done" I am pretty convinced that it is a step in the right direction. So I have started to work on a "proof assistant" based on this system. I figured that it makes sense to program what there is and that in the process I get a better feeling for what has to be modified and how. I have though about proof assistants quite a bit last year and in particular about what are they really good for or should be good for. I decided that for them to be useful it is crucial that they have "memory" which can be "queried". Simplifying things a bit I see the "workflow" as follows. In type theory statements (propositions as they call it) are just types of a special kind (what this "kind" is becomes very clear in the H-lambda). Theorems are propositions which have members (members themselves encode proofs). Hence an ideal (and impossible) proof assistant would be a program where I can input a type expression and the system will return either a term (member) of this type or will tell me that this type has no members. New type expressions are usually built from some previously known ones. Since one does not want to write all definitions from point zero there should be a library of existing types where one can get building blocks for the type expression which forms the query. Hence the memory - to contain all questions which have been asked previously (type expressions) and all answers which have been found (terms). This memory or at least some parts of it should be shared (using some kind of web sharing paradigm) so that if someone places a query or find an answer to a query everybody else has access to it. Right now I am thinking about the structure of such a memory. I feel this has to be done at least on conceptual level before everything else. My feeling is that it might get pretty large and that it is crucial to organize it in a way which makes using it *fast* for the computer so in particular I am thinking about an essentially binary format (not expressions themselves but a structure formed by already parsed expressions connected by references to each other). I also feel that it is Ok if it contains a lot of repeats and redundancy (e.g. a thousand slightly different definition of what a group is) since it is not to be directly accessed by humans and since it is not a problem for a computer to compare to each other a thousand arrays of length thousand. That's where I am now. I have just started this memory thing and I hope to get a better feel for it in a week or two. Volodia. ----------------------------------------------------------------------------- ------=_Part_12630_1502917587.1507735583187 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Here is another old email from Vladimir to me.=C2=A0 He re= ports that he has found a model for
dependent type theory in simplicial= sets and begun thinking about writing his own
proof assistant.

----------------------------------------------= -------------------------------

From: Vladimir Voe= vodsky <vl...@ias.edu>
Date: May 1, 2006 9:26:06 PM EDT (CA= )
To: Vladimir Voevodsky <vl...@ias.edu>
Subject:= Re: computers and math and education

Dear Dan,

sorry for a slow reply. I am in a kind of a transiti= onal state in=C2=A0=C2=A0
my work on all this proof related stuff= and could not decide what=C2=A0=C2=A0
is the best way to proceed= . I think I still need a week or two to=C2=A0=C2=A0
get to a poin= t where I know myself what I want to do next.

I re= member what we talked about last time but do not remember=C2=A0=C2=A0
=
anything about your code. What language are you using? What kind of=C2= =A0=C2=A0
formalism? Here is my story:

I= have come a long way since our last conversations. I have learned=C2=A0=C2= =A0
to some extend three existing "proof assistants" (w= ell, "learned"=C2=A0=C2=A0
is a bit too strong....) Miz= ar (based on ZF-theory), PVS (based on=C2=A0=C2=A0
simple type th= eory) and Coq (based on a polymorphic, dependent type=C2=A0=C2=A0
system called 'calculus of inductive constructions' which is not= =C2=A0=C2=A0
really described anywhere. See the e-mail from Carlo= s Simpson below.).

I got convinced that dependent = type systems is the best available=C2=A0=C2=A0
framework for form= alization of math. The first problem with these=C2=A0=C2=A0
syste= ms is that they lack(ed) "standard" model. I think I have=C2=A0= =C2=A0
invented such a model. It takes values in the homotopy cat= egory=C2=A0=C2=A0
such that the model of the type of say groups i= s (equivalent to)=C2=A0=C2=A0
the nerve of the groupoid of groups= and isomorphisms.

Having this new semantics I mad= e some progress in modification of=C2=A0=C2=A0
existing type syst= ems to make them more complete for this "H-=C2=A0
model"= ;. The homotopy lambda calculus which I gave some talks about=C2=A0=C2=A0
is this modification.=C2=A0 I am not entirely happy with the defin= ition=C2=A0=C2=A0
I have and keep thinking about how to make it b= etter. I am also=C2=A0=C2=A0
working on proving the existence of = H-models for it and for some=C2=A0=C2=A0
more basic type systems = rigorously. This activity is basically a=C2=A0=C2=A0
mixture of c= ategory theory and homotopy theory of simplicial sets=C2=A0=C2=A0
with some basic type theory.=C2=A0 Below is a copy of my message to=C2=A0= =C2=A0
Peter May with one of he questions related to this activit= y.

Despite the fact that homotopy lambda calculus = is far from being=C2=A0=C2=A0
"done" I am pretty convin= ced that it is a step in the right=C2=A0=C2=A0
direction. So I ha= ve started to work on a "proof assistant" based=C2=A0=C2=A0
=
on this system. I figured that=C2=A0 it makes sense to program what=C2= =A0=C2=A0
there is and that in the process I get a better feeling= for what=C2=A0=C2=A0
has to be modified and how.

<= /div>
I have though about proof assistants quite a bit last year and in= =C2=A0=C2=A0
particular about what are they really good for or sh= ould be good=C2=A0=C2=A0
for. I decided that for them to be usefu= l it is crucial that they=C2=A0=C2=A0
have "memory" whi= ch can be "queried". Simplifying things a bit I=C2=A0=C2=A0
=
see the "workflow" as follows.

In t= ype theory statements (propositions as they call it) are just=C2=A0=C2=A0
types of a special kind (what this "kind" is becomes ver= y clear in=C2=A0=C2=A0
the H-lambda). Theorems are propositions w= hich have members=C2=A0=C2=A0
(members themselves encode proofs).= Hence an ideal (and impossible)=C2=A0=C2=A0
proof assistant woul= d be a program where I can input a type=C2=A0=C2=A0
expression an= d the system will return either a term (member) of=C2=A0=C2=A0
th= is type or will tell me that this type has no members.

=
New type expressions are usually built from some previously known=C2= =A0=C2=A0
ones. Since one does not want to write all definitions = from point=C2=A0=C2=A0
zero there should be a library of existing= types where one can get=C2=A0=C2=A0
building blocks for the type= expression which forms the query.

Hence the memor= y=C2=A0 - to contain all questions which have been asked=C2=A0=C2=A0
<= div>previously (type expressions) and all answers which have been found=C2= =A0=C2=A0
(terms). This memory or at least some parts of it shoul= d be shared=C2=A0=C2=A0
(using some kind of web sharing paradigm)= =C2=A0 so that if someone=C2=A0=C2=A0
places a query or find an a= nswer to a query everybody else has=C2=A0=C2=A0
access to it.

Right now I am thinking about the structure of such a= memory. I=C2=A0=C2=A0
feel this has to be done at least on conce= ptual level before=C2=A0=C2=A0
everything else. My feeling is tha= t it might get pretty large and=C2=A0=C2=A0
that it is crucial to= organize it in a way which makes using it=C2=A0=C2=A0
*fast* for= the computer so in particular I am thinking about an=C2=A0=C2=A0
essentially binary format (not expressions themselves but a=C2=A0=C2=A0
structure formed by already parsed expressions connected by=C2=A0= =C2=A0
references to each other). I also feel that it is Ok if it= contains=C2=A0=C2=A0
a lot of repeats and redundancy (e.g. a tho= usand slightly different=C2=A0=C2=A0
definition of what a group i= s) since it is not to be directly=C2=A0=C2=A0
accessed by humans = and since it is not a problem for a computer to=C2=A0=C2=A0
compa= re to each other a thousand arrays of length thousand.

=
That's where I am now. I have just started this memory thing and I= =C2=A0=C2=A0
hope to get a better feel for it in a week or two.

Volodia.

-----------------= ------------------------------------------------------------

------=_Part_12630_1502917587.1507735583187-- ------=_Part_12629_1725708205.1507735583186--