Tutorium 6

Gruppen 5 und 7
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa

Übungsblätter

Nachtrag 1

Was ist das Problem dieses Codestücks?

numAcc (x:xs) n
        | (x == 1) = n
        | otherwise = numAcc xs n+1

Nachtrag 2

Call by Value: Was ist ein Wert?
-> Jede Abstraktion ist ein Wert (unabh. ob in Normalform oder nicht)

Nachtrag 3

Typ (Show ([Char] -> a)) => ([Char] -> a) -> ([Char] -> a):

• Wir können immer Typklassen für Funktionen definieren (s.u.)
• Typparameter dürfen nur nicht teilinitialisiert sein: Hierfür Flags notwendig

instance Show (a -> b) where
    show x = "whatever this shows..."
f a = a
show f

"whatever this shows..."

instance Show ([Char] -> b) where
    show x = "bla"

<interactive>:1:10: error:
    • Illegal instance declaration for ‘Show (String -> b)’
        (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 -> b)’

Nachtrag 4

Normalreihenfolge: Was hat Vorrang? Linkestes oder Äußerstes?

Macht keinen Unterschied

Aufgabe 1.1

1. c0 c1 (c2 c3 c4) c5
2. (c0 c1 c2) (c3 c4 c5)
3. c0 c1 (c2 c3 c4) (c5 c6)
4. c0 c1 (c2 c3 c4) c5 c6
5. c0 (c1 (c2 c3 c4)) c5 c6
6. (λy . c0 c1 c2) (c3 c4 c5)
7. (λy . c0 (λz. c1 c2 )) (c3 c4 c5)

c0 c1 (c2 c3 c4) c5

((c0 c1) ((c2 c3) c4)) c5

(c0 c1 c2) (c3 c4 c5)

((c0 c1) c2) ((c3 c4) c5)

c0 c1 (c2 c3 c4) (c5 c6)

((c0 c1) ((c2 c3) c4)) (c5 c6)

c0 c1 (c2 c3 c4 ) c5 c6

(((c0 c1) ((c2 c3) c4)) c5) c6

c0 (c1 (c2 c3 c4)) c5 c6

(((c0 (c1 ((c2 c3) c4))) c5) c6)

(λy . c0 c1 c2) (c3 c4 c5)

(λy . ((c0 c1) c2)) ((c3 c4) c5)

(λy . c0 (λz. c1 c2 )) (c3 c4 c5)

(λy . (c0 (λz. (c1 c2)))) ((c3 c4) c5)

Aufgabe 1.2

Welcher Term repräsentiert den gleichen Term wie λy . y c0?

1. (λy . y ) c0
2. λy . (y c0)

Aufgabe 1.3

Substitution:

1. x=λy.y in den Term (x) c0
2. x=(λy.y) in den Term x c0
3. x=λy.y in den Term x c0

Aufgabe 1.4

(λa.a) (λb.b) ((λc.c) ((λd.d) (λe.e) (λf .f ))) (λg .g ) ((λh.h) (λi.i)).

Aufgabe 2: Church-Zahlen

type Church t = (t -> t) -> t -> t
int2church :: Integer -> Church t
church2int :: Church Integer -> Integer

type Church t = (t->t) -> t -> t
int2church 0 = \s z -> z
int2church n = \s z -> int2church (n-1) s (s z)

church2int n = n (+1) 0

church2int (int2church 10)

10

Aufgabe 3

t1 = (λt. λf. f) ((λy. (λx. x x) (λx. x x)) ((λx. x) (λx. x))) (λt. λf. f)

t2 = λy. (λz. (λx. x) (λx. x) z) y

Aufgabe 4: Church-Paare

Fragen?

Wavelength

Regelsysteme

Frege'scher Schlussstrich
Bekannt aus GBI

Typsysteme

fun6 :: (Enum a, Enum b, Enum c) => a -> b -> c
fun6 x y = succ (toEnum (last [fromEnum x..fromEnum y]))

Polymorpher Typ mit Typvariablen a, b, c

Auch anwendbar auf Lambda-Kalkül!

• Basistypen bool, int, ...
• Funktionstypen $\tau_1 \rightarrow \tau_2$ (rechtsassoziativ)
• Typvariablen $\alpha, \alpha_1, \beta, \dots$

Typsystem: $\Gamma \vdash t : T$

$\Gamma \vdash t : \tau$ im Typkontext $\Gamma$ hat Term $t$ den Typ $\tau$
$\Gamma$ ordnet freien Variablen x ihre Typen $\Gamma\left(x\right)$ zu

Beispiel: Typen im Lambdakalkül

pair = $\lambda a.\lambda b.\lambda f. f a b$
Typ?

Übung: Typherleitung

Polymorphie

Typvariablen, Typvariablen, Typvariablen

Typschemata

$\forall \alpha_1. \forall \alpha_2. \dots \forall \alpha_n. \tau$
Steht für unendl. viele Typen mit initialisierten Typvariablen $\alpha_1 \dots \alpha_n$

$\forall \alpha. \alpha \rightarrow \alpha \succeq$ int -> int
$\forall \alpha. \alpha \rightarrow \alpha \succeq$ bool -> bool

Problem: $\lambda f.\ f\ (f\ \texttt{true})$ : ($\alpha$ -> int) -> int

Angepasste Regeln

Beispiel