Tutorium 7

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

Organisatorisches

Tutorien in der Weihnachtszeit

    1. Dezember: Nur ein Tut um 11:30 Uhr im Raum 236
    1. 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

grafik.png

grafik.png

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$
    sterblich(X) :- mensch(X), nichtChuckNorris(X).
    
    Das X ist hier zu verstehen als $\forall X. \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
In [1]:
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/tmpjghm4ojg/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 swipl

Übung

  1. John ist der Vater von Peter
  2. Peter ist der Vater von Nick
  3. Wenn X der Vater von Y ist und Y der Vater von Z ist, dann ist X der Großvater von Z
  4. Wer ist der Großvater von Nick?
In [15]:
father(peter,nick).
father(john,peter).

grandfather(X,Y) :- father(X,Z),father(Z,Y).

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

In [3]:
formula(A,B,C,R) :- R is A+(A*B)-C-(C/A).

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

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

Fibonacci-Zahlen

In [18]:
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
Warning: /tmp/tmp42f2ho2j/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).
    
In [5]:
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

In [21]:
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
Warning: /tmp/tmpm6miwmtn/code.pl:13:
	Clauses of father/2 are not together in the source-file
	  Earlier definition at /tmp/tmpm6miwmtn/code.pl:10
	  Current predicate: mother/2
	  Use :- discontiguous father/2. to suppress this message
Warning: /tmp/tmpm6miwmtn/code.pl:15:
	Clauses of mother/2 are not together in the source-file
	  Earlier definition at /tmp/tmpm6miwmtn/code.pl:12
	  Current predicate: father/2
	  Use :- discontiguous mother/2. to suppress this message
Warning: /tmp/tmpm6miwmtn/code.pl:17:
	Clauses of father/2 are not together in the source-file
	  Earlier definition at /tmp/tmpm6miwmtn/code.pl:10
	  Current predicate: mother/2
	  Use :- discontiguous father/2. to suppress this message
Warning: /tmp/tmpm6miwmtn/code.pl:18:
	Clauses of mother/2 are not together in the source-file
	  Earlier definition at /tmp/tmpm6miwmtn/code.pl:12
	  Current predicate: father/2
	  Use :- discontiguous mother/2. to suppress this message
Warning: /tmp/tmpm6miwmtn/code.pl:24:
	Singleton variables: [Z]
Warning: /tmp/tmpm6miwmtn/code.pl:25:
	Singleton variables: [Y]
ERROR: /tmp/tmpm6miwmtn/code.pl:28:
	Full stop in clause-body?  Cannot redefine ,/2
ERROR: /tmp/tmpm6miwmtn/code.pl:29:
	Full stop in clause-body?  Cannot redefine ,/2
ERROR: /tmp/tmpm6miwmtn/code.pl:30:
	Full stop in clause-body?  Cannot redefine ,/2
Warning: /tmp/tmpm6miwmtn/code.pl:32:
	Singleton variables: [X]
 
----------------------------------------- 
 Call of: 	 ancestor(_3200,nick) 
 TRUE with:	 ancestor(nick,nick) 
 TRUE with:	 ancestor(samuel,nick) 
 TRUE with:	 ancestor(john,nick) 
 TRUE with:	 ancestor(peter,nick) 
 TRUE with:	 ancestor(luke,nick) 
 TRUE with:	 ancestor(laura,nick) 
 TRUE with:	 ancestor(sara,nick) 
 TRUE with:	 ancestor(ann,nick)

grafik.png

In [ ]: