---
# System prepended metadata

title: Lista 6
tags: [MP]

---

---
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.

``` racket=
(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.

```r 
(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 φ.


``` c 
(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.

```racket=
(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.
```racket=
( 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
![](https://i.imgur.com/Vzj85Yp.png)

W moim przypadku odwzorowanie T: to-nnf, a F: helper-nnf
```racket=
( 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.

```racket=
( 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.



```racket=
(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.


