DEA 01/02        

DEA  20/11/01

Résumé: cours du 20/11/01


cours précédent ........ cours suivant..........tous les cours    
Contenu du cours: Sémantiques.
Logique minimale, correspondance de Curry-Howard. Sémantique ensembliste.
Exercices.
  • De quel énoncé $lam xym.mxy$ est-il la preuve?
  • Donner une preuve de $(A =>B =>C) => B => (B=>A)=>C$.
  • Donner une preuve de $((A =>B)=>B =>C) => B =>C$. Y a-t-il unicité?
  • Trouver un énoncé qui a deux preuves (normales) distinctes.
  • Trouver un énoncé qui a une infinité de preuves (normales) deux à deux distinctes.
  • Donner un lambda terme pur pour $succ$. Votre terme est-il typable?
  • Donner un type simple qu'on pourrait appeler type des arbres binaires de Church (à coefficients entiers).
  • Donner trois signatures permettant de représenter les entiers.
  • Donner une signature permettant de représenter les rationnels.


    cours précédent ........ cours suivant..........tous les cours    
       
    Andre.HIRSCHOWITZ
    Last modified:  Nov 8