Detailed Content
Initiation au Lambda-Calcul
Le Lambda-Calcul est a été introduit par Alonzo Church. L'objectif initial était l'étude des fondements des mathématiques. En d'autres termes, Church tentait de répondre à la question : "quel est le système formel minimal qui permet de générer toutes les mathématiques ?". Ce modèle s'est avéré très utile pour la spécification des langages de programmation fonctionnels.
L'étude du Lambda-Calcul est présentée pour permettre :
- Une meilleure compréhension des langages de programmation fonctionnels,
- L'utilisation de cette notation pour prouver des programmes écrits dans un langage fonctionnel.
Dans ce chapitre, nous allons voir :
- Présentation des Systèmes Formels,
- Présentation de la logique du premier ordre comme un Système Formel,
- Le Lambda-Calcul :
- L'historique du modèle,
- La notation Lambda et son utilité,
- Lambda-réduction
- La logique combinatoire
- La calculabilité en Lambda-Calcul
- La programmation en Lambda-Calcul
- Le Lambda-Calcul simplement typé :
- Le langage des types
- Système de Curry
- La réduction dans le Lambda-Calcul typé.
- Exemple de langage de programmation fonctionnel : LISP
Logique classique et Intuitionniste
Dans ce chapitre, nous allons reprendre la notion de la logique classique pour la comparer à une autre logique non-classique qui est la logique intuitionniste (ou constructive). L'objectif est d'étudier en particulier la correspondance de Curry-Howard, non pas dans ses bases purement logiques, mais dans un contexte lié aux langages de programmation fonctionnels. C'est à dire, comment pouvons nous obtenior des systèmes de preuve et des langages de programmation à partir du Lambda-Calcul.
Dans cette partie, nous allons voir :
- Logique constructive
- Déduction naturelle
- Systèmes de type polymorphe
- Représentation des structures des données
Sémantique formelle
La sémantique formelle des langages désigne l'étude de la signification d'un programme. Contrairement au syntaxe du programme, la sémantique définit ce que fait le programme. Généralement, la signification, dans ce cas, est définie par des objets mathématiques. Dans ce chapitre, nous allons découvrir cette notion en suivant le plan :
- Définition de la sémantique formelle,
- Objectif et utilité de la sémantique formelle,
- Types de la sémantique formelle :
- Sémantique opérationnelle
- Sémantique dénotationnelle
- Sémantique axiomatique
Expression formelle de sémantiques.
L'implémentation de la sémantique formelle permet d'obtenir à la fois un système de preuve et un système de génération automatique du compilateur. En effet, avoir l'implémentation d'une sémantique formelle est l'équivalent d'avoir un système d'exécution d'un programme écrit dans le langage décrit.
Pour voir du pré cette importance, nous allons voir dans ce chapitre les éléments suivants :
- Exemple d'une sémantique formelle et son application
- Le langage exemple L1
- La sémantique opérationnelle du langage L1
- Preuve des programmes en L1
- Introduction au langage ML
- Introduction au langage Coq