25 Juin 2018

"Faire et défaire c'est toujours travailler" - Gilles Dowek

Version 2.6 de Dedukti

La release sur OPAM a été effectuée. Gilles: Pourquoi garder lampdapi et Dedukti ?

• Problèmes de performances de lambdapi Tant que lambdapi ne type-checke pas les mêmes choses que Dedukti et à peu près à la même vitesse, on ne passe pas à lambdapi Problèmes à garder deux systèmes
• Duplication du travail
• Risque de perdre tout le code lambdapi et les développements associés (variable d'unification) quand Rodolphe part.
  • Les membres capables de potentiellement reprendre le développement : Franck, Bruno, Frédéric Autre problèmes on a plusieurs branches parallèles (polarized, sizechange, acu, universo, réécriture conditionnelle, etc) qui n'ont toujours pas été mergées. Gilles: en septembre ces branches devraient être mergées (au moins les plus petites).

Github

Quels outils de l'équipe sont sur Github ? Lesquelles font l'objet d'une intégration continue ?

• Zenon est encore sur la forge, les fichiers générés sont sur le site de l'équipe. Ils mettent 1h à être vérifiés. Le lien est sur la page de Dedukti.
• Focalize : c'est pas notre problème, c'est le projet d'une autre équipe. Trop de systèmes ("des milliers", -Gilles) génèrent du Dedukti, on ne peut pas s'occuper de tous.
• iProverModulo est sur le compte de Guillaume -> à déplacer sur le repo de l'équipe. Le lien est sur la page de Dedukti. Quelques petites corrections à effectuer (dans les Makefile, etc).
• Holide, Matita, Coqine, etc génèrent des fichiers typecheckable par Dedukti mais pas d'intégration continue mise en place. Les bibliothèques générées pas ces fichiers sont stockés quelque part et sont type checkés de temps en temps manuellement par Dedukti.

-> Modifier la page de l'équipe pour afficher l'adresse OPAM de Dedukti.

Dedukti polarisé

Syntaxe proposée pour les règles polairsée: -->+, -->- Implémentation encourageante, passe plusieurs exemples écrit à la main.

• TODO: Faire passer la branch au benchmarking. Développement dans Dedukti exclusivement, pas dans le lambdapi. Développement rapide, possibilité de faire le même -> Voir si c'est mergeable avec ACU.

Réécriture conditionnelle: demander à Bruno et Raphaël un exemple (minimal) qui utilise la réécriture conditionnelle pour justifier l'ajout de la feature à Dedukti (et constituer un premier test de la feature).

Point Logipedia

-> Possibilité de faire directement référence (via lien URL) à des théorèmes sur Logipedia sans les télécharger. On fait confiance à Logipedia pour la correction de la preuve. Dépendances indirectes constituent en fait un contexte dans lequel:

• Notre théorème a le type Prop.
• Il existe une preuve (pas forcément fournie) habitant le théorème. -> Nécessité de vérifier que le contexte utilisé dans la définition du théorème (et sa preuve) est compatible avec le contexte actuel (la théorie dans laquelle on travaille).

Attention, le problème d'alignement des concepts est trop compliqué dans un premier temps. Potentiellement assez dur pour faire l'objet d'une thèse en soi: On ne peut importer le théorème de Fermat sur les entiers unaires que dans une signature qui implémente les entiers unaires.

Objectif à court terme:

• Possibilité de télécharger un format "court" (via un bouton "download bis") qui contient tout les théorèmes prouvés mais sans les termes de preuve. Il faut donc faire confiance à Logipedia.
• Minimiser les dépendances d'une preuve en terme de symboles et règles de réécriture. Essayer de ne pas importer un "fichier" dépendant mais simplement les éléments qui sont nécessaires à la preuve.
• Vérifier que les dépendances sont "vérifiées" à l'import. C'est à dire que les symboles et les règles de réécriture requis par la preuve sont déjà dans la signature.

Syntaxe Dedukti

Parmi les objectifs du projet lambdapi: avoir un Dedukti interactif. Nécessité d'augmenter la syntaxe avec les commandes qui seront nécessaires à l'interactivités:

• Ajouter les règles polarisée : -->+ et -->-
• Annotation de symboles: retirer def et ajouter const
• Avoir un let dans la syntaxe qui serait du sucre syntaxique pour un beta-redex. (cf Bruno, peut-être qu'il y a une subtilité au niveau du typage des let).
• #REQUIRE
• Possibilité d'ajouter Sukerujo dans Dedukti
• Possibilité d'avoir des symboles infixes
• Notation (x : A) -> B (pour x : A -> B) deux positions:
  • Rodolphe: hack dans le parser, pas naturel. Si on veut cette notation alors on la rend standard et on force son utilisation partout
  • Guillaume et François: très utile, très naturel, coûte rien à implémenter (3 lignes de parser).

Note: Coq a trois langages: Terms, Tactic, Vernacular Dedukti était à la base censé être un langage généré fait pour des ordinateurs. Maintenant on tend vers une utilisation ou le code est de plus en plus écrit manuellement (théories, exemples, etc) -> Nécessité d'avoir une syntaxe plus expressive et plus lisible.

Minimalité: Le type-checker (kernel) doit rester petit ! Mais si on développe un langage de tactiques, c'est pas un problème d'avoir un parser très riche. Est-ce que le parser ne pourrait pas être considéré comme un générateur de Dedukti ?

Dedukti a le droit de grandir (un peu) avec le temps mais ne doit surtout pas exploser.

Symboles injectifs

• Dans lambdapi, si un symbole (même définissable) n'a aucune règle, alors il est injectif (et on utilise cette propriété dans le typage des règles). Problème: rien ne garantit que le symbole va rester injectif:
• Dans Dedukti on interdit Frédéric: c'est un bon sujet pour l'année prochaine
• Soit on s'assure qu'un symbole dont l'injectivité a été utilisée le reste dans la suite du code
• Soit on permet de déclarer un symbole comme injectif et on a le droit d'utiliser les propriétés.

### Sujet du sens de SUCCESS dans Dedukti. Consensus approximatif: si Dedukti réponds SUCCESS, alors il existe un arbre de dérivation du dernier jugement de typage du fichier.

• Nécessité de prouver la correction de l'algo de typage/reduction de Dedukti.
• A-t-on besoin de subject reduction (et donc de confluence) ?
• A-t-on besoin de la terminaison d'un système ? Il semblerait que non. Si le système est non terminant, alors il pourrait boucler mais il ne répondra pas SUCCESS à un jugement de typage non dérivable.