CRADT20100202

Compte-rendu de la journée ADT égalité et terminaison du 2 février 2010 à La Ciotat

Voir la page ADT pour les transparents des exposés.

Participants: Andreas Abel, Assia Mahboubi, Benjamin Grégoire, Cody Roux, Cyril Cohen, Frédéric Blanqui, Hugo Herbelin, Jorge Luis Sacchini, Medhi Dogguy, Pierre Corbineau, Pierre Letouzey, Pierre-Yves Strub, Stéphane Glondu, Tom Hutchinson, Vincent Gross, Vincent Siles, Yves Bertot.

---

Pierre-Yves Strub (CoqMT)

L'exposé a été annulé. CoqMT est téléchargeable depuis la page de Pierre-Yves.

---

Pierre Corbineau (intégrer l'axiome K de Streicher dans le CIC)

Hugo asks if we can replace the reduction rule κ for K by an equality axiom stating say, that "JMeq_eq refl = refl"? Would that also imply say, that "K H = H" for H:P(refl) and corresponding axioms for eq_rect_eq, UIP, etc. in the same way as we can prove that JMeq_eq, K, UIP and eq_rect_eq are equivalent.

---

Bruno Barras (reminder of current termination checking algorithm)

The current algorithm accept cbv-looping terms. Is this acceptable?

Efficiency problem because of on-demand delta-reduction (e.g. with "Fixpoint F x := id (id (id F)) (pred x)")

Efficiency problem because of eager reduction of variable size (e.g. with "Fixpoint F x := if long-computation then F (pred x)") (even if there is a workaround by first defining F' abstracted over the long-computation).

Wrong optimizations:

• a term containing no subterm variable cannot be a subterm: wrong because of empty types
• no need to propagate size info for non-recursive types: wrong because option types (e.g.) can have recursive types as arguments

Benjamin asks why not first check the guard w/o reduction and try reduction only if it fails?

Bruno says that it would increase the number of cases with inefficient checks. He suggests instead to have lazy evaluation of sizes (but it needs more works in the implementation).

Yves asks if it would be possible, following a remark of Thorsten Altenkirch, if it where possible to mix inductivity and coinductivity in the same definition. Andreas says that some further work has to be done.

---

Jorge Luis Sacchini (type based termination dans Coq) (jointly with Benjamin Gregoire)

CIC^ ("CIC sombrero") satisfies confluent reduction, subject reduction. It has a decidable type-checking (assuming strong normalization) that is sound and complete (in some sense).

No normalization result.

No way currently to type append with type list(s) -> list(r) -> list(s+r). It is only possible to type it of type list(s) -> list(r) -> list(∞).

Subtle discussion between Jorge, Cody, Frédéric and Benjamin.

---

Andreas Abel (integration of type based termination with implicit quantification and proof irrelevance)

About "irrelevance": Andreas proposes a definition that does not restrict to Prop: T is irrelevant if forall t, t' in T, t=t'. For instance, unit, and eq are irrelevant.

About eta-expansion: more power but probably slower to deal with.

Eta-expansion for function types can be done by adding some ↑ and ↓ operators to the reduction mechanism.

Eta-expansion applicable also to inductive families which have only one inhabitant in each component.

In the more general sense, we then have that the forall, imp, and, unit, eq, bot fragment (w/o atoms) is irrelevant.

Awodey and Bauer have another approach based on "bracket" type.

Miquel has irrelevance using implicit product.

Andreas present examples with implicit product in MiniAgda.

Andreas suggests to use the implicit product of the implicit calculus to represent the sizes of types and to base termination on them.

Talk ends with a "let us add eta to Coq".

---

Discussion

Benjamin pense qu'il est préférable d'étendre l'algorithme de filtrage dépendant plutôt que d'implanter ce qui est dans l'article « A new elimination rule for CIC ». Concernant K, il est convenu que Pierre Corbineau passait à l'implantation de sa règle de typage modifiée. C'est redondant avec la proof-irrelevance au niveau de l'expressivité logique mais pas au niveau de l'expressivité calculatoire (sans compter que la modification en jeu est élégante).

Pour éta, les types flèches et records peuvent être gérés au niveau de la conversion sans utiliser les opérateurs ↑ et ↓ mais a priori pas les types vides et singletons (unit, identity, empty) posent problème sans ↑ et ↓ ces types ne sont pas réversibles (ce sont des 0 et 1 de la logique linéaire, pas des ⊥ et ⊤). À suivre.

Pas de discussion et pas de conclusion sur la terminaison par les types. Le statut de ces extensions reste ouvert.

Benjamin pose la question du statut du proto avec calcul implicite.