Interrogation N^o 1 : Jeudi 16 décembre, (second sujet)

Exercice 1 (typage)   Quel est le type des expressions suivantes (expliquer rapidement pourquoi) :

3.0+.3.05;;
fun x ->(x=3)::[];;
let f g x = (g (x+2)) or true;;

Correction 1  

• float
• int -> bool list , car = est de type 'a -> 'a -> bool, en lui passant un argument entier, on instancie le paramètre a par int donc x doit être de type int et x=3 de type bool. :: est de type 'a * 'a list -> 'a list, en l'appliquant à x=3, on instancie le paramètre 'a par bool d'ou le résultat.
• (int -> bool) -> int -> bool car comme en 2, x doit être de type int, (x+2) doit être de type int, et comme or est de type bool -> bool -> bool, (g (x+2)) doit etre de type bool, donc g est de type int ->bool.

Exercice 2 (Récursion)   On donne le type des entiers naturels :

type nat = O | S of nat;;

1.

Écrire le prédicat isSup a b qui teste si l'entier a de type nat est supérieur à l'entier b de type nat.

2.

Écrire prédicat recursif isPaire a qui teste si l'entier a de type nat est paire.

3.

Réécrire isPaire a en une ligne en utilisant l'itérateur nat_it.

let rec nat_it f b n = match n with 
        O -> b
       |S x ->f (nat_it f b x);;

Correction 2  

let rec isSup x y = match (x,y) with
    (O,_)->false
    |(_,O)->true
    |((S a),(S b))->isSup a b;;
ou 
let rec isSup x y = match x with
    O->false
    |S a->match y with 
         O->true
        |S b->isSup x y;;

let rec isPair n = match n with 
       O->true
      |S x->not (isPair x);;

let isPair = nat_it (fun x->not x) true;;

Exercice 3 (Preuve de correction)   Écrire de façcon récursive profonde la fonction supprime s l qui supprime un élément s d'une liste l. Faire la preuve de correction de fonction écrite.

Correction 3  

let rec supprime s l= match l with 
 []->[]
 |x::xs -> if (x=s) then (supprime s xs) else x::(supprime s xs);;

Preuve de correction:
On considère le prédicat:''(supprime s l) a les mêmes éléments que l moins s, et ils sont dans le même ordre'' .

• Vrai pour []
• On suppose que cela est vrai pour q et on considere y::q
  • si y=s,(supprime s y::q) = (supprime s q) et donc vérifie le prédicat.
  • sinon (supprime s y::q) = y::(supprime s q). (supprime s q) a les mêmes éléments que q moins s, et ils sont dans le même ordre, et comme ys, y::(supprime s q) a les mêmes éléments que y::q moins s, et ils sont dans le même ordre.

Exercice 4 (Recursion terminale)   Écrire de façon récursive terminale, la fonction qui inverse les éléments d'une liste l.

Correction 4  

let inverse l = 
 let rec aux l acc = match l with
      []->acc
      |x::xs->aux xs x::acc
in aux l [];;

Exercice 5   On donne le type suivant représentant des expressions algèbriques:

type exp = Var of string |Int of int| Plus of exp*exp |Mult of exp*exp;;

1.

Définir l'expression représentant : x+(4*(y+6))

2.

Définir une fonction d'évaluation de ces expressions arithmétiques.

3.

Définir une valuation (i.e une fonction associant des valeura à des variables) de façon que l'évaluation de : x+(4*(y+6)) donne 56.

Correction 5  

 Plus((Var "x"),(Mult((Int 4),Plus((Var "y"),(Int 6)))));;

let rec eval e env = match e with 
 Var x -> env x
 |Int x->x
 |Plus (x,y)->(eval x env)+(eval y env)
 |Mult (x,y)->(eval x env)*(eval y env);; 

let valuation  x = match x with
 "x"->16
 |"y"->4
;;

eval (Plus((Var "x"),(Mult((Int 4),Plus((Var "y"),(Int 6)))))) valuation;;