Univalent Foundations Program - important update.

[Vladimir Voevodsky]

Dear All,

it is only now that we have fully realized that the plan for the next year program at the IAS as it is stated in the web description:

We plan to have four main working groups oriented towards the goals described below. However applications from people with interest in other aspects of mathematics and computer science related to the univalent semantics of type theories will also be considered.

For general information on Univalent Foundations and Homotopy Type Theory see Homotopy Type Theory website and Vladimir Voevodsky’s homepage .

In connection with the activities of Group 1 there will probably be a series of presentations based on the "Univalent Foundations" library as it will be by that time.

For all other purposes we plan to have a weekly seminar where each of the groups will be given, on average, one spot per month.

Group 1. Practical formalization of set-level mathematics in Coq based on the univalent approach.

Goals: developing skills for collective work on libraries of formalized mathematics, locating the points of "tension" between constructive and non-constructive approaches especially in the formalization of analysis, creating libraries for future use.

Group 2. Computational issues in constructive type theory related to the univalence axiom.

Goals: looking for approaches to the proof of the "main computational conjecture" of the univalent approach with a special focus on looking for practical algorithms for automatic construction of fully constructive terms from terms build with the help of extensionality axioms.

Group 3. Formalization of advanced homotopy-theoretic structures in constructive type theory.

Goals: looking for approaches to formalize higher coherence structures (simplicial types, H-types, n-1-categories and n-1-functors etc.). Looking for possible syntax and computation rules for higher inductive definitions. Looking for the constructions of elements in homotopy groups of spheres as mappings between the corresponding loop "functors".

Group 4. Relation of constructive type theory to set-theoretic foundations.

Goals: formalizations of type theories and known constructions of their models in ZFC and related theories. Looking for new models of constructive type theories, especially for non-standard models of the univalence axiom.

must be changed.

We reason as follows. The ultimate goal of the univalent program is to make formalized and computer verified proofs a standard in pure and eventually in applied mathematics. A necessary intermediate goal is to have a proof assistant based on a type system which is compatible with the univalent model and implements resizing rules.  

Because of this fact we decided put as Group 1 a group which will start working on a type system and a proof assistant with required properties. 

It is a very serious change but we feel strongly that it is necessary. 

The further discussion related to this issue will be only posted to HOTT ( homotopyt...@googlegroups.com ) so please subscribe to it if you would like to follow the discussion and/or participate in the project itself. 

Steve Awodey, Thierry Coquand and Vladimir Voevodsky (organizers of the Univalent Foundations program).

[Michael Shulman]

On Wed, May 30, 2012 at 5:36 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> A necessary intermediate goal is to have a proof
> assistant based on a type system which is compatible with the univalent
> model and implements resizing rules.
>
> Because of this fact we decided put as Group 1 a group which will start
> working on a type system and a proof assistant with required properties.

I have been wondering whether it would it be possible to design a
"generic" proof assistant which is not tied to one particular type
system, but rather could be configured with different "modules" for
different type theories as the user chooses? That way we would not
have to decide once and for all what "the best" type system to use is;
we could leave future mathematicians the option to augment or modify
the type system without needing to start over with a new proof
assistant.

According to my very limited knowledge, it seems that the proof
assistant Isabelle is an attempt to create something of this sort,
although in practice it seems to be mostly used with its "HOL"
library. The underlying level of Isabelle seems to be a
Logical-Framework-style type theory in which one can formulate the
derivation rules for the judgments of whatever object language one
wants to study. It even seems that someone has implemented at least a
rudimentary version of an extensional dependent type theory this way
(Isabelle/CTT).

Undoubtedly there are good reasons why Isabelle itself is not usable
as a proof assistant for HoTT (assuming someone were to write an
intensional DTT library). I'd be interested in hearing what they are.
In particular, are they fundamental to the idea of a "generic proof
assistant", or could they be remedied in a new project?

Mike

[Andrej Bauer]

> I have been wondering whether it would it be possible to design a
> "generic" proof assistant which is not tied to one particular type
> system, but rather could be configured with different "modules" for
> different type theories as the user chooses?

You are not the only one thinking about this.

There are at least two problems as I see them.

(1) If users are allowed to specify arbitrary conversion rules, that
may destroy normalization properties. This in itself is not
catastrophic, it just means the proof assistant might diverge or
become unable to type check things that are type checkable. However,
if it finds a proof, the proof is ok.

(2) If the system is very flexible, then it is hard(er) to do fancy
things, such as type inference, automated equational reasoning, etc.
The cure here would be, I think, to provide very good tactics language
with a lot of reflection properties.

Because different people might end up using different axioms and
conversion rules, they won't all agree on which proofs are actually
valid. But we would still have a correctness guarantee. If I get
Mike's proofs which he did in his version of the system, and my system
checks the proofs, then they _are_ proofs. Even if they fall from the
moon or are sent to me as part of a Nigerian e-mail scam, they are
still proofs, as long as my system is happy with them.

