dependent type theory in simplicial sets and begun thinking about writing his own
proof assistant.
-----------------------------------------------------------------------------
From: Vladimir Voevodsky <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 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.
-----------------------------------------------------------------------------