Résumé :
|
Ce livre présente deux paradigmes de calcul sous l'angle de la logique. La réduction, étudiée à travers le lambda-calcul et les systèmes de réécriture, est à la base de la programmation fonctionnelle, où la notion de type et les propriétés de confluence et de terminaison sont primordiales. La résolution s'illustre en programmation logique où ce sont la validité, la complétude, voire l'équité du calcul, qui importent. Les systèmes d'inférence et les méthodes sémantiques de la logique sont présentées et appliquées à l'étude de ces propriétés, et à des problèmes d'effectivité. Deux langages de programmation récents, l'un fonctionnel, CAML, et l'autre logique, NU-Prolog, sont utilisés tout au long de cet ouvrage pour illustrer la mise en oeuvre de ces principes. Chaque chapitre est suivi d'exercices, dont certains sont résolus.
|