We should think very seriously about having such a system. Then it
would be possible to experiment with various universe axioms, etc.

With kind regards,

Andrej

[Noam Zeilberger]

On Thu, Jun 7, 2012 at 11:48 PM, Michael Shulman <virit...@gmail.com> wrote:
> I have been wondering whether it would it be possible to design a
> "generic" proof assistant which is not tied to one particular type
> system, but rather could be configured with different "modules" for
> different type theories as the user chooses?  That way we would not
> have to decide once and for all what "the best" type system to use is;
> we could leave future mathematicians the option to augment or modify
> the type system without needing to start over with a new proof
> assistant.

I think this is closely related to the question of what do you need in
a general-purpose programming language in order to be able to embed
different domain-specific languages with as little possible overhead.
For example, rather than having to write a full interpreter for an
inductively-defined syntax, ideally one could define a DSL by
describing a few extra features to be added to the host language, and
programs of the DSL would be able to freely call routines of the host
language without incurring significant extra costs.

A paper I like about this topic is

Embedded Probabilistic Programming
Oleg Kiselyov and Chung-chieh Shan
http://www.cs.rutgers.edu/~ccshan/rational/dsl-paper.pdf

where they show how to do just that for the case of a probabilistic
DSL embedded into OCaml, applying some general techniques. (I've been
spending some time trying to understand what these techniques mean,
and working out more examples in Agda...)

Noam

[Robert Harper]

this sort of thing has long been envisioned, but never realized in practice. as someone mentioned, isabelle is largely an implementation of hol, despite it's generic foundations. for many years the gothenburg people were developing ALF as the foundation for type theory; it's an equational logical framework (unlike lf) in which one can encode the rules of various forms of type theory. (this is described in the nordstrom et al type theory book, now available for free on the web.) agda has pretty much overtaken this work, afaict, but is not at all generic with respect to the underlying type theory. lf and twelf have been very successful in supporting generic manipulations of formal systems, but they are very much based on a formal encoding, rather than a semantic embedding, into a kernel type theory. we've used these tools for decades for dozens, if not hundreds, of formalisms. but what it is pretty much not suitable for is using these encodings as the foundation for a serious proof development environment for an encoded logic. a piece of this puzzle is how to support computation on proofs (tactics and such), the subject of the beluga and delphin projects, and much of dan licata's phd (and work with noam zeilberger on focusing).

i don't mean to be excessively pessimistic, but i think it's wise to avoid being excessively optimistic about such things! it seems to be much harder than it sounds.

bob

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To post to this group, send email to HomotopyT...@googlegroups.com.
> To unsubscribe from this group, send email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/HomotopyTypeTheory?hl=en.
>

[Guillaume Yziquel]

Le Thursday 07 Jun 2012 à 14:48:54 (-0700), Michael Shulman a écrit :
> On Wed, May 30, 2012 at 5:36 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> > A necessary intermediate goal is to have a proof
> > assistant based on a type system which is compatible with the univalent
> > model and implements resizing rules.
> >
> > Because of this fact we decided put as Group 1 a group which will start
> > working on a type system and a proof assistant with required properties.
>
> I have been wondering whether it would it be possible to design a
> "generic" proof assistant which is not tied to one particular type
> system, but rather could be configured with different "modules" for
> different type theories as the user chooses? That way we would not
> have to decide once and for all what "the best" type system to use is;
> we could leave future mathematicians the option to augment or modify
> the type system without needing to start over with a new proof
> assistant.

You raise a very good point about generic proof assistants. I simply
wish to point out that there's another issue worth worrying about:
generic framework for type systems for compilers of functional-like
languages. Currently, there's no generic framework to hook into a
compiler to provide a modular development style for type systems.

If people wish to work out generic proof assistants, they should keep in
mind that it would be very nice to be able to hook it into a compiler
framework for functional languages. Which brings another issue: You not
only want a generic framework for type systems, you also want generic
framework for lambda-calculi and other weirder calculi to support object
systems or whatever.

Would be sad to see a generic proof assistant with unwieldly integration
into compilers. It would very nice to keep in mind the concept of a
whole compiler stack. Which makes me a bit skeptical about LF in
Isabelle as it currently stands.

To be somewhat more precise, I'm a bit warry of type systems that come
in the form of an application that bundles various IO functionalities
that make assumptions on the file extensions or layout, that bundles the
type system with a syntax expressing it, that bundles the type system
with the calculus that it types, etc... It's not only type systems, but
a proof assistant that makes these kind of assumptions may be useful for
mathematicians but is a pain to reuse properly in a custom compiler and
hardly comes close to making it easier to write custom compilers with
custom type systems, which kind of remains a one-time effort.

A generic proof assistant, yes, but it really needs to be a library and
a modular one. Ideally, this would typically mean being able to refine,
say, STLC into ML and ML into ML^F without code duplication, and
abstracting the concrete representation of the underlying calculus which
should also be progressively refinable to target various backends,
architectures or extensions of the calculus. To date, however cute Beluga
seems to be, it doesn't fit these goals in my opinion.

