I   Les types de base

1. Booléens. Les constantes booléennes sont modélisées de la façon suivante:

   vrai = λ x . λ y . x

   faux = λ x . λ y . y

   Définir dans ce modèle les relations et (et logique), ou (ou logique) et non (non logique), puis imp (⇒) et equiv (⇔).
   
   
   
2. Entiers. Modéliser la fonction succ (successeur) sur les entiers naturels de Church:
   

   0 = λ f . λ x . x

   1 = λ f . λ x . (f   x)

   · · ·

   n = λ f . λ x .(f   (f   ...   (f   n   ×   x)   ... ))

   Définir l'addition, la multiplication et la puissance sur ces entiers.

II   Les autres types

1. n-uplets.
   1. Modéliser la fonction tuple3 qui crée un triplet et les fonctions index1, index2 et index3 qui en renvoient les composantes.
      
      
   2. Modéliser la curryfication pour les fonctions à 3 arguments.
   
   
2. Listes (récursivité).
   
   On modélise les constructeurs de listes cons et nil (liste vide) de la manière suivante:

   cons = λ h . λ t . λ c . (c   h   t)

   nil = λ x . vrai

   
   
   1. Modéliser la fonction long qui donne la longueur d'une liste quelconque.
   2. Modéliser la fonction somme qui calcule la somme des valeurs
      d'une liste d'entiers de Church.

This document was translated from L^AT_EX by H^EV^EA.