Examen — Sujet et Correction

Question 1 — Lambda-calcul et codage de Church [4 pts]

On considere le lambda-calcul non type avec ses deux constructions : l'abstraction (λx. M) et l'application (M N). Le codage de Church encode les entiers naturels et les operations arithmetiques dans ce formalisme.

1.1 Fonction successeur [1 pt]

Donnez le terme du lambda-calcul pour la fonction successeur : une fonction qui, appliquee a un entier de Church ‹n›, retourne ‹n+1›. Montrez qu'elle est correcte en l'appliquant a ‹0› et en montrant que le resultat est bien ‹1›.

1.2 Entiers de Church [1 pt]

Donnez le terme du lambda-calcul pour la constante zero ‹0› et pour ‹1›, puis verifiez que succ ‹0› se reduit bien vers ‹1›.

1.3 Addition de Church [1 pt]

En vous basant sur le mecanisme du codage de Church, donnez le terme du lambda-calcul pour l'addition de deux entiers de Church. Expliquez en une phrase comment cette addition fonctionne.

1.4 Multiplication de Church [1 pt]

Donnez le terme du lambda-calcul pour la multiplication de deux entiers de Church. Expliquez en une phrase pourquoi la multiplication « repose » sur l'addition.

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

Verification avec 0 :
succ 0 = (λn.λf.λx. f (n f x)) 0
       →_β λf.λx. f (0 f x)
Or 0 f x = (λg.λy. y) f x →_β (λy. y) x →_β x
Donc succ 0 →_β λf.λx. f x = 1  ✓

0 = λf.λx. x
1 = λf.λx. f x

Verification :
succ 0 = (λn.λf.λx. f (n f x)) (λf.λx. x)
       →_β λf.λx. f ((λf.λx. x) f x)
       →_β λf.λx. f ((λx. x) x)
       →_β λf.λx. f x = 1  ✓

add = λm.λn.λf.λx. m f (n f x)

Principe : add m n demande a m d'appliquer f m fois
sur le resultat de n qui applique f n fois sur x,
soit m + n applications au total.

mul = λm.λn.λf.λx. m (n f) x

Principe : m est applique non pas a f directement,
mais a la fonction (n f) qui correspond a l'application
de f n fois. Ainsi m applique (n f) m fois, ce qui
donne m × n applications de f.

Question 2 — OCaml : manipulation de listes [5 pts]

On considere les definitions suivantes :

let rec fold_left f acc = function
  | [] -> acc
  | x :: xs -> fold_left f (f acc x) xs

let rec map f = function
  | [] -> []
  | x :: xs -> f x :: map f xs

let rec filter p = function
  | [] -> []
  | x :: xs -> if p x then x :: filter p xs
               else filter p xs

2.1 Types infers [1 pt]

Donnez le type infere de chaque fonction (fold_left, map, filter).

2.2 Longueur avec fold_left [1 pt]

En utilisant uniquement fold_left, implementez longueur : 'a list -> int qui retourne la longueur d'une liste.

2.3 Renverser avec fold_left [1 pt]

En utilisant uniquement fold_left, implementez renverser : 'a list -> 'a list qui retourne la liste inversee. (Indice : penser a la concatenation @.)

2.4 Compter les pairs [1 pt]

Implementez compter_pairs : int list -> int qui compte le nombre d'elements pairs d'une liste, en utilisant List.filter et List.length (ou fold_left).

2.5 Minimum avec fold_left [1 pt]

En utilisant uniquement fold_left, implementez minimum : int list -> int qui retourne le minimum d'une liste d'entiers non vide. On donnera une valeur arbitraire (ex. : 0) si la liste est vide.

fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
map       : ('a -> 'b) -> 'a list -> 'b list
filter    : ('a -> bool) -> 'a list -> 'a list

let longueur lst =
  fold_left (fun acc _ -> acc + 1) 0 lst

let renverser lst =
  fold_left (fun acc x -> x :: acc) [] lst

let compter_pairs lst =
  List.length (List.filter (fun x -> x mod 2 = 0) lst)

(* Alternative avec fold_left : *)
let compter_pairs lst =
  fold_left (fun acc x -> if x mod 2 = 0 then acc + 1 else acc) 0 lst

let minimum lst =
  match lst with
  | [] -> 0
  | x :: xs -> fold_left (fun acc y -> if y < acc then y else acc) x xs

Question 3 — OCaml : types algebriques [4 pts]

On considere le type suivant representant des expressions arithmetiques :

type expr =
  | Cst of float
  | Add of expr * expr
  | Mul of expr * expr

3.1 Expression OCaml [1 pt]

Ecrivez l'expression OCaml qui represente mathematiquement (2 + 3) × 4.

3.2 Evaluation [1 pt]

Implementez eval : expr -> float qui evalue une expression arithmetique.

3.3 Comptage des operateurs [1 pt]

Implementez nb_op : expr -> int qui compte le nombre total d'operateurs (Add et Mul) dans l'expression. Utilisez le pattern matching sur le type expr.

3.4 Comptage des constantes [1 pt]

Implementez nb_variables : expr -> int qui compte le nombre de constantes (feuilles) dans l'expression.

Mul (Add (Cst 2.0, Cst 3.0), Cst 4.0)

let rec eval = function
  | Cst c        -> c
  | Add (e1, e2) -> eval e1 +. eval e2
  | Mul (e1, e2) -> eval e1 *. eval e2

let rec nb_op = function
  | Cst _        -> 0
  | Add (e1, e2) -> 1 + nb_op e1 + nb_op e2
  | Mul (e1, e2) -> 1 + nb_op e1 + nb_op e2

let rec nb_variables = function
  | Cst _        -> 1
  | Add (e1, e2) -> nb_variables e1 + nb_variables e2
  | Mul (e1, e2) -> nb_variables e1 + nb_variables e2

Question 4 — Coq : logique des propositions [4 pts]

Prouvez les theoremes suivants en Coq. Donnez la tactique utilisee a chaque etape.

4.1 Transitivite de l'implication [1 pt]

Lemma imp_trans : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> P -> R.

4.2 Commutativite de la conjunction [1 pt]

Lemma and_comm_simple : forall P Q : Prop,
  P /\ Q -> Q /\ P.

4.3 Association de la disjonction [1 pt]

Lemma or_assoc : forall P Q R : Prop,
  P \/ (Q \/ R) -> (P \/ Q) \/ R.

4.4 Negation de la conjunction [1 pt]

Lemma not_and_or : forall P Q : Prop,
  ~ (P /\ Q) -> ~ P \/ ~ Q.

Lemma imp_trans : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros H1 H2 HP.
  apply H2.
  apply H1.
  exact HP.
Qed.

Lemma and_comm_simple : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros H.
  split.
  - destruct H as [HP HQ]. exact HQ.
  - destruct H as [HP HQ]. exact HP.
Qed.

Lemma or_assoc : forall P Q R : Prop,
  P \/ (Q \/ R) -> (P \/ Q) \/ R.
Proof.
  intro H.
  destruct H as [HP | [HQ | HR]].
  - left. left. exact HP.
  - left. right. exact HQ.
  - right. exact HR.
Qed.

Lemma not_and_or : forall P Q : Prop,
  ~ (P /\ Q) -> ~ P \/ ~ Q.
Proof.
  intros H.
  destruct (classic P) as [HP | HnP].
  - right. intro HQ. apply H. split. exact HP. exact HQ.
  - left. exact HnP.
Qed.

Question 5 — Coq : preuve par induction [3 pts]

Prouvez le theoreme suivant en Coq. Expliquez brievement la structure de la preuve.

Lemma add_comm : forall n m : nat,
  n + m = m + n.

Lemma add_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IH].
  - (* Cas de base : 0 + m = m + 0 *)
    simpl. symmetry. reflexivity.
  - (* Cas inductif : S n' + m = m + S n' *)
    simpl.
    rewrite -> IH.
    reflexivity.
Qed.