Tutorium 7¶
Gruppen 5 und 7
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa
Organisatorisches¶
Tutorien in der Weihnachtszeit
- Dezember: Nur ein Tut um 11:30 Uhr im Raum 236
- Januar wie immer
Geht hin wo ihr wollt...
Übungsblätter¶
Vorbemerkung 1¶
Was kommt bei dieser Formel raus?
(10 * 10 + 15 - 8 / 2)
((10 * 10) + 15 - (8 / 2)) = 111
=> Implizite Klammerung!
f1 a b c = --something
f1 1 f1 2
f1 1 (f1 2)
Aufgabe 1.1: Why tho¶
$$ (\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) $$Aufgabe 1.2: Why tho¶
a) $$ \omega' = (\lambda x.\ x\ x) (\lambda y.\ m\ (y\ y)\ n) $$
b) $$ (\lambda x.\ x\ x) (\lambda y.\lambda n.\ isZero\ n\ c_1\ ((y\ y)\ (sub\ n\ c_1)))\ c_2 $$ Terminiert, wenn wir die richtigen Ausdrücke auswerten!
Aufgabe 2¶
Haskell nach Lambda
Fragen?
Aufgabe 3¶
Aufgabe 4¶
$$ \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}\\ $$
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$Das X ist hier zu verstehen als $\forall X. \text{mensch}(X)\land\text{nichtChuckNorris}(X) \implies \text{sterblich}(X)$sterblich(X) :- mensch(X), nichtChuckNorris(X).
- Zielklausel:
$\neg x_1 \lor \neg x_2 \ \ \ \ \ \equiv \ \ \ \ \ x_1 \land x_2 \implies 0$
Prolog Query:Details in Formale Systeme?- mensch(sokrates), sterblich(sokrates).
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
Regeln werden wie bei Haskell List-Comprehensions reerfüllt: Jede mögliche Kombination wird durchgespielt
Prolog mit swipl
Ü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?
father(peter,nick).
father(john,peter).
grandfather(X,Y) :- father(X,Z),father(Z,Y).
QUERYSTART
grandfather(G,nick)
QUERYEND
Backtracking¶
Mit swipl
Arithmetik¶
formula(A,B,C,R) :- R is A+(A*B)-C-(C/A).
QUERYSTART
formula(1,2,3,R)
QUERYEND
Zusätzlich: <,<=,>=,>,=:=,=\=
Fibonacci-Zahlen¶
fib(0,0).
fib(1,1).
fib(N,R) :- N>1,
C is N-1,
D is N-2,
fib(C,A),
fib(D,B),
R is A+B.
QUERYSTART
fib(8,R)
QUERYEND
Listen¶
[|]als Cons-Operatormember(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
Nützliche Prädikate¶
not(X): Negation vonX: Wie? -> Nächste Woche!atom(X): IstXmit Atom instanziiert?integer(X): IstXmit Ganzzahl instanziiert?float(X): IstXmit Gleitkommazahl instanziiert?atomic(X): IstXmit Atom oder Zahl instanziiert?
Übungsaufgabe: Vorfahren¶
father(samuel, john).
father(john,peter).
mother(laura, peter).
father(peter, nick).
father(luke, ann).
mother(sara,ann).
mother(ann, nick).
father(john, guy).
mother(laura, guy).
ancestor(X,X).
ancestor(X,Y) :- father(X,Z), ancestor(Z,Y).
ancestor(X,Y) :- mother(X,Z), ancestor(Z,Y).
containsAncestors(X,[Y|Z]):-ancestor(X,Y).
containsAncestors(X,[Y|Z]):-containsAncestors(X,Z).
sibling(X,Y): mother(Z,X), mother(Z,Y).
auntOrUncle(X,Y): mother(Z,Y), sibling(Z,X).
auntOrUncle(X,Y): father(Z,Y), sibling(Z,X).
QUERYSTART
ancestor(X, nick)
QUERYEND
