Tutorium 6¶

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

Organisatorisches¶

Tutorien in der Weihnachtszeit
Tutorien am 22. und 23. Dezember finden statt

Übungsblätter¶

Aufgabe 1: Haskell zu $\lambda$-Kalkül¶

fib :: Integer -> Integer
fib 0 = 1
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

Ohne Pattern Matching:

fib n = if n == 0 || n == 1 then 1 else fib (n-1) + fib (n-2)
-- Funktional:
F f n = if n == 0 || n == 1 then 1 else f (n-1) + f (n-2)

$$ F = \lambda f.\ \lambda n.\ (\text{isZero}\ (\text{pred}\ n))\ c_1\ (\text{plus}\ (f\ (\text{sub}\ n\ c_1) )\ (f\ (\text{sub}\ n\ c_2) ) )\\ \text{fib} = Y F $$

Aufgabe 2¶

Aufgabe 3¶

$$ \frac{ \Gamma \vdash \lambda x.\ \lambda y.\ x:\alpha\rightarrow\beta\rightarrow\alpha\ \ \ \ \ \ \ \ \ \ \ \ \ \ \Gamma,k:\forall\alpha.\forall\beta.\alpha\rightarrow\beta\rightarrow\alpha \vdash k\ a\ (k\ b\ c):\text{int} }{ \Gamma \vdash \textbf{let } k=\lambda x.\ \lambda y.\ x \textbf{ in } k\ a\ (k\ b\ c):\text{int} } $$

Mit Instanziierungen $$ \forall\alpha.\forall\beta.\alpha\rightarrow\beta\rightarrow\alpha \succeq \text{int}\rightarrow\text{bool}\rightarrow\text{int}\\ \forall\alpha.\forall\beta.\alpha\rightarrow\beta\rightarrow\alpha \succeq \text{bool}\rightarrow\text{char}\rightarrow\text{bool}\\ $$

Aufgabe B.1¶

$$ (\lambda x.\ x\ x) (\lambda y.\ m\ y\ n)\\ (\lambda x.\ x\ x) (\lambda y.\ f\ y)\\ (\lambda x.\ x\ x) (\lambda y.\ (f\ y)\ y) $$

$$ (\lambda x.\ x\ x) (\lambda y.\ m\ y\ n) \Rightarrow m\ (\lambda y.\ m\ y\ n)\ n\\ (\lambda x.\ x\ x) (\lambda y.\ f\ y) \Rightarrow f\ (\lambda y.f\ y)\\ (\lambda x.\ x\ x) (\lambda y.\ (f\ y)\ y) \Rightarrow f\ (\lambda y. (f\ y)\ y)\ (\lambda y.(f\ y)\ y) $$

Aufgabe B.2¶

a) $$ \omega' = (\lambda x.\ x\ x) (\lambda y.\ m\ (y\ y)\ n) $$

$$ \Rightarrow \cdots \Rightarrow m\ (m\ (m\ (\Theta\ \Theta)\ n)\ n)\ n $$

mit $\Theta = (\lambda y.\ m\ (y\ y)\ n) (\lambda y.\ m\ (y\ y)\ n)$

Aufgabe B.2¶

b) $$ (\lambda x.\ x\ x) (\lambda y.\lambda n.\ \text{isZero}\ n\ c_1\ ((y\ y)\ (\text{sub}\ n\ c_1)))\ c_2 $$ Terminiert, wenn wir die richtigen Ausdrücke auswerten!

$$ \text{count} = (\lambda y.\lambda n.\ \text{isZero}\ n\ c_1\ ((y\ y)\ (\text{sub}\ n\ c_1))) $$$$ (\lambda x.x\ x)\ \text{count}\ c_2\\ \Rightarrow\text{count}\ \text{count}\ c_2\\ \Rightarrow(\lambda y.\lambda n.\ \text{isZero}\ n\ c_1\ ((y\ y)\ (\text{sub}\ n\ c_1)))\ \text{count}\ c_2\\ \Rightarrow\left(\underline{\text{isZero}\ c_2}\right)\ c_1\ ((\text{count}\ \text{count})\ (\text{sub}\ c_2\ c_1))\\ \cdots\\ \Rightarrow c_1 $$

