Tutorium 4

Gruppen 2 und 4
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa

Übungsblätter

Typen und Typklassen

fun1 xs = (xs == [])
fun2 f a = foldr f "a"
fun3 f a xs c = foldl f a xs c
fun4 f xs = map f xs xs
fun5 a b c = (maximum [a..b], 3 * c)
fun6 x y = succ (toEnum (last [fromEnum x..fromEnum y]))
fun7 x = if show x /= [] then x else error
fun1 xs = (xs == [])
fun1 :: (Eq t) => [t] -> Bool
fun2 f a = foldr f "a"
fun2 :: (Foldable c) => (a -> [Char] -> [Char]) -> b -> c a -> [Char]
fun3 f a xs c = foldl f a xs c
fun3 :: (Foldable t) => ((d -> e) -> a -> d -> e) -> (d -> e) -> t a -> d -> e
fun4 f xs = map f xs xs

Nicht typisierbar: Liste kann nicht auf xs angewendet werden

fun5 a b c = (maximum [a..b], 3 * c)
fun5 :: (Enum s, Ord s, Num t) => s -> s -> t -> (s, t)

-- What's Enum?
class Enum a where
    toEnum :: Int -> a 
    fromEnum :: a -> Int
    -- ...
    succ :: a -> a
fun6 x y = succ (toEnum (last [fromEnum x..fromEnum y]))
fun6 :: (Enum a, Enum b, Enum c) => a -> b -> c
fun7 x = if show x /= [] then x else error
fun7 :: (Show ([Char] -> a)) => ([Char] -> a) -> ([Char] -> a)
-- weil:
error :: [Char] -> a

Aufgabe 2: Abstrakte Syntaxbäume

Beispiel für eine Datenstruktur

data Exp t
    = Var t
    | Const Integer
    | Add (Exp t) (Exp t)

Beispiel für eine eval Funktion:

eval :: Env a -> Exp a -> Integer
eval env (Var v) = env v
eval env (Const c) = c
eval env (Add e1 e2) = (eval env e1) + (eval env e2)

Aufgabe 2: Abstrakte Syntaxbäume

data Exp t
    = Var t
    | Const Integer
    | Add (Exp t) (Exp t)
    | Less (Exp t) (Exp t)
    | And (Exp t) (Exp t)
    | Not (Exp t)
    | If (Exp t) (Exp t) (Exp t)
    deriving Eq

Aufgabe 2: Abstrakte Syntaxbäume

eval :: Env a -> Exp a -> Integer
eval env (Var v) = env v
eval env (Const c) = c
eval env (Add e1 e2) = (eval env e1) + (eval env e2)
eval env (Less e1 e2)
    | eval env e1 < eval env e2 = 1
    | otherwise = 0
eval env (And e1 e2)
    | eval env e1 == 0 || eval env e2 == 0 = 0
    | otherwise = 1
eval env (Not e1)
    | eval env e1 == 0 = 1
    | otherwise = 0
eval env (If b t e)
    | eval env b == 0 = eval env e
    | otherwise = eval env t

Aufgabe 2: Abstrakte Syntaxbäume

instance Show a => Show (Exp a) where
    show (Var a) = show a
    show (Const i) = show i
    show (Add e1 e2) = "(" ++ show e1 ++ " + " ++ show e2 ++ ")"
    show (Less e1 e2) = "(" ++ show e1 ++ " < " ++ show e2 ++ ")"
    show (And e1 e2) = "(" ++ show e1 ++ " & " ++ show e2 ++ ")"
    show (Not e) = "!(" ++ show e ++ ")"
    show (If b t e) = "(" ++ show b ++ " ? " ++ show t ++ " : " ++ show e ++ ")"

Aufgabe 3: Ropes: Länge

data Rope
= Leaf String
| Inner Rope Int Rope
ropeLength :: Rope -> Int
ropeLength (Leaf s) = length s
ropeLength (Inner _ w r) = w + ropeLength r

Aufgabe 3: Ropes: Concat

data Rope
= Leaf String
| Inner Rope Int Rope
ropeConcat :: Rope -> Rope -> Rope
ropeConcat l r = Inner l (ropeLength l) r

Aufgabe 3: Ropes: splitAt

data Rope
= Leaf String
| Inner Rope Int Rope
ropeSplitAt :: Int -> Rope -> (Rope, Rope)
ropeSplitAt i (Leaf s) = (Leaf (take i s), Leaf (drop i s))
ropeSplitAt i (Inner l w r)
    | i < w = let (ll, lr) = ropeSplitAt i l
                in (ll, ropeConcat lr r)
    | i > w = let (rl, rr) = ropeSplitAt (i-w) r
                in (ropeConcat l rl, rr)
    | otherwise = (l, r)

Aufgabe 3: Ropes: Insert

data Rope
= Leaf String
| Inner Rope Int Rope
ropeInsert :: Int -> Rope -> Rope -> Rope
ropeInsert i s rope = l `ropeConcat` s `ropeConcat` r
    where (l, r) = ropeSplitAt i rope

Aufgabe 3: Ropes: Delete

data Rope
= Leaf String
| Inner Rope Int Rope
ropeDelete i j r = ropeConcat a d
where
    (a, _) = ropeSplitAt i r
    (_, d) = ropeSplitAt j r

1206565371256380727Anonymous_lambda.svg.hi.png

Der untypisierte $\lambda$-Kalkül

$\lambda$-Terme

