TypiCal

Matrices represented by computer programs, also called black-box matrices,
are a popular topic in Computer Algebra. Since the seminal paper
(Wiedemann 86), algorithms to do arithmetic operations on them, as
multiplication, determinant, minimal polynomial, etc., have been intensely
studied and are now well understood.

The status of transposition of black box matrices is much less clear. It
is a (not so well known) theorem in Algebraic Complexity that black-box
matrices given by (non-uniform) arithmetic circuits can be transposed
without changing the complexity of the circuit. In the more familiar
Turing model, this translates to a principle, often known as
"transposition principle" or "Tellegen's principle" in the Computer
Algebra community, that gives a "recipe" to "transpose" an algorithm
"without changing its complexity".

In this talk I will give a formal proof of the transposition principle in
the touring model and sketch the implementation of a compiler that
transposes algorithms written in our ad-hoc algebraic language
Transalpyne. (Maybe not so) Surprisingly, we discovered some connections
with Type Systems and Categoty Theory while attacking this problem: I will
try to explain these connections and point out some possible research
directions.

Je parlerai de quelques aspects du travail mené dans l'équipe Parsifal, et de la façon dont cela pourrait s'articuler avec Coq.

Dans une première partie je présenterai les logiques avec points fixes (définitions inductives et coinductives) que nous utilisons, en comparant un peu avec le calcul des constructions inductives. Cela me permettra d'introduire certains fragments et des stratégies de recherche de preuve, en discutant de la pertinence de leur adaptation à Coq.

Dans une seconde partie, je traiterai de la notion plus délicate de quantification générique (nabla). Cette notion apporte une expressivité très intéressante à nos logiques, puisqu'elle permet de spécificier naturellement des systèmes tels que le lambda ou le pi-calcul, mais son "adaptation" à Coq semble difficile; j'évoquerai cependant des pistes.

Le thème central de cet exposé prend ces racines dans une question philosophique : quelle est la signification des constants logiques ? Ou encore, et avec plus d’ambition : y a-t-il un critère pour identifier les ‘bonnes’ constants logiques ?

Une réponse possible à ces questions peut être trouvée dans la maxime wittgensteinienne selon laquelle ‘la signification est l’usage (dans le langage)’ ; en l’appliquant au cas des constants logiques cela conduit à l’idée que leur signification est donnée par leurs règles d’inférence (position inférentialiste). Mais, ainsi formulée, cette idée est encore trop naïve, comme cela a été montré par A. Prior, grâce au connecteur pathologique tonk. Ce connecteur est défini par des règles d’inférence apparemment légitimes, mais qui, ajoutées à celles des connecteurs logiques standards, amène à l’inconsistance du système. Une manière d’éviter des connecteurs pathologiques de ce type est d'exiger la propriété de l’élimination des coupures. Toutefois, rajouter cette propriété à notre cahier des charges pour l’identification des bonnes constants logiques nous dit seulement comment éviter certaines constants pathologiques, mais elle n’explique pas la cause de la pathologie. C’est seulement en passant par une traduction de tonk dans une système d’inférence modulo certaines règles de réécriture (i.e. dans la déduction modulo) que cette explication devient possible.

Enfin, à l’aide de cette approche via règles de réécriture, j’essayerai de montrer comme même l’élimination des coupures n’est pas une condition suffisante pour l’identification des bonnes constants logiques. Ce type d’investigation me permettra aussi de regarder de plus près certaines conditions imposées sur le système de réécriture utilisés en déduction modulo (notamment la propriété de non-confusion des connecteurs).

We consider the problem of automating and checking the use of previously proved lemmas in the proof of some main theorem. In particular, we call the collection of such previously proved results a table and use a partial order on the table's entries to denote the (provability) dependency relationship between tabled items. We incorporate tables into sequent calculus proofs by performing two steps. First, cuts are used to incorporate tabled items into a proof: one premise of the cut requires a proof of the lemma and the other premise has the lemma inserted into the set of assumptions. Second, to ensure that lemmas are not reproved, we exploit the non-canonicity of focusing systems and specify two specific focusing disciplines for tabled formulas.

1. We allow only atomic formulas in tables. Then, by exploiting the fact that, in focusing systems, atoms can be assigned positive or negative polarity, we impose the following polarity discipline: atoms that are in the table are given positive polarity and those not in the table are given negative polarity.
2. We restrict tabled formulas to fixed point literals, that is, fixed points and their negations, and universally quantified fixed point literals, denoting both finite successes and finite failures. Then, by exploiting the fact that fixed points can be frozen and be treated like atoms, we impose a second focusing discipline: fixed points that are instances of a tabled formula are frozen and those that are not instances of a tabled formula are not frozen.

10:00 - 11:00 Tjark Weber: Integrating SAT and SMT in Isabelle/HOL (slides)
11:00 - 11:30 BREAK
11:30 - 12:30 Michael Armand: Integrating SAT in Coq (slides)
12:30 - 13:00 discussions

14:00 - 15:00 Sascha Boehme: Integrating SMT in Isabelle/HOL (slides)
15:00 - 15:30 BREAK
15:30 - 16:30 Pascal Fontaine: The veriT solver
16:30 - ... discussions