--
Guillaume Yziquel

[Robert Harper]

Guillaume's suggestion is inspiring, but I must say that it's also one of the oldest unsolved problems in CS, the UNCOL problem. Wikipedia summarizes the history and intent quite well. Since time immemorial people have envisioned a universal compiler infrastructure that has yet to materialize, despite considerable effort. We had this in mind with TIL, stressing well-defined typed intermediate languages, but being universal is much, much harder than it sounds, it seems.

So, a good goal to keep in mind, but not one I would place on the critical path towards other ends.

Bob

Sent from my iPad

[Frederic Blanqui]

Hello.

In proof assistants, there is in general a clear separation between the
kernel of the system, the proof checker (hopefully sound, complete and
decidable), and its interface, all the (possibly unsound, incomplete,
semi-decidable) tools that allows the user to build a proof that, in the
end, is sent to the proof checker for verification. The interface and
the kernel do not need to use exactly the same language, but the
user-defined type system and theory need to be translatable into the
kernel language.

One possible approach to such an architecture, that can accommodate
different user-defined type systems/theories, is natural deduction or
type theory modulo some congruence on terms and propositions/types
generated by some set of user-defined rewrite rules [1,7,...]
(generalizing usual beta and iota reductions). For instance, considering
first-order logic and natural deduction modulo, by using appropriate
sets of rewrite rules, one can encode higher-order logic [2], Peano
arithmetic [3], Zermelo set theory [4], etc. In lambda-pi modulo (pure
type system with simple and term-dependent types only), one can encode
any functional pure type system including an arbitrary number of
universes [5] (but the case of pure type systems with subtyping has not
been studied yet). The use of type-level rewriting is essential for
these encodings to work.

Mathieu Boespflug developed a type-checker for lambda-pi modulo called
Dedukti [6]. But it is just a type-checker: there is currently no
interface. Some works have been done for translating Coq [8] or
HOL-light proofs [9] into lambda-pi modulo.

Hope this can help,

Frederic.

[1] G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal
of Automated Reasoning, 31, 2003, pp. 33-72.

[2] G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an
intentional first-order expression of higher-order logic, Mathematical
Structures in Computer Science, 11, 2001, pp. 1-25.

[3] G. Dowek and A. Miquel, Cut elimination for Zermelo set theory
(manuscript).

[4] G. Dowek and B. Werner, Arithmetic as a theory modulo, in J. Giesel
(Ed.), Term rewriting and applications, Lecture Notes in Computer
Science 3467, Springer-Verlag, 2005, pp. 423-437.

[5] D. Cousineau and G. Dowek, Embedding Pure Type Systems in the
lambda-Pi-calculus modulo, in S. Ronchi Della Rocca, Typed lambda
calculi and applications, Lecture Notes in Computer Science 4583,
Springer-Verlag, 2007, pp. 102-117.

[6] http://www.lix.polytechnique.fr/dedukti/

[7] F. Blanqui. Definitions by rewriting in the Calculus of
Constructions. Mathematical Structures in Computer Science 15(1), p.
37-92, 2005.

[8] http://www.ensiie.fr/~guillaume.burel/blackandwhite_coqInE.html.en

[9]
http://www.lix.polytechnique.fr/~keller/Documents-recherche/Talks/corias11-10.pdf



Le 08/06/2012 05:48, Michael Shulman a �crit :

[Michael Shulman]

Thanks everyone for the very informative answers, and for indulging my
ignorance and inexperience. I more or less expected to hear what Bob
said, which seems to be basically that very general LF-like frameworks
are (at the present level of technology) *too* general to support the
kind of infrastructure necessary for serious proof development in any
particular system. (Please correct me if that's not an accurate
summary.)

But it still seems reasonable to me to hope that one could design a
serious proof assistant that could handle some class of fairly similar
type systems. This seems to be roughly the sort of thing that
Frederic is envisioning.

Perhaps we could start from the other end, beginning with a particular
type theory (hopefully one implemented by some powerful proof
assistant like Coq or Agda) and asking how that type theory can be
generalized. Vladimir's resizing axioms are an example: if I recall
correctly, he has proposed that an implementation should allow the
user to specify arbitrary resizing axioms (including, of course,
inconsistent ones). More generally, one might envision allowing the
user to specify arbitrary additional typing rules or subtyping rules
--- though perhaps that would fall on the far side of "too general".

A different sort of generalization, which would be very useful for
working with higher inductive types, would be to allow the user to
assert new axiomatic definitional equalities. Of course, as Andrej
says, this could destroy normalization properties.

To what extent would it be possible to add capabilities of this sort
to existing proof assistants? Or to design a proof assistant around a
type system that is extensible in these sorts of limited ways? Would
it be incompatible with important features like tactics and program
extraction?

Mike