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

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

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

Correction 1  

1.

bool.

2.

int -> int list, + est de type int->int->int, donc x est de type int, x+1 est de type int. :: est de type 'a * 'a list -> 'a list, en l'appliquant à x+1, on instancie le paramètre 'a par int d'ou le résultat.

3.

int -> (int -> bool) -> 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 isInf a b qui teste si l'entier a de type nat est inférieur à l'entier b de type nat.

2.

Écrire un prédicat recursif isImpaire a qui teste si l'entier a de type nat est Impaire.

3.

Réécrire isImpaire 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 isInf  x y = match (x,y) with
    (_,O)->false
    |(O,_)->true
    |((S x),(S y))->isInf x y;;

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

let isImpair = nat_it (fun x->not x) false;;

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

Correction 3  

let rec inverse l = match l with 
 []->[]
 |x::xs->(inverse xs)@[x];;

Preuve de correction:
On considère le prédicat:''Si y est à la place i dans l, il est à la place (longueur l)-i+1 dans (inverse l)''.

• Vrai pour []
• On suppose que cela est vrai pour q et que y est à la place i dans x::q. On a alors : inv x::q = (inv q)@[x], donc,
  • si y=x, y passe de la place 1 à la place (longueur l)-1+1 = (longueur l).
  • sinon y est à la place i-1 dans q donc par HI, à la place (longueur q)-(i-1)+1=(longueur q)+1-i+1=(longueur l)-i+1 dans inv q donc aussi dans (inv q)@[x]=inv x::q.

Exercice 4 (Récursion terminale)   Écrire de façon récursive terminale, la fonction qui calcule de nombre d'occurences d'un élément e dans une liste.

Correction 4  

let nocc e l = 
   let rec aux l acc = match l with
       []->acc
       |x::xs->if e=x then (aux xs (acc+1)) else (aux xs acc)
  in aux l 0;;

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 : (7+x)*(8+y)

2.

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

3.

Définir une valuation (i.e une fonction associant des valeurs à des variables) de façon que l'évaluation de : (7+x)*(8+y) donne 240.

Correction 5  

Mult ((Plus((Int 7),(Var "x"))),Plus((Int 8),(Var "y")));;
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''->3
 |"y''->16
;;
eval (Mult ((Plus((Int 7),(Var "x"))),Plus((Int 8),(Var "y")))) valuation;;