---
title: "Lista 6"
---

### Zadanie 1
Przypomnij sobie definicję funkcji map. Następnie pokaż, że dla dowolnych funkcji
f i g oraz listy xs zachodzi (map f (map g xs)) ≡ (map (lambda (x) (f (g x)))
xs). Możesz założyć, że funkcje f i g poprawnie obliczają się do wartości dla
dowolnego argumentu.

(define (map f xs)
    (if (empty? xs)
        empty
        (cons (f (first xs) ) (map f (rest xs)))))

Twierdzenie: ∀ f, g (map f (map g xs)) ≡ (map (lambda (x) (f (g x))) xs)

Zasada indukcji wzgledem xs:
*P := (map f (map g xs)) ≡ (map (lambda (x) (f (g x))) xs)*
- P(empty)
- Dla każdej listy xs, jeśli P(xs), to P((cons ? xs))
Wówczas dla dowolnej listy xs zachodzi P(xs)

I. P(empty)
L = (map f (map g empty)) = (map f empty) = empty
P = (map (lambda (f ( g x))) empty) =empty
$L=P$

Krok indukcyjny
Zalozmy, ze zachodzi P(xs) : (map f (map g xs)) ≡ (map (lambda (x) (f (g x))) xs)
Pokazemy, (map f (map g (cons x xs))) = *(map (lambda (x) (f (g x))) (cons x xs))*

L = (map f (map g (cons x xs))) = (map f (cons (g x) (map g xs))) = (cons (f (g x)) (map f (map g xs)))

P = (map (lambda (x) (f (g x))) (cons x xs)) =
(cons ((lambda (x) (f (g x))) x) (map (lambda (x) (f (g x))) xs))= (upraszczajac lambde, i z zal ind)
(cons (f (g x)) (map f (map g xs)) )

$L = P$
*Na mocy zasady indukcji wlasnosc P zostala udowodniona*

### Zadanie 2
Pokaż, że funkcja append zawsze oblicza się do wartości, tzn. pokaż, że dla do-
wolnych list xs i ys istnieje lista zs taka, że (append xs ys) ≡ zs.

(define (append xs ys)
    (if (empty? xs)
     ys
     (cons (first xs) (append (rest xs) ys))))

P(xs) = ∀ ys ∃ zs (append xs ys) ≡ zs

Dowod:
- Baza
xs = empty
(append empty ys) = ys

- Krok indukcyjny:
Zal, ze zachodzi P(xs), pokazemy ∀ ys ∃ zs (append (cons x xs) ys) ≡ zs
Wtedy korzystajac z definicji appenda mamy:
(cons x (append xs ys)) = (korzystajc z zalozenia indukcyjnego) = (cons x zs)
Wiec mozna przyjac $zs'$ $=$ $(cons$ $x$ $zs)$

