65 views

Skip to first unread message

May 30, 2012, 8:36:28 AM5/30/12

to types...@lists.seas.upenn.edu, homotopyt...@googlegroups.com

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).

Jun 7, 2012, 5:48:54 PM6/7/12

to homotopyt...@googlegroups.com

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
> 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.

"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

Jun 8, 2012, 4:12:05 AM6/8/12

to homotopyt...@googlegroups.com

> 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.
> "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?

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

Jun 8, 2012, 12:48:01 PM6/8/12

to homotopyt...@googlegroups.com

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
> 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.

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

Jun 8, 2012, 2:23:58 PM6/8/12

to homotopyt...@googlegroups.com

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.

>

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.

>

Jun 9, 2012, 7:44:30 AM6/9/12

to homotopyt...@googlegroups.com

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
> 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.

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

Jun 9, 2012, 11:26:03 PM6/9/12

to homotopyt...@googlegroups.com

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

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

Jun 10, 2012, 11:49:34 PM6/10/12

to HomotopyT...@googlegroups.com

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 :

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 :

Jun 11, 2012, 6:31:37 PM6/11/12

to homotopyt...@googlegroups.com

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

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu