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

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

</source> | </source> | ||

+ | |||

+ | |||

+ | |||

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

## Inhaltsverzeichnis

## 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
```

## 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`

.

- We prove it the lemma by structural induction on

- Let
`ys`

and`zs`

be arbitrary and`P(xs) ≡ go (go xs ys) zs = go ys (xs ++ zs)`

- Let

**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
```

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

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

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

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