Loading [MathJax]/jax/output/HTML-CSS/jax.js

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¶

(λx. x x)(λy. m y n)(λx. x x)(λy. f y)(λx. x x)(λy. (f y) y)

Aufgabe 1.2: Why tho¶

a) ω′=(λx. x x)(λy. m (y y) n)

b) (λx. x x)(λy.λn. isZero n c1 ((y y) (sub n c1))) c2 Terminiert, wenn wir die richtigen Ausdrücke auswerten!

Aufgabe 2¶

Haskell nach Lambda
Fragen?

Aufgabe 3¶

grafik.png

grafik.png

Aufgabe 4¶

Γ⊢λx. Î»y. x:α→β→α              Î“,k:∀α.∀β.α→β→α⊢k a (k b c):intΓ⊢let k=λx. Î»y. x in k a (k b c):int

Mit Instanziierungen ∀α.∀β.α→β→α⪰int→bool→int∀α.∀β.α→β→α⪰bool→char→bool

Das wars erstmal zum λ¶

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 ¬x1∨¬x2∨¬x3∨¬x4∨y

Kann man dann auch schreiben als: x1∧x2∧x3∧x4⟹y

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

Exkurs: Hornklauseln¶

Typen von Horn-Klauseln:

  • Faktenklausel:
    y     â‰¡     y⟹1
    mensch(sokrates).
    nichtChuckNorris(sokrates).
    
  • Definite Hornklausel:
    ¬x1∨¬x2∨y     â‰¡     x1∧x2⟹y
    sterblich(X) :- mensch(X), nichtChuckNorris(X).
    
    Das X ist hier zu verstehen als ∀X.mensch(X)∧nichtChuckNorris(X)⟹sterblich(X)
  • Zielklausel:
    ¬x1∨¬x2     â‰¡     x1∧x2⟹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 [ ]: