Lösungsvorschlag Formal Methods And Functional Programming FS17: Unterschied zwischen den Versionen

Aus VISki
Wechseln zu: Navigation, Suche
K (Assignment 4: Navigating in rose trees)
Zeile 199: Zeile 199:
       where path' = Step (reverse $ take x ys) path (reverse $ drop (x+1) ys)
       where path' = Step (reverse $ take x ys) path (reverse $ drop (x+1) ys)
== Assignment 5 ==
We only need to add a EiffelLoop-rule:
-------------------------------------------------------------------------------------------------------- EiffelLoop
  <from <math>s_1</math> until <math>s_w</math> loop <math>s_2</math> end, σ> <math>\rightarrow_1</math> <<math>s_1</math>; if <math>b</math> then skip end else from <math>s_1</math> until b loop <math>s_2</math> end, σ>
== Assignment 8: LTL ==
== Assignment 8: LTL ==

Aktuelle Version vom 15. August 2019, 11:54 Uhr

Assignment 1: Typing


1) a → (a → a → b) → b

2) Not well-typed (loop)

3) (a → b, a) → b

4) Num a => [a]


Γ = y:(Int  Bool), x:𝜏1
                                                             -------------- Var   ---------------- Int
                                                               Γ  y :: 𝜏5          Γ  0 :: Int
                               ----------------------- Var    ----------------------------------- Tuple
                                   Γ  x :: 𝜏4  𝜏3              Γ  (y, 0) :: 𝜏4
   ---------------------- Var    ------------------------------------------------- App
      Γ  y :: 𝜏3  𝜏2               Γ  (x (y, 0)) :: 𝜏3
  ----------------------------------------------------------- App             ------------------- Var
           Γ  y(x (y,0)) :: 𝜏2                                                 x:Int  x :: Int
        ------------------------------------------ Abs                   --------------------------- iszero
           y:(Int  Bool)  λx. y(x (y,0)) :: 𝜏0                           x:Int  iszero x :: Bool
       --------------------------------------------- Abs               -------------------------------- Abs
          (λy. λx. y(x (y,0))) :: (Int  Bool)  𝜏0                      (λx. iszero x) :: Int  Bool
       ------------------------------------------------------------------------------------------------ App
                                (λy. λx. y(x (y,0))) (λx. iszero x) :: 𝜏0

𝜏0 = 𝜏1  𝜏2
𝜏3 = Int
𝜏2 = Bool
𝜏1 = 𝜏4  𝜏3
𝜏4 = (𝜏5, Int)
𝜏5 = Int  Bool

Assignment 2: Proofs about funct. programms

Statement: ∀xs::[a] xrev (xrev xs) = xs

First we prove the lemma: go (go xs ys) zs = go ys (xs ++ zs)

We prove it the lemma by structural induction on xs.
Let ys and zs be arbitrary and P(xs) ≡ go (go xs ys) zs = go ys (xs ++ zs)
Base case P([]):
To show: go (go [] ys) = go ys ([] ++ zs)
go (go [] ys) zs = go ys zs            -- go.1
                 = go ys ([] ++ zs)    -- app.1
Inductive Step P(xs)→P(x:xs)
To show: go (go (x:xs) ys) zs = go ys ((xxs) ++ zs)
I.H: xs, ys, zs :: [a] go (go xs ys) zs = go ys (xs ++ zs)
go (go (x:xs) ys) zs = go (go xs (x:ys)) zs    -- go.2
                     = go (x:ys) (xs ++ zs)    -- I.H
                     = go ys (x:(xs ++ zs))    -- go.2
                     = go ys (x:xs) ++ zs      -- app.2

We now show that xs::[a] xrev (xrev xs) = xs
Let xs be arbitrary then:

xrev (xrev xs) = xrev (go xs [])      -- xrev
               = go (go xs []) []     -- xrev
               = go [] (xs ++ [])     -- lemma
               = go [] xs             -- app_Nil
               = xs                   -- go.1


Assignment 3: Fun with lists



group [] = []
group xs = (takeWhile p xs):group (dropWhile p xs) where p = (== head xs)

Alternative (not as elegant ;)):

group :: Eq a => [a] -> [[a]]
group [] = [[]]
group [x] = [[x]]
group (x:xs) = go [x] x xs
        go :: Eq a => [a] -> a -> [a] -> [[a]]
        go cur z []         = cur : []
        go cur z (y:ys)
            | z == y        = go (y:cur) y ys
            | otherwise     = cur : (go [y] y ys)


encode xs = zip (map head g) (map length g) where g = group xs


encode :: Eq a => [a] -> [(a, Int)]
encode xs = map (\ys -> (head ys, length ys)) (group xs)


decode xs = concatMap rep xs where rep (x,0) = ""
                                   rep (x,y) = x:rep (x,y-1)

Alternative (which is kind of the same):

decode :: [(a,Int)] -> [a]
decode = concat . map (\(x,y) -> (replicate y x))

{- if you're wondering what concat does: -}
concat' :: [[a]] -> [a]
concat' [] = []
concat' (x:xs) = x ++ (concat' xs)

{- if you're wondering what replicate does: -}
replicate' :: Int -> a -> [a]
replicate' x y  | x < 1     = []
                | otherwise = y : (replicate' (x-1) y)


    Note: when trying this function
          (ex in GHCi) rename it to
          `iterate'` to avoid conflicts
          with Prelude
iterate f x = x:(iterate f (f x))

looknsay = iterate flat [1] where flat xs = concat [[y,x] | (x,y) <- encode xs]


looknsay :: [[Int]]
looknsay = iterate go [1]
        go y = concat (map (\(a,b) -> [b,a]) (encode y))

Assignment 4: Navigating in rose trees


a) foldRose :: (a -> b) -> ([b] -> b) -> Rose a -> b


foldRose lf nf (Leaf a) = lf a
foldRose lf nf (Node ts) = nf [foldRose lf nf t | t <- ts]


foldRose f g (Leaf x) = f x
foldRose f g (Node rs) = g $ map (foldRose f g) rs

c) foldRose id concat fmfp = "FFPM"


mapRose f t = foldRose (\x -> Leaf (f x)) (\x -> Node x) t


mapRose f = foldRose (Leaf . f) Node



unfocus :: Zipper a -> Rose a
unfocus (focus, Top) = focus
unfocus (focus, Step l p r) = unfocus (Node (reverse l ++ [focus] ++ reverse r), p)


goto :: [Int] -> Zipper a -> Maybe (Zipper a)
goto [] z = Just z
goto _ (Leaf x, _) = Nothing
goto (x:xs) (Node ys, path)
    | x < length ys = goto xs (ys !! x, path')
    | otherwise     = Nothing
      where path' = Step (reverse $ take x ys) path (reverse $ drop (x+1) ys)

Assignment 5

We only need to add a EiffelLoop-rule:

-------------------------------------------------------------------------------------------------------- EiffelLoop
 <from  until  loop  end, σ>  <; if  then skip end else from  until b loop  end, σ>

Assignment 8: LTL

A) LTL definitions: https://en.wikipedia.org/wiki/Linear_temporal_logic

`□x` = "always x" = `x -> x -> x -> x -> ...`
`○x` = "next x" = `? -> x -> ? -> ...`
`◇x` = "eventually x" = `? -> ... -> ? -> x -> ? -> ...` (or `x -> ? -> ...` would also work!)


1) False
2) True
3) False
4) True

1) □○(s∨p):

Note: s∨p == s || p
`□○(s∨p)` = `□(○(s∨p))` ="from every state you can allways (in one step you can go to a state where either `s` or `p` holds)"

`(s∨p)` holds in states `s2`, `s3`, `s4`. It doesn't hold in states `s1`, `s5` `○(s∨p)` holds in states `s1 (->s2 or ->s3)`, `s2 (->s2 or ->s4)`, `s3 (->s4)`. It doesn't hold in `s4`, `s5` (in `s4` you can only get to `s5` and in `s5` you can only go to `s1` using one transition. Thus `□○(s∨p)` doesn't hold, as `○(s∨p)` doesn't hold for states `s4` and `s5`

2) ○○p ⇒ ◇d:

`○○p ⇒ ◇d` = `(○○p) ⇒ ◇d` = `(○(○p)) ⇒ ◇d` = "if we are able to reach a state in 2 steps from the start, where `p` holds, then eventually `d` will hold as well."

States reachable in 2 steps from the start: `s1 (s1->s3->s1)`, `s2 (s1->s2->s2)`, `s4 (s1->s2->s4 || s1->s3->s4)` Since `p` does hold in `s4` but neither in `s1` nor `s2` we only need to examine state `s4` further. The only possible next step from `s4` is `s5`. `d` holds in `s5` and thus `○○p ⇒ ◇d` holds.

3) □(p ⇒ ○d):

`□(p ⇒ ○d)` = "always, if `p` holds, we can reach a state within one step, where `d` will hold as well"

We prove, that `□(p ⇒ ○d)` doesn't hold by a counter example. In state `s3`, `p` holds and thus we should be able to reach a state where `d` holds within one step. The reachable states from `s3` with one transition are `s1` and `s4`. In none of these states `d` holds, thus `□(p ⇒ ○d)` doesn't hold.

4) □(○d ⇒ p):

`□(○d ⇒ p)` = "for every state (that is able to reach a state where `d` holdes in one step, must hold `p`)".

States where `d` holds: `s5` States that are able to reach `s5` in one step: `s4` States where `p` holds: `s3`, `s4` Since `s4` is the only state satisfying `○d` and `s4` satisfies `p`, we can conclude, that `□(○d ⇒ p)` holds.

Note: A Video explaining '''safety''' and '''liveness''' properties can be found here: https://www.youtube.com/watch?v=7dL285YWFcg

B) □○(s∨p):

`□○(s∨p)` = `□(○(s∨p))` = "We're always in a state, where we can reach a state in one step, where either `s` or `p` holds"

This is a regular safety property, as once it's violated, we can't do anything to recover from it. Ex. once we reach state `s4` there is no way to reach any state with one step where `(s∨p)` holds. A regex for this would be:


Explanation: We don't know or care about the first state we're in. All we care is if from there we're able to reach a state where `(s∨p)` holds. Assuming there is no second state after the first one, the safety propery is violated. In that case the `(s∨p)*` part of our regex was never used. If there however is a second state that satisfies `(s∨p)` (in our case this is both state `s2` as well as `s3` we continue from there. A visualisation of this regex can be seen here: https://regex101.com/r/jVC12F/4 the first character (Group 1) doesn't matter, followed by any amount of `p` and `s` (Group 2) and then any character except for `p` or `s` (Group 3) and it doesn't matter what happens after this (there can again be `p` or `s` but once the regex is triggered it stays in that state).

C) ○○p => ◇d:

`○○p => ◇d` = `(○○p) => (◇d)` = `(○(○p)) => (◇d)` = "If we are able to reach a state where `p` holdes in 2 steps from the start, we will eventually reach a step, where `d` holds"

This is a Liveness property, as we can't be certain in finite time if we won't ever reach `d`. Example: `aapaa...aadaa...`. In this examle `○○p` does hold and we are able to reach `d` somewhere in the future. If `○○p` would not hold, the formula would trivialy be true It is no safety propery, as it can't be violated in finite time (as we could still eventually reach `d`).