% --------------------------------------------------------------------- % $Id: options.pl,v 1.9 2002/12/02 23:22:51 vermaat Exp $ % part of Grail % % Grail author: % Richard Moot % % Refactoring, Cleanup, Fit'n'Finish: % Xander Schrijen, Gert Jan Verhoog % % % --------------------------------------------------------------------- :- object options. % --------------------------------------------------------------------- % Options % --------------------------------------------------------------------- unary_semantics(inactive). % fNf: OBSOLETE -- value of latex_output_format/1 is unused. % latex_output_format(?Format) % Format can be one of the atoms 'fitch','nd' or 'none'. This % version does not support sequent output latex_output_format(nd). % eta_long_proofs(?Flag) % Setting this flag to 'yes' will cause the eta reduction of the % natural deduction proof to be skipped. eta_long_proofs(no). % hypo_scope(?Flag) % This flag determines whether to indicate the scope of hypotheses % in a fitch style natural deduction proof by a vertical bar hypo_scope(yes). % ignore_brackets(?Mode) % Often, too many brackets will make the output unreadable. When % you are not interested in certain brackets (because they are % associative, for example, and more readable in list-like notation) % use this declaration. This will not remove associativity inferences % from the derivation. ignore_brackets('$MODE'). % never remove this clause ignore_brackets(0). ignore_brackets(a). % macro_reduce(?Flag) % If this flag is set to value 'yes', the macro definitions will % be applied in order to reduce every formula as far as possible macro_reduce(no). % output_expl_brackets(?Flag) % Setting this flag to 'no' will not output brackets when the % precedence of the operators allows this. % For example, this will produce A*B/C instead of (A*B)/C. output_expl_brackets(no). % output_labels(?Flag) % If this flag is set to value 'yes', the structure label corresponding % to each part of the proof will be displayed. output_labels(yes). % output_semantics(?Flag) % If this flag is set to value 'yes', the lambda term corresponding % to each part of the proof will be displayed. output_semantics(yes). % output_subst_lex_sem(?Flag) % If this flag is set to value 'yes', the lambda term meaning recipies % found in the lexicon will be substituted for the semantic variables % normally assigned to lexical assumptions. output_subst_lex_sem(yes). % output_reduced_sem(?Flag) % Will display only beta/eta-normal forms of lambda terms when set % to 'yes'. output_reduced_sem(yes). output_text_sem(yes). % output_sr(?Flag) % If this flag is set to 'yes', all structural rules will be displayed % explicitly. If you are only interested in the logical aspects of the % proof, set this flag to 'no'. output_sr(no). % collapse_sr(?ListOfNames,?Name) % sequences (>1) of structural (= non-logical, see logical_rule/1) % rules which are all in ListOfNames are abbreviated by a single % structural rule step labeled Name. % Examples: % collapse_sr(['Ass'],'Ass*'). Will print a sequence of 'Ass' inferences % as a single 'Ass*' step. % collapse_sr(_,'SR'). Will replace any sequence of structural % rules by a single rule named 'SR'. % collapse_sr(X,X). Will replace any sequence of structural % rules by the _multiset_ of rules used. %collapse_sr(X,X). collapse_sr('dummy argument','dummy arguments'). % boring_rule(?RuleName) % sequences of rules declared as boring (by rule name) are % abbreviated by writing a series of dots as premiss of the % last 'interesting' rule. Does not make sense when % latex_output_format is set to 'fitch' boring_rule(ax). %boring_rule(rdl(_)). %boring_rule(ldl(_)). %boring_rule(rdr(_)). %boring_rule(ldr(_)). %boring_rule(rp(_)). %boring_rule(lp(_)). %boring_rule(rdia(_)). %boring_rule(ldia(_)). %boring_rule(rbox(_)). %boring_rule(lbox(_)). boring_rule(lex). %boring_rule(hyp(_)). %boring_rule(uhyp). %boring_rule(dri(_)). %boring_rule(dre(_)). %boring_rule(dli(_,_)). %boring_rule(dle(_,_)). %boring_rule(pi(_)). %boring_rule(pe(_,_,_)). %boring_rule(boxi(_)). %boring_rule(boxe(_)). %boring_rule(diai(_)). %boring_rule(diae(_,_)). % logical_rule(?RuleName) % identifies the names of the logical rules. logical_rule(lex). logical_rule(hyp(_)). logical_rule(uhyp). logical_rule(dri(_,_)). logical_rule(dre(_)). logical_rule(dli(_,_)). logical_rule(dle(_)). logical_rule(pi(_)). logical_rule(pe(_,_,_)). logical_rule(boxi(_)). logical_rule(boxe(_)). logical_rule(diai(_)). logical_rule(diae(_,_)). :- end_object options. % --------------------------------------------------------------------- % Updated for DLP by M.Hildebrand 02/2003 % % $Id: graphs.pl,v 1.7 2002/12/02 23:22:50 vermaat Exp $ % part of Grail % % Grail author: % Richard Moot % % Refactoring, Cleanup, Fit'n'Finish: % Xander Schrijen, Gert Jan Verhoog % % % --------------------------------------------------------------------- :- object graphs : [auxiliaries,reduce_sem,tokenize,knowledge_base]. var fragment = lexicon. get_init(Init) :- get_msecs(Init). get_stop(Stop) :- get_msecs(Stop). parse_words(ListOfWords, Goal, Results) :- get_init(Init), findall(Result, parse(ListOfWords, Goal, Result), Results), get_stop(Stop), Time is (Stop - Init), format('time = ~w msecs~n', [Time]). % --------------------------------------------------------------------- % parse(+ListOfWordsOrSyn, +GoalType, ResultTerm) % % Parses ListOfWordsOrSyn as goal type GoalType; ResultTerm is the data % structure containing the Semantic Meaning. % --------------------------------------------------------------------- parse(ListOfWordsOrSyn, Goal, result(Meaning)) :- format('**goal formula is ~w~n',[Goal]), init_parser(ListOfWordsOrSyn, Goal, Meaning0, [E|Es], [], Subst, NVAR), copy_term(t(Es,E), t(Es0,E0)), prove(Es, E, Es0, E0), substitute_sem(Subst, Meaning0, Meaning1, NVAR, _), reduce_sem(Meaning1, Meaning2), rewrite_sem(Meaning2, Meaning). % --------------------------------------------------------------------- % init_parser(ListOfWords, Goal, Semantics, Label, % Edges0, Edges, Subst, NVAR) % % --------------------------------------------------------------------- init_parser(ListOfWords, Goal, Semantics, VertexEdges, Edges,Subst, NVAR) :- VertexEdges = [vertex(0,Bs,Ps)|Edges0], initial_graph(ListOfWords, 0, M, 1, N, Edges0, Edges1, Subst, []), macro_expand(Goal, G), link0(G, Semantics, _Label, 0, M, N, NVAR, Bs, [], Ps, [], Edges1, Edges). % --------------------------------------------------------------------- % initial_graph(ListOfWords, M0, M, N0, N, Edges0, Edges, Subst0, Subst) % % --------------------------------------------------------------------- initial_graph([],M,M,N,N,Es,Es,List,List). initial_graph([W|Ws],M0,M,N0,N,Vertex,Es,N0Sem,S) :- Vertex = [vertex(N0,As,Ps)|Es0], N0Sem = [N0-Sem|S0], catch_fail(lex(W,Syn0,Sem),'Lexical lookup failed: ',W), macro_expand(Syn0,Syn), M1 is M0+1, N1 is N0+1, link1(Syn,'$VAR'(N0),M0-W,M0,M1,N1,N2,As,[],Ps,[],Es0,Es1), initial_graph(Ws,M1,M,N2,N,Es1,Es,S0,S). catch_fail(Goal,_Message,_Indicator) :- lookup_attr1(lexicon, Goal), format('** ~w~n',[Goal]). catch_fail(Goal,Message,Indicator) :- member_attr_fail(lexicon, Goal), teller <- output([Message,' ',Indicator]), fail. % --------------------------------------------------------------------- % fNf: code below is still uncharted territory. % --------------------------------------------------------------------- % = antecedent types link1(lit(A),V,S,Pos0,Pos1,N,N,NegPosList,As,Ps,Ps,Es,Es) :- !, NegPosList = [neg(A,V,S,Pos0,Pos1)|As]. link1(dia(J,X),V,R,Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_dia_test(J,Pos0,Pos1,Pos2,Pos3), N1 is N0+1, link1(X,dedia(V),unzip(J,R),Pos2,Pos3,N1,N,As0,As,Ps0,Ps,Es0,Es). link1(box(J,X),V,R,Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_dia_test(J,Pos0,Pos1,Pos2,Pos3), link1(X,debox(V),zip(J,R),Pos2,Pos3,N0,N,As0,As,Ps0,Ps,Es0,Es). link1(dr(J,X,Y),U,R,Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5), link0(Y,V,S,Pos3,Pos4,N0,N1,As0,As1,Ps0,Ps1,Es0,Es1), link1(X,appl(U,V),p(J,R,S),Pos2,Pos5,N1,N,As1,As,Ps1,Ps,Es1,Es). link1(dl(J,Y,X),U,R,Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5), link0(Y,V,S,Pos5,Pos2,N0,N1,As0,As1,Ps0,Ps1,Es0,Es1), link1(X,appl(U,V),p(J,S,R),Pos4,Pos3,N1,N,As1,As,Ps1,Ps,Es1,Es). link1(p(J,X,Y),V,R,Pos0,Pos1,N0,N,As,As,[N0N1|Ps],Ps,Vertex,Es) :- !, N0N1 = N0-N1, Vertex = [vertex(N0,Bs,Qs),vertex(N1,Cs,Rs)|Es0], continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5,c(N0)), N1 is N0+1, N2 is N1+1, link1(X,fst(V),l(J,R),Pos2,Pos4,N2,N3,Bs,[],Qs,[],Es0,Es1), link1(Y,snd(V),r(J,R),Pos5,Pos3,N3,N,Cs,[],Rs,[],Es1,Es). % = succedent types link0(lit(A),V,S,Pos0,Pos1,N,N,PosList,As,Ps,Ps,Es,Es) :- !, PosList = [pos(A,V,S,Pos0,Pos1)|As]. link0(dia(J,X),condia(V),zip(J,R),Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_dia_test(J,Pos0,Pos1,Pos2,Pos3), link0(X,V,R,Pos2,Pos3,N0,N,As0,As,Ps0,Ps,Es0,Es). link0(box(J,X),conbox(V),unpack(J,R),Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_dia_test(J,Pos0,Pos1,Pos2,Pos3), link0(X,V,R,Pos2,Pos3,N0,N,As0,As,Ps0,Ps,Es0,Es). link0(dr(J,X,Y),Lambda,DR,Pos0,Pos1,N0,N,As,As,[N0N1|Ps],Ps,Vertex,Es) :- !, Lambda = lambda('$VAR'(N0),V), DR = dr(J,R,x-'$VAR'(N0)), N0N1 = N0-N1, Vertex = [vertex(N0,Bs,Qs),vertex(N1,Cs,Rs)|Es0], continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5,c(N0)), N1 is N0+1, N2 is N1+1, link1(Y,'$VAR'(N0),x-'$VAR'(N0),Pos3,Pos4,N2,N3,Bs,[],Qs,[],Es0,Es1), link0(X,V,R,Pos2,Pos5,N3,N,Cs,[],Rs,[],Es1,Es). link0(dl(J,Y,X),Lambda,DL,Pos0,Pos1,N0,N,As,As,[N0N1|Ps],Ps,Vertex,Es) :- !, Lambda = lambda('$VAR'(N0),V), DL = dl(J,x-'$VAR'(N0),R), N0N1 = N0-N1, Vertex = [vertex(N0,Bs,Qs),vertex(N1,Cs,Rs)|Es0], continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5,c(N0)), N1 is N0+1, N2 is N1+1, link0(X,V,R,Pos5,Pos3,N2,N3,Bs,[],Qs,[],Es0,Es1), link1(Y,'$VAR'(N0),x-'$VAR'(N0),Pos4,Pos2,N3,N,Cs,[],Rs,[],Es1,Es). link0(p(J,X,Y),pair(U,V),p(J,R,S),Pos0,Pos1,N0,N,As0,As,Ps0,Ps,Es0,Es) :- !, continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5), link0(Y,V,S,Pos5,Pos3,N0,N1,As0,As1,Ps0,Ps1,Es0,Es1), link0(X,U,R,Pos2,Pos4,N1,N,As1,As,Ps1,Ps,Es1,Es). continuous_dia_test(J,Pos0,Pos1,Pos2,Pos3) :- call(fragment, continuous_dia(J)), Pos2=Pos0, Pos3=Pos1, !. continuous_dia_test(_J,_0,_1,_2,_3). continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5) :- call(fragment, continuous(J)), Pos2=Pos0, Pos3=Pos1, Pos4=Pos5, !. continuous_test(_J,_0,_1,_2,_3,_4,_5). continuous_test(J,Pos0,Pos1,Pos2,Pos3,Pos4,Pos5,N) :- call(fragment, continuous(J)), Pos2=Pos0, Pos3=Pos1, Pos4=N, Pos5=N, !. continuous_test(_J,_0,_1,_2,_3,_4,_5,_N). % ============================================================ % Resolution % ============================================================ prove([],vertex(_,[],[]),_,_) :- !. prove([G0|Gs0],G,[H0|Hs0],H) :- select_atom(neg(A,V,S0,P0,P1),vertex(N,As,Ps), neg(A,W,S1,P0,P1),vertex(N,A1s,Ps), [G,G0|Gs0],Gs1,[H,H0|Hs0],Hs1), select_conj(neg(A,V,S,P0,P1),vertex(M,Bs,Qs), neg(A,W,S1,P0,P1),vertex(M,B1s,Qs), Gs1,Gs2,Hs1,Hs2), \+ cyclic(vertex(N,As,Ps),vertex(M,Bs,Qs),Gs2), merge_vertices(vertex(N,As,Ps),vertex(M,Bs,Qs),Gs2,Gs3), merge_vertices(vertex(N,A1s,Ps),vertex(M,B1s,Qs),Hs2,Hs3), reduce_graph(Gs3,[G4|Gs4]), reduce_graph(Hs3,[H4|Hs4]), remove_divisions(S0,S), prove(Gs4,G4,Hs4,H4). select_atom(neg(B,V,S,P0,P1),vertex(N,[],[]), neg(B,W,S1,P0,P1),vertex(N,[],[]),G0,G,H0,H) :- duo_select(vertex(N,[neg(B,V,S,P0,P1)],[]), vertex(N,[neg(B,W,S1,P0,P1)],[]),G0,G,H0,H), ground(S), !. select_conj(neg(B,V,S,P0,P1),vertex(N,As,Ps), neg(B,W,S1,P0,P1),vertex(N,Cs,Ps),G0,G,H0,H) :- duo_select(vertex(N,[A|As0],Ps), vertex(N,[C|Cs0],Ps),G0,G,H0,H), duo_select(pos(B,V,S,P2,P3), pos(B,W,S1,P2,P3),[A|As0],As,[C|Cs0],Cs), P0=P2, P1=P3. % ============================================================ % Graph Reductions % ============================================================ % = reduce_graph(+OldGraph,-ReducedGraph) % % the graph is reduced according to Danos' graph contraction % condition. If a vertex N is found from which both destinations % of a par pair reach the same par link M, then vertices M and N % are identified. This proceeds until no more reductions can be % performed. The final graph is checked for connectedness. reduce_graph(G0,G) :- select(vertex(N,As,Ps0),G0,G1), select(M-M,Ps0,Ps), !, select(vertex(M,Bs,Qs),G1,G2), merge_vertices(vertex(N,As,Ps),vertex(M,Bs,Qs),G2,G3), reduce_graph(G3,G). reduce_graph(G,G) :- connected(G). % = merge_vertices(+Vertex1,+Vertex2,+OldGraph,-NewGraph) % % Vertex1 and Vertex2 are merged into a single vertex, with the vertex % id of Vertex1 and all references to the id of Vertex2 are replaced % by references to Vertex1. merge_vertices(vertex(N,As,Ps),vertex(M,Bs,Qs),G0,Vertex) :- Vertex = [vertex(N,Cs,Rs)|G], append(Bs,As,Cs), append(Qs,Ps,Rs), replace_edges(G0,M,N,G). % = replace_edges(+OldGraph,VertexId1,VertexId2,-NewGraph) % % All references to VertexId1 in OldGraph are replaced by references % to VertexId2 in NewGraph. replace_edges([],_,_,[]) :- !. replace_edges(Vertex1,X,Y,Vertex2) :- Vertex1 = [vertex(N,As,Ps)|Ls], Vertex2 = [vertex(N,As,Qs)|Ms], replace_edges1(Ps,X,Y,Qs), replace_edges(Ls,X,Y,Ms). replace_edges1([],_,_,[]) :- !. replace_edges1([P1P2|Ps],X,Y,[Q1Q2|Qs]) :- P1P2 = P1-P2, Q1Q2 = Q1-Q2, replace_vertex(P1,X,Y,Q1), replace_vertex(P2,X,Y,Q2), replace_edges1(Ps,X,Y,Qs). replace_vertex(V,X,Y,W) :- V=X, !, W=Y. replace_vertex(V,_X,_Y,W) :- W=V. % = connected(+Graph) % % true if it is still possible to make Graph connected through % performing axiom links. % A graph with a single vertex is connected. A vertex which does not % have atomic formulas (and therefore will not be further connected % to other vertices) is only connected if it has at least one par pair connected([_]) :- !. connected(L) :- connected1(L). connected1(Vertex) :- Vertex = [vertex(_,As,Ps)|R], As = [], !, Ps = [_|_], connected1(R). connected1(Vertex) :- Vertex = [vertex(_,_As,_Ps)|R], !, connected1(R). connected1([]). % = cyclic(+Vertex1,+Vertex2,+Graph) % true if linking Vertex1 and Vertex2 in Graph will produce % a cycle for some switching of Graph. % - If Vertex1 and Vertex2 don't have a common ancestor, linking % them won't produce a cycle. % - If Vertex1 and Vertex2 have a common ancestor, linking them % will produce a cycle unless they are on different branches % of a par link. cyclic(E1,E2,G0) :- select(A,[E1,E2|G0],G1), ancestor(A,E1,G1,_,Path1,[]), ancestor(A,E2,G1,_,Path2,[]), !, \+ branches(Path1,Path2). branches([X|_Xs],[Y|_Ys]) :- X=l(P),Y=r(P), !. branches([X|_Xs],[Y|_Ys]) :- X=r(P),Y=l(P), !. branches([X|Xs],[Y|Ys]) :- X=Y, !, branches(Xs,Ys). ancestor(vertex(N,_,_Ps),vertex(M,_,_Rs),_G0,_G,L0,L) :- N=M, L=L0, !. ancestor(vertex(_N,_,Ps),vertex(M,_,Rs),G0,G,L0,L) :- Ps=[P1-P2|_Ps0], select(vertex(P1,_,Qs),G0,G1), L0=[l(P1-P2)|L1], !, ancestor(vertex(P1,_,Qs),vertex(M,_,Rs),G1,G,L1,L). ancestor(vertex(_N,_,Ps),vertex(M,_,Rs),G0,G,L0,L) :- Ps=[P1-P2|_Ps0], select(vertex(P2,_,Qs),G0,G1), L0=[r(P1-P2)|L1], !, ancestor(vertex(P2,_,Qs),vertex(M,_,Rs),G1,G,L1,L). ancestor(vertex(N,_,Ps),vertex(M,_,Rs),G0,G,L0,L) :- Ps=[_P1-_P2|Ps0], ancestor(vertex(N,_,Ps0),vertex(M,_,Rs),G0,G,L0,L). % ============================================================ % Label Reductions % ============================================================ % = normalize(+Label,-NormalLabel) % perform label reductions and rewrite according to % structural postulates until a normal label results. % search is breadth first with closed set, and succeeds only once. % solution(Label) = normal(Label) % child(Parent,Child) = rewrite(Parent,Child) normalize(Start0,Answer) :- remove_divisions(Start0,Start), breadth_star1([],1,[Start|B],B,node(Start,0,empty,empty),Answer). % normalize(+Label,+NormalLabel,-PathHead,?PathTail) % as normalize/2 but now with dl pair representing path to solution normalize(S0,S,Path0,Path) :- remove_divisions(S0,S1,Path0,Path1), breadth_first_search(S1,S,Path1,Path), !. % = normal(+Label) % a label is normal if all occurences of unzip, unpack, % dl, dr, l and r have been reduced, the words are in the % right order, and it contains no grammar-internal modes. % normal labels can contain logical constants of the form x-X normal(Label) :- normal(Label,-1,_). normal(M-_,N0,N) :- M=x, !, N=N0. normal(M-_,N0,N) :- !, M is N0+1, N=M. normal(p(I,A,B),N0,N) :- call(fragment, external(I)), normal(A,N0,N1), normal(B,N1,N). normal(zip(I,A),N0,N) :- call(fragment, external_dia(I)), normal(A,N0,N). % = select_divisions(+Label,-LabelWithHole,-DList) % when called with a Label select divisions will return a copy of that % label with a hole on the place of the divisions in it, and a % difference list containing Division-Hole pairs. The pairs are % ordered in such a way that a Division is ground when all Holes % before it one the list are filled select_divisions(N-W,N-W,[]) :- !. select_divisions(zip(I,A0),zip(I,A),L) :- !, select_divisions(A0,A,L). select_divisions(unzip(I,A0),unzip(I,A),L) :- !, select_divisions(A0,A,L). select_divisions(unpack(I,A0),H,L) :- !, select_divisions(A0,A,L1), [unpack(I,A)-H] = L2, append(L1,L2,L). select_divisions(dr(I,A0,V),H,L) :- !, select_divisions(A0,A,L1), [dr(I,A,V)-H] = L2, append(L1,L2,L). select_divisions(dl(I,V,A0),H,L) :- !, select_divisions(A0,A,L1), [dl(I,V,A)-H] = L2, append(L1,L2,L). select_divisions(p(I,A0,B0),p(I,A,B),L) :- !, select_divisions(A0,A,L1), select_divisions(B0,B,L2), append(L1,L2,L). select_divisions(l(I,A0),l(I,A),L) :- !, select_divisions(A0,A,L). select_divisions(r(I,A0),r(I,A),L) :- !, select_divisions(A0,A,L). % remove_divisions(+Label,-DivFreeLabel) % remove all dr, dl occurences from label % first select_divisions/4 is called, which returns a (possibly % non-ground) DivFreeLabel and a difference-list containing % Division-Hole pairs remove_divisions(S0,S) :- select_divisions(S0,S1,L), remove_divisions1(L,S1,S). % = remove_divisions(+ListOfDHPairs,?LabelWithHole,-GroundLabel) % successively remove the divisions from the list of pairs and put % them back in the corresponding holes remove_divisions1([],S0,S) :- !, breadth_star([],1,[S0|B],B,node(S0,0,empty,empty),S). % check lp even if there are no divisions remove_divisions1([DH|Rest],S0,S) :- DH = D-H, breadth_star([],1,[D|B],B,node(D,0,empty,empty),H), remove_divisions1(Rest,S0,S). % FnF: no comment for remove_divisions/4 ? remove_divisions(S0,S,Path0,Path) :- select_divisions(S0,S1,L), remove_divisions1(L,S1,S,Path0,Path). remove_divisions1([],S0,S,Path0,Path) :- !, breadth_first_search1(S0,S,Path0,Path). remove_divisions1([DH|Rest],S0,S,Path0,Path) :- DH = D-H, breadth_first_search1(D,H,Path0,Path1), remove_divisions1(Rest,S0,S,Path1,Path). % breadth first search which returns dl path to solution % because we know there is a solution we represent the Open % set as a dl instead of a queue breadth_first_search(Start,Answer,Path0,Path) :- breadth_star([],1,[Start/[]|Rest],Rest,[Start],[],RevPath,Answer), reverse_dl(RevPath,Path0,Path). breadth_first_search1(Start,Answer,Path0,Path) :- breadth_star([],1,[Start/[]|Rest],Rest,[Start],[],RevPath,Answer), check_lp1(Answer), reverse_dl(RevPath,Path0,Path). % search is breadth first with closed set, and succeeds only once % % solution(Label) = check_lp(Label) % child(Parent,Child) = rewrite(Parent,Child) % = breadth_star(+NewChildren,+QLength,+QFront,+QBack,+Closed,?Answer) breadth_star([],N0,[Node|_F],_B,_Closed,Answer) :- N0 > 0, check_lp(Node), !, Answer = Node. breadth_star([],N0,[Node|F],B,Closed,Answer) :- N0 > 0, N is N0-1, !, children(Node,Children), union(Children,Closed,Closed1,Children1,[]), breadth_star(Children1,N,F,B,Closed1,Answer). breadth_star([X|Xs],N0,F,[X|B],Closed,Answer) :- N is N0+1, breadth_star(Xs,N,F,B,Closed,Answer). % FnF: no comment for breadth_star/8 breadth_star([],N0,[NodeNodePath|_Front],_Back,_Closed,_NodePath0,RevPath,Answer) :- NodeNodePath = Node/NodePath, N0 > 0, Answer = Node, RevPath = NodePath, !. breadth_star([],N0,[NodeNodePath|Front],Back,Closed,_NodePath0,RevPath,Answer) :- NodeNodePath = Node/NodePath, N0 > 0, N is N0-1, !, labelled_children(Node,Children), lb_ord_union(Closed,Children,Closed1,Children1), breadth_star(Children1,N,Front,Back,Closed1,NodePath,RevPath,Answer). breadth_star([ChildLabel|Children],N0,F,[ChildLabelPath|B],Closed, Path,RevPath,Answer) :- ChildLabel = Child-Label, ChildLabelPath = (Child/[Label|Path]), N is N0+1, breadth_star(Children,N,F,B,Closed,Path,RevPath,Answer). breadth_star1([],N0,[Node|_F],_B,_Closed,Answer) :- N0 > 0, normal(Node), !, Answer = Node. breadth_star1([],N0,[Node|F],B,Closed,Answer) :- N0 > 0, N is N0-1, !, children(Node,Children), union(Children,Closed,Closed1,Children1,[]), breadth_star1(Children1,N,F,B,Closed1,Answer). breadth_star1([X|Xs],N0,F,[X|B],Closed,Answer) :- N is N0+1, breadth_star1(Xs,N,F,B,Closed,Answer). % = Linear precedence % = check_lp(+Label) % % true if the words in Label are in the order they appear in the % input list of words. This is only checked for modes which are % declares as transparent, since it's not necessarily true that % we can put the words in the right order immediately. check_lp(Node) :- check_lp(Node,x,_). % check_lp(+Node,+GreaterThan,-Max) check_lp(N-_,X,Y) :- N = x, !, X = Y. check_lp(N-_,X,Y) :- precedes(X,N), !, N = Y. check_lp(p(I,A,B),N0,N) :- call(fragment, transparent(I)), !, check_lp(A,N0,N1), check_lp(B,N1,N). check_lp(p(_I,A,B),_N0,_N) :- !, check_lp(A,x,_),check_lp(B,x,_). check_lp(zip(I,A),N0,N) :- call(fragment, transparent_dia(I)), !, check_lp(A,N0,N). check_lp(zip(_I,A),_N0,_N) :- !, check_lp(A,x,_). check_lp(unzip(_,A),N0,N) :- !, check_lp(A,N0,N). check_lp(unpack(_,A),N0,N) :- check_lp(A,N0,N). check_lp(dl(_,_,A),N0,N) :- !, check_lp(A,N0,N). check_lp(dr(_,A,_),N0,N) :- !, check_lp(A,N0,N). check_lp(l(_,A),N0,N) :- !, check_lp(A,N0,N). check_lp(r(_,A),N0,N) :- !, check_lp(A,N0,N). % = check_lp1(_-_) :- !. check_lp1(zip(_,A)) :- !, check_lp1(A). check_lp1(p(_,A,B)) :- !, check_lp1(A), check_lp1(B). check_lp1(l(_,A)) :- !, check_lp1(A). check_lp1(r(_,A)) :- !, check_lp1(A). check_lp1(unzip(_,A)) :- !, check_lp1(A). % = children/2 will generate a set of children from a given parent. children(ParentNode,ChildrenNodes) :- findall(ChildNode,rewrite(ParentNode,ChildNode),ChildrenNodes). labelled_children(ParentNode,ChildrenSet) :- findall(ChildNode-Label,rewrite(ParentNode,ChildNode,Label),ChildrenNodes), keysort(ChildrenNodes,ChildrenSet). % = add_children([],_,L,L) :- !. add_children([ChildLabel|Children],Path,[ChildLabelPath|L0],L) :- ChildLabel = Child-Label, ChildLabelPath = (Child/[Label|Path]), add_children(Children,Path,L0,L). % = % rewrite(+Label0,?Label) % true if Label0 is obtainable from Label in a single residuation % reduction or postulate rewrite rewrite(D,D1) :- reduce(D,D1), !. rewrite(D,D1) :- call(fragment, postulate(D,D1,_Name)), !. rewrite(unpack(J,D),unpack(J,D1)) :- !, rewrite(D,D1). rewrite(unzip(J,D),unzip(J,D1)) :- !, rewrite(D,D1). rewrite(zip(J,D),zip(J,D1)) :- !, rewrite(D,D1). rewrite(l(J,D),l(J,D1)) :- !, rewrite(D,D1). rewrite(r(J,D),r(J,D1)) :- !, rewrite(D,D1). rewrite(p(J,D,G),p(J,D1,G)) :- rewrite(D,D1). rewrite(p(J,G,D),p(J,G,D1)) :- !, rewrite(D,D1). rewrite(dr(J,D,G),dr(J,D1,G)) :- !, rewrite(D,D1). rewrite(dl(J,G,D),dl(J,G,D1)) :- !, rewrite(D,D1). % rewrite(+Label0,?Label,?Name) % true if Label0 is obtainable from Label in a single residuation % reduction or postulate rewrite by applying the rule indicated % by Name rewrite(unpack(J,D0),unpack(J,D),L) :- !, rewrite(D0,D,L). rewrite(unzip(J,D0),unzip(J,D),L) :- !, rewrite(D0,D,L). rewrite(zip(J,D0),zip(J,D),L) :- !, rewrite(D0,D,L). rewrite(l(J,D0),l(J,D),L) :- !, rewrite(D0,D,L). rewrite(r(J,D0),r(J,D),L) :- !, rewrite(D0,D,L). rewrite(p(J,D0,G),p(J,D,G),L) :- rewrite(D0,D,L). rewrite(p(J,G,D0),p(J,G,D),L) :- !, rewrite(D0,D,L). rewrite(dr(J,D0,G),dr(J,D,G),L) :- !, rewrite(D0,D,L). rewrite(dl(J,G,D0),dl(J,G,D),L) :- !, rewrite(D0,D,L). rewrite(D0,D,D0) :- reduce(D0,D), !. rewrite(D0,D,sr(Name,D0,D)) :- call(fragment, postulate(D0,D,Name)), !. % = Residuation reductions reduce(p(J,LJD,RJD),D) :- % product !, LJD = l(J,D), RJD = r(J,D). reduce(dr(J,PJGD,D),G) :- % division right PJGD = p(J,G,D), !. reduce(dl(J,D,PJDG),G) :- % division left PJDG = p(J,D,G), !. reduce(zip(J,UNZIP),D) :- % diamond !, UNZIP = unzip(J,D). reduce(unpack(J,ZIP),D) :- % box !, ZIP = zip(J,D). % ============================================================ % Auxiliaries % ============================================================ generate_antecedent(L-W,L-W) :- !. generate_antecedent(p(I,X,Y),sp(I,A,B)) :- !, generate_antecedent(X,A), generate_antecedent(Y,B). generate_antecedent(zip(I,X),sdia(I,A)) :- !, generate_antecedent(X,A). reverse_dl([],Y,Y) :- !. reverse_dl([X|Xs],Ys,Zs) :- reverse_dl(Xs,Ys,[X|Zs]). % = duo_select(X,Y,[X|Xs],Xs,[Y|Ys],Ys). duo_select(V,W,[X|Xs],[X|Vs],[Y|Ys],[Y|Ws]) :- duo_select(V,W,Xs,Vs,Ys,Ws). % lb_ord_union/4 is ord_union/4 (form Quintus library(ordsets) % where NewSet and ReallyNew are Item-Label pairs and OldSet and % Union lists of Items % lb_ord_union(+OldSet, +NewSet, ?Union, ?ReallyNew) % is true when Union is NewSet U OldSet and ReallyNew is NewSet \ OldSet. % This is useful when you have an iterative problem, and you're adding % some possibly new elements (NewSet) to a set (OldSet), and as well as % getting the updated set (Union) you would like to know which if any of % the "new" elements didn't already occur in the set (ReallyNew). lb_ord_union([], Set2, Set2, Set2) :- !. lb_ord_union([Head1|Tail1], Set2, Union, New) :- lb_ord_union_1(Set2, Head1, Tail1, Union, New). lb_ord_union_1([], Head1, Tail1, [Head1|Tail1], []) :- !. lb_ord_union_1([Head2Label|Tail2], Head1, Tail1, Union, New) :- Head2Label = Head2-Label, compare(Order, Head1, Head2), lb_ord_union(Order, Head1, Tail1, Label, Head2, Tail2, Union, New). lb_ord_union(<, Head1, Tail1, Label, Head2, Tail2, [Head1|Union], New) :- !, lb_ord_union_2(Tail1, Label, Head2, Tail2, Union, New). lb_ord_union(>, Head1, Tail1, Label, Head2, Tail2, [Head2|Union], [Head2Label|New]) :- !, Head2Label = Head2-Label, lb_ord_union_1(Tail2, Head1, Tail1, Union, New). lb_ord_union(=, Head1, Tail1, _, _, Tail2, [Head1|Union], New) :- !, lb_ord_union(Tail1, Tail2, Union, New). lb_ord_union_2([], Label, Head2, Tail2, [Head2|Tail2], [Head2Label|Tail2]) :- !, Head2Label = Head2-Label. lb_ord_union_2([Head1|Tail1], Label, Head2, Tail2, Union, New) :- compare(Order, Head1, Head2), lb_ord_union(Order, Head1, Tail1, Label, Head2, Tail2, Union, New). % expand macro definitions macro_expand(S0,S) :- apply_macro(S0,S1), !, macro_expand(S1,S). macro_expand(S,S). % reduce macro definitions macro_reduce(S0,S) :- apply_macro(S1,S0), !, macro_reduce(S1,S). macro_reduce(S,S). apply_macro(dia(I,S0),dia(I,S)) :- !, apply_macro(S0,S). apply_macro(box(I,S0),box(I,S)) :- !, apply_macro(S0,S). apply_macro(p(I,R0,S),p(I,R,S)) :- apply_macro(R0,R). apply_macro(p(I,R,S0),p(I,R,S)) :- !, apply_macro(S0,S). apply_macro(dl(I,R0,S),dl(I,R,S)) :- apply_macro(R0,R). apply_macro(dl(I,R,S0),dl(I,R,S)) :- !, apply_macro(S0,S). apply_macro(dr(I,R0,S),dr(I,R,S)) :- apply_macro(R0,R). apply_macro(dr(I,R,S0),dr(I,R,S)) :- !, apply_macro(S0,S). apply_macro(S0,S) :- call(fragment, macro(S0,S)), !. apply_macro(S,lit(S)) :- literal(S), !. % = literal(+Syn) % true if Syn abbreviates lit(Syn), i.e. is a basic syntactic category literal(X) :- atom(X), !. %literal(X) :- % atomic_formula(X). :- end_object graphs. % --------------------------------------------------------------------- % $Id: reduce_sem.pl,v 1.10 2002/12/04 21:17:45 gjv Exp $ % part of Grail % % Grail author: % Richard Moot % % Refactoring, Cleanup, Fit'n'Finish: % Xander Schrijen, Gert Jan Verhoog % % % --------------------------------------------------------------------- :- object reduce_sem : [options,auxiliaries]. % --------------------------------------------------------------------- % Lambda term normalization % --------------------------------------------------------------------- reduce_sem(Term0,Term) :- reduce_sem1(Term0,Term1), !, reduce_sem(Term1,Term). reduce_sem(Term,Term). reduce_sem1(appl(Lambda,Y),T) :- Lambda = lambda(X,T0), !, replace_sem(T0,X,Y,T). reduce_sem1(Lambda,F) :- Lambda = lambda(X,appl(F,X)), !. reduce_sem1(fst(Pair),T) :- !, Pair = pair(T,_). reduce_sem1(snd(Pair),T) :- !, Pair = pair(_,T). reduce_sem1(Pair,T) :- Pair = pair(fst(T),snd(T)), !. reduce_sem1(condia(Dedia),T) :- !, Dedia = dedia(T). reduce_sem1(dedia(Condia),T) :- !, Condia = condia(T). reduce_sem1(conbox(Debox),T) :- !, Debox = debox(T). reduce_sem1(debox(Conbox),T) :- !, Conbox = conbox(T). reduce_sem1(condia(T),T) :- unary_semantics(inactive), !. reduce_sem1(dedia(T),T) :- unary_semantics(inactive), !. reduce_sem1(conbox(T),T) :- unary_semantics(inactive), !. reduce_sem1(debox(T),T) :- unary_semantics(inactive), !. % = DRS merge; simply appends contexts and conditions reduce_sem1(Merge,drs(Z,E)) :- Merge = merge(drs(X,C),drs(Y,D)), !, append(X,Y,Z0), sort(Z0,Z), append(C,D,E). % = recursive case reduce_sem1(T,U) :- T =.. [F|Ts], reduce_list(Ts,Us), U =.. [F|Us]. reduce_list([T|Ts],[U|Ts]) :- reduce_sem1(T,U), !. reduce_list([T|Ts],[T|Us]) :- reduce_list(Ts,Us). replace_sem(X,X,Y,Y) :- !. replace_sem(U,X,Y,V) :- functor(U,F,N), functor(V,F,N), replace_sem(N,U,X,Y,V). replace_sem(0,_,_,_,_) :- !. replace_sem(N0,U,X,Y,V) :- N0>0, N is N0-1, arg(N0,U,A), replace_sem(A,X,Y,B), arg(N0,V,B), replace_sem(N,U,X,Y,V). substitute_sem(L,T0,T) :- substitute_sem(L,T0,T,0,_). substitute_sem(_, _, _, 0). substitute_sem(L, T0, T, NVAR) :- substitute_sem(L, T0, T, NVAR, _). substitute_sem([],T,T,N,N) :- !. substitute_sem([XU|Rest],T0,T,N0,N) :- XU = X-U, numbervars(U,N0,N1), replace_sem(T0,'$VAR'(X),U,T1), substitute_sem(Rest,T1,T,N1,N). rewrite_sem(appl(T1,T2), Term) :- !, rewrite_sem(T1, Term1), rewrite_sem(T2, Term2), Term1 =.. [F|Args], Term =.. [F,Term2|Args]. rewrite_sem(append(S1,S2,S3), S) :- !, atom_list_concat([S1,S2,S3], S). rewrite_sem(quant(Q,X,T), quant(Q,X,Term)) :- !, rewrite_sem(T, Term). rewrite_sem(lambda(X, T), lambda(X, Term)) :- !, rewrite_sem(T, Term). rewrite_sem(bool(T1,Con,T2), bool(Term1,Con,Term2)) :- !, rewrite_sem(T1, Term1), rewrite_sem(T2, Term2). rewrite_sem(X, X) :- atom(X), !. rewrite_sem('$VAR'(X), '$VAR'(X)). :- end_object reduce_sem. :- object tokenize. tokenize(Atom, List, EndMark) :- atom_to_string(Atom, String), string_length(String, Length), tokenize_words(String, 0,0,Length, List, EndMark). tokenize_words(_String, _Start, Current, End, _List, _Type) :- Current == End, !, teller <- output('no endmark (!,?,.) found'), fail. tokenize_words(String, _Start, Current, End, _List, _Type) :- string_char_at(String, Current, C), member(C, ['?','!','.']), End1 is End - 1, Current < End1, !, teller <- output('Endmark in middle of sentence'), fail. tokenize_words(String, Start, Current, _End, [], C) :- string_char_at(String, Current, C), member(C, ['?','!','.']), Start == Current, !. tokenize_words(String, Start, Current, _End, [Atom], C) :- string_char_at(String, Current, C), member(C, ['?','!','.']), !, substring(String, Start, Current, Word), string_to_atom(Word, Atom). tokenize_words(String, Start, Current, End, [Atom|Rest], Type) :- string_char_at(String, Current, C), C == ' ', !, Next is Current + 1, substring(String, Start, Current, Word), string_to_atom(Word, Atom), tokenize_words(String, Next, Next, End, Rest, Type). tokenize_words(String, Start, Current, End, List, Type) :- string_char_at(String, Current, C), C == ',', !, Next is Current + 1, tokenize_words(String, Start, Next, End, List, Type). tokenize_words(String, Start, Current, End, List, Type) :- Next is Current + 1, tokenize_words(String, Start, Next, End, List, Type). :- end_object tokenize. % --------------------------------------------------------------------- % $Id: auxiliaries.pl,v 1.9 2002/12/02 23:22:49 vermaat Exp $ % part of Grail % % Grail author: % Richard Moot % % Refactoring, Cleanup, Fit'n'Finish: % Xander Schrijen, Gert Jan Verhoog % % % --------------------------------------------------------------------- :- object auxiliaries. % calculate the number of tabs necessary to print a list % of numbers right-justified. calculate_tabs([X|Xs],Tabs) :- max_size(Xs,X,Max), num_tabs([X|Xs],Max,Tabs). num_tabs([],_,[]). num_tabs([X|Xs],Max,[T|Ts]) :- Y is X // 10, size(Y,1,N), T is Max-N, num_tabs(Xs,Max,Ts). max_size([],X,M) :- Y is X // 10, size(Y,1,M). max_size([X|Xs],Y,M) :- Z is max(X,Y), max_size(Xs,Z,M). size(0,N0,N) :- !, M is (N0-1) // 3, N is N0+M. size(X,N0,M) :- X>0, Y is X // 10, N is N0+1, size(Y,N,M). % = time(+Call) % print time used to find the first solution (if any) to Call time(Call) :- statistics(runtime,[T0|_]), call1(Call), statistics(runtime,[T|_]), Time is (T-T0)*0.001, write('CPU Time used: '),write(Time),nl. % = call1(Goal) % call goal once, succeed always call1(Call) :- call(Call),!. call1(_). % = more list handling tail([],X,X,[]). tail([Y|Ys],Z,X,[Z|Zs]) :- tail(Ys,Y,X,Zs). reverse([],L,L). reverse([X|Xs],Ys,Zs) :- reverse(Xs,[X|Ys],Zs). % precedes(+LPNumber0,+LPNumber) % true if LPNumber0 precedes LPNumber. LPNumbers can be either a % number or the constant 'x' which stands for an unknown position precedes(x,_) :- !. precedes(X,Y) :- X @=< Y. % also includes precedes(Num,x) % = member_check(X,[X|_]) :- !. member_check(X,[_|Ys]) :- member_check(X,Ys). union([],AVL,AVL,RN,RN). union([X|Xs],AVL0,AVL,RN0,RN) :- insert(AVL0,X,AVL1,RN0,RN1,_), union(Xs,AVL1,AVL,RN1,RN). insert(empty, Key, node(Key,0,empty,empty), [Key|RN], RN, 1). insert(node(K,B,L,R), Key, Result, RN0, RN, Delta) :- compare(O, Key, K), insert(O, Key, Result, Delta, K, B, L, R, RN0, RN). insert(=, Key, node(Key,B,L,R), 0, _, B, L, R, RN, RN). insert(<, Key, Result, Delta, K, B, L, R, RN0, RN) :- insert(L, Key, Lavl, RN0, RN, Ldel), Delta is \(B) /\ Ldel, % this grew iff left grew and was balanced B1 is B-Ldel, ( B1 =:= -2 -> % rotation needed Lavl = node(Y,OY,A,CD), ( OY =< 0 -> NY is OY+1, NK is -NY, Result = node(Y,NY,A,node(K,NK,CD,R)) ;/* OY = 1, double rotation needed */ CD = node(X,OX,C,D), NY is 0-((1+OX) >> 1), NK is (1-OX) >> 1, Result = node(X,0,node(Y,NY,A,C),node(K,NK,D,R)) ) ; Result = node(K,B1,Lavl,R) ). insert(>, Key, Result, Delta, K, B, L, R, RN0, RN) :- insert(R, Key, Ravl, RN0, RN, Rdel), Delta is \(B) /\ Rdel, % this grew iff right grew and was balanced B1 is B+Rdel, ( B1 =:= 2 -> % rotation needed Ravl = node(Y,OY,AC,D), ( OY >= 0 -> NY is OY-1, NK is -NY, Result = node(Y,NY,node(K,NK,L,AC),D) ;/* OY = -1, double rotation needed */ AC = node(X,OX,A,C), NY is (1-OX) >> 1, NK is 0-((1+OX) >> 1), Result = node(X,0,node(K,NK,L,A),node(Y,NY,C,D)) ) ; Result = node(K,B1,L,Ravl) ). % ============================================================ % File I/O % ============================================================ %generate_file_name(Dir,File,DirFile) :- % name(Dir,DirS), % name(File,FileS), % append(DirS,[47|FileS],DirFileS), % name(DirFile0,DirFileS), % canonicalize_path(DirFile0,DirFile). :- end_object auxiliaries.