2:- module(betaConversionDRT,[betaConvert/2]). 3
4:- use_module(boxer(alphaConversionDRT),[alphaConvertDRS/2]). 5:- use_module(boxer(mergeDRT),[mergeDrs/2]). 6:- use_module(semlib(errors),[warning/2]). 7:- use_module(semlib(options),[option/2]). 8
9
13
14betaConvert(X,Y):- betaConvert(X,Y,[]), !.
15
16betaConvert(X,X):- warning('beta-conversion failed for ~p',[X]).
17
18
22
23betaConvert(X,Y,[]):- var(X), !, Y=X.
24
25betaConvert(X,Y,L):- var(X), !, wrapArguments(L,X,Y).
26
27betaConvert(app(Functor,Argument),Result,Stack):-
28 nonvar(Functor), !,
29 alphaConvertDRS(Functor,Converted),
30 betaConvert(Argument,ConArg), 31 betaConvert(Converted,Result,[ConArg|Stack]).
32
33betaConvert(lam(X,Formula),Result,[X|Stack]):- !,
34 betaConvert(Formula,Result,Stack).
35
36betaConvert(lam(X,Formula),lam(X,Result),[]):- !,
37 betaConvert(Formula,Result).
38
39betaConvert(merge(B1,B2),Result,[]):- !,
40 betaConvert(B1,K1),
41 betaConvert(B2,K2),
42 mergeDrs(merge(K1,K2),Result).
43
44betaConvert(sdrs([],C),sdrs([],C),[]):- !.
45
46betaConvert(sdrs([B1|L1],C1),Result,[]):- !,
47 betaConvert(B1,B2),
48 betaConvert(sdrs(L1,C1),sdrs(L2,C2)),
49 mergeDrs(sdrs([B2|L2],C2),Result).
50
51betaConvert(lab(X,B1),lab(X,B2),[]):- !,
52 betaConvert(B1,B2).
53
54betaConvert(sub(B1,B3),sub(B2,B4),[]):- !,
55 betaConvert(B1,B2),
56 betaConvert(B3,B4).
57
58betaConvert(B1:drs(D1,C1),B1:drs(D2,C3),[]):-
59 option('--elimeq',true),
60 select(_:[]:eq(X1,Y1),C1,C2),
61 select(B2:[]:Y2,D1,D2), B1==B2, Y1==Y2, !, X1=Y1,
62 betaConvertConditions(C2,C3).
63
64betaConvert(B:drs(D,C1),B:drs(D,C2),[]):- !,
65 betaConvertConditions(C1,C2).
66
67betaConvert(alfa(T,B1,B2),Result,[]):- !,
68 betaConvert(B1,K1),
69 betaConvert(B2,K2),
70 mergeDrs(alfa(T,K1,K2),Result).
71
72betaConvert(app(B1,B2),app(K1,K2),[]):- !,
73 betaConvert(B1,K1),
74 betaConvert(B2,K2).
75
76betaConvert(X,Y,L):- !,
77 wrapArguments(L,X,Y).
78
79
83
84betaConvertConditions([],[]).
85
86betaConvertConditions([B:I:C1|L1],[B:I:C2|L2]):- !,
87 betaConvertCond(C1,C2),
88 betaConvertConditions(L1,L2).
89
90
94
95betaConvertCond(not(A1),not(B1)):- !, betaConvert(A1,B1).
96betaConvertCond(pos(A1),pos(B1)):- !, betaConvert(A1,B1).
97betaConvertCond(nec(A1),nec(B1)):- !, betaConvert(A1,B1).
98betaConvertCond(prop(X,A1),prop(X,B1)):- !, betaConvert(A1,B1).
99betaConvertCond(or(A1,A2),or(B1,B2)):- !, betaConvert(A1,B1), betaConvert(A2,B2).
100betaConvertCond(imp(A1,A2),imp(B1,B2)):- !, betaConvert(A1,B1), betaConvert(A2,B2).
101betaConvertCond(duplex(T,A1,X,A2),duplex(T,B1,X,B2)):- !, betaConvert(A1,B1), betaConvert(A2,B2).
102betaConvertCond(C,C).
103
104
108
109wrapArguments([],X,X).
110
111wrapArguments([A|L],X,Y):- wrapArguments(L,app(X,A),Y)