### Zadanie 3
Formuły w negacyjnej postaci normalnej to takie formuły rachunku zdań, w któ-
rych wszystkie negacje znajdują się przy zmiennych zdaniowych. Dokładniej,
formuły w negacyjnej postaci normalnej, składają się z koniunkcji, alternatywy
i literałów, gdzie literały to zanegowane lub niezanegowane zmienne zdaniowe.
Takie formuły można opisać następującym typem danych, sparametryzowanym
typem opisującym zmienne.
( define-type ( NNF 'v)
( nnf-lit [ polarity : Boolean ] [ var : 'v ])
( nnf-conj [l : ( NNF 'v)] [r : ( NNF 'v) ])
( nnf-disj [l : ( NNF 'v)] [r : ( NNF 'v) ]) )
Flaga polarity w konstruktorze literału oznacza, czy zmienna jest zanegowana
(wartość #f), czy nie (wartość #t). Sformułuj zasadę indukcji dla typu NNF.

*Zasada indukcji*
Niech P(x) bedzie wlasnoscia formuly w nnf. Jesli zachodzi:
- Dla kazdego literalu v jest spelnione P(v)
- Dla wszystkich formul ϕ i ψ jesli zachodzi P(ϕ) i P(ψ), to P(ϕ v ψ) i P(ψ ∧ ϕ)
jest rowniez spelnione.

To wlasnosc zachodzi dla wszystkich formul w nnf.

### Zadanie 4.
Zdefiniuj funkcję neg-nnf typu ((NNF 'a) -> (NNF 'a)) negującą formułę w ne-
gacyjnej postaci normalnej. Następnie pokaż, że (neg-nnf (neg-nnf φ)) ≡ φ dla
dowolnej formuły φ.

(define (neg-nnf f)
    (if (nnf-lit? f)
        (nnf-lit (not (nnf-polarity f)) (nnf-var f))
        (cond
        [(nnf-conj? f) (nnf-disj (neg-nnf (nnf-conj-l f)) (neg-nnf (nnf-conj-r f)))] ; z praw de Morgana
        [else (nnf-conj (neg-nnf (nnf-disj-l f)) (neg-nnf (nnf-disj-r f)))])))

Twierdzenie: P(f) := (neg-nnf (neg-nnf φ)) ≡ φ
Dowod przez indukcje strukturalna: \pfi
Weźmy dowolny literal v, wtedy
Rozpatrzmy przypadki:
* I literal jest zanegowany v = (neg-lit #t (nnf-lit-var v)))
Wtedy z def. neg-nnf
(neg-nnf (neg-nnf v)) = (neg-nnf (neg-nnf (neg-lit #t (nnf-lit-var v))))) =
= (neg-nnf (neg-lit (not #t) (nnf-lit-var v)))) = (neg-nnf (neg-lit #f (nnf-lit-var v)))) =
= (neg-lit (not #f) (nnf-lit-var v)) = (neg-lit #t (nnf-lit-var v))) = v

* II nie jest
Podobnie jak w I przypadku (zamienic wszystkie wystapienia #t na #f)

*Krok indukcyjny*
Zal, że (neg-nnf (neg-nnf s)) ≡ s i (neg-nnf (neg-nnf t)) ≡ t, dla pewnych formul s,t w nnf
Pokazemy, ze zachodzi (neg-nnf (neg-nnf s ∨ t)) ≡ s v t
(neg-nnf (neg-nnf s ∧ t)) ≡ s ∧ t

Dla alternatywy:
(neg-nnf (neg-nnf s ∨ t)) = (neg-nnf (nnf-conj (neg-nnf s) (neg-nnf t))) =
= (nnf-disj (neg-nnf (neg-nnf s)) (neg-nnf (neg-nnf s))) = (z zal ind) =
(nnf-disj s v t) = s v t

Dla ∧ podobnie (wszystkie wystapienia disj zamienic na conj i ∨ na ∧)

### Zadanie 5
Zdefiniuj funkcję eval-nnf typu (('a -> Boolean) (NNF 'a) -> Boolean) interpre-
tującą formułę w negacyjnej postaci normalnej, przy zadanym wartościowa-
niu zmiennych (funkcji typu ('a -> Boolean)). Następnie pokaż, że dla dowol-
nej formuły φ i wartościowania σ zachodzi (eval-nnf σ (neg-nnf φ)) ≡ (not
(eval-nnf σ φ)). Możesz założyć, że funkcja σ zawsze się zatrzymuje.

(define (eval-nnf val neg-f)
  (if (nnf-lit? neg-f)
      [if (equal? (val (nnf-lit-var neg-f)) #t)
            (not (val (nnf-lit-var neg-f)))
            (val (nnf-lit-var neg-f))]
      (cond
        [(nnf-conj? neg-f) (and (eval-nnf val (nnf-conj-l neg-f)) (eval-nnf val (nnf-conj-r neg-f)))]
        [else         (or (eval-nnf val (nnf-disj-l neg-f)) (eval-nnf val (nnf-disj-r neg-f)))])))

P(ψ) := Dla dowolnej formuly ψ i wart σ zachodzi (eval-nnf σ (neg-nnf ψ )) ≡ (not (eval-nnf σ ψ ))

Dowod:
*Baza*
Wezmy dowolny literal ψ i wartosciowanie σ:

-Rozpatrzmy przypadki
1. ψ jest zanegowanym literalem, czyli ψ := (neg-lit #t v)
L = (eval-nnf σ (neg-nnf ψ )) = (eval-nnf σ (neg-nnf (neg-lit #t v))) =
(z def. neg-nnf) = (eval-nnf σ (neg-lit (not # t) v)) = (eval-nnf σ (neg-lit #f v)) =
(z def eval-nnf) = (σ v)

P = (not (eval-nnf σ ψ )) = (not (eval-nnf σ (neg-lit #t v)) ) =
= (z def eval-nnf) = (not (not σ v)) = (σ v)
$L=P$

2. ψ jest niezanegowanym literalem, czyli ψ := (neg-lit #f v)

L = (eval-nnf σ (neg-nnf ψ )) = (eval-nnf σ (neg-nnf (neg-lit #f v))) =
= (z def. neg-nnf) = (eval-nnf σ (neg-lit #t v)) = (z def. eval-nnf) =
(not (σ v))

P = (not (eval-nnf σ ψ )) = (not (eval-nnf σ (neg-lit #f v)) ) =
(z def. eval-nnf) = (not (σ v))

$L=P$

*Krok ind.*
Zal, ze dla dowolnej formuly ψ, θ i wart σ zachodzi (eval-nnf σ (neg-nnf ψ )) ≡ (not (eval-nnf σ ψ ))
(eval-nnf σ (neg-nnf θ )) ≡ (not (eval-nnf σ θ ))

Pokazemy:
1. Alternatywa
(eval-nnf σ (neg-nnf (disj ψ θ) )) ≡ (not (eval-nnf σ (disj ψ θ) ))

L = (eval-nnf σ (neg-nnf (disj ψ θ ) )) = (z def neg-nnf) =
= (eval-nnf σ (nnf-conj (neg-nnf ψ ) (neg-nnf θ ))) = (z def eval-nnf) =
= (and (eval-nnf σ (neg-nnf ψ )) (eval-nnf σ (neg-nnf θ ))) = (z zal. ind) =
= (and (not (eval-nnf σ ψ )) (not (eval-nnf σ θ ))) = (z praw de Morgana) =
= (not (eval-nnf σ (disj ψ θ) )) = P
2. Koniunkcja
(eval-nnf σ (neg-nnf (conj ψ θ) )) ≡ (not (eval-nnf σ (conj ψ θ) ))

L = (eval-nnf σ (neg-nnf (conj ψ θ) )) = (z def. neg-nnf) = (eval-nnf σ (disj (nnf-neg ψ) (neg-nnf θ)))
= (z def eval-nnf) = (or (eval-nnf σ (nnf-neg ψ )) (eval-nnf σ (nnf-neg θ)))
= (z zal ind) = (or (not (eval-nnf σ ψ )) (not (eval-nnf σ θ ))) = (z praw de Morgana)=
= (not (and (eval-nnf σ ψ ) (eval-nnf σ θ ))) = (not (eval-nnf σ (conj ψ θ)))

### Zadanie 6.
Formuły rachunku zdań możemy opisać następującym typem.

( define-type ( Formula
    ( var [ var : 'v ])
    ( neg [ f : ( Formula 'v) 'v) ])
    ( conj [ l : ( Formula 'v)] [r : ( Formula 'v) ])
    ( disj [ l : ( Formula 'v)] [r : ( Formula 'v) ]) )

Zdefiniuj funkcję to-nnf transformującą formułę do równoważnej formuły w ne-
gacyjnej postaci normalnej. Możesz definiować funkcję pomocnicze, ale wszyst-
kie funkcje (wzajemnie) rekurencyjne powinny używać rekursji strukturalnej.

$Rozwiazanie$
Korzystam z Whitebook'a

W moim przypadku odwzorowanie T: to-nnf, a F: helper-nnf

( define-type ( Formula 'v)
    ( var [ var : 'v ])
    ( neg [ f : ( Formula 'v)])
    ( conj [ l : ( Formula 'v)] [r : ( Formula 'v) ])
    ( disj [ l : ( Formula 'v)] [r : ( Formula 'v) ]))

(define (helper-nnf f)
  (cond [(var? f) (nnf-lit #f f)]
        [(neg? f) (to-nnf (neg-f f))]
        [(conj? f) (nnf-disj (helper-nnf (conj-l f) ) (helper-nnf (conj-r f)))]
        [(disj? f) (nnf-conj (helper-nnf (disj-l f) ) (helper-nnf (disj-r f)))]))
         

(define (to-nnf f)
  (cond [(var? f) (nnf-lit #t f)]
        [(neg? f) (helper-nnf (neg-f f))]
        [(conj? f) (nnf-conj (to-nnf (conj-l f) ) (to-nnf (conj-r f)))]
        [(disj? f) (nnf-disj (to-nnf (disj-l f) ) (to-nnf (disj-r f)))]))

### Zadanie 7.
Zdefiniuj funkcję eval-formula interpretującą formuły z poprzedniego zadania.
Następnie pokaż, że (eval-nnf σ (to-nnf φ)) ≡ (eval-formula σ φ). Możesz za-
łożyć, że funkcja σ zawsze się zatrzymuje.

( define-type ( Formula 'v )
 ( var [ var : 'v ])
 ( neg [ f : ( Formula 'v ) ])
 ( conj [ l : ( Formula 'v ) ] [ r : ( Formula 'v ) ])
 ( disj [ l : ( Formula 'v ) ] [ r : ( Formula 'v ) ]) )

( define-type ( NNF 'v )
   ( nnf-lit [ polarity : Boolean ] [ var : 'v ])
   ( nnf-conj [ l : ( NNF 'v ) ] [ r : ( NNF 'v ) ])
   ( nnf-disj [ l : ( NNF 'v ) ] [ r : ( NNF 'v ) ]) )

(define (eval-nnf val neg-f)
  (if (nnf-lit? neg-f)
      [if (equal? (val (nnf-lit-var neg-f)) #t)
            (not (val (nnf-lit-var neg-f)))
            (val (nnf-lit-var neg-f))]
      (cond
        [(nnf-conj? neg-f) (or (eval-nnf val (nnf-conj-l neg-f)) (eval-nnf val (nnf-conj-r neg-f)))]
        [else         (and (eval-nnf val (nnf-disj-l neg-f)) (eval-nnf val (nnf-disj-r neg-f)))])))

(define (helper-nnf f)
  (cond [(var? f) (nnf-lit #f f)]
        [(neg? f) (to-nnf (neg-f f))]
        [(conj? f) (nnf-disj (helper-nnf (conj-l f) ) (helper-nnf (conj-r f)))]
        [(disj? f) (nnf-conj (helper-nnf (disj-l f) ) (helper-nnf (disj-r f)))]))
         

(define (to-nnf f)
  (cond [(var? f) (nnf-lit #t f)]
        [(neg? f) (helper-nnf (neg-f f))]
        [(conj? f) (nnf-conj (to-nnf (conj-l f) ) (to-nnf (conj-r f)))]
        [(disj? f) (nnf-disj (to-nnf (disj-l f) ) (to-nnf (disj-r f)))]))


(define (eval-formula σ φ)
  (cond [(var? φ)
         (σ φ)]
        [(neg? φ)
         (not (eval-formula σ (neg-f φ)))]
        [(conj? φ)
         (and (eval-formula σ (conj-l φ))
              (eval-formula σ (conj-r φ)))]
        [(disj? φ)
         (or (eval-formula σ (disj-l φ))
             (eval-formula σ (disj-r φ)))]))

Twierdzenie: P(ψ) := (eval-nnf σ (to-nnf ψ )) ≡ (eval-formula σ ψ)

Dowod przez indukcje:

Baza:
Wezmy dowolna zmienna zdaniowa p
L = (eval-nnf σ (to-nnf p)) = (z def. to-nnf) =(eval-nnf σ (nnf-lit #f f)) = (σ f)
P = (eval-formula σ p) = (σ p)
$L=P$

*Krok indukcyjny*
Zal, ze P zachodzi dla dowolnych formul ψ, θ
Zalozenie: (eval-nnf σ (to-nnf ψ )) ≡ (eval-formula σ ψ)
(eval-nnf σ (to-nnf θ )) ≡ (eval-formula σ θ )
**Teza**:
* Alternatywa: (eval-nnf σ (to-nnf (disj ψ θ) )) ≡ (eval-formula σ (disj ψ θ ))

L =(eval-nnf σ (to-nnf (disj ψ θ) ))= (z def. to-nnf) =
(eval-nnf σ (nnf-disj (to-nnf ψ ) (to-nnf θ))) = (z def. eval-nnf)=
(or (eval-nnf σ (to-nnf ψ )) (eval-nnf σ (to-nnf θ))) = (z zal ind)=
(or (eval-formula σ ψ) (eval-formula σ θ )) = (z def eval-formula) =
(eval-formula σ (disj ψ θ )) = P

* Koniunkcja: (eval-nnf σ (to-nnf (conj ψ θ) )) ≡ (eval-formula σ (conj ψ θ ))

L = (eval-nnf σ (to-nnf (conj ψ θ) )) =
= (eval-nnf σ (nnf-conj (to-nnf ψ) (to-nnf θ)))
= (and (eval-nnf σ (to-nnf ψ )) (eval-nnf σ (to-nnf θ))) = (z zal ind)=
= (and (eval-formula σ ψ) (eval-formula σ θ )) = (z def eval-formula) =
= (eval-formula σ (conj ψ θ )) = P

* Negacja: (eval-nnf σ (to-nnf (neg ψ) )) ≡ (eval-formula σ (neg ψ))

*Korzystam z lematu:*
(not (eval-nnf σ (to-nnf φ))) ≡ (eval-nnf σ (helper-nnf φ))

(eval-nnf σ (to-nnf (neg φ))) ≡ (eval-formula σ (neg φ))
(not (eval-nnf σ (to-nnf (neg φ)))) ≡ (eval-nnf σ (helper-nnf (neg φ)))

L ≡ (eval-nnf σ (to-nnf (neg φ))) ≡
(eval-nnf σ (helper-nnf φ)) ≡

P ≡ (eval-formula σ (neg φ)) ≡
(not (eval-formula σ φ)) ≡ (z zał. ind)
(not (eval-nnf σ (to-nnf φ))) ≡ (eval-nnf σ (helper-nnf φ)) ≡ L (z lematu)

**Dowod lematu:**
(not (eval-nnf σ (to-nnf φ))) ≡ (eval-nnf σ (helper-nnf φ))

i) Wezmy dowolna zmiennA p
L ≡ (not (eval-nnf σ (to-nnf p))) ≡
(not (eval-nnf σ (nnf-lit #t p)) ≡
(not (σ (nnf-lit-var φ)))

P ≡ (eval-nnf σ (helper-nnf p)) ≡
(eval-nnf σ (nnf-lit #f p)) ≡
(not (σ (nnf-lit-var φ))) ≡ L

*Krok indukcyjny*
Wezmy dowolne formuły ψ, θ
Zalozenia:
(not (eval-nnf σ (to-nnf φ))) ≡ (eval-nnf σ (helper-nnf φ))
(not (eval-nnf σ (to-nnf θ))) ≡ (eval-nnf σ (helper-nnf θ))

Alternatywa: (not (eval-nnf σ (to-nnf (disj φ θ)))) ≡ (eval-nnf σ (helper-nnf (disj φ θ)))
L ≡ (not (eval-nnf σ (to-nnf (disj φ θ)))) ≡
(not (eval-nnf σ (nnf-disj (to-nnf φ) (to-nnf θ)) ≡
(not (or (eval-nnf σ (to-nnf φ)) (eval-nnf σ (to-nnf θ))) ≡
(and (not (eval-nnf σ (to-nnf φ)) (not (eval-nnf σ (to-nnf θ))) ≡
(and (eval-nnf σ (helper-nnf φ)) (eval-nnf σ (helper-nnf θ)))

P ≡ (eval-nnf σ (helper-nnf (disj φ θ))) ≡
(eval-nnf σ (nnf-conj (helper-nnf φ ) (helper-nnf θ)) ≡
(and (eval-nnf σ (helper-nnf φ )) (eval-nnf σ (helper-nnf θ))) ≡ L

Konjunkcja: (not (eval-nnf σ (to-nnf (conj φ θ)))) ≡ (eval-nnf σ (helper-nnf (conj φ θ)))

L ≡ (not (eval-nnf σ (to-nnf (conj φ θ)))) ≡
(not (eval-nnf σ (nnf-conj (to-nnf φ) (to-nnf θ)) ≡
(not (and (eval-nnf σ (to-nnf φ)) (eval-nnf σ (to-nnf θ))) ≡
(or (not (eval-nnf σ (to-nnf φ)) (not (eval-nnf σ (to-nnf θ))) ≡
(or (eval-nnf σ (helper-nnf φ)) (eval-nnf σ (helper-nnf θ)))

P ≡ (eval-nnf σ (helper-nnf (conj φ θ))) ≡
(eval-nnf σ (nnf-disj (helper-nnf φ ) (helper-nnf θ)) ≡
(or (eval-nnf σ (helper-nnf φ )) (eval-nnf σ (helper-nnf θ))) ≡ L

Negacja: (not (eval-nnf σ (to-nnf (neg φ)))) ≡ (eval-nnf σ (helper-nnf (neg φ)))

L ≡ (not (eval-nnf σ (to-nnf (neg φ)))) ≡
(not (eval-nnf σ (to-nnf (neg φ)))) ≡
(not (eval-nnf σ (helper-nnf φ))) ≡ (z zał. ind)
(not (not (eval-nnf σ (to-nnf φ)))) ≡
(eval-nnf σ (to-nnf φ))
P ≡ (eval-nnf σ (helper-nnf (neg φ))) ≡
(eval-nnf σ (to-nnf φ)) ≡ L

**Na mocy zasady indukcji strukturalnej wlasnosc P zostala udowodniona**

### Zadanie 8.
Zdefiniuj predykat sorted? : ((Listof Number) -> Boolean) sprawdzający czy li-
sta jest posortowana oraz funkcję insert : (Number (Listof Number) -> (Listof
Number)) wstawiającą element do listy posortowanej. Następnie udowodnij, że
jeśli (sorted? xs) ≡ #t to (sorted? (insert x xs)) ≡ #t.

(define (insert x xs)
    (if (empty? xs)
        (cons x empty)
        (if (< x (first xs))
            (cons x xs)
            (cons (first xs) (insert x (rest xs))))))

 (define (bound x xs)
    (if (empty? xs)
        #t
        (<= x (first xs))))

 (define (sorted? xs)
    (if (empty? xs)
        #t
        (and (sorted? (r xs)) (bound? (first x) (rest xs)))))      

Funkcja *insert* w algorytmie
*insertion-sort* zachowuje fakt, ze lista jest posortowana

*P(xs) := Jesli (sorted? xs) = #t ⟹ (sorted? (insert x xs)) = #t*

Dowód przez indukcje strukturalna względem xs
Baza: xs = empty

P(empty)
L = (sorted? empty) = #t (bo lista pusta jest posortowana)
P = (sorted? (insert x empty)) = (sorted? (cons x empty)) = #t (bo lista jednoelementowa jest posortowana)

Krok indukcyjny:
Zalozenie: (sorted? xs) = #t ⟹ (sorted? (insert y xs)) = #t
Teza: (sorted? (cons x xs)) = #t ⟹ (sorted? (insert y (cons x xs))) = #t

P = (sorted? (insert y (cons x xs)))
Rozpatrzymy przypadki:
x - (first xs)
1. y <= x
(insert y (cons x xs)) =
(cons y (cons x xs)
Wiemy, ze (sorted? (cons x xs)) = #t (z zal) i y <= x, wiec
jezeli wstawimy y do (cons x xs), to (sorted? (cons y (cons x xs))) = #t

2. y > x
(insert y (cons x xs)) =(cons x (insert y xs))
Z zal ind. wiem, ze (sorted? (insert y xs)) = *#t,* i ze
(sorted? xs) = #t (bo xs jest posortowane)
(bound? y xs) = #t (bo każdy element w xs jest mniejszy lub równy $y$)
czyli po wstawieniu $y$ do listy $xs$,
stworzy sie nowa lista posortowana, ale juz z wstawionym $y$. Korzystajac z faktu, że $y>x$
mozemy wywnioskować, że (sorted? (insert y (cons x xs))) = *#t*

Na mocy zasady indukcji strukturalnej wlasnosc P zostala udowodniona.