Tutorium 5

Gruppen 5 und 7
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

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?

$$ \lambda f. \left( \lambda x.\left(\left(f\ x\right)\ y\right)\ \right) $$

$\lambda$-Terme: Keine Strings

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

$$ (\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 ̈uberfuhrt werden kann.

=> Isomorphismus zwischen den Syntaxbäumen

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

Ü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 z

• Church-Zahlen

Fibonacci Zahlen im $\lambda$-Kalkül

einfach weil es halt geht...

fun1 :: Eq t => [t] -> Bool
fun1 xs = (xs == [])

Redundant bracket

Found:

(xs == [])

Why Not:

xs == []

Use null

Found:

xs == []

Why Not:

null xs

instance (Show a) => Show ([Char] -> a) where
    show :: ([Char] -> a) -> [Char]
    show x = x "hi"

test :: [Char] -> Char
test x = 'c'

show test

Use String

Found:

([Char] -> a) -> [Char]

Why Not:

(String -> a) -> String

Use String

Found:

[Char] -> Char

Why Not:

String -> Char

<interactive>:1:22: error:
    • Illegal instance declaration for ‘Show (String -> a)’
        (All instance types must be of the form (T a1 ... an)
         where a1 ... an are *distinct type variables*,
         and each type variable appears at most once in the instance head.
         Use FlexibleInstances if you want to disable this.)
    • In the instance declaration for ‘Show (String -> a)’