========= Esercizio 1 ============ L ::= [] | X :: L In Matita: inductive lista : Type[0] = [] : lista | (::) : X -> lista -> lista assumo che :: sia associativo a dx X si espanda agli elementi della lista es: 1 :: 5 :: 3 :: [] è una lista di interi Problema 1: data una lista L di numeri priva di elementi ripetuti, calcolare l'insieme delle parti di L come lista di liste di numeri Soluzione: p(L) p([]) = [] :: [] p(X::L) = p(L) @ i(p(L),X) Sintassi Matita: (* let rec = sia definita per ricorsione p = nome della funzione U = argomento on U = definita per ricorsione strutturale sull'argomento U *) let rec p U on U = (* procedo per casi sulle forme di U *) match U with [ [] => [] :: [] | (X::L) => p L @ i (p L) X (*notate che f(X,Y) si scrive f X Y*) ] Problema 2: data una lista di liste di numeri, aggiungere un elemento X a ogni elemento della lista di liste Soluzione: i(LL,X) es: i((1::2::[])::[]::[], 3) = (3::1::2::[])::(3::[])::[] i([],X) = [] i(L::LL,X) = (X::L) :: i(LL,X) let rec i U X on U = match U with [ [] => [] | (L::LL) => (X::L) :: i LL X ] test: i((1::2::[])::[]::[], 3) = (3::1::2::[]) :: i([]::[], 3) = (3::1::2::[]) :: (3::[]) :: i([],3) = (3::1::2::[]) :: (3::[]) :: [] Problema 3: data due liste, restituire la lista che contiene l'unione delle due Soluzione: L1 @ L2 [] @ L2 = L2 (X::L) @ L2 = X :: (L @ L2) ========= Esercizio 2 ============ T ::= Int | T o T B ::= tt | ff In Matita: inductive T : Type[0] := num : Int -> T | o : T -> T -> T inductive B : Type[0] := tt : B | ff : B es: 3 o ((4 o 5) o 7) Problema 1: dato un albero T scrivere una funzione che restituisca tt sse i numeri contenuti nelle foglie dell'albero letti da sx a dx sono in ordine non decrescente Soluzione: c(T) es: c( 3 o ((4 o 5) o 7)) = tt es: c( 3 o ((3 o 5) o 7)) = tt es: c( 3 o ((5 o 2) o 7)) = ff c(x) = tt c(T1 o T2) = c(T1) && c(T2) && dx(T1) <= sx(T2) Problema 2: dato un albero T calcolare la foglia più a dx Soluzione: dx(T) dx(x) = x dx(T1 o T2) = dx(T2) Problema 3: dato un albero T calcolare la foglia più a sx Soluzione: sx(T) sx(x) = x sx(T1 o T2) = sx(T1)