MATH0980 : contenu algorithmique des démonstrations mathématiques - Historique des versions

Hyvernat : /* Nouvelles */

2008-02-20T17:38:31Z

Nouvelles

← Version précédente		Version du 20 février 2008 à 17:38
Ligne 23 :		Ligne 23 :
	'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".		'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".

			* 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''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''théorème de Church-Rosser, applications, premiere definition du typage simple''		* 15 février 2008 à 10:15 (CET) : '''4ème séance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''théorème de Church-Rosser, applications, premiere definition du typage simple''
	* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''le lambda-calcul pur, definitions de base''		* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''le lambda-calcul pur, definitions de base''

Hyvernat : /* Le théorème de Church-Rosser */

2008-02-15T09:28:34Z

Le théorème de Church-Rosser

← Version précédente		Version du 15 février 2008 à 09:28
Ligne 170 :		Ligne 170 :

	===Le théorème de Church-Rosser===		===Le théorème de Church-Rosser===

			;Théorème (Church-Rosser):
			<math>\to_\beta^</math> est confluente : si<math>u\to_\beta^ v_1</math> et <math>u\to_\beta^* v_2</math> alors <math>v_1\to_\beta^* t</math> et <math>v_1\to_\beta^* t</math> pour un terme <math>t</math>

			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

Hyvernat : /* Plan (provisoire) du cours */

2008-02-15T09:22:36Z

Plan (provisoire) du cours

← Version précédente		Version du 15 février 2008 à 09:22
Ligne 61 :		Ligne 61 :
	* Séance 14 : 24 avril (KN et/ ou PH) ''Examen final.''		* Séance 14 : 24 avril (KN et/ ou PH) ''Examen final.''


			==Support de TD==

			* [http://www.lama.univ-savoie.fr/~hyvernat/Enseignement/0708/math980/td1.pdf TD 1]
			* [http://www.lama.univ-savoie.fr/~hyvernat/Enseignement/0708/math980/td2.pdf TD 2]

	==Quelques références==		==Quelques références==

Hyvernat : /* Nouvelles */

2008-02-15T09:15:06Z

Nouvelles

← Version précédente		Version du 15 février 2008 à 09:15
Ligne 23 :		Ligne 23 :
	'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".		'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".

			* 15 février 2008 à 10:15 (CET) : '''4ème séance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''théorème de Church-Rosser, applications, premiere definition du typage simple''
	* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''le lambda-calcul pur, definitions de base''		* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|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...		* 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.		* 4 janvier 2008 à 14:16 (CET) : création du wiki.


	==Plan (provisoire) du cours==		==Plan (provisoire) du cours==

Hyvernat : /* Details techniques / administratifs */

2008-02-13T15:43:43Z

Details techniques / administratifs

← Version précédente		Version du 13 février 2008 à 15:43
Ligne 22 :		Ligne 22 :

	'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".		'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".


	* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''le lambda-calcul pur, definitions de base''		* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|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...		* 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.		* 4 janvier 2008 à 14:16 (CET) : création du wiki.


	==Plan (provisoire) du cours==		==Plan (provisoire) du cours==
Ligne 60 :		Ligne 60 :

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

	==Contenu des séances==

	===Séance 1===

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

Hyvernat : /* Nouvelles */

2008-02-13T15:40:34Z

Nouvelles

← Version précédente		Version du 13 février 2008 à 15:40
Ligne 21 :		Ligne 21 :
	Les nouvelles importantes pour le cours (les plus récentes en haut).		Les nouvelles importantes pour le cours (les plus récentes en haut).

	'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~</nowiki></tt>".		'''Rq''' : pour mettre la date dans le wiki, il suffit de mettre "<tt><nowiki>~~~~~</nowiki></tt>".


	* [[Utilisateur:Hyvernat\|Hyvernat]] ~~23 janvier 2008 à 09:23 (CET~~) : le ~~cours~~ ~~a disparu~~, ~~mais il revient ! Nous commencerons donc avec une semaine~~ de ~~retard...~~		* 8 février 2008 : '''3ème seance''' ([[Utilisateur:Hyvernat\|Hyvernat]]) : ''le lambda-calcul pur, definitions de base''
	* ~~[[Utilisateur:Hyvernat\|Hyvernat]] 4~~ janvier 2008 à 14:16 (CET) : ~~création~~ du ~~wiki~~.		* 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==		==Plan (provisoire) du cours==

Hyvernat : /* Quelques références */

2008-02-13T13:31:56Z

Quelques références

← Version précédente		Version du 13 février 2008 à 13:31
Ligne 74 :		Ligne 74 :

	* le livre "Proofs and Types" de Jean-Yves Girard, Yves Lafont et Paul Taylor. Ce livre est épuisé mais est disponible sur [http://iml.univ-mrs.fr/~lafont/publications.html la page d'Yves Lafont]		* le livre "Proofs and Types" de Jean-Yves Girard, Yves Lafont et Paul Taylor. Ce livre est épuisé mais est disponible sur [http://iml.univ-mrs.fr/~lafont/publications.html la page d'Yves Lafont]

			* un cours de lambda-calcul donné par C. Berline, avec des notes de cours. [http://www.pps.jussieu.fr/~berline/Cours.html 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 [http://www.cs.chalmers.se/~coquand/cor3.ps notes] de Thierry Coquand.		* pour un éclairage '''très différent''' du même sujet (contenu calculatoire de la logique classique), vous pouvez lire les [http://www.cs.chalmers.se/~coquand/cor3.ps notes] de Thierry Coquand.

Hyvernat : /* Le $\lambda$ -calcul... */

2008-02-04T15:02:07Z

Le <math>\lambda</math>-calcul...

← Version précédente		Version du 4 février 2008 à 15:02
Ligne 91 :		Ligne 91 :

	==Le <math>\lambda</math>-calcul...==		==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===

			...

Hyvernat : /* Contenu algorithmique des démonstrations mathématiques */

2008-02-04T13:38:39Z

Contenu algorithmique des démonstrations mathématiques

← Version précédente		Version du 4 février 2008 à 13:38
Ligne 89 :		Ligne 89 :
	==Déduction naturelle et traduction de Gödel==		==Déduction naturelle et traduction de Gödel==


	===blabla===
			==Le <math>\lambda</math>-calcul...==
	...

Hyvernat : /* Quelques références */

2008-02-04T11:08:20Z

Quelques références

← Version précédente		Version du 4 février 2008 à 11:08
Ligne 73 :		Ligne 73 :
	* 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 [http://www.pps.jussieu.fr/~krivine page web]		* 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 [http://www.pps.jussieu.fr/~krivine 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~~ [http://iml.univ-mrs.fr/~lafont/publications.html ~~ici~~]		* le livre "Proofs and Types" de Jean-Yves Girard, Yves Lafont et Paul Taylor. Ce livre est épuisé mais est disponible sur [http://iml.univ-mrs.fr/~lafont/publications.html 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 [http://www.cs.chalmers.se/~coquand/cor3.ps notes] de Thierry Coquand.		* pour un éclairage '''très différent''' du même sujet (contenu calculatoire de la logique classique), vous pouvez lire les [http://www.cs.chalmers.se/~coquand/cor3.ps notes] de Thierry Coquand.

MATH0980 : contenu algorithmique des démonstrations mathématiques - Historique des versions

Hyvernat : /* Nouvelles */

Hyvernat : /* Le théorème de Church-Rosser */

Hyvernat : /* Plan (provisoire) du cours */

Hyvernat : /* Nouvelles */

Hyvernat : /* Details techniques / administratifs */

Hyvernat : /* Nouvelles */

Hyvernat : /* Quelques références */

Hyvernat : /* Le \lambda-calcul... */

Hyvernat : /* Contenu algorithmique des démonstrations mathématiques */

Hyvernat : /* Quelques références */

Hyvernat : /* Nouvelles */

Hyvernat : /* Le théorème de Church-Rosser */

Hyvernat : /* Plan (provisoire) du cours */

Hyvernat : /* Nouvelles */

Hyvernat : /* Details techniques / administratifs */

Hyvernat : /* Nouvelles */

Hyvernat : /* Quelques références */

Hyvernat : /* Le $\lambda$ -calcul... */

Hyvernat : /* Contenu algorithmique des démonstrations mathématiques */

Hyvernat : /* Quelques références */