Tutorium 5

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

Nachtrag

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

Advent of Code

Gute Gelegenheit um Haskell, Prolog oder andere Sprache (z.B. Lambda-Kalkül ;) ) zu üben!

www.adventofcode.com

Falls ihr Motivation braucht:
Private Leader Board: 1100658-1030daa6

Ich selbst arbeite mit Rust

Übungsblätter

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

Angenommen x=c0 c1 welche Aussagen gelten? Umfrage

Aufgabe 1.5

(λ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

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

Vorher:

Angepasste Regel:

let-Polymorphismus

Für die Typisierung von Ausdrücken wie $\lambda f.\ f\ (f\ \texttt{true})$ : ($\alpha$ -> int) -> int

Beispiel