L'interaction entre assistants de preuves peut permettre d'utiliser des théorèmes "aisément" prouvés dans un assistant de preuve donné, dans un autre assistant de preuve dans lequel ils auraient été plus difficiles à prouver. Cependant, les systèmes de preuves peuvent parfois être très différents.

Dans cet exposé, je présenterai une méthode pour importer des preuves de HOL-Light en Coq, basée sur la réflection. Après avoir présenté HOL-Light rapidement, j'expliquerai comment d'une part construire un modèle de HOL-Light en Coq prouvé correct, d'autre part enregistrer et exporter les termes de preuve de HOL-Light.

We give a new elegant proof that decreasing diagrams imply conflu-
ence based on a proof reduction technique, which is then the basis of a novel
completion method which proof-reduction relation transforms arbitrary proofs
into rewrite proofs even in presence of non-terminating reductions. Unlike pre-
vious methods, no ordering of the set of terms is required, but can be used if
available. Unlike ordered completion, rewrite proofs are closed under
instantiation. Examples are presented, including Kleene’s and Huet’s classical examples
showing that non-terminating local-confluent relations may not be confluent.

Joint work with Vincent van Oostrom (cf. ICALP 09)

In this talk, we will propose generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom.

Intervenant : Barbara Petit (ENS Lyon)

Date et lieu : 11/06/09, salle de conférence du Lix

Résumé : Le lamba-calcul avec constructeurs, de Arbiser, Miquel et Rios est une extension du lambda calcul avec un mecanisme de filtrage. Le filtrage "a la ML" y est decomposé en deux opérations elementaires: une analyse de cas sur des constantes, et une regle de commutation -surprenante au premier abord- entre le case et l'application.
Apres avoir presenté ce calcul, je lui definirai un systeme de types polymorphe avec unions et intersections. Enfin je montrerai un modele de realisabilite (proche candidats de reductibilites de Girard) pour ce systeme, et les proprietes de normalisation forte et de sureté vis a vis du filtrage qui en decoulent.

Liens : http://perso.ens-lyon.fr/barbara.petit/recherche.php

Intervenant: D. Pous

Date et lieu: Jeudi 23 avril 2009, 14h00-16h00, salle de conférence du LIX

Résumé: Formaliser des choses dans un assistant de preuve s'avère souvent pénible, de nombreuses étapes de raisonnement devant être explicitées alors qu'elles sont d'habitude laissées au relecteur scrupuleux. Ceci est en particulier vrai lorsque l'on doit travailler sur des relations binaires (réécriture, réductions, équivalences, etc...), très intuitives, mais pas complètement triviales.

Lorsque c'est possible, une première astuce consiste à considérer les relations de façon algébrique : en montant le niveau d'abstraction, on facilite la formalisation de certaines preuves. Une fois ce pas franchi, on réalise que les relations binaires sont un modèle des algèbres de Kleene, décidables par la théorie des automates finis.

Nous exposerons un travail en cours, sur une formalisation Coq des automates - via des matrices, afin d'obtenir une tactique de décision des algèbres de Kleene, par réflection. Plus généralement, nous exposerons les outils que nous développons pour raisonner sur ce genre de structures algébriques.

Intervenant: Alexandre Miquel (ENS Lyon)

Date et lieu: 16/04/2009, 14h Salle de conférence du Lix

Résumé: Mon deuxième exposé (qui fera suite à l'exposé du matin) sera consacré à l'extraction classique dans le cadre de l'assistant à la preuve Coq. Dans un premier temps, je montrerai comment la théorie de la réalisabilité classique de Krivine - définie à l'origine pour l'arithmétique classique du second ordre - peut être étendue au calcul des constructions inductives (pICC) avec tiers-exclu. Ensuite je présenterai le schéma d'extraction classique étendu à pICC ainsi que les diverses optimisations mises en oeuvre dans le module d'extraction classique (notamment en ce qui concerne la représentation des entiers). Enfin, je terminerai mon exposé par quelques exemples de programmes extraits à partir de preuves classiques, sous la forme d'une démo.

Liens: Les transparents de l'exposé.

Intervenant: Alejandro Díaz-Caro (LIG)

Date et lieu: 04/05, 14h, salle de réunion du préfabriqué du Lix

Résumé: The Linear-Algebraic Lambda-Calculus (arXiv:quant-ph/0612199) is a higher-order lambda-calculus together with the possibility to make linear combinations of terms. Terms can be seen as forming a vectorial space. However, dealing with concepts such as orthogonality and unitarity is not trivial. The scalar type system (arXiv:0903.3741) is a System F-like type system with scalars in the types. It can be seen as a first step towards a vectorial type system, with which to reason about orthogonality and unitarity. The additive type system is a type system with sums of types on it, which can be seen as a subset of the intuitionistic-multiplicative-exponential linear logic (IMELL). Finally, the vectorial type system puts scalar and additive together, making a vectorial space of types. In this seminar we will present these three type systems and some clues as to whether the last one enables us to check for orthogonality.

Liens: Les transparents de l'exposé.