Session

Exercice IV de juin:
Etant donnée une liste xs d'entiers, soit L une liste d'entiers définie en compréhension comme-suit:
L=[x*x|x <- xs;impair x].
1: Evaluer L sachant que xs=[1;2;4;7;12].
2: Les fonctions impair et carre étant supposées connues, définir cette liste à l'aide de fonctions connues.

1/
L=[1;49]
2/
liste (xs) = appliquer carré (filtrer impair xs)
* écriture utilisant des versions ccurrifiées d'appliquer et de filtrer.

Exercice III de septembre:
La fonction alloc est définie de la manière suivante:
assoc xys x = tete[y|(x',y) <- xys;x'=x].
IIIa: Quel est le résultat de l'évaluation de assoc [(1,2);(3,4);(5,6);(3,11)]3?
IIIb: Préciser clairement la spécification de assoc dans le cas général.
IIIc: Proposer alors une définition récursive de assoc en CAML.

a/
assoc [(1,2);(3,4);(5,6);(3,11)] 3 = tête [4;11] = 4
b/
C'est la tête de la liste des y tel que le couple (x',y) parcourt xys en respectant x'=x.
c/
assoc [] = T inversé
assoc (x',y)::xys x = y si x'=x
assoc (x',y)::xys x = assoc xys x sinon

let rec assoc = function
[] -> failwith "erreur"
|(x',y)::xys -> if x=x' then y
else assoc x xys;;

Exercice VI de Septembre :
VIa: Rappeler les définitions par filtrage de renverser et de @.
VIb: Montrer par induction que, pour toutes les listes finies xs et ys:
renverser (xs@ys)= renverser ys@renverser xs.

rappel: généralise le raisonnement par récurrence:
- cas initial (n=0)
- cas général : passage de n à n+1
ici: - cas initial : []
- cas général : passage d'une liste donnée (L) à x::L

a/ renverser [] = [] (1)
renverser (x::xs) = (renverser (xs))@[x] (2)

@ [] L = L (1)
@ x::xs L = x::(@ xs L) (2)

b/
i) initial
renverser ([]@L)=renverser (L)=renverser(L)@renverser([])
=renverser(L)@[]
car []@L=L et renverser([])=[]
ici xs=[]

ii)général
On suppose l'affirmation vraie pour xs
donc renverser(xs@ys)=renverser(ys)@renverser(xs)

renverser(x::xs@ys)
=renverser(x::(xs@ys)) {cf (2) définition de @}
=(renverser(xs@ys))@[x] {cf (2) définition de renverser}
{propriétés de la concaténation
=(renverser(ys))@(renverser(xs)@[x])
=renverser(ys)@renverser(x::xs) {cf (2) définition de renverser}

On a prouvé que notre hypothèse était vrai au rang n+1.
Par suite, on a toujours:
renverser(xs@ys)=renverser(ys)@renverser(xs)