/* plugSUR.pl Nathan Vaillette June 11, 1999 Updated May 11, 2001 Last Updated April 19, 2003 Plugging algorithm with polymorphic type-checking for Scopally Underspecified Representations (SURs) */ :- use_module(library(lists)). %% Operator Definitions :- op(40,yfx,>). % implication :- op(30,yfx,v). % disjunction :- op(30,yfx,&). % conjunction :- op(20, fy,~). % negation :- op(500,xfy,:). % typing judgement operator /* (1) Introduction This program implements a resolution algorithm for underspecified representations of formulas of a typed lambda calculus (see http://www.ling.ohio-state.edu/ftp/def-plug.ps). The typing system also allows for some polymorphicity; see below. Some of the techniques used are based on chapter 3 of Blackburn and Bos (1997) (Patrick Blackburn & Johan Bos. *Representation and Inference for Natural Language. A First Course in Computational Semantics*. Lecture Notes for ESSLLI'97, Aix-en-Provence, August 1997. Claus Report Nr. 90. Available from http://www.coli.uni-sb.de/~bos/comsem/book1.html) Specifically, I follow them in using an "Outsc" list to check constraint satisfaction locally. Unlike them, I seek to do this while maintaining a simple and clean correspondence between theory and implementation, instead of relying on a number of confusing (and brittle) bits of Prolog-specific trickery, such as using Prolog variables simultaneously for object-language variables, SUR-lables, and SUR-holes. The core of the program is the interpret/4 predicate, which folds together the processes of generating and testing pluggings and applying them to the top hole to yield a hole-less formula into one algorithm. (2) SUR Encoding The formulas manipulated are Prolog terms, and SUR's are encoded thus: datastructure for SUR: sur( Lforms, %% (duplicate-free) list of labelled formulas (lfomrs) %% of form: lf(Label, Formula) Constraints, %% list of constraints of form: sub(Label, Hole) TopHole ) The formulas will be those of first-order logic embedded within a simple lambda calculus ("formula" here just means "expression" throughout). All applications are of the form apply(Form,Form). All abstractions are of the form abstr(Var,Form). Beta-eta reduction is not implemented, so the formulas can get hard to read. Oh well. Note also that holes are represented as (ground) prolog terms wrapped in h( ). The predicate compileSUR/2 transforms such a SUR into slightly easier-to-use format, where each labelled formula lf(Lab,Form) is replaced by a term of the form lf(Lab, Form, Holes), where Holes is the list of holes in Form, in their order of occurence. (3) Type-Checking This version incorporates type-checking. The SUR manipulation predicates have one argument for a list (or actually accumulator-pair; see below) of typing judgements of the form Formula:ConstType (ConstTypes are discussed below). So for instance, when interpreting a SUR, one provides a judgement for each basic symbol occuring in the lforms of the SUR. Variables have to have their types declared in this way too. Also, recall that holes are constants, and as such should have thier types declared in just the same way. Result types of complex formulas need not be declared; they will be inferred on-line as pluggings are executed. The fact that a separate typing context is maintained ("Curry-style") is intended to save the formulas from utter illegibility, which would probably be the result if every occurance of every basic expression had to typed in the expressions themselves ("Church-style"). (That would actually be more efficient in the long run, removing all the calls to member/2 in has_type/3, so maybe a good compromise would be to compile automatically from Curry-style to Church-style representations.) The judgement list is actually threaded through as an accumulator, so when the type inferencing judges expression E to have type T, E:T is added to the output judgement list. This can cut down on redundant type inference. (3.1) Polymorphic Types The particular type-system implemented here allows for polymorphic types. Although the only type-constructor used is the one corresponding to function-space formation (here written funTC(Dom,Ran) ), various other kinds of types can be simulated (such a record types, variant types, recursive types, and parametrically defined types) by a method to be discussed below. (The same method could be used to simulate subtyping.) (3.1.1) Type Variables and Type Inference Polymorphism is achieved via type variables. There is no binding of type variables nor explicit supplying of type-parameters to generic functions. Rather, type variables are dealt with as implicity universally quantified. Type inference on complex formulas with generic subformulas is accomplished by using type unification to compute principal types as in a Hindley-Milner sort of system. In this program, Prolog variables are used to represent type variables. This allows type unification to be reduced to Prolog term unification. This has certain drawbacks; e.g. the scope of implicit quantification will not necessarily be local to a given type expression. An important practical example of this is the fact that the same type variable can't be reused in the Judgements lists: e.g. if one formula phi of a basic polymorphic type occurs on the list, and another psi of a polymorphic functional type occurs on the same list, typing phi as A and psi as funTC(A,A) will allow the unwanted side effect that the 2 A's can become bound together to the same ground term by the unification used in type inference. To avoid this pitfall, we need to name the variables apart, e.g. typing psi as funTC(B,B). Although I objected above to using Prolog variables to represent object-language variables, the use I make here of such a strategy is minimally ojectionable (since e.g. the type variables are not bound by anything anyway, we can't get into trouble involving the scope of operators, at least within the same type-expression-- cf. first-order logic variables) and maximally useful (since unification is used to implement unification---a sensible choice---rather than to implement something it can't really implement straightforwardly, like e.g. term subtitution: cf. again first-order variables, and also SUR holes). However, I have set the program up so that it can be minimally modified to use a completely ground representation for types along with a type-unification algorithm written in Prolog: simply redefine type_var/1 (which currently just checks whether its argument is a Prolog variable) to accord with however you prefer to identify type variables, and redefine type_unification/3 and apply_mgu/3 (which currently hook onto prolog unification) as needed. (3.1.2) Constrained Types ("ConstrTypes") Now, to implement various restrictions on type variables, we give formulas, instead of types, rather ConstTypes: ConstrType ::= Type + List[Constr] Constr ::= isa(Restr, Type) | subtype(Type,Type) | ... Restr ::= erel | e_or_t | e_or_erel | ... To see how this works, consider the problem of simulating variant types. Say we have some basic types f and g, but we want a new type that comprises all of f and g. This could be used for a function phi with a kind of limited polymorphism that takes as an argument either an f or a g and returns an f or a g, respectively. phi would have type funTC(A,A), but this would not be its principal type. We need some way to modify this type expression to express the necessary constraint on A. We do this with the ConstrType funTC(A,A)+[isa(f_or_g, A)]. When type inferencing is done, the terms in the Constr list are called as Prolog goals. Then Prolog disjunction can be used to implement type disjunction. Similarly, a recursive Prolog predicate can be used to simulate recursive types. The recursive type "erel" for example comprises all the types interpreted as curried relations over type e objects, so funTC(e,t), funTC(e,funTC(e,t)), etc. This recursive restriction is called in the interpretation of ex2 below. The abstraction and application rules are set up so that the ConstrType of a comples formula accumulates all the Restrs from its sub formulas, so e.g. f(x) has ConstrType b+C, where f:funTC(a,b)+C1, x:b+C2, and C is the concatenation of C1 and C2. Note that at present, the calling of the Restrs of the ConstrTypes to check the constraints expressed therein is done by the appropriate/3 predicate (not e.g. has_type/3), which is not the most natural place for this to happen. Also, I think that since the constraints get accumulated, they may get unecessarily rechecked alot. (4) Organization The program is divided roughly into 3 parts for readability: I: Plugging Algorithm II: Type-Checking III: Testing and Examples */ %%%........................................................................... %%% Part I: Plugging Algorithm %%%........................................................................... % interpret(+CompiledSUR, ?Formula, ?Plugging,+Judgements) % interpret/4 nondeterministically selects proper, resolving Plugging % of CompiledSUR and applies it to yield Formula as a result. interpret( sur(LFs, Cons, TopHole), Result, Plugging, Judgements) :- findReplacement(TopHole, Result, LFs-[], Cons, []-Plugging, [], Judgements-_JudgementsOut). % pickPlug(+Hole, ?Lform, ?LformAcc, +Conditions, % ?PluggingAcc, +Outsc, ?JudgementAcc)) % pickPlug/7 non-deterministically picks a candidate value for P(Hole) % from the input list of the LformAcc accumulator pair and removes it. % It makes sure the chosen lform is appropropriate for Hole, and that % the resulting (partial) plugging would be a resolution of the SUR % under consideration, by looking at the Conditions and the list Outsc % of holes that will outscope whatever is chosen for P(Hole). If so, it % records the choice in the output of the PluggingAcc accumulator. pickPlug(Hole, lf(Lab,Form,Hls), LFs0-LFs1, Cons, Plugging-[p(Hole,Lab)|Plugging], Outsc, Judgements) :- %% deleteFromList( lf(Lab,Form,Hls), LFs0, LFs1), select( lf(Lab,Form,Hls), LFs0, LFs1), appropriate( lf(Lab,Form), Hole, Judgements), checkCons(Lab, Cons, [Hole|Outsc]). % findReplacement(+Hole, ?Formula, ?LformAcc, % +Cons, ?PluggingAcc, +Outsc, ?JudgementAcc) % findReplacement/7 is just the composition of pickPlug/7 with % plugLf/7; i.e. it finds an lf(Label,Formula) = P[P(Hole)] and returns % Formula. findReplacement(Hole, Form, LFs0-LFs2, Cons, Plugging0-Plugging2, Outsc, Judgements-Judgements2) :- pickPlug(Hole, Lform, LFs0-LFs1, Cons, Plugging0-Plugging1, Outsc, Judgements-Judgements1), plugLf(Lform, lf(_,Form,_), LFs1-LFs2, Cons, Plugging1-Plugging2, [Hole|Outsc], Judgements1-Judgements2). % plugLf(+LFormIn, ?LformOut, ?LFAcc, +Cons, % ?PluggingAcc, +Outsc, ?JudgementAcc)) % plugLf/7 plugs all of the holes in Lform0 with hole-less formulae. plugLf( lf(Lab,Form,[]), lf(Lab,Form,[]), LFs-LFs, _Cons, Plugging-Plugging, _Outsc, Judgements-Judgements ). plugLf( lf(Lab,Form0, [Hole|Hls1]), lf(Lab,Form2,Hls3), LFs0-LFs2, Cons, Plugging0-Plugging2, Outsc, Judgements-Judgements2) :- plugHole(Hole, lf(Lab,Form0,[Hole|Hls1]), lf(Lab,Form1,Hls2), LFs0-LFs1, Cons, Plugging0-Plugging1, Outsc, Judgements-Judgements1), plugLf( lf(Lab, Form1,Hls2), lf(Lab,Form2, Hls3), LFs1-LFs2, Cons, Plugging1-Plugging2, Outsc, Judgements1-Judgements2). % plugHole(+Hole, +LformIn, ?LformOut, ?LformAcc, % +Cons, ?PluggingAcc, +Outsc, ?JudgementAcc) % plugHole/8 takes in an lform Lab:Form, finds a hole-less replacement % for Hole, and subsitutes it in for each occurance of Hole in Form. plugHole(Hole, lf(Lab,Form0,Hls0), lf(Lab,Form2,Hls1), LFs0-LFs1, Cons, Plugging0-Plugging1, Outsc, Judgements) :- findReplacement(Hole, Form1, LFs0-LFs1, Cons, Plugging0-Plugging1, Outsc, Judgements), replaceInForm(Hole, Form1, Form0, Form2), %% removeAll(Hole, Hls0, Hls1). delete(Hls0,Hole,Hls1). % checkCons(+Label, +Conditions, +Outsc) % Whenever an lform l:k is chosen, checkCons/3 checks to make sure that % if Sub_U(l:k,Hole), then Sub_P(l:k,Hole) will hold in the % result. It is simple to prove that if this holds for every l:k, it % follows that the plugging resolves the SUR. Thanks to the Outsc % argument, whether this does indeed hold for l:k can be checked % locally: the predicates that call checkCons make sure that the input % Outsc contains exactly those holes that will outscope the lform in the % result; this is achieved by the way holes are added to this argument % by these other predicates. checkCons(_Lab, [], _Outsc). checkCons(Lab, [sub(Lab,Hole)| Cons], Outsc) :- member(Hole, Outsc), checkCons(Lab, Cons, Outsc). checkCons(Lab0, [sub(Lab1,_)|Cons], Outsc):- \+ Lab0=Lab1, checkCons(Lab0, Cons, Outsc). % some simple formula manipulation predicates: replaceInForm(X,Y, X,Y) :- !. replaceInForm(X,Y, Form0, Form1) :- ( atomic(Form0) -> Form1 = Form0 ; (Form0 =.. List0, map_replaceInForm(X,Y, List0, List1), Form1 =.. List1) ). map_replaceInForm(_,_,[],[]). map_replaceInForm(X,Y,[Form0|Forms0], [Form1|Forms1]):- replaceInForm(X,Y,Form0,Form1), map_replaceInForm(X,Y,Forms0,Forms1). holes(h(X), [h(X)]) :- !. holes(Form, Holes) :- ( atomic(Form) -> Holes = [] ; ( Form =.. List, hls(List,Holes) ) ). hls([],[]). hls([Form|Forms], Holes0):- holes(Form,Holes1), hls(Forms, Holes2), append(Holes1, Holes2, Holes0). map_addHoleList([],[]). map_addHoleList([lf(Lab,Form) | LFs0], [lf(Lab,Form,Holes) | LFs1]) :- holes(Form, Holes), map_addHoleList(LFs0, LFs1). %%%......................................................................... %%% Part II: Type Checking %%%......................................................................... appropriate(lf(_Lab,Form), Hole, Judgements-Judgements2) :- has_type(Form, T1, Judgements-Judgements1), has_type(Hole, T2, Judgements1-Judgements2), type_match(T1,T2). type_match(T1+C1,T2+C2) :- type_unification(T1,T2,_MGU), map_call(C1), map_call(C2). map_hook([], _Judgements). map_hook([H|T], J) :- hook(H,J), map_hook(T,J). map_call([]). map_call([H|T]) :- H, map_call(T). /* my type rules (Hindley-Milner system but with ConstrTypes and accumulation of constraints on them): '(+)' is list-append: Sigma |- v:(s+C1) Sigma |- e:(t+C2) -----------------------------------------[ABS] Sigma |- \v.e:(s->t + C1(+)C2) Sigma |- e1:(s1->t+C1) Sigma |- e2:(s2+C2) where s1 and s2 unify via -----------------------------------------[APPL] mgu @, and all type variables Sigma |- e1(e2):(@(t)+ C1(+)C2 ) occuring free t occur free in s1 2 things to note: the Constraints in the C's aren't checked here (rather by type_match/3); and the typing judgements arrived at are added to the output Judgements so they don't have to be recomputed later. */ isa(erel, X) :- typeVar(X). isa(erel, funTC(e,t)). isa(erel, funTC(e,X) ) :- isa(erel,X). typeVar(V) :- var(V). isa(t_or_erel, t). isa(t_or_erel, X) :- isa(erel,X). type_unification(X,X,X). apply_mgu(_MGU,X,X). %%% [ANY] has_type(C,T,Judgements-Judgements) :- member(C:T, Judgements). %%% [ABS] has_type(abstr(v(V), Body), funTC(S,T)+C, Judgements-[abstr(v(V), Body):funTC(S,T)+C | Judgements2]) :- has_type(v(V), S+C2, Judgements-Judgements1), has_type(Body,T+C1, Judgements1-Judgements2), append(C1,C2,C). %%% [APPL] has_type(apply(Exp1, Exp2), T+C, Judgements-[apply(Exp1,Exp2):T+C|Judgements2]) :- has_type(Exp1, funTC(S1,T1)+C1, Judgements-Judgements1), has_type(Exp2, S2+C2, Judgements1-Judgements2), type_unification(S1,S2,MGU), apply_mgu(MGU, T1,T), append(C1,C2,C). %%% these are the type rules for non-atomic first-order formulas: has_type(forall(V,B), t+C, Judgements-[forall(V,B):t+C|Judgements2]) :- has_type(V,_+C1, Judgements-Judgements1), has_type(B,t+C2, Judgements1-Judgements2), append(C1,C2,C). has_type(exists(V,B), t+C, Judgements-[exists(V,B):t+C|Judgements2]) :- has_type(V,_+C1, Judgements-Judgements1), has_type(B,t+C2, Judgements1-Judgements2), append(C1,C2,C). has_type(A&B, t+C, Judgements-[A&B:t+C|Judgements2]) :- has_type(A,t+C1, Judgements-Judgements1), has_type(B,t+C2, Judgements1-Judgements2), append(C1,C2,C). has_type(A>B, t+C, Judgements-[A>B:t+C|Judgements2]) :- has_type(A,t+C1, Judgements-Judgements1), has_type(B,t+C2, Judgements1-Judgements2), append(C1,C2,C). has_type(~A, t+C, Judgements-[~A:t+C|Judgements1]) :- has_type(A, t+C, Judgements-Judgements1). %%%......................................................................... %%% Part III Testing and Examples %%%......................................................................... % Testing stuff: test(N):- ex(N, Sur0, Judgements), compileSUR(Sur0,Sur1), doAll( subtest(Sur1, Judgements) ), nl,write('(no more solutions)'),nl. subtest(Sur, Judgements) :- interpret(Sur,Formula, Plugging, Judgements), nl,write(Formula),nl,write('by Plugging: '), nl,write(Plugging),nl, write('------------------------------------------------------------'). compileSUR( sur(LFs0, Cons, Top), sur(LFs1 , Cons, Top) ) :- map_addHoleList(LFs0, LFs1). doAll(X) :- X, fail, !. doAll(_). % Examples: % example 1 is a run-of-the-mill quantifier-scope amibiguity case. % `Every boxer loves some woman' ex(1, sur( [ lf(l1,forall(v(x), apply(boxer,v(x))>h(1) )), lf(l2,exists(v(y), apply(woman,v(y))&h(2) )), lf(l3, apply(apply(love,v(y)),v(x))) ], [ sub(l1,h(0)), sub(l2,h(0)), sub(l3,h(1)), sub(l3,h(2)) ], h(0) ) , [boxer:funTC(e,t)+[], woman:funTC(e,t)+[], love:funTC(e, funTC(e,t))+[], h(0):t+[], h(1):t+[], h(2):t+[], v(x):e+[], v(y):e+[] ]%-[] ). % Example 2 is a more complex benchmark testcase. It implements my % approach to plural semantics whereby a polymorphic cumulation operator % sigma is underspecified as to what relation it applies to, in % particular to how saturated the relation is. The SUR below allows it % to apply to any possibility; to the unsaturated relation `love' or % either of its partially saturated versions. Meanwhile, the method of % dissociating certain lambdas from their bodies used to achieve this % effect also gets (intraclausal) scope ambiguities automatically. % This example crucially relies on type-information to constrain the % pluggings. You are invited to add the clause: % appropriate(_,_,J-J). % to the definition of appropriate/3 to see how many unwanted results % the type-checking actually prunes away. % `The men love a woman' ex(2, sur( [ lf(l1, loves), lf(l2, apply(apply(h(1),v(y)), v(x))), lf(l3, apply(apply(some,h(11)), h(12) )), lf(l4, abstr(v(y), h(3))), lf(l5, abstr(v(x), h(4))), lf(l6, apply(sigma, h(5))), lf(l7, woman), lf(l8, apply(h(16),the_men)) ] , [ sub(l3,h(0) ), sub(l7,h(11)), sub(l4,h(12)), sub(l2,h(3) ), sub(l1,h(1) ), sub(l1,h(5) ), % sub(l6,h(0) ), % not needed; no change in semantics sub(l2,h(4) ), sub(l5,h(16)), sub(l8,h(0)), sub(l6,h(16)) ] , h(0) ), [ loves:funTC(e,funTC(e,t))+[], sigma:funTC(A,A)+[isa(erel,A)], some:funTC(funTC(e,t), funTC( funTC(e,t), t))+[], woman:funTC(e,t)+[], the_men:e+[], v(x):e+[], v(y):e+[], h(0):t+[], h(1):funTC(e,funTC(e,t))+[], h(3):B+[isa(t_or_erel,B)], h(4):C+[isa(t_or_erel,C)], h(5):D+[isa(erel,D)], h(11):funTC(e,t)+[], h(12):funTC(e,t)+[], h(16):funTC(e,t)+[] ] ). /* here's the output of "?- test(2)." in semi-readable form: apply( apply(some,woman), abstr( v(y), apply( abstr( v(x), apply( apply( apply(sigma,loves), v(y) ), v(x) ) ), the_men) ) ) by Plugging: [p(h(5),l1),p(h(1),l6),p(h(4),l2),p(h(16),l5), p(h(3),l8),p(h(12),l4),p(h(11),l7),p(h(0),l3)] ------------------------------------------------------------ apply( apply(some,woman), abstr( v(y), apply( apply( sigma, abstr( v(x), apply( apply(loves,v(y)), v(x) ) ) ), the_men ) ) ) by Plugging: [p(h(1),l1),p(h(4),l2),p(h(5),l5),p(h(16),l6), p(h(3),l8),p(h(12),l4),p(h(11),l7),p(h(0),l3)] ------------------------------------------------------------ apply( abstr( v(x), apply( apply(some,woman), abstr( v(y), apply( apply( apply(sigma,loves), v(y) ), v(x) ) ) ) ), the_men ) by Plugging: [p(h(5),l1),p(h(1),l6),p(h(3),l2),p(h(12),l4), p(h(11),l7),p(h(4),l3),p(h(16),l5),p(h(0),l8)] ------------------------------------------------------------ apply( abstr( v(x), apply( apply(some,woman), apply( sigma, abstr( v(y), apply( apply(loves,v(y)), v(x) ) ) ) ) ), the_men ) by Plugging: [p(h(1),l1),p(h(3),l2),p(h(5),l4),p(h(12),l6), p(h(11),l7),p(h(4),l3),p(h(16),l5),p(h(0),l8)] ------------------------------------------------------------ apply( apply( sigma, abstr( v(x), apply( apply(some,woman), abstr( v(y), apply( apply(loves,v(y)), v(x) ) ) ) ) ), the_men ) by Plugging: [p(h(1),l1),p(h(3),l2),p(h(12),l4),p(h(11),l7), p(h(4),l3),p(h(5),l5),p(h(16),l6),p(h(0),l8)] ------------------------------------------------------------ */ %%% A similar example: ex(3, sur( [ lf(v4, hired), lf(v1, apply(apply(h(1),v(y)), v(x))), lf(o, apply(some_secretary, h(6) )), lf(v3, abstr(v(y), h(3))), lf(v2, abstr(v(x), h(2))), lf(v5, apply(sigma, h(4))), lf(s, apply(three_lawyers,h(5))) ] , [ sub(v4,h(1)), sub(v4,h(4)), sub(v1,h(2)), sub(v1,h(3)), sub(v2,h(5)), sub(v3,h(6)), sub(v5,h(0)), sub(s,h(0)), sub(o,h(0)) ] , h(0) ), [ hired:funTC(e,funTC(e,t))+[], sigma:funTC(A,A)+[isa(erel,A)], some_secretary:funTC( funTC(e,t), t)+[], three_lawyers:funTC( funTC(e,t), t)+[], v(x):e+[], v(y):e+[], h(0):t+[], h(1):funTC(e,funTC(e,t))+[], h(5):funTC(e,t)+[], h(6):funTC(e,t)+[], h(4):D+[isa(erel,D)], h(2):B+[isa(t_or_erel,B)], h(3):C+[isa(t_or_erel,C)] ] ). %%% EOF