Version du 4 février 2008 à 15:02

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

Hyvernat 23 janvier 2008 à 09:23 (CET) : le cours a disparu, mais il revient ! Nous commencerons donc avec une semaine de retard...
Hyvernat 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.

Contenu des séances

Séance 1

-- à compléter au fur et à mesure --

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

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

Déduction naturelle et traduction de Gödel

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

...

@@ Ligne 91 : / Ligne 91 : @@
 ==Le <math>\lambda</math>-calcul...==
+===Introduction, historique===
+Le <math>\lambda</math>-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 "<math>\widehat x(\phi x)</math>" ([http://quod.lib.umich.edu/cgi/t/text/pageviewer-idx?c=umhistmath&cc=umhistmath&idno=aat3201.0001.001&frm=frameset&view=image&seq=46 un exemple]). Plus tard, dans les années 30, Church a transformé cette notation en "<math>\widehat{\ }x(\phi x)</math>", puis "<math>\lambda x(\phi x)\!</math>". (À verifier...)
+Cette notation est similaire à (mais beaucoup plus pratique que) la notation mathématique habituelle "<math>x\mapsto\sin(x+\pi/2)</math>" représentant "la fonction qui, à <math>x</math> associe <math>\sin(x+\pi/2)</math>".
+===Définitions===
+Reportez-vous au livre de Krivine pour une approche entièrement formelle...
+====Termes====
+On se donne un ensemble infini dénombrable <math>\mathcal{V}</math> de ''variables''. En général, on les notes <math>x</math>, <math>y'</math>, <math>z_{42}</math>, <math>f</math>...
+Les expressions du <math>\lambda</math>-calcul, appelée "<math>\lambda</math>-termes, sont obtenue grace aux rêgles suivantes
+* si <math>x</math> est une variable, alors <math>x</math> est un <math>\lambda</math>-terme (''variable'')
+* si <math>x</math> est une variable et si <math>u</math> est un <math>\lambda</math>-terme, alors <math>\lambda x.u</math> est un <math>\lambda</math>-terme (''abstraction'')
+* si <math>u</math> et <math>v</math> sont des <math>\lambda</math>-termes, alors <math>(u)v</math> est un <math>\lambda</math>-terme (''application'')
+'''Attention :''' en mathématique, l'application d'une fonction est notée <math>f(u)\!</math>, alors qu'elle est notée "<math>(f)u\!</math>" en <math>\lambda</math>-calcul !
+On note <math>(u)\,v_1\,v_2\,...\,v_n</math> pour <math>(...(((u)\,v_1)\,v_2)\,...)\,v_n</math> et <math>\lambda xyz.t\!</math> pour <math>\lambda x.\lambda y.\lambda z.t\!</math>.
+ définition de "sous-terme"
+Les ''variables libres'' d'un terme sont définie par récurrence sur le terme :
+* <math>\mathcal{L}(x) = \{x\}</math>
+* <math>\mathcal{L}(\lambda x.u) = \mathcal{L}(u) \setminus\{x\}</math>
+* <math>\mathcal{L}\big((u)v\big) = \mathcal{L}\big(u\big) \cup \mathcal{L}\big(v\big)</math>
+====<math>\alpha</math>-équivalence====
+En notant <math>u\langle x:=y\rangle</math> pour le terme dans lequel la variable <math>x</math> est remplacée par la variable <math>y</math>, on définit
+* <math> x\equiv y\!</math> ssi <math>x=y\!</math>
+* <math> (u)v\equiv (u')v'\!</math> ssi <math> u\equiv u'\!</math> et <math> v\equiv v'\!</math>
+* <math>\lambda x.u \equiv \lambda x'.u'\!</math> ssi <math> u\langle x:=y\rangle\equiv u'\langle x':=y\rangle</math> pour toutes les variables <math>y</math> n'apparaissant ni dans <math>u</math> ni dans <math>u'</math>.
+Cette relation est appelée "<math>\alpha</math>-é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 <math>\beta</math>-réduction====
+La substitution est définit comme suit :
+* <math>x[x:=t] = u</math> et <math>y[x:=t] = y</math> si <math>x\neq y</math>
+* <math>(u)v[x:=t] = (u[x:=t])v[x:=t]</math>
+* <math>\lambda y.u[x:=t] = \lambda y.u[x:=t]</math> '''à condition que <math>y</math> ne soit pas libre dans <math>t</math>'''
+Si la condition dans le cas de l'abstraction n'est pas vérifiée, on renome la variable <math>y</math> en une variable qui n'apparait n'est pas libre dans <math>t</math>.
+La <math>\beta</math>-réduction est la relation suivante appliquée pour n'importe quel sous-terme
+ <math>(\lambda x.u)\,t\quad\to\quad u[x:=t]</math>
+C'est aussi une rêgle de réecriture...
+On note <math>\to^+\!</math>, <math>\to^*\!</math> et <math>\approx_\beta\!</math> pour les clotures ''transitive'', ''reflexives et transitives'' et ''reflexive, transitive et symmétrique'' de la relation <math>\to\!</math>.
+====exemples====
+ ...
+===Le théorème de Church-Rosser===
+ ...

« MATH0980 : contenu algorithmique des démonstrations mathématiques » : différence entre les versions

Version du 4 février 2008 à 15:02

Sommaire

Details techniques / administratifs

Nouvelles

Plan (provisoire) du cours

Contenu des séances

Séance 1

Quelques références

Contenu algorithmique des démonstrations mathématiques

Introduction

Déduction naturelle et traduction de Gödel

Le $\lambda$ -calcul...

Introduction, historique

Définitions

Termes

$\alpha$ -équivalence

substitution et $\beta$ -réduction

exemples

Le théorème de Church-Rosser

Menu de navigation

« MATH0980 : contenu algorithmique des démonstrations mathématiques » : différence entre les versions

Version du 4 février 2008 à 15:02

Details techniques / administratifs

Nouvelles

Plan (provisoire) du cours

Contenu des séances

Séance 1

Quelques références

Contenu algorithmique des démonstrations mathématiques

Introduction

Déduction naturelle et traduction de Gödel

Le λ {\displaystyle \lambda } -calcul...

Introduction, historique

Définitions

Termes

α {\displaystyle \alpha } -équivalence

substitution et β {\displaystyle \beta } -réduction

exemples

Le théorème de Church-Rosser

Menu de navigation

Rechercher

« MATH0980 : contenu algorithmique des démonstrations mathématiques » : différence entre les versions

Le $\lambda$ -calcul...

$\alpha$ -équivalence

substitution et $\beta$ -réduction