MATH0980 : contenu algorithmique des démonstrations mathématiques

Ce wiki est un complément pour le cours du Master deuxième année intitulé "contenu algorithmique des démonstrations mathématiques". Le cours est donné par Karim Nour et Pierre Hyvernat à l'université Claude Bernard, à Lyon...

Nous encourageons tous les étudiants à y participer en l'augmentant au fur et à mesure de l'avancement du cours.

Pour pouvoir modifier les pages, inscrivez-vous pour obtenir un login et mot de passe. (S'il vous plaît, utilisez votre vrai nom...)

Allez regarder ici pour vous familiariser avec les wikis.

Vous pouvez également utiliser la page de discussion pour ... discuter (ou poser des questions).

Exercice : créez-vous un compte et essayez de modifier cette page (correction de fôtes d'aurtograffe, rajout de détails, mise en page, ...)

Details techniques / administratifs

Nouvelles

Les nouvelles importantes pour le cours (les plus récentes en haut).

Rq : pour mettre la date dans le wiki, il suffit de mettre "~~~~~".

• 20 février 2008 à 18:38 (CET) : je viens de voir que la seance de demain n'est pas dans le planning provisoire... J'espère qu'il y aura des gens. (Normalement oui, vu que je l'ai bien précisé la semaine dernière...
• 15 février 2008 à 10:15 (CET) : 4ème séance (Hyvernat) : théorème de Church-Rosser, applications, premiere definition du typage simple
• 8 février 2008 : 3ème seance (Hyvernat) : le lambda-calcul pur, definitions de base
• 23 janvier 2008 à 09:23 (CET) : le cours a disparu, mais il revient ! Nous commencerons donc avec une semaine de retard...
• 4 janvier 2008 à 14:16 (CET) : création du wiki.

Plan (provisoire) du cours

Comme nous commençons avec une semaine de retard, il faudra ajuster ce plan : soit en décalant les seances, soit en rattrapant les deux heures du 17 janvier en rallongeant d'autres séances...

• Séance 1 : 17 janvier (KN) Présentation du cours ; déduction naturelle et traduction de Gödel.

• Séance 2 : 24 janvier (KN) Sémantiques pour les logiques classiques et intuitionniste.

• Séance 3 : 31 janvier (KN) Calcul des séquents et élimination des coupures.

• Séance 4 : 7 février (PH) Introduction au lambda-calcul : Church-Rosser.

• Séance 5 : 14 février (PH) Représentation des fonctions récursives.

• Séance 6 : 28 février (PH) Lambda-calcul typé : préservation de type et forte normalisation.

• Séance 7 : 6 mars (PH) Fonctions représentables en lambda-calcul typé.

• Séance 8 : 13 mars (KN et/ou PH) Contrôle.

• Séance 9 : 20 mars (KN) Lambda-mu-calcul : Church-Rosser et préservation de type.

• Séance 10 : 27 mars (KN) Plusieurs preuves de forte normalisation du lambda-mu-calcul typé.

• Séance 11 : 3 avril (KN) Entiers classiques et mise en mémoire.

• Séance 12 : 10 avril (PH) Sémantique du lambda-calcul (1).

• Séance 13 : 17 avril (PH) Sémantique du lambda-calcul (2).

• Séance 14 : 24 avril (KN et/ ou PH) Examen final.

Support de TD

• TD 1
• TD 2

Quelques références

• logique générale : "Introduction à la Logique Théorie de la démonstration" de René David, Karim Nour et Christophe Raffalli ; édité par Dunod. (Voir ici pour plus de détails...)

• lambda-calcul : "Lambda-calcul, types et modèles" de Jean-Louis Krivine ; édité par Masson (1990). Cet ouvrage est epuisé, mais il y en a deux exemplaires à la bibliothèque de mathématiques. JL Krivine a également mis la version anglaise de son livre sur sa page web

• le livre "Proofs and Types" de Jean-Yves Girard, Yves Lafont et Paul Taylor. Ce livre est épuisé mais est disponible sur la page d'Yves Lafont

• un cours de lambda-calcul donné par C. Berline, avec des notes de cours. cours de lambda-calcul

• pour un éclairage très différent du même sujet (contenu calculatoire de la logique classique), vous pouvez lire les notes de Thierry Coquand.

---

---

Contenu algorithmique des démonstrations mathématiques

Introduction

-- à compléter --

Le $\lambda$-calcul...

Introduction, historique

Le $\lambda$-calcul est à l'origine une notation prenant les notions de fonctions et d'application comme primitives. Historiquement, on peut le voir comme issu des notations utilisées dans "Principia Mathematica" de Whitehead et Russel (1910-13) où la notation était "${\widehat {x}}(\phi x)$" (un exemple). Plus tard, dans les années 30, Church a transformé cette notation en "${\widehat {\ }}x(\phi x)$", puis "$\lambda x(\phi x)\!$". (À verifier...)

Cette notation est similaire à (mais beaucoup plus pratique que) la notation mathématique habituelle "$x\mapsto \sin(x+\pi /2)$" représentant "la fonction qui, à $x$ associe $\sin(x+\pi /2)$".

Définitions

Reportez-vous au livre de Krivine pour une approche entièrement formelle...

Termes

On se donne un ensemble infini dénombrable ${\mathcal {V}}$ de variables. En général, on les notes $x$, $y'$, $z_{42}$, $f$...

Les expressions du $\lambda$-calcul, appelée "$\lambda$-termes, sont obtenue grace aux rêgles suivantes

• si $x$ est une variable, alors $x$ est un $\lambda$-terme (variable)
• si $x$ est une variable et si $u$ est un $\lambda$-terme, alors $\lambda x.u$ est un $\lambda$-terme (abstraction)
• si $u$ et $v$ sont des $\lambda$-termes, alors $(u)v$ est un $\lambda$-terme (application)

Attention : en mathématique, l'application d'une fonction est notée $f(u)\!$, alors qu'elle est notée "$(f)u\!$" en $\lambda$-calcul !

On note $(u)\,v_{1}\,v_{2}\,...\,v_{n}$ pour $(...(((u)\,v_{1})\,v_{2})\,...)\,v_{n}$ et $\lambda xyz.t\!$ pour $\lambda x.\lambda y.\lambda z.t\!$.

définition de "sous-terme"

Les variables libres d'un terme sont définie par récurrence sur le terme :

• ${\mathcal {L}}(x)=\{x\}$
• ${\mathcal {L}}(\lambda x.u)={\mathcal {L}}(u)\setminus \{x\}$
• ${\mathcal {L}}{\big (}(u)v{\big )}={\mathcal {L}}{\big (}u{\big )}\cup {\mathcal {L}}{\big (}v{\big )}$

$\alpha$-équivalence

En notant $u\langle x:=y\rangle$ pour le terme dans lequel la variable $x$ est remplacée par la variable $y$, on définit

• $x\equiv y\!$ ssi $x=y\!$
• $(u)v\equiv (u')v'\!$ ssi $u\equiv u'\!$ et $v\equiv v'\!$
• $\lambda x.u\equiv \lambda x'.u'\!$ ssi $u\langle x:=y\rangle \equiv u'\langle x':=y\rangle$ pour toutes les variables $y$ n'apparaissant ni dans $u$ ni dans $u'$.

Cette relation est appelée "$\alpha$-équivalence.

C'est une relation d'equivalence, et on considerera toujours les termes à cette équivalence prêt.

rq : on peut toujours se ramener à des termes où aucune variable libre n'est liée dans un sous-terme.

substitution et $\beta$-réduction

La substitution est définit comme suit :

• $x[x:=t]=u$ et $y[x:=t]=y$ si $x\neq y$
• $(u)v[x:=t]=(u[x:=t])v[x:=t]$
• $\lambda y.u[x:=t]=\lambda y.u[x:=t]$ à condition que $y$ ne soit pas libre dans $t$

Si la condition dans le cas de l'abstraction n'est pas vérifiée, on renome la variable $y$ en une variable qui n'apparait n'est pas libre dans $t$.

La $\beta$-réduction est la relation suivante appliquée pour n'importe quel sous-terme

$(\lambda x.u)\,t\quad \to \quad u[x:=t]$

C'est aussi une rêgle de réecriture...

On note $\to ^{+}\!$, $\to ^{*}\!$ et $\approx _{\beta }\!$ pour les clotures transitive, reflexives et transitives et reflexive, transitive et symmétrique de la relation $\to \!$.

exemples

...

Le théorème de Church-Rosser

Théorème (Church-Rosser)

$\to _{\beta }^{*}$ est confluente : si$u\to _{\beta }^{*}v_{1}$ et $u\to _{\beta }^{*}v_{2}$ alors $v_{1}\to _{\beta }^{*}t$ et $v_{1}\to _{\beta }^{*}t$ pour un terme $t$

On utilise la preuve classique de Tait et Martin-Löf avec la réduction parallèle.

...

Le lambda-calcul simplement typé

une premiere definition du typage