Skip to content

Latest commit

 

History

History
184 lines (133 loc) · 3.77 KB

11rap1.md

File metadata and controls

184 lines (133 loc) · 3.77 KB
Raw

Wnioskowanie o programach

Dzięki zasadzie przejrzystości i typom, rozumowanie o programach w Haskellu często jest łatwiejsze niż w innych językach.

Własności przeważnie mają postać równości, np

reverse (xs++ys) = reverse ys ++ reverse xs

fmap id x = x
fmap (f . g) x = (fmap f . fmap g) x

Zasady wnioskowania równościowego

Symetria: (x = y) → (y = x)

Przechodniość: (x = y) ∧ (y = z) → (x = z)

Zasada Leibniza: P(x) ∧ (x = y) → P(y)

Kongruencja (szczególny przypadek): (x = y) → (f x = f y)

Z definicji: jeśli w programie mamy definicję f x = e to dla dowolnego y (odpowiedniego typu) f y = e[x := y]

ale uwaga na definicje, w której przypadki nie są ściśle rozłączne, np

isZero 0 = True
isZero n = False

tu nie możemy wnioskować, że isZero y = False dla dowolnego y. Dlatego tutaj posługujemy się tylko definicjami o ściśle rozłącznych przypadkach.

Rozgrzewka: liczby naturalne

import Test.QuickCheck
data Nat = Z | S Nat deriving(Eq,Show)

Indukcja na liczbach naturalnych

P(Z)      ∀n.P(n) → P(S n)
———————————————————————————
        ∀n.P(n)

Dodawanie

add :: Nat -> Nat -> Nat
add Z y     = y           {- add1 -}
add (S x) y = S(add x y)  {- add2 -}

Notacja: x + y = add x y

Lemat (addZ): ∀x.x + Z = x

addZ :: Nat -> Bool
addZ x = add x Z == x

Dowód przez indukcję po x dla P(x) ≡ x + Z = x

  1. Z + Z ={ add1[y := Z] }= Z
  2. Załóżmy IH: x + Z = x. Chcemy wykazać, że S x + Z = S x
    S x + Z   ={ add2 }=
    S(x + Z)  ={ S(IH) }=
    S x       □

Lemat (addS): ∀ x y.x + S y = S(x+y)

  1. Z + S y = S(Z+y)
    Z + S y   ={ add1 }=
    S y       ={ S(add1←) }=
    S(Z+y)    □
  1. (IH: x + S y = S(x+y)) → (S x + S y = S(S x + y))
    S x + S y   ={ add1 }=
    S(x + S y)  ={ S(IH) }=
    S(S(x+y))   ={ S(add2←) =}
    S(S x + y)  □

Ćwiczenie: ∀ x y. x + y = y + x

Ćwiczenie: ∀ x y t. x + (y + t) = (x + y) + t

Listy

data [a] = [] | a : [a]

Indukcja na listach

    P([])    ∀ x xs.P(xs) → P(x:xs)
    ————————————————————————————————
               ∀ xs.P(xs)

    (++) :: [a] -> [a] -> [a]
    []     ++ ys = ys          {- append1 -}
    (x:xs) ++ ys = x:(xs++ys)  {- append2 -}

Lemat(appendNil): ∀ xs. xs ++ [] = xs

Dowód: jak addZ (ćwiczenie)

appendNil :: [Int] -> Bool
appendNil xs = xs ++ [] == xs

rev :: [a] -> [a]
rev [] = []
rev (x:xs) = rev xs ++ [x]

Lemat(revAppend): rev(xs++ys) = rev ys ++ rev xs

revAppend :: [Int] -> [Int] -> Bool
revAppend xs ys = rev(xs++ys) == rev ys ++ rev xs

Dowód: ćwiczenie

Twierdzenie: ∀ xs. rev(rev xs) = xs

  1. rev(rev []) = rev [] = [] □
  2. (IH: rev(rev xs) = xs) → rev(rev(x:xs)) = x:xs
    rev(rev(x:xs))    ={ rev2 =}
    rev(rev xs++[x])  ={ revAppend =}
    rev[x] ++ rev(rev xs) ={ IH }=
    rev[x] ++ xs          ={ rev }=
    [x] ++ xs         ={ append }=
    x:xs              □

Wolno płynące napisy końcowe:

main = do
 writeln "addZ"
 qc addZ
 writeln "appendNil"
 qc appendNil
 writeln "revAppend"
 qc revAppend

writeln = putStrLn
qc :: Testable prop => prop -> IO ()
qc = quickCheck

nat :: Int -> Nat
nat 0 = Z
nat n | n > 0 = S(nat(n-1))
      | otherwise = error "nat: negative argument"

instance Arbitrary Nat where
  arbitrary = sized $ \n -> nat <$> choose(0,n)