Aufgabe B.2¶

c) $$ \omega' = (\lambda x.\ x\ x) (\lambda y.\ m\ (y\ y)\ n) $$ Wie viele Reduktionsschritte kann man auf $\omega'$ anwenden?

Aufgabe B.3¶

a) Geben Sie einen Term W an, welcher unter $\beta$-Reduktion nach und nach die Form $f (f (f (f (f (f (\dots))))))$ annimmt

$$ W = (\lambda x.x\ x)(\lambda y. f\ (y\ y)) $$

Aufgabe B.3¶

b) Beschreiben Sie, welche Form der Term $X=\lambda f. (\lambda x.x\ x)(\lambda y. f\ (y\ y))$ nach und nach annimmt

$$ (\lambda f. f (f (f (f (f (f (\dots))))))) $$

Aufgabe B.3¶

c) Führen Sie einen $\beta$-Reduktionsschritt von $X=\lambda f. (\lambda x.x\ x)(\lambda y. f\ (y\ y))$ aus. Welcher Term entsteht?

$$ X \Rightarrow \lambda f. (\lambda x. f\ (x\ x))(\lambda x. f\ (x\ x)) = Y $$

Aufgabe B.4¶

Geben Sie unter Benutzung von $X$ einen Term an, welcher zu $\omega$ reduziert
$X=\lambda f. (\lambda x.x\ x)(\lambda y. f\ (y\ y))$

$$ X (\lambda x. x) \Rightarrow (\lambda x.x\ x)(\lambda y. (\lambda x. x)\ (y\ y)) \Rightarrow (\lambda x.x\ x)(\lambda x.x\ x) $$

Das wars erstmal zum $\lambda$¶

Fragen?

Prolog¶

Logische Programmierung

Atome: Beginnend mit Kleinbuchstaben fritz
Zahlen: Wie üblich 1,2,3,4.2
Variablen: Beginnend mit Großbuchstaben oder Unterstrich X, _X
Funktor: Zusammensetzung mensch(fritz), alter(fritz, 17)
- Atom = Nullstelliger Funktor
- Funktor -> Prädikat: Jedem Funktor werden Wahrheitswerte zugeordnet

Exkurs: Hornklauseln¶

Flashback GBI: Aussagenlogik

Disjunktionen mit höchstens einem positiven Literal $$ \neg x_1 \lor \neg x_2 \lor \neg x_3 \lor \neg x_4 \lor y $$

Kann man dann auch schreiben als: $$ x_1 \land x_2 \land x_3 \land x_4 \implies y $$

Horn-Klauseln können in Polynomialzeit auf Erfüllbarkeit getestet werden!

Exkurs: Hornklauseln¶

Typen von Horn-Klauseln:

Faktenklausel:
$y \ \ \ \ \ \equiv\ \ \ \ \ y \implies 1$
```
mensch(sokrates).
nichtChuckNorris(sokrates).
```
Definite Hornklausel:
$\neg x_1 \lor \neg x_2 \lor y \ \ \ \ \ \equiv \ \ \ \ \ x_1 \land x_2 \implies y$
```
sterblich(X) :- mensch(X), nichtChuckNorris(X).
```
Das X ist hier zu verstehen als $\text{mensch}(X)\land\text{nichtChuckNorris}(X) \implies \text{sterblich}(X)$
Zielklausel:
$\neg x_1 \lor \neg x_2 \ \ \ \ \ \equiv \ \ \ \ \ x_1 \land x_2 \implies 0$
Prolog Query:
```
?- mensch(sokrates), sterblich(sokrates).
```
Details in Formale Systeme

liebt(fritz,fische). %Atome: fritz und fische, Funktor/Prädikat: liebt
liebt(hans,inge).
liebt(inge,fritz).
liebt(julia,fritz).
liebt(anna,X) :- liebt(julia,X). % liebt(anna,X) wahr, wenn liebt(julia,X) wahr

QUERYSTART
liebt(Y,fritz)
QUERYEND

Warning: /tmp/tmpgd0pbgjn/code.pl:16:
	Singleton variables: [Y]
 
----------------------------------------- 
 Call of: 	 liebt(_3200,fritz) 
 TRUE with:	 liebt(inge,fritz) 
 TRUE with:	 liebt(julia,fritz) 
 TRUE with:	 liebt(anna,fritz)

