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

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

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 "Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle (f)u\!} " en Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \lambda} -calcul !

On note Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle (u)\,v_1\,v_2\,...\,v_n} pour $(...(((u)\,v_{1})\,v_{2})\,...)\,v_{n}$ et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \lambda xyz.t\!} pour Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \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 :

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \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 )}$

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \alpha} -équivalence

En notant Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u\langle x:=y\rangle} pour le terme dans lequel la variable Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle x} est remplacée par la variable $y$ , on définit

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle x\equiv y\!} ssi Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle x=y\!}
Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle (u)v\equiv (u')v'\!} ssi Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u\equiv u'\!} et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle v\equiv v'\!}
Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \lambda x.u \equiv \lambda x'.u'\!} ssi Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u\langle x:=y\rangle\equiv u'\langle x':=y\rangle} pour toutes les variables Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle y} n'apparaissant ni dans Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u} ni dans Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u'} .

Cette relation est appelée "Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \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 Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \beta} -réduction

La substitution est définit comme suit :

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle x[x:=t] = u} et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle y[x:=t] = y} si Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle x\neq y}
Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle (u)v[x:=t] = (u[x:=t])v[x:=t]}
Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \lambda y.u[x:=t] = \lambda y.u[x:=t]} à condition que Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle y} ne soit pas libre dans Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle t}

Si la condition dans le cas de l'abstraction n'est pas vérifiée, on renome la variable Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle y} en une variable qui n'apparait n'est pas libre dans Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle t} .

La Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \beta} -réduction est la relation suivante appliquée pour n'importe quel sous-terme

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle (\lambda x.u)\,t\quad\to\quad u[x:=t]}

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

On note Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \to^+\!} , Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \to^*\!} et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \approx_\beta\!} pour les clotures transitive, reflexives et transitives et reflexive, transitive et symmétrique de la relation Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \to\!} .

exemples

...

Le théorème de Church-Rosser

Théorème (Church-Rosser)

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \to_\beta^*} est confluente : siÉchec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u\to_\beta^* v_1} et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle u\to_\beta^* v_2} alors Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle v_1\to_\beta^* t} et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle v_1\to_\beta^* t} pour un terme Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle 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

MATH0980 : contenu algorithmique des démonstrations mathématiques

Sommaire

Details techniques / administratifs

Nouvelles

Plan (provisoire) du cours

Support de TD

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

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \alpha} -équivalence

substitution et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \beta} -réduction

exemples

Le théorème de Church-Rosser

Le lambda-calcul simplement typé

Menu de navigation

MATH0980 : contenu algorithmique des démonstrations mathématiques

Details techniques / administratifs

Nouvelles

Plan (provisoire) du cours

Support de TD

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

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \alpha} -équivalence

substitution et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \beta} -réduction

exemples

Le théorème de Church-Rosser

Le lambda-calcul simplement typé

Menu de navigation

Rechercher

Le $\lambda$ -calcul...

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \alpha} -équivalence

substitution et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \beta} -réduction