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

Wechseln zu: Navigation, Suche

## Assignment 1: Typing

a)

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

2) Not well-typed (loop)

3) (a → b, a) → b

4) Num a => [a]

b)

Γ = 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


${\displaystyle (\lambda y.\lambda x.y(x(y,0)))\ (\lambda x.\mathbf {iszero} \ x)::(({\text{Int}}\rightarrow {\text{Bool}},{\text{Int}})\rightarrow {\text{Int}})\rightarrow {\text{Bool}}}$

## Assignment 2: Proofs about funct. programms

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

First we prove the lemma: ${\displaystyle \forall xs,ys,zs::[a]}$ 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: ${\displaystyle \forall }$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 ${\displaystyle \forall }$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


QED

## Assignment 3: Fun with lists

1.

a)

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
where
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)


b)

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


Alternative:

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


c)

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)


2.

a)
{-
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))


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


Alternative:

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


## Assignment 4: Navigating in rose trees

1.

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

b)

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


Alternative:

foldRose f g (Leaf x) = f x
foldRose f g (Node rs) = g $map (foldRose f g) rs  c)  foldRose id concat fmfp = "FFPM" d) mapRose f t = foldRose (\x -> Leaf (f x)) (\x -> Node x) t  Alternative: mapRose f = foldRose (Leaf . f) Node  2. a) unfocus :: Zipper a -> Rose a unfocus (focus, Top) = focus unfocus (focus, Step l p r) = unfocus (Node (reverse l ++ [focus] ++ reverse r), p)  b) 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 ${\displaystyle s_{1}}$ until ${\displaystyle s_{w}}$ loop ${\displaystyle s_{2}}$ end, σ> ${\displaystyle \rightarrow _{1}}$ <${\displaystyle s_{1}}$; if ${\displaystyle b}$ then skip end else from ${\displaystyle s_{1}}$ until b loop ${\displaystyle s_{2}}$ 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!)


tl;dr:

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:

(true)(s∨p)*(¬s∧¬p)

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