Regeln werden wie bei Haskell List-Comprehensions reerfüllt: Jede mögliche Kombination wird durchgespielt

Prolog mit SWI Prolog online
SWISH

swish.swi-prolog.org

Übung¶

John ist der Vater von Peter
Peter ist der Vater von Nick
Wenn X der Vater von Y ist und Y der Vater von Z ist, dann ist X der Großvater von Z
Wer ist der Großvater von Nick?

% ???

QUERYSTART
grandfather(G,nick)
QUERYEND

Warning: /tmp/tmp5rqvffcc/code.pl:15:
	Singleton variables: [G]
 
----------------------------------------- 
 Call of: 	 grandfather(_3200,nick) 
 TRUE with:	 grandfather(john,nick)

Backtracking¶

Mit swipl

Arithmetik¶

formula(A,B,C,R) :- R is A+(A*B)-C-(C/A).

QUERYSTART
formula(1,2,3,R)
QUERYEND

Warning: /tmp/tmpdpg6o0r7/code.pl:12:
	Singleton variables: [R]
 
----------------------------------------- 
 Call of: 	 formula(1,2,3,_3228) 
 TRUE with:	 formula(1,2,3,-3)

Zusätzlich: <,<=,>=,>,=:=,=\=

Fibonacci-Zahlen¶

fib(0,0).
%???
    
QUERYSTART
fib(8,R)
QUERYEND

Warning: /tmp/tmpk5rxslil/code.pl:19:
	Singleton variables: [R]
 
----------------------------------------- 
 Call of: 	 fib(8,_3200) 
 TRUE with:	 fib(8,21)

Listen¶

[|] als Cons-Operator

member(X,[X|R]).
member(X,[Y|R]) :- member(X,R).

append([],L,L).
append([X|R],L,[X|T]) :- append(R,L,T).

rev([],[]).
rev([X|R],Y) :- rev(R,Y1),append(Y1,[X],Y).

startsWith1([X|_]) :- X is 1.


QUERYSTART
startsWith1([Z,2,3])
QUERYEND

Warning: /tmp/tmp5196whlo/code.pl:13:
	Singleton variables: [Z]
 
----------------------------------------- 
 Call of: 	 startsWith1([_3244,2,3]) 
 TRUE with:	 startsWith1([1,2,3])

Nützliche Prädikate¶

not(X): Negation von X: Wie? -> Nächste Woche!
atom(X): Ist X mit Atom instanziiert?
integer(X): Ist X mit Ganzzahl instanziiert?
float(X): Ist X mit Gleitkommazahl instanziiert?
atomic(X): Ist X mit Atom oder Zahl instanziiert?

Übungsaufgabe: Vorfahren¶

father(samuel, john).
father(john,peter).
father(peter, nick).
father(luke, ann).
father(john, guy).
mother(laura, peter).
mother(sara,ann).
mother(ann, nick).
mother(laura, guy).

ancestor(X,X).
ancestor(X,Y) :- father(X,Z), ancestor(Z,Y).
ancestor(X,Y) :- mother(X,Z), ancestor(Z,Y).

%Does list L contain ancestors?
%containsAncestors(...,...):-...
%...

% Further predicates
parent(X,Y):- %...
sibling(X,Y):- %....
auntOrUncle(X,Y):- %...

ERROR: /tmp/tmpt4jdm2ug/code.pl:31:23: Syntax error: Unexpected end of file

Splits¶

splits(L,Res)

Bei Reerfüllung: Alle möglichen Zerlegungen von L in Res der Form (L1,L2)

%???

QUERYSTART
splits([1,2,3,4,5],R)
QUERYEND

Warning: /tmp/tmpge14d7aj/code.pl:12:
	Singleton variables: [R]
 
----------------------------------------- 
 Call of: 	 splits([1,2,3,4,5],_3294)
ERROR: /tmp/tmpge14d7aj/code.pl:12:
	doa/1: Undefined procedure: splits/2
Warning: /tmp/tmpge14d7aj/code.pl:12:
	Goal (directive) failed: user:doa([splits([1,2,3,4,5],_3294)])