<div class="notebook open-fullscreen">
<div class="nb-cell program" name="p7">
% Auszug aus betaConversion.pl
%
% adapted by Wiebke Petersen
</div>
<div class="nb-cell markdown" name="md5">
### Implementierung der beta-Konversion
</div>
<div class="nb-cell program" data-background="true" data-singleline="true" name="p5">
% Syntax-semantics rules
s(app(NP,VP))--> np(NP), vp(VP).
np(app(Det,Noun))--> det(Det), noun(Noun).
np(PN)--> pn(PN).
vp(IV)--> iv(IV).
vp(app(TV,NP))--> tv(TV), np(NP).
% Proper Names
pn(lam(P,app(P,vincent)))--> [vincent].
pn(lam(P,app(P,mia)))--> [mia].
% Transitive Verbs
tv(lam(X,lam(Y,app(X,lam(Z,love(Y,Z))))))--> [loves].
tv(lam(X,lam(Y,app(X,lam(Z,like(Y,Z))))))--> [likes].
% Intransitive Verbs
iv(lam(Y,snort(Y)))--> [snorts].
iv(lam(Y,walk(Y)))--> [walks].
% Determiners
det(lam(P,lam(Q,all(X,imp(app(P,X),app(Q,X))))))--> [every].
det(lam(P,lam(Q,some(X,and(app(P,X),app(Q,X))))))--> [a].
% Nouns
noun(lam(X,woman(X)))--> [woman].
noun(lam(X,boxer(X)))--> [boxer].
noun(lam(X,footmassage(X)))--> [foot,massage].
</div>
<div class="nb-cell markdown" name="md6">
Zur beta-Konversion eines komplexen Ausdrucks mit funktionalen Applikationen und Abstraktionen gehen wir wie folgt vor:
* wir beginnen mit einem leeren Stack;
</div>
<div class="nb-cell program" data-background="true" name="p1">
/*========================================================================
Beta-Conversion (introducing stack)
========================================================================*/
% ?- betaConvert(app(lam(U,app(U,mia)),lam(X,smoke(X))),Converted).
% introduce empty stack
betaConvert(X,Y):-
betaConvert(X,Y,[]).
</div>
<div class="nb-cell markdown" name="md3">
* immer wenn der Ausdruck eine funktionale Applikation ist, packen wir das Argument auf den Stack;
</div>
<div class="nb-cell markdown" name="md1">
Einkommentieren, um Stackentwicklung zu sehen:
</div>
<div class="nb-cell program" data-background="true" name="p4">
/*========================================================================
Beta-Conversion (comment-in for tracing)
========================================================================*/
%betaConvert(X,_,S):-
% numbervars((X,S),1,_End,[]),
% nl, write('Expre: '), print(X),
% nl, write('Stack: '), print(S), nl,
% fail.
</div>
<div class="nb-cell program" data-background="true" name="p2">
/*========================================================================
Beta-Conversion (core stuff)
========================================================================*/
% expression is a variable => do nothing
betaConvert(X,Y,[]):-
var(X), !,
Y=X.
% expression is application => push argument to stack
betaConvert(Expression,Result,Stack):-
nonvar(Expression),
Expression = app(Functor,Argument),
%% To suppress alpha-conversion:
% alphaConvert(Functor,Converted), %% comment-out this line
Functor=Converted, %% comment-in this line
betaConvert(Converted,Result,[Argument|Stack]), !.
</div>
<div class="nb-cell markdown" name="md4">
* wenn der Ausdruck eine Abstraktion ist, dann nehmen wir das oberste Element vom Stack und substituieren es für die abstrahierte Variable;
</div>
<div class="nb-cell program" data-background="true" name="p3">
% expression is abstraction + stack is not empty => pop argument from stack
betaConvert(Expression,Result,[X|Stack]):-
nonvar(Expression),
Expression = lam(X,Formula),
betaConvert(Formula,Result,Stack), !.
</div>
<div class="nb-cell markdown" name="md7">
* ist der Stack leer und der Ausdruck eine Abstraktion, dann splitten wir den Ausdruck
</div>
<div class="nb-cell program" data-background="true" name="p14">
% other expression => break down complex expression
betaConvert(Formula,Result,[]):-
nonvar(Formula), !,
Formula=..[Functor|Formulas],
betaConvertList(Formulas,ResultFormulas),
Result=.. [Functor|ResultFormulas].
betaConvert(Exp,app(Exp,Y),[X]):- %% Impossible to perform application.
betaConvert(X,Y).
/*========================================================================
Beta-Convert a list
========================================================================*/
betaConvertList([],[]).
betaConvertList([Formula|Others],[Result|ResultOthers]):-
betaConvert(Formula,Result),
betaConvertList(Others,ResultOthers).
</div>
<div class="nb-cell query" name="q2">
trace,s(Sem,[mia,walks],[]),betaConvert(Sem,SemConv).
</div>
<div class="nb-cell markdown" name="md8">
Wieder gibt es die Möglichkeit sich mit =printInfix/1= das Ergebnis in Infix-Notation anzeigen zu lassen.
</div>
<div class="nb-cell query" name="q6">
s(Sem,[a,woman,walks],[]),betaConvert(Sem,SemConv),printInfix(SemConv).
</div>
<div class="nb-cell program" data-background="true" data-singleline="true" name="p6">
% printInfix/1: druckt eine in Präfix-Form gegebene Formel in Infix-Form.
printInfix(X):- numbervars(X,1,_End,[]),printInfix1(X).
printInfix1(X):- var(X), write(X),!.
printInfix1(not(X)):- write('~'), write('('), printInfix1(X), write(')'),!.
printInfix1(and(X,Y)):- write('('), printInfix1(X), write(' & '), printInfix1(Y), write(')'),!.
printInfix1(or(X,Y)):- write('('), printInfix1(X), write(' v '), printInfix1(Y), write(')'),!.
printInfix1(imp(X,Y)):- write('('), printInfix1(X), write(' > '), printInfix1(Y), write(')'),!.
printInfix1(eq(X,Y)):- write('('), printInfix1(X), write(' = '), printInfix1(Y), write(')'),!.
printInfix1(some(X, F)):- write('some ('), write_term(X,[numbervars(true)]), write(' '), printInfix1(F), write(')'),!.
printInfix1(all(X, F)):- write('all ('), write_term(X,[numbervars(true)]), write(' '), printInfix1(F), write(')'),!.
printInfix1(lam(X, F)):- write('lam '), write_term(X,[numbervars(true)]), write(' '), printInfix1(F),!.
printInfix1(app(X,Y)):- write('('), printInfix1(X), write(' @ '), printInfix1(Y), write(')'),!.
printInfix1(A):- write(A),!.
</div>
<div class="nb-cell markdown" name="md9">
**Übung:**
* Kommentiere den Block zur Anzeige der Stackentwicklung ein und betrachte den Output für Sätze wie _mia loves a woman_, _every boxer walks_ und _a woman loves every boxer_.
* Im obenstehenden Code wird keine alpha-Konversion durchgeführt. Konstruiere eine Formel, die zeigt, warum das problematisch ist.
* Schaue dir im Trace-Modus das Beispiel zur Aufsplittung des Stacks an (kommentiere vorher die Anzeige der Stackentwicklung wieder aus.
</div>
<div class="nb-cell query" name="q1">
trace, betaConvert(lam(X,app(lam(Y,run(Y)),X)),Conv).
</div>
<div class="nb-cell markdown" name="md10">
### Implementierung von alpha-Konversion
</div>
<div class="nb-cell program" data-background="true" name="p15">
/*========================================================================
Alpha Conversion (introducing substitutions)
========================================================================*/
% initializing list of substitutions and difference list of free variables
alphaConvert(F1,F2):-
alphaConvert(F1,[],[]-_,F2).
/*========================================================================
Alpha Conversion
========================================================================*/
% expression is a variable
alphaConvert(X,Sub,Free1-Free2,Y):-
var(X),
(
member(sub(Z,Y),Sub),
X==Z, !,
Free2=Free1
;
Y=X,
Free2=[X|Free1]
).
% expression is a some(_,_)
alphaConvert(Expression,Sub,Free1-Free2,some(Y,F2)):-
nonvar(Expression),
Expression = some(X,F1),
alphaConvert(F1,[sub(X,Y)|Sub],Free1-Free2,F2).
% expression is a all(_,_)
alphaConvert(Expression,Sub,Free1-Free2,all(Y,F2)):-
nonvar(Expression),
Expression = all(X,F1),
alphaConvert(F1,[sub(X,Y)|Sub],Free1-Free2,F2).
% expression is a lam(_,_)
alphaConvert(Expression,Sub,Free1-Free2,lam(Y,F2)):-
nonvar(Expression),
Expression = lam(X,F1),
alphaConvert(F1,[sub(X,Y)|Sub],Free1-Free2,F2).
% expression is a que(_,_,_) (for questions coming later in the course
% alphaConvert(Expression,Sub,Free1-Free3,que(Y,F3,F4)):-
% nonvar(Expression),
% Expression = que(X,F1,F2),
% alphaConvert(F1,[sub(X,Y)|Sub],Free1-Free2,F3),
% alphaConvert(F2,[sub(X,Y)|Sub],Free2-Free3,F4).
% expression is something else
alphaConvert(F1,Sub,Free1-Free2,F2):-
nonvar(F1),
\+ F1 = some(_,_),
\+ F1 = all(_,_),
\+ F1 = lam(_,_),
\+ F1 = que(_,_,_),
F1=..[Symbol|Args1],
alphaConvertList(Args1,Sub,Free1-Free2,Args2),
F2=.. [Symbol|Args2].
/*========================================================================
Alpha Conversion (listwise)
========================================================================*/
alphaConvertList([],_,Free-Free,[]).
alphaConvertList([X|L1],Sub,Free1-Free3,[Y|L2]):-
alphaConvert(X,Sub,Free1-Free2,Y),
alphaConvertList(L1,Sub,Free2-Free3,L2).
</div>
<div class="nb-cell markdown" name="md2">
**Aufgabe**
* Kommentiere oben im 3. Programmblock bei `betaConvert/2` die Zeile 16 ein und 17 aus und stelle erneut die Anfrage, die zuvor ein Problem für `betaConvert/2` dargestellt hat. Falls du keine Idee für eine solche Anfrage hast, dann nimm `betaConvert(app(app(lam(X,lam(Y,love(X,Y))),Y),X),SemConv).`
</div>
<div class="nb-cell query" name="q5">
</div>
<div class="nb-cell markdown" name="md12">
* Formuliere Anfragen an das Prädikat alphaConvert/2 und stelle sicher, dass du es verstanden hast. Verfolge die Anfrage im trace-Modus. Beispiel
`?- alphaConvert(all(X,love(X,Y)),Result)`.
</div>
<div class="nb-cell query" name="q4">
trace, alphaConvert(all(X,love(X,Y)),Result).
</div>
<div class="nb-cell markdown" name="md13">
* Öffne jetzt `betaConversion.pl` mit deinem lokalen Prolog-Compiler und mache dich mit dem Aufbau dieser Datei und der geladenen Module vertraut.
* Lasse die TestSuite laufen und wechsle in den Infix-Modus.
* Erweitere die TestSuite um ein eigenes Beispiel.
</div>
<div class="nb-cell html" name="htm1">
</div>
</div>