Organisation

Le cours de TL1 contient 11 cours, 10 TD  et un TP/projet noté. Sauf semaine exceptionnelle, il y a un cours et un TD/TP par semaine. Le contenu des cours est décrit ci-dessous avec des liens vers les supports de cours.

Des quizzs rapides (5-10 min), à passer entre le cours et le TD, vous permettent de valider votre compréhension du cours. Ils sont disponibles pendant 15 jours après le cours dans l'outil Exercices de Chamilo (lien en bas de cette page).

Les exercices traités en TDs sont pris du recueil de TD qui vous a été distribué à la première séance.

Pour faciliter vos révisions, des annales d'examen couvrant les trois dernières années sont disponibles dans le répertoire Documents/Annales du cours.

 

Notions abordées

Partie Automates et langages

Partie Grammaires

  • Cours 8 : Grammaire et hiérarchie de Chomsky
  • Cours 9 : Grammaire hors-contexte : Propriété de décomposition, Ambiguité. principe de preuve sur les grammaires
  • Cours 10 : Modélisation et Expressivité : Description des LP, grammaire étendues, Hiérarchie de chomsky : inclusion et lemme de la pompte pour les HC
  • Cours 11 : Langages et décidabilité. Modélisation par automate : Résultat de décidabilité, algorithmes de reconnaissance, Application des automates à la vérification

 

Contenu des TD

Les exercices traités en TDs sont pris du recueil de TD. Les exercices et questions marqués [À savoir faire] ou [Avancé] ne sont en général pas traités en séances. Ils vous servent à déterminer où vous en êtes dans votre apprentissage.
Voici les exercices qui sertont traités à chaque séance, la partie entre parenthèse est optionnelle :

  • TD 1 : exercices 1, 2, 3, (4, 8)
  • TD 2 : exercices 6, 7, 11, 12, 13, (16, 17, 19)   (le 13 sera repris au TP)
  • TD 3 : exercices 20, 21, 24, (22, 25, 26)
  • TD 4 : exercices 28, 29, 35, (33, 34, 36)
  • TP 5 : sujet et fichiers source à récupérer dans Documents/TP/Sujet Python
  • TD 6 : exercices 38, 39, 40, 41, (42, 45, 46)
  • TD 7 : exercices 49, 50, 51, 52, (46) (lemme de l'étoile et fermeture)
  • TD 8 : exercices 55, 56, 57 (grammaires)
  • TD 9 : exercices 61, 62 (hors-contexte)
  • TD 10 : exercices 60, 63
  • TD 11 : exercice 58, 59 + exercices précédents non terminés sur grammaires / propriétés de fermeture

La correction de ces exercices est disponible dans le recueil corrigé.

TP / projet

Il est à faire soit en binôme soit en monôme. Dans les deux cas, vous devez créer une équipe dans le projet Teide créé pour l'occasion, voir https://teide.ensimag.fr/ (VPN nécessaire si vous êtes hors de l'Ensimag). La date limite de création d'une équipe est le jeud 07/11/24 à 23h59.

Le rendu de votre projet se fera sur Teide, au plus tard le 8/12/23 à 23h59. Il devra y avoir un rendu par équipe, qui comptera pour tous les membres de l'équipe.

Sujet Python

Votre rendu ne devra contenir que le fichier tp.py (récupéré lors du TP) complété.
Pour information :
- les questions 0, 1, 3, 4 ne sont pas évaluées, elles sont là pour vous guider ;
- les questions 9, 13 et 16 sont à rédiger mais ne sont pas evaluées dans le projet, en revanche elles peuvent faire l'objet d'une question à l'examen ;
- les questions 2, 5, 6, 7, 8, 10, 11, 12, 14, 15 sont à réaliser dans le fichier tp.py.

Les questions à rédiger nécessitent des parties du cours que vous allez voir dans les semaines à venir (CM7 pour la question 13, CM9 pour les question 9 et 16) mais le reste peut être fait dès maintenant.

 

Sujet Coq

Le sujet Coq nécessite deux choses : d'une part, un apprentissage en autonomie de l'assistant de preuves Coq;  d'autre part, la formalisation et la preuve d'une partie du cours de TL1 en Coq.

Pour l'installation de l'assisant de preuves Coq, allez voir sur son site web.

La première partie est basée sur le volume 1 de la série de livres Software Foundations et toute autre ressource que vous pourrez trouver en ligne. Vous aurez besoin d'avoir vu le chapitre IndPrinciples et toutes ses dépendances (9 chapitres au total).

Pour la partie de formalisation, le début (correspondant à une partie des deux premiers CM) est commun mais dans la suite, vous avez trois possibilités, qui viennent chacune avec un fichier de départ différent :

  • la construction de l'automate produit et une preuve de correction et complétude sur une grammaires (exercices 20 et 62 du recueil de TD),
  • l'élimination des ε-transitions dans un automate,
  • la déterminisation d’un automate sans ε-transition.

Si cela vous intéresse, vous pouvez également réaliser plus d'une de ces parties, en partant du fichier de départ complet. Les fichiers de départ se trouvent dans le répertoire Documents/TP/Sujet Coq.

Votre rendu devra contenir un unique fichier Coq complété et commenté. Vous devez compléter les définitions et énoncés manquants (indiqués par « TODO » ) ainsi que réaliser des preuves (indiquées par « Preuve à compléter »). Un fichier entièrement complété ne doit plus contenir de TODO ni de preuve admise.

Afin d'éviter des problèmes d'inclusion entre fichiers, une partie importante du fichier de départ contient des résultats et preuves préliminaires, et la partie à compléter commence à la ligne 625.
En cas de besoin, il sera possble d'organiser des séances de permanence dédiées à ce sujet de projet.

Quelques conseils :

  • Ce projet est long (il vous faut apprendre tout un langage !), n'attendez pas le dernier moment pour vous y mettre.
  • Les preuves sont de difficultés inégales, vous pouvez en sauter une provisoirement et y revenir plus tard.
  • Il est vivement conseillé d'avoir la preuve détaillée sur papier avant de se lancer dans une preuve en Coq.
DocumentsDocuments
ExercicesExercices