/*****************************************************************************
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])) ] ) )]
) ] ) ).