Bezeichnung Notation Beispiele aus der Vorlesung
Variablen $x$ $x$ $y$ $z$
Abstraktion $\lambda x. t$ $\lambda f.\lambda x. f x$
Funktionsanwendung $t_1 t_2$ $f y$
  • Funktionsanwendung linksassoziativ
  • Funktionsanwendung bindet stärker als Abstraktion
$$ \lambda f. \lambda x.f x y $$

Wo würden hier die Klammern sitzen?

Umfrage

$\lambda$-Terme: Keine Strings

$$ \lambda x.f\ x\ y $$

Bildschirmfoto%20vom%202019-11-18%2017-27-37.png

$$ (\lambda x.f\ x)\ y \neq \mathbf{\lambda x.f\ x\ y} = \lambda x.(f\ x\ y) $$

$\alpha$-Äquivalenz

$t_1$ und $t_2$ heißen $α$-äquivalent, wennt $t_1$ in $t_2$ durch konsistente Umbenennung der λ-gebundenen Variablen überführt werden kann.

Beispiel: $$ \lambda x.(\lambda z.f(\lambda y.z\ y)\ x)=^\alpha\lambda y.(\lambda x.f(\lambda z.x\ z)\ y) $$

$\eta$-Äquivalenz

Extensionalitäts-Prinzip: 2 Funktionen gleich, wenn Ergebnis für alle Argumente gleich

Terme $λx.f\ x$ und $f$ heißen $\eta$-aquivalent, falls $x$ nicht freie Variable von f Beispiel:

  • $\eta$-äquivalent: $f\ z$ und $\lambda x. f\ z\ x$
  • nicht $\eta$-äquivalent: $g\ x$ und $\lambda x. g\ x\ x$

"Ausführung" von $\lambda$-Termen

  • Redex ist ein $\lambda$-Term der Form $(\lambda x.t_1)\ t_2$
  • Substitution $t_1\left[x\mapsto t_2\right]$ ersetzt in $t_1$ alle freien Vorkommen von $x$ durch $t_2$
  • $\beta$-Reduktion entspricht einer Funktionsanwendung:
    $\left(\lambda x.t_1\right) t_2 \Rightarrow t_1 \left[x \mapsto t_2\right]$
  • Normalform ist ein Term, der nicht weiter reduziert werden kann

Warum ist der $\lambda$-Kalkül so cool?

  • Turingmächtiges Berechnungsmodell
  • In den 1930er Jahren ohne (!) Computer entwickelt
  • Sehr simple Semantik, aber trotzdem sehr mächtig

Tücken in der Substitution

Umfrage

Übung zu $\beta$-Reduktionen

Auswertungsstrategien

  • Normalreihenfolge: Immer der linkeste äußerste Redex wird reduziert
  • Call-by-Name: Linkesten, äußeren Redex aber nicht, wenn von $\lambda$ umgeben
  • Call-by-Value: Linkesten Redex, der nicht von $\lambda$ umgeben, dessen Argument Wert ist

Church Rosser Eigenschaft

Der untypisierte $\lambda$-Kalkül ist konfluent:
Wenn $t \Rightarrow^* t_1$ und $t \Rightarrow^* t_2$,
dann gibt es ein $t'$ mit $t_1 \Rightarrow^* t'$ und $t_2 \Rightarrow^* t'$

Eindeutigkeit der Normalform

Die Normalform eines $\lambda$-Terms $t$ ist - sofern sie existiert - eindeutig.

Auswertungsstrategien vol. 2

  • Call-by-Name und Call-by-Value werten nicht immer zu Normalform aus, aber darauf $\beta$-reduzierbar
  • Call-by-Name ist quasi Lazy Evaluation
  • Call-by-Name terminiert öfter

Divergenz

ALLES sind Funktionen

  • Boolsche Werte
    $\lambda x. \lambda y. $ if x then x else y
  • Church-Zahlen

Fibonacci Zahlen im $\lambda$-Kalkül

einfach weil es halt geht...

In [3]:
fib' n = fibAcc n 1 0
    where fibAcc m acc1 acc0
            | m == 0 = acc0
            | m == 1 = acc1
            | otherwise = fibAcc (m-1) (acc1+acc0) acc1
fib' 30
832040

Backup

Typklassen

...endlich...

  • Zusammenfassen von Typen anhand von definierter Operationen
  • Java: ~Interfaces Beispiel Eq:
    class Eq t where
      (==) :: t -> t -> Bool
      (/=) :: t -> t -> Bool
    
    Default Implementierungen:
    x /= y = not (x == y)
      x == y = not (x /= y)
    

Typklassen implementieren

instance Eq Bool where
    True == True = True
    False == False = True
    x == y = False

Auch für Polymorphe Typen:

In [14]:
data Maybe t = Nothing | Just t

class Defaultable t where
    getDefault :: t a -> a -> a
    
instance Defaultable Maybe where
    getDefault (Just x) c = x
    getDefault Nothing c = c

getDefault Nothing 1
getDefault (Just 10) 1
1
10

Übungsaufgabe

Typklasse für Datenstrukturen die Mappable sind.

Wir wollen:

  • Typklasse die uns die Funktion dMap auf algebraischen Datentypen mit einem Parameter erlaubt
    class Mappable -- ...
    
  • Eine Implementierung dieser Typklasse für Tree
    instance Mappable Tree -- ...
    
In [7]:
-- Übungsaufgabe 5
class Mappable t where
    dMap :: (a->b) -> t a -> t b

instance Mappable Tree where
    dMap f t = treeMap f t
Eta reduce
Found:
dMap f t = treeMap f t
Why Not:
dMap = treeMap
In [ ]: