--- title: Zadania z indukcji (dodatkowe) --- 1. (append (map f xs) (map f ys)) = (map f (append xs ys)) 2. (length (append xs ys)) = (+ (length xs) (length ys)) 3. (filter p (map f xs)) = (map f (filter (lambda (x) (p (f x))) xs) 4. niech ns będzie lista liczb całkowitych. (foldr + 0 ns) = (foldl + 0 ns) 1) Dla każdej listy ys: P(xs) := (append (map f xs) (map f ys)) = (map f (append xs ys)) ```racket= (define (append xs ys) (if (null? xs) ys (append (cdr xs) (cons (car xs) ys)))) (define (map f xs) (if (null? xs) null (cons (f (car xs)) (map f (cdr xs))))) ``` Baza: xs=null P(null) L = (append (map f null) (map f ys)) = (append null (map f ys)) = (map f ys) P = (map f ys) Krok ind. Zal: P(xs) Teza: P((cons x xs)) P((cons x xs)): L = (append (map f (cons x xs)) (map f ys)) = (def map) = (append (cons (f x) (map f xs)) (map f ys)) = (def append) = (append (map f xs) (cons (f x) (map f ys)) ##### Zadanie 3 ```racket! (define (filter p xs) (if (null? xs) null (if (p (car xs)) (cons (car xs) (filter p (cdr xs))) (filter p (cdr xs))))) (define (map f xs) (if (null? xs) null (cons (f (car xs)) (map f (cdr xs))))) ``` P(xs) := (filter p (map f xs)) = (map f (filter (lambda (x) (p (f x))) xs) **Baza indukcji:** P(null) L = (filter p (map f null)) = (filter p null) = null P = (map f (filter (lambda(x) p (f x)) null)) = (map f null) = null $L=P$ **Krok indukcyjny** Zal.ind P(xs) Pokażemy, dla P((cons x xs)) P((cons x xs)): $L$ = (filter p (map f (cons x xs))) = (filter p (cons (f x) (map f xs))) = 1. (p (f x)) = #t (cons (f x) (filter p (map f xs))) = (z zal. ind) = (cons (f x) (map f (filter (lambda (x) (p (f x))) xs)) 2. (p (f x)) = #f (filter p (map f xs)) = **(map f (filter (lambda (x) (p (f x))) xs) = P** $P$ = (map f (filter (lambda (x) (p (f x))) (cons x xs))) = 1. ((lambda (x) (p (f x))) x) = #t -> (p (f x)) = #t (map f (cons x (filter (lambda (x) (p (f x))) xs))) = (def map'a) (cons (f x) (map f (filter (lambda (x) (p (f x))) xs))) = L 2. ((lambda (x) (p (f x))) x) = #f -> (p (f x)) = #f (map f (filter (lambda (x) (p (f x))) xs)) = **(filter p (map f xs)) = L** *Lemat pomocniczy* (filter p (map f x)) $\equiv$ (map f (filter (lambda (x) (p (f x))) xs)) #### Niech ns będzie lista liczb całkowitych. Pokaż, (foldr + 0 ns) = (foldl + 0 ns) ```racket! (define (foldr f x xs) (if (empty? xs) x (f (first xs) (foldr f x (rest xs))))) (define (foldl f x xs) (if (empty? xs) x (foldl f (f (first xs) x) (rest xs)))) ``` (foldr f x (cons A (cons B (cons C (cons D null))))) NALEŻY ODCZYTYWAĆ JAKO (f A (f B (f C (f D x)))) (foldl f x (cons A (cons B (cons C (cons D null))))) ODCZYTUJ JAKO (f D (f C (f B (f A x)))) P(ns) := (foldr + 0 ns) = (foldl + 0 ns) **Baza indukcji:** P(null) := L = (foldr + 0 null) = 0 P = (foldl + 0 null) = 0 $L = P$ **Krok indukcyjny:** Zał.ind: P(ns) Teza: (P (cons n ns)), gdie $n\in \mathbb{N}$ i ns - dowolna lista liczba naturalnych P(xs) -> P((cons x xs)) zał. dla dowolnego y i z (+ y (foldl + z xs)) = (foldl + (+ y z) xs) teza: (+ y (foldl + z (cons x xs))) = (foldl + (+ y z) (cons x xs)) L = (+ y (foldl + z (cons x xs))) = (+ y (foldl + (+ x z) xs)) = z zał (foldl + (+ y (+ x z)) xs) P = (foldl + (+ y z) (cons x xs)) = (foldl + (+ x (+ y z)) xs) = przemienności dodawania (foldl + (+ y (+ x z)) xs) ### Drzewa Zadanie z indukcji: przypomnijmy definicję drzewa z wykładu 4: (define-struct leaf () #:transparent) (define-struct node (l elem r) #:transparent) drzewo to: - albo (leaf) - albo (node l elem r), gdzie l i r to drzewa ```racket! (define (tree? x) (cond [(leaf? x) #t] [(node? x) (and (tree? (node-l x)) (tree? (node-r x)))] [else #f])) ;i zdefiniujmy lustrzane odbicie drzewa: (define (mirror t) (if ( leaf? t ) (leaf) (node (mirror (node-r t)) (node-elem t ) (mirror (node-l t))))) ``` --- **Zasada indukcji:** Jeśli P jest własnością drzew oraz - P((leaf)) - dla wszystkich drzew l i r oraz dla wszystkich elementów x, jeśli P(l) i P(r) to P((node l x r)) Wtedy P zachodzi dla wszystkich drzew --- Udowodnić, że (mirror (mirror t)) ≡ t dla wszystkich drzew t. P(t) := (mirror (mirror t)) ≡ t **Baza indukcji:** P((leaf)) = (mirror (mirror (leaf))) = (mirror (leaf)) = (leaf) **Krok indukcyjny:** Założenia (zachodzi dla dowolnego lewego i prawego poddrzewa) H1: P(l)= (mirror (mirror l)) ≡ l H2: P(r )= (mirror (mirror r)) ≡ r Pokażemy,dla dowolnego x, że P((node l x r )) P((node l x r )) = (mirror (mirror (node l x r))) = (z def mirror) (mirror (node (mirror r) x (mirror l)) = (z def mirror) (node (mirror (mirror l)) x (mirror (mirror r)) = (z zal.ind) (node l x r) Zadanie 2: to samo, ale dla drzew, które przechowują elementy w liściach a nie w wierzchołkach wewnętrznych. **Zasada indukcji** - dla wszystkich elementów x, jeśli P((x leaf)) - dla wszystkich drzew l i r jeśli P(l) i P(r) to P((node l x r)) Wtedy P zachodzi dla wszystkich drzew- P((leaf)) - dla wszystkich drzew l i r oraz dla wszystkich elementów x, jeśli P(l) i P(r ) to P((node l r)) Wtedy P zachodzi dla wszystkich drzew Ciekawsze zadanie: udowodnić, że dwie implementacje flatten z listy 4 liczą to samo. ```racket! (define (flatten t) (if (leaf? t) null (append (flatten (node-l t)) (cons (node-elem t) (flatten (node-r t)))))) (define (flat-append t xs) (if (leaf? t) xs (flat-append (node-l t) (cons (node-elem t) (flat-append (node-r t) xs))))) (define (flatten2 t) (flat-append t '())) (define (append xs ys) (if (null? xs) ys (cons (car xs) (append (cdr xs) ys)) ``` **P(t) := (flatten t) = (flatten2 t)** ekwiwalentnie (flatten t) = (flat-append t '()) **Baza indukcji:** P((leaf)): L = (flatten (leaf)) = null P = (flatten2 (leaf)) = (flat-append (leaf) null) = null Spróbujemy najpierw przeprowadzić dowód mechanicznie **Krok indukcyjny:** Założenia (zachodzi dla lewego i prawego poddrzewa) Dla dowolnego drzewa l i r oraz dowolnego elementu x IH1: P(l) := (flatten l) = (flatten2 l) IH2: P(r ) := (flatten r) = (flatten2 r) **Lemat pomocniczy:** Dla dowolnego drzewa t, i dla dowolnej listy xs Q(t) := (append (flatten t) xs) = (flat-append t xs) Dowód: Dla dowolnej listy xs Q((leaf)) : L = (append (flatten (leaf)) xs) = (append null xs) = xs P = (flat-append (leaf)) = xs Krok indukcyjny: Dla dowolnej listy xs Q((node l x r)): L = (append (flatten (node l x r)) xs) = (z def flatten) = (append (append (flatten l) (cons x (flatten r))) xs) = (z zał ind) (append (flat-append l (cons x (flatten r))) xs) = (z def. flat-append) (append) L = (append (flatten (node l x r)) xs) = (append (append (flatten l) (cons x (flatten r))) xs) (z definicji flatten) = (append (flat-append l (cons x (flatten r))) xs) (z ZI) = (flat-append l (append (cons x (flatten r)) xs)) (z definicji flat-append) P = (flat-append (node l x r) xs) = (flat-append l (cons x (flat-append r xs)))