/***************************************************************************** Prolog Implementation of Scope Generation Algorithm *****************************************************************************/ /*---------------------------------------------------------------------------- Representation of wffs: A wff of the form 'p(arg1,...,argn)' is represented as the Prolog term wff(p,[arg1',...,argn']) where argi' is the encoding of the subexpression argi. A constant term is represented by the homonymous Prolog constant. A quantified term is represented by the Prolog term term(quant,var,restrict') where restrict' is the encoding of the wff that forms the restriction of the quantifier. ----------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------- Scope Generation Routines ----------------------------------------------------------------------------*/ % gen(Form,ScopedForm) % ==================== % % Form ==> a wff with in-place quantifier terms % ScopedForm <== a full scoping of Form gen(Form, ScopedForm) :- pull(Form, true, ScopedForm). % pull(Form, Complete?, ScopedForm) % ================================= % % Form ==> a wff with in-place quantifier terms % Complete? ==> true iff only full scopings are allowed % ScopedForm <== a full or partial scoping of Wff % % Applies terms at various level of embedding in Form, including % applying to the entire Form, and to opaque argument positions % inside Form. pull(Form, Complete, ScopedForm) :- pull_opaque_args(Form, PulledOpaques), apply_terms(PulledOpaques, Complete, ScopedForm). % pull_opaque_args(Wff, ScopedWff) % ================================ % % Wff ==> a wff with in-place quantifier terms % ScopedWff <== Wff with opaque argument positions recursively scoped % % Scopes arguments of the given Wff recursively. pull_opaque_args(wff(Pred,Args), wff(Pred, ScopedArgs)) :- !, pull_opaque_args(Pred, 1, Args, ScopedArgs). pull_opaque_args(Term, Term). % pull_opaque_args(Pred, ArgIndex, Args, ScopedArgs) % ================================================== % % Pred ==> the predicate of the wff whose args are being scoped % ArgIndex ==> the nindex of the argument currently being scoped % Args ==> list of args from ArgIndex on % ScopedArgs <== Args with opaque argument positions recursively scoped % % Scopes a given argument if opaque; otherwise, scopes its % subparts recursively. % No more arguments. pull_opaque_args(_Pred,_ArgIndex,[],[]) :- !. % Current argument position is opaque; scope it. pull_opaque_args(Pred, ArgIndex, [FirstArg|RestArgs], [ScopedFirstArg|ScopedRestArgs]) :- opaque(Pred,ArgIndex), !, pull(FirstArg,false,ScopedFirstArg), NextIndex is ArgIndex+1, pull_opaque_args(Pred, NextIndex, RestArgs, ScopedRestArgs). % Current argument is not opaque; don't scope it. pull_opaque_args(Pred, ArgIndex, [FirstArg|RestArgs], [ScopedFirstArg|ScopedRestArgs]) :- pull_opaque_args(FirstArg,ScopedFirstArg), NextIndex is ArgIndex+1, pull_opaque_args(Pred, NextIndex, RestArgs, ScopedRestArgs). % apply_terms(Form, Complete?, ScopedForm) % ======================================== % % Form ==> a wff with in-place quantifier terms % Complete? ==> true iff only full scopings are allowed % ScopedForm <== a full or partial scoping of Wff % % Applies one or more terms to the Form alone (not to any embedded % forms. apply_terms(Form, _Complete, Form) :- not(term(Form,_Term)), !. apply_terms(Form, false, Form). apply_terms(Form, Complete, ScopedForm) :- applicable_term(Form, Term), apply(Term, Form, AppliedForm), apply_terms(AppliedForm, Complete, ScopedForm). % apply(QuantTerm,Wff,NewWff) % =========================== % % QuantTerm ==> a quantified term % Wff ==> the wff to apply QuantTerm to % NewWff <== Wff with the quantifer wrapped around it apply(term(Quant,Var,Restrict), Scope, wff(Quant,[Var,PulledRestrict,OutScope])) :- % scope the restriction of the term pull(Restrict, false, PulledRestrict), % replace the inplace term with the variable subst(Var,term(Quant,Var,Restrict),Scope,OutScope). % applicable_term(Form, Term) % =========================== % % Form ==> an expression in the logical form language % Term <== a top-level term in Form (that is, a term embedded in % no other term) which is not free in any variable bound % along the path from Form to the Term. applicable_term(Form, Term) :- applicable_term(Form, Term, []). % applicable_term(Form,Term,BlockingVars) % ======================================= % % Form ==> an expression in the logical form language % Term <== a top-level term in Form (that is, a term embedded in % no other term) which is not free in any variable bound % along the path from Form to the Term. % BlockingVars ==> % a list of variables bound along the path so far % A term is a safe top-level term. applicable_term(term(Q,V,R),term(Q,V,R), BVs) :- % if it's safe. not(free_in(BVs, R)). % A top-level term of the restriction or scope of a quantifier is safe % only if the variable bound by the quantifier is not free in the term. applicable_term(wff(Quant,[Var,Restrict,Scope]),Term, BVs) :- quantifier(Quant), !, (applicable_term(Restrict,Term,[Var|BVs]); applicable_term(Scope,Term,[Var|BVs])). % A top-level term of an argument list is a top_level term. applicable_term(wff(_Pred,Args),Term, BVs) :- applicable_term(Args, Term, BVs). % A top_level term of any argument is a top_level term of the whole % list. applicable_term([F|R],Res, BVs) :- applicable_term(F,Res,BVs) ; applicable_term(R,Res,BVs). % Note the absence of a rule looking for top_level terms inside of % quantified terms. /*---------------------------------------------------------------------------- Scope Generation Utility Routines ----------------------------------------------------------------------------*/ % term(Form, Term) % ================ % % Form ==> an expression in the logical form language % Term <== a top-level term in Form (that is, a term embedded in % no other term) term(term(Q,V,R),term(Q,V,R)). term(wff(_Pred,Args),Term) :- term(Args,Term). term([F|R],Res) :- term(F,Res) ; term(R,Res). % Note the absence of a rule looking for top_level terms inside of % quantified terms. This is acceptable since we only use term as a % predicate checking if any terms exist and don't rely on a complete % coverage. % free_in(Variables,Form) % ======================= free_in([Var|Vars],Form) :- rec_member(Var,Form) ; free_in(Vars,Form). /*---------------------------------------------------------------------------- Generic Prolog Utilities ----------------------------------------------------------------------------*/ % rec_member(Element,Term) % ======================== rec_member(Element,Element) :- !. rec_member(_Element,Other) :- atomic(Other), !, fail. rec_member(Element,[First|Rest]) :- !, (rec_member(Element,First) ; rec_member(Element,Rest)). rec_member(Element,Term) :- Term =.. List, rec_member(Element,List). % subst(New,Old,In,Out) % ===================== % % Substitutes the term New for all occurrences of the term Old in % the term In yielding the term Out. subst(New,Old,Old,New) :- !. subst(_New,_Old,[],[]) :- !. subst(_New,_Old,Atom,Atom) :- atomic(Atom), !. subst(New,Old,[First|Rest],[OutFirst|OutRest]) :- !, subst(New,Old,First,OutFirst), subst(New,Old,Rest,OutRest). subst(New,Old,In,Out) :- In =.. List, subst(New,Old,List,OutList), Out =.. OutList. % not(P) % ====== % % Fails iff P succeeds. not(F) :- F, !, fail. not(_F). % remove(Element,List, NewList) % ============================= remove(_Element,[],[]). remove(Element,[Element|List],NewList) :- !, remove(Element,List,NewList). remove(Element,[Other|List],[Other|NewList]) :- remove(Element,List,NewList). /*---------------------------------------------------------------------------- Test Formulas ----------------------------------------------------------------------------*/ % quantifier(Quant) % ================= quantifier(every). quantifier(some). quantifier(most). quantifier(a). quantifier(few). quantifier(many). test(Id) :- test(Id,W), bagof(R,gen(W,R),B), length(B,L), print(L). % "Every man sleeps." % One complex term. One reading. test(1, wff(sleeps,[term(every,m,wff(man,[m]))])). % "Every man loves some woman." % Two sibling complex terms. Two readings. test(2, wff(loves,[term(every,m,wff(man,[m])), term(some,w,wff(woman,[w]))])). % "Every department in most companies folds." % Two complex terms, one embedded. Two readings. test(3, wff(folds,[term(every, d, wff(and, [wff(department,[d]), wff(in,[d, term(most, c, wff(company,[c]))])]))])). % Should be 1 reading (blocking variable). test('3a', wff(foo,[term(every, d, wff(and, [wff(department,[d]), wff(in,[d, term(most, c, wff(company,[c,d]))])]))])). % "Every representative of a company saw most samples." % 5 readings. test(4, wff(saw, [term(every, r, wff(and, [wff(representative, [r]), wff(of, [r, term(a, c,wff(company,[c]))])])), term(most,s,wff(sample,[s]))])). % "Some representative of every department in most companies % sees few samples." % 14 readings. test(5, wff(see, [term(some, r, wff(and, [wff(representative, [r]), wff(of, [r, term(every, d, wff(and, [wff(department,[d]), wff(in,[d, term(most,c,wff(company,[c]))])]))])])), term(few,s,wff(sample,[s]))])). % "Some of every of most companies saw few of many companies." % 42 readings. test(6, wff(saw, [term(some, r, wff(of, [r, term(every, d, wff(in,[d,term(most,c,wff(company,[c]))]))])), term(few, f, wff(in,[f,term(many,e,wff(company,[e]))]))])). % Every man seems to love some woman." % "seem" is opaque in its first argument. % 6 readings. opaque(seem,1). test(7, wff(seem,[wff(loves,[term(every,m,wff(man,[m])), term(some,w,wff(woman,[w]))])])). % Test of blocking variables. % 1 reading. test(8, wff(foo,[term(every, d, wff(and, [wff(department,[d]), wff(in,[d, term(most, c, wff(company,[c,d]))])]))])). % Test of blocking variables % 2 readings. test(9, wff(foo,[term(every, d, wff(and, [wff(department,[d]), wff(in,[d, term(most, c, wff(company,[c,d]))])])), term(some, y, wff(p,[y]))])). % Save as 9 but no free variable in embedded term (for comparison). % 5 readings. test(10, wff(foo,[term(every, d, wff(and, [wff(department,[d]), wff(in,[d, term(most, c, wff(company,[c]))])])), term(some, y, wff(p,[y]))])). % Test of blocking variable within opaque position % 2 readings. test(11, wff(f, [ term(every, x, wff(seem, [wff(p,[term(some, y, wff(g, [x,y]))]) ] ) ) ] ) ). % Test of opaque within transparent position % 2 readings. test(12, wff(f, [ wff(seem, [wff(p,[term(some, y, wff(g, [y]))]) ] ) ] ) ). % Test of blocking variable within opaque position. % 2 readings. test(13, wff(seem, [wff(p,[term(every, x, wff(f, [ term(some, y, wff(g, [x,y])) ] ) )] ) ] ) ). % Same as 13 but no free variable in embedded term (for comparison). % 5 readings. test(14, wff(seem, [wff(p,[term(every, x, wff(f, [ term(some, y, wff(g, [y])) ] ) )] ) ] ) ).