Proceedings of EACL '99 
Ambiguous propositions typed 
Tim Fernando 
Philosophy Department 
University of Texas 
Austin, TX 78712-1180, USA 
f ernando~ims, uni-stuttgart, de* 
Abstract 
Ambiguous propositions are analyzed in 
a type system where disambiguation is 
effected during assembly (i.e. by coer- 
cion). Ambiguity is introduced through 
a layer of types that are underspecified 
relative to a pre-existing collection of de- 
pendent types, construed as unambigu- 
ous propositions. A simple system of 
reasoning directly with such underspec- 
ification is described, and shown to be 
sound and complete for the full range of 
disambiguations. Beyond erasing types, 
the system supports constraints on dis- 
ambiguations, including co-variation. 
1 Introduction 
A widely held view expressed in (Carbonell and 
Hayes, 1987) is that "if there were one word to 
describe why natural language processing is hard, 
it is ambiguity." For any given natural language 
utterance, a formal language such as predicate 
logic typically offers several non-equivalent (well- 
formed) formulas as possible translations. An ob- 
vious approach is to take the disjunction of all 
alternatives, assuming (for the sake of the argu- 
ment) that the disjunction is a formula. Even if it 
were, however, various objections have been raised 
against this proposal (e.g. (Deemter, 1996)). For 
the purposes of the present paper, what is inter- 
esting about a word, phrase, sentence or discourse 
that is ambiguous in isolation is how it may get 
disambiguated when combined with other expres- 
sions (or, more generally, when placed in a wider 
context); the challenge for any theory of ambigu- 
ity is to throw light on that process of disambigua- 
tion. 
*From June to mid-August 1999, I will be visiting 
IMS, Uni Stuttgart, Azenbergstr 12, 70174 Stuttgart, 
Germany. Where I might be after that is unclear. 
More concretely, suppose • were a binary con- 
nective on propositions A and B such that A • B is 
a proposition ambiguous between A and B. Under 
the "propositions-as-types" paradigm (e.g. (Gi- 
rard et al., 1989)) identifying proofs of a proposi- 
tion with programs of the corresponding type (so 
that "t: A" can be read as t is a proof of proposi- 
tion A, or equivalently, t is a program of type A), 
disambiguation may take the form of type coer- 
cion. An instructive example with F as the con- 
text 
is 
x:(A-+ B) oC, y:DoA 
r ~- ap(p.(x),q.(y)):B (1) 
where ap is function application (corresponding to 
modus ponens), while p. and qo are the first and 
second o-projections, so that 
and 
x:(A ~ B)•C ~ p,(x):A ~ B 
y:D.A ~- qo(y):A. 
Evidently, there is something conjunctive (never 
mind disjunctive) about o; but beyond the ques- 
tion as to whether the unambiguous propositions 
constituting the possible readings of an ambigu- 
ous proposition form a conjunctive or disjunctive 
set (whatever that may precisely mean), there is 
also the matter of the interconnected choices from 
such sets, mediated by terms such as p°(x) and 
q°(Y). 
To ground these abstract considerations in nat- 
ural language processing, a few words about how 
to think of the terms t and types A are useful. 
For predicate logic formulas A, the terms t might 
be intuitionistic natural deduction proofs, related 
by the Curry-Howard isomorphism to a suitable 
typed A-calculus. A notable innovation made 
in Intuitionistic Type Theory (ITT, (Martin-LSf, 
86 
Proceedings of EACL '99 
1984)) is to allow proofs to enter into judgments of 
well-formedness (propositionhood). This stands 
in sharp contrast to ordinary predicate logic (be it 
intuitionistic or classical), where well-formedness 
is a trivial matter taken for granted (rather than 
analyzed) by the Curry-Howard isomorphism. For 
a natural language, however, it is well-formedness 
that is addressed by building types A over sen- 
tences, nouns, etc (in categorial grammar; e.g. 
(Morrill, 1994)) or LFG f-structures (in the "glue" 
approach, (Dalrymple et al., 1993; Dalrymple et 
al., 1997)). Now, while ITT's rules for proposi- 
tionhood hardly constitute an account of gram- 
maticality in English, the combination (in ITT) 
of assertions of well-formedness (A type) and the- 
oremhood (t: A) re-introduces matters of informa- 
tion content (over and above grammatical form), 
which have been applied in (Ranta, 1994) (among 
other places) to discourse semantics (in particu- 
lar, anaphora). The present paper assumes the 
machinery of dependent functions and sums in 
ITT, without choosing between grammatical and 
semantic applications. In both cases, what ambi- 
guity contributes to the pot is indeterminacy in 
typing, the intuition being that an expression is 
ambiguous to the extent that its typing is inde- 
terminate. 
That said, let us return to (1) and consider how 
to capture sequent inferences such as 
rI-x:(A-+ B).C rFy:D°A 
V }- ap(p°(x),q°(y)):B 
(i) and more complicated cases from iterated appli- 
cations of., nested among other type constructs. 
The idea developed below is to set aside the con- and 
nective • (as well as notational clutter p., q.), (ii) 
and to step up from assertions t : A to (roughly) 
t :: A, where A is a set of types A (roughly, 
t : A : ,4). For instance, a direct transcription of 
the -~-introduction rule into :: is 
F,x::A }- t::B 
F }- Ax.t::A -+/3 (2) 
where .4 --+/3 abbreviates the set 
{A --+ B I A E Aand B E/3}. 
But what exactly could t ::A mean? The disjunc- 
tive conception 
t::A iff t:A for someAEA (3) 
would have as a consequence the implication 
t::-4 and .4 C B implies t::B. 
Now, if combinatorial explosion is a problem for 
ambiguity, then surely we ought to avoid feeding 
it with cases of spurious ambiguity. A comple- 
mentary alternative is conjunction, 
t::A iff t:A for allAEA, (4) 
the object this time being to identify the C_-largest 
such set A, as (4) supports 
t::A and B C .4 implies t::B . 
But while (4) and (2) will do for Ax.y where y is 
a variable distinct from x, (4) suggests that (2) 
overgenerates for Ax.x. Spurious ambiguity may 
also arise to the left of ~- (not just to the right), 
if we are not careful to disambiguate the context. 
(1) illustrates the point; compare 
F ~- x::{A --~ B,C} F ~- y::{A,D} (5) 
r I- ap(=,v)::{B} 
where the context F is left untouched, to 
F }-- x::{A -+ B,C} F }- y::{A,D} (6) 
x::{A -+ B},y:: {A} }- ap(x,y):: {B} 
where the context gets trimmed. (5) and (2) yield 
F Ax.Ay.ap(x,y)::{A -~ B,C} -~ ({A,D} -~ {B}) 
whereas (6) and (2) yield 
I- Ax.Ay.ap(x,y):: (A -+ B} + ((A} -~ {B}) . 
To weed out spurious ambiguity, we will 
attach variables onto sets .4 of types, to form 
decorated expressions ct 
collect constraints on a's in sets C, hung as 
subscripts, }-c, on ~-. 
(3) and (4) are then sharpened by a contextual 
characterization, semantically interpreting judg- 
ments of the form t :: a and a typ by disambigua- 
tions respecting suitable constraints. 
2 Two systems 
Let us begin with a system of dependent types, 
confining our attention to three forms of judg- 
ments, F context, A type and t:A. (That is, for 
simplicity, we leave out equations between types 
and between terms.) Contexts can be formed from 
the empty sequence () 
(Oc) }- 0 context 
(tc) F ~ A type x ~ Var(P) 
F, x : A context 
87 
Proceedings of EACL '99 
where Var(F) is the set of variables occurring in 
F. Assumptions cross \[-- 
(As) ~- F, x: A context 
F,x:A~-x:A 
and contexts weaken to the right 
F ~- O ~- F, A context 
(Weak) F, A ~- O 
(where O ranges over judgments A type and t : 
A). Next come formation (F), introduction (I) 
and elimination (E) rules for dependent functions 
rI (generalizing non-dependent functions -+) 
(l'I F) ~- F, x: A context F, z : A ~- B type 
(HI) 
(HE) 
r F (I'Ix:A)B type 
F,z:A I- t:B 
F ~- )~z.t:(1-Iz:A)B 
r F t:(Hz:A)B r F u:A 
r F ap(t,~,):B\[~ := ~\] 
(where B\[x := u\] is B with x replaced by u) 
and for dependent sums Y\]. (generalizing Carte- 
sian products x) 
(~-\]. F) ~- F,x:A context r,x:A ~- B type 
F ~- (~E\]x:A)B type 
r f- t:A r l- ~:B\[: := t\] (El) 
r F (t,u):(Ez:A)B 
FF t:(Ex:A)B 
(EEp) r F p(t):A 
r F t:(~,x:A)S 
(EEq) r ~-q(t):B\[x :=p(t)\] " 
Now for the novel part: a second system, with 
terms t as before, but colons squared, and :- 
types A, B replaced by decorated expressions a, j3 
and unadorned expressions .4 generated simulta- 
neously according to 
o I(H I (E 
,(II :::a), I (E :::a), i 
a~{t} J aP \[ aq{t} 
where a belongs to a fixed countable set X of vari- 
ables. The intent (made precise in the next sec- 
tion) is that a u-expression .4 describes a set of 
:-types, while a d-expression a denotes a choice 
from such a set. D-expressions of the form a~, a p, 
aq{t} and a/~{t} are said to be non-dependent, 
and are used, in conjunction with constraints of 
the form fcn(a,/3), sum(a) and eq(a,/3), to infer 
sequents relativized to finite sets C of constraints 
as follows 
r F-c t::a r I-c' u::X3 (\[In) 
r Fcuc, u{f~(~,~)} ap(t, u)::as{u} 
F \["c t::a 
(EnP) F FCu(sum(a)} p(t)::aP 
F \[-C t::a 
(E nq) r Fco{sum(o)} q(t)::aq{p(t)} ' 
where each of the three rules have the side condi- 
tion that a is non-dependent. 1 In addition, 
r Fc t::(I'\[z::a)X~ r Fc, u::~r 
(HE)¢ r FCUC'U{eq(a,'y)} ap(t,u)::~\[x := u\] 
with the side condition a # % The intuition (for- 
malized in clauses (c2)-(c4) of the next section) is 
that 
- the constraint eq(a, 7) is satisfied by a dis- 
ambiguation equating a with % 
- fcn(a, i3) is satisfied by a disambiguation of (~ 
and/3 to :-types of the form (H z : A)B and 
A respectively 
and 
- sum(a) is satisfied by a disambiguation of a 
to a :-type of the form (~-'~ x: A)B). 
Rules of the previous system translate to 
(()c)° F~ () cxt 
F I-C -4 typ x ~ Var(F) (tc)° Fc r,z::A~ coot 
(As)O Fc F,x::a cxt 
F,x::a ~-c x::a 
F I-c 0 I-c, F, A cxt 
(Weak)° F, A I-cue' 0 
(iiF)O Fc r,x::a cxt r,x::a Fc' B typ 
F \[-CuO (l'I x::a) B typ 
F,x::a I-c t::~ (llI) ° 
r I-c ~z.t::(H z::a)x~ 
r I-c t::(IIz::a)~ r I-c' u::a 
(liE)° r Fcuc, ap(t,u)::~\[z := u\] 
(~F)O J-c I',z::a cxt F,x::a ~-c' B typ 
r Fcuc' (~z::a)B typ 
r kc t::a r bc, u::~\[x := t\] 
(EI)° r Fc~c, (t,~)::(E~::a)~ 
(EEp)O r Fct::(Ex::a)~ 
F ~-c p(t)::a 
r kC t::(Ez::a)~ (E E~) ° 
r Vc q(t)::~\[x := p(t)\] " 
1Variations on this side condition ~e taken up in 
§5 below. 
88 
Proceedings of EACL '99 
Further rules provide co-varying choices 
F l-c t::a z ¢ Vat(r) 
(::c) l-cC, z::a cxt 
(YIc) l-c r,x::a cxt r,x::a l-o t::t~ 
l-cuc' r,y::(l'Ix::a)/~ cxt 
(~c) l-c r,x::a cxt r,x::a t-o t::t3 
t-cuc, r,y::(5:~::a)t~ ¢xt ' 
where (Hc) and (~"\].c) each have the side condition 
y ¢ Var(r) u {z}. 
3 Disambiguating :: 
Let Ty be the collection of :-type expressions A, 
and for every d-expression a, let 
- X(a) be the set of variables in 2:' occurring 
in a 
- D(a) be the set of (sub-)d-expressions/~ oc- 
curring in a (including a) 
and 
- U(a) be the set of (sub-)u-expressions A oc- 
curring in a. 
Suppressing the tedious inductive definitions of 
D(a) and U(a), let us just note that, for instance, 
D((l-I x::a=)(~'\]~y::a'y)a= ) is 
 (II 
a=, a~V, az} 
and U((I- I x ::a=)(~'~. y::a'y)az) is 
o, o'}. 
Next, given a d-expression a0 and a function p : 
D(ao) --+ Ty, let -P be the function from U(a0) 
to Pow(Ty) such that for a E X(ao), 
a p = Ty , 
for (I-\[ x::a)A e U(ao), 
((I~x::a)x) p = {(Hx:p(a))A I A E A p} 
and for ()-~.=::a)A e U(ao), 
((~-~x::a)A) p = {(Zx:p(a))A I A e AP} . 
Now, call p a disambiguation of ao if the following 
conditions hold: 
(i) for every A= E D(a0), p(,4=) E A p 
(ii) for every (1FIx::a)/3 E D(ao), 
p((H ~:: a)Z) = (H ~: p(a))p(x~) 
(iii) for every (~x::a)/3 E D(ao), 
p((~ x :: a)lh) = (~ x :p(a))p(13) 
(iv) for every a~{t} E D(ao), 
p(a) = (rl x :p(/~))A 
for some x and A with A\[x := t\] = p(a~{t}) 
(v) for every a p e D(ao), 
p(a) = (~x:p(aP))B for some x and B 
and 
(vi) for every aq{t} E D(ao), 
p(a) = (~x:A)B 
for some x, A and B with 
Six := t\] = p(aq{t}). 
Next, let us pass from a single d-expression ao 
to a fixed set Do of d-expressions. A disambigua- 
tion of the set Do of d-expressions is a function p 
from U{D(a) \] a E Do} to Ty such that for all 
a E Do, p restricted to D(a) is a disambiguation 
of a. 2 A disambiguation p of Do respects a set C 
of constraints if there is an extension p+ _D p so 
that 
(cl) p+ is a disambiguation of 
Do U {a I a is mentioned in C} 
(c2) whenever eq(a,/~) E C, p+(a) --- P+(I~) 
(c3) whenever fcn(a,/3) e C, 
p+(a) = (Ilx:p+(l~))B for some x and B 
and 
(c4) whenever sum(e) E C, 
p+(a) = (~x:A)B for some x, A and B. 
Given a sequence F of the form 
Xl:el, ...~Xn:an~ 
let irna(F) = {al,...,an}, and for every disam- 
biguation p of a set Do containing ima(F), let 
Fp = Xl:P(al), "", xn:p(an) • 
Let us say that l-c F cxt can be disambiguated 
to l- F' context if there is a disambiguation p of 
ima(F) respecting C such that F' = Fp. Similarly, 
F l-c a typ (t :: a) can be disambiguated to F' l- 
A type (t : A) if there is a disambiguation p of 
irna(F) U {a} respecting C such that F' = Fp and 
A = p(a). 
2It is crucial for this formulation that the set Var(F) 
mentioned in side conditions for various rules in the 
previous section include all variables in P, whether 
they occur freely or bound. 
89 
Proceedings of EACL '99 
4 Relating the derivations 
Observe that to derive a sequent other than }- 
0 context in the first system, or ~¢ 0 cxt in the 
second, we need to assume a non-empty set 7" 
of sequents. Let us agree to write F ~_r O to 
mean that the sequent F }- O is derivable from 
T, and ~_T F context to mean that }- F context is 
derivable from 7". Similarly, for the second system 
(with ~- replaced by ~-c, context by cxt, etc). As 
every rule (R) for the first system has a counter- 
part (R) ° in the second system, it is tempting to 
seek a natural translation .° from the first system 
to the second system validating the following 
Claim: F ~-?" O implies F ° ~-~'° 0% 
For example, if 7" consists of the sequent ~- A type, 
F is empty, and O is Az.x: (\[i z:A)A, then 7"o is 
{~-¢ a typ}, F ° is empty, and O ° is Ax.z :: (I\] x :: 
ax)ax. Replacing F by y:A, and O by ~z.y:(YIx: 
A)A, we get y :: ay for F ° and ~z.y :: (l'I x :: az)% 
for 0% 
To pin down a systematic definition of .°, it is 
easy enough to fix a 1-1 mapping X ~4 a x of 
atomic :-types X to variables a x in ~Y, and set 
x o = ,,x (7) 
((Hx:A)B)° = (1-\[x::A°.)B ° (8) 
((E x:A)B)° = (E x::A°,)B ° (9) 
(A type) ° = A ° typ (10) 
(*:A) ° = z::A°,. (11) 
While (11) induces a translation F ° of a context 
F, what about (t : A) °, where t is not just, as in 
(11), a variable x? Before revising the definition 
of d-expressions a to accommodate subscripts t 
on A °, let us explore what we can do with (7)- 
(11). Define a simple type base 7" to be a set of 
sequents of the form F ~- A type. Given a simple 
type base 7", let 7"0 be its translation into :: ac- 
cording to equations (11) and (10). By induction 
on derivations from 7", we can prove a reformu- 
lation of the claim above, where F ° and O ° are 
replaced by disambiguations. 
Proposition 1. Let 7" be a simple type base. 
(a) r context implies ~0 F' cxt for some F' 
such that ~-o F' cxt can be disambiguated to 
F context. 
(b) F ~T A type implies F' ~° a typ for some 
r' and a such that F' ~-0 a typ can be dis- 
ambiguated to F ~ A type. 
(c) F ~_ 7" t : A implies F' ~-o ~ t :: a for some F' 
and a such that F' ~-o t :: a can be disam- 
biguated to F ~- t:A. 
Moreover, as the rules (1-In), (~\] nv) and (~ nq) 
can, for disambiguations that meet the appropri- 
ate constraints, be replaced by (1"I E), (~\] Ep) and 
(~ Eq), it follows that 
Proposition 2. Let 7" be a simple type base. 
(a) /f ~-c ~ F cxt and \[-c F cxt can be d/sam- 
biguated to ~- F' context, then ~" F' context. 
(b) Ifr ~- ¢ T~ a typ and r ~-c a typ can be disam- 
biguated to F' ~- A type, then F' ~_T A type. 
(c) Ifr \[--c r° t::a andr ~-c t::a can be disam- 
biguated to r' F- t:A, then F' ~_r t:A. 
Conversely, going from (liE) °, (~Ep) ° and 
(E Eq) ° to (\[in), (Y\]~ np) and ()-~ nq), we have 
Proposition 3. Let 7" be a simple type base. 
(a) /f ~_r r' context and ~-c r cxt can be disam- 
biguated to ~- F' context, then ~-c y° F cxt. 
(b) IfF' ~_7" A type and P ~-c a typ can be disam- 
biguated to r' S A type, then P ~-~ a typ. 
(c) If F' ~-~" t : A and F ~-c t :: a can be disam- 
biguated to F' ~- t:A, then F ~o t::t~. 
Proposition 3(c) is roughly ~ of (3), while Propo- 
sition 2(c) approximates =~ of (4). If Proposi- 
tion 2 says that the system for :: above is sound, 
Proposition 3 says it is complete. 3 To tie together 
Propositions 2 and 3 in an equivalence, it is useful 
to define a set C of constraints to be satisfiable 
if 0 is a disambiguation (of 0) respecting C. Note 
that sequents ~-c F and F ~-c e have disambigua- 
tions exactly when C is satisfiable. Consequently, 
Propositions 2 and 3 yield (focussing on ::) 
Corollary 4. Given a simple type base 7" and a 
satisfiable set C of constraints, the following are 
equivalent. 
O) r 
(ii) F' ~_T t : A, for every sequent F' ~- t : A to 
which F ~-c t::a can be disambiguated 
(iii) F' ~_T t : A, for some sequent £' ~- t : A to 
which F ~-c t::a can be disambiguated. 
SAs for how this relates to soundness and com- 
pleteness in say, classical predicate logic, please see 
the discussion of translation versus entailment in the 
concluding paragraph below. 
90 
Proceedings of EACL '99 
The formulation above of Corollary 4 depends on 
the possibility of deriving sequents F ~c O where 
C is not satisfiable. We could have, of course, 
added side conditions to (1-In), (~-~. nj,) and (~"~ nq) 
checking that the constraints are satisfiable. By 
electing not to do so, we have exposed a certain 
separability of inference from constraint satisfac- 
tion, which we will explore in the next section. 
For now, turning to the general case of a set T 
of :-sequents, observe that if 7" is to be compatible 
with the first system, then 
(i) whenever F }- Ax.t:C belongs to 7", 
C must have the form (rI x:A)B with 
F,x:A }_7- t:B 
(ii) whenever F }- (t, u):C belongs to T, 
C must have the form (~\[: z: A)B with 
F \]_r t:A and F }_.7" u:B\[x := t\] 
whenever F }- ap(t,u):B belongs to 7", 
F \]_r t : (1-\[ x : A)B for some x and A such 
that F \]_'r u: A 
whenever F ~- p(t) :A belongs to T, 
F }_7" t:(~\]x:A)B for some x and B 
whenever P }- q(t):B belongs to T, 
F ~_r t:(~_,x:A)B for some x and A 
whenever F ~- e belongs to 7", ~'r F context 
whenever ~- F,x : A context or F ~- t : A 
belongs to T, F ~_7" A type 
(iii) 
(iv) 
(v) 
(vi) 
(vii) 
and 
(viii) whenever F }- (1-I z:A)B type or 
r ~- (~'\]~z:A)B type belongs to T, 
F \[_r A type and F, x:A }_7" B type. 
Thus, a base set T compatible with the first sys- 
tem can be assumed without loss of generality to 
consist of sequents of two forms: F ~ A type and 
F }- t: B, where A and t are atomic (i.e. indecom- 
posable by I-i, ~ and A, (,), ap,p, q respectively). 
By clause (vii) above, it follows that for every se- 
quent F ~- t : B in T, there is some To C_ T 
such that F ~_7~ B type. So starting with sim- 
ple type bases To, we can take (for B) the D- 
expression/3 which Proposition l(b) returns, given 
F \[-% B type. We can then define T ° by trans- 
lating F ~- t:B as F ° }- t ::/3. Alternatively, we 
might make do with simple type bases by refor- 
mulating t as a variable xt, and smuggling zt into 
enriched contexts F' for which a T-derivation of 
F' ~- O' is sought (with O' adjusted for zt, rather 
than t). That is, instead of injecting t on top of 
\]- (within some superscript 7"), we might add it 
(along with the context it depends on) to the left 
of ~-. 
5 Variations and refinements 
The sequent rules for :: chosen above lie between 
two extremes. The first is obtained by dropping 
the side conditions of (I-In), (~-~. np) and (~-'~. nq), 
rendering the four rules (\[i E) °, (~-\] Ep) °, (~ nq) ° 
and (H E)¢ redundant. The idea is to put off con- 
straint satisfaction to the very end. Alternatively, 
the side conditions of (I'\[n), (~-~. np), (~-~ n~) and 
(l-I E)# might be strengthened to check that the 
constraints are satisfiable (adding to (1-In), for ex- 
ample, the requirement that sum(a) ~ C U C' and 
eq(a,~') ¢ C U C' for all 8' 6 D(/3)). Assum- 
ing that we did, we might as well rewrite the rel- 
evant d-expressions, and dispense with the sub- 
script C. (For example, with the appropriate side 
conditions, (\[In) might be revised to 
r t::a I" F- u::# 
r\[a := (1J=::#)a\] F- ap(t,=)::a\[x := =1 
where F\[a := (I-I x::B)a\] is F with a replaced by 
(\[i z ::/3)a.) An increase in complexity of the side 
conditions is a price that we may well be willing 
to pay to get rid of subscripts C. Or perhaps not. 
Among the considerations relevant to the inter- 
play between inference and constraint satisfaction 
are: 
(z) the diffficulty/ease of applying/abusing infer- 
ence rules 
(D) the difficulty of disambiguating (i.e. of veri- 
fying the assumption in Corollary 4 of a "sat- 
isfiable set C" ) 
(W) wasted effort on spurious readings (i.e. se- 
quents F ~-c O with non-satisfiable C). 
Designing sequent rules balancing (I), (D) and (W) 
is a delicate language engineering problem, about 
which it is probably best to keep an open mind. 
Consider again the binary connective • mentioned 
in the introduction (which we set aside to concen- 
trate instead on certain underspecified representa- 
tions). It is easy enough to refine the notion of a 
disambiguation to an e-disambiguation, where e is 
a function encoding the readings specified by o. In 
particular, example (1) can be re-conceptualized 
in terms of 
(i) the instance 
F ~-o z::a r I-o y::~ 
r F{fcn(c~,~)} ap(z,y)::a~{y} 
of the rule (1"I n) where F is the context x :: 
a,y::/3, and say, a is % and/3 is a'~ (against 
the base set of sequents }-e a typ and ~-$ 
a' typ) 
91 
Proceedings of EACL '99 
and 
(ii) an c-disambiguation of a~{y}, where ~(a) = 
{A --+ B, C} and e(/3) = {A, D}. 
Given a (partial) function e from some set 
Do of d-expressions to Pow(Ty) - {0}, an e- 
disambiguation of Do is a disambiguation p of 
Do such that for every a in the domain of ¢, 
p(a) E e(a). 4 Now, there are at least two ways 
to incorporate e-disambiguations into Corollary 4. 
The first is to leave the sequent rules for :: as be- 
fore, but to relativize the notion of a satisfiable 
set C of constraints to e (adding to the defini- 
tion of "p respects C" the requirement that the 
extension p+ be an e-disambiguation). A more 
interesting approach is to bring e into the sequent 
rules by forming constraints to guarantee that dis- 
ambiguations are e-disambiguations (the general 
point being that all kinds of information might 
be encoded within the subscripts C on ~-). For 
starters, we might change the rule (0c) ° to 
(Oc)° I-o,  0 cxt 
where the subscript 0, e denotes a constraint set 
requiring that for every a in the domain of e, 
a can only be disambiguated into an element of 
e(a). The rules (l-in), (~nv) , (~'~ nq) and (FI E)¢ 
might then be modified to trim the sets e(a) so 
that in example (1), for instance, the applica- 
tion of (Fin) reduces e(a) = {A -~ B, C) to 
e'(a) = {A --+ B}. More specifically, let (l'In) 
be 
r I-c,, x::a r ~c,,e y::~ (Fin) 
r 
with the side condition that 
~x is non-dependent, and e is consistent 
with 4 (i.e. for every a in the domain of 
both e and d, ~(a) n e'(a) # 0) 
and where C" is C t3 C'U {fcn(a,B)} and e" com- 
bines e and e' in the obvious way (e.g. map- 
ping every a in the domain of both ¢ and e' to 
e(a)nd(a)). (Subscripts C, e may, as in the case of 
0, ¢, be construed as single constraint sets, which 
are convenient for certain purposes to decompose 
into pairs C, e.) 
We could put a bit more work into (Fin) as 
follows. Given an integer k > 0, let Du(/3) be 
4We can also introduce, as a binary connective on 
u-expressions and/or on d-expressions, although this 
would require a bit more work and would run against 
the spirit of underspecified representations, insofar as 
• spells out possible disambiguations. 
the subset of the set D(~) of sub-d-expressions 
of B, from which ~ can be constructed with < k 
applications of d-expression formation rules. (For 
example, D1 ((~ x :: a)(It Y ::/3)7) is 
with ~ and 7 buried too deeply to be included.) 
Now, for a fixed k, add to the side condition of 
(l'\]n) the requirement that sum(a) 9~ C U C' and 
eq(a, ff) 9~ C U C' for all/3' e Dk(/~); and choose 
e" to also rule out the possibility that a is ff for 
some ff E Dk(~). Clearly, the larger k is, the 
stronger the rule becomes. But so long as a satisfi- 
ability check is made after inference (as suggested 
by Corollary 4), it is not necessary that the con- 
straint set C in a sequent F I-c O that has been 
derived be reduced (to make all its consequences 
explicit) any more than it is necessary to require 
that C be satisfiable. (Concerning the latter, no- 
tice also that spurious sequents may drop out as 
further inferences are made, eliminating the need 
there to ever disambiguate.) 
To establish (the analog of) Corollary 4, a cru- 
cial property for a sequent rule 
rl t-cl O1 --- r, t-c. O, (,) 
r -cO 
to have is monotonicity: for every disambiguation 
p respecting C, p respects Ci for 1 < i < n. s (This 
is a generalization of Ci _C C, suggested by the en- 
coding above of e-disambiguations/, in terms of 
constraints.) To weed out spurious readings (con- 
sideration (W) above), side conditions might be 
imposed on (*), which ought (according to (I)) 
to be as simple as possible. The trick in design- 
ing C (and (*)) is to make inference }- just com- 
plicated enough so as, (D), not to put an undue 
burden on disambiguating at the end. The whole 
idea is to distribute the work between inferring se- 
quents and (subsequently) checking satisfiability. 
The claim is that the middle ground between the 
two extremes mentioned at the beginning of this 
section (i.e. between lax side conditions that leave 
the bulk of the work to disambiguation at the end, 
and strict side conditions that essentially reduce:: 
to :) is fertile. 
6 Discussion 
More than one reader (of a previous draft of this 
paper) has asked about linguistic examples. The 
5Compare to (Alshawi and Crouch, 1992). Mono- 
tonicity is used above for soundness, Proposition 2. 
Completeness, Proposition 3, follows from having 
enough such rules (*) (or equivalently, making the side 
conditions for (*) comprehensive enough). 
92 
Proceedings of EACL '99 
short, easy answer is that the sort of ambiguity 
addressed here can be syntactic (with types A 
ranging over grammatical categories) or seman- 
tic (with types drawn, say, from a higher-order 
predicate logic). Clearly, more must be said -- 
for example, to properly motivate the rules (:: c), 
(I-\[c) and (~"\]c) mentioned at the end of §2. De- 
tailed case studies are bound to push :: in various 
directions; and no doubt, after applying enough 
pressure, the system above will break: 
Be that as it may, I hope that case studies 
will be carried out (by others and/or by myself), 
testing, by stretching, the basic idea above. I 
close with a few words on that idea, and, beg- 
ging the reader's indulgence, on the theoretical 
background out of which, in my experience, it 
grew. From examining the binary connective • 
in (Fernando, 1997), I concluded that • is unlike 
any ordinary logical connective related to entail- 
ment because the force of • is best understood rel- 
ative not to entailment, but to translation. Un- 
derlying the distinction between entailment and 
translation is that between well-formed formulas 
and possibly ambiguous expressions (correspond- 
ing, in the present work, to :-types, on the one 
hand, and d: and u-expressions, on the other). An 
abstract picture relating the processes of trans- 
lation and entailment is framed in (Femando, in 
press), which I have attempted to flesh out here for 
the case of ITT, with a view to extending ITT's 
applications beyond anaphora to underspecifica- 
tion. The obvious step is to drop all types, and 
construe the terms as belonging to a type-free A- 
calculus. The twist above is that ambiguous ex- 
pressions are typed by d-expressions a, distinct 
from u-expressions .4. The construction is, in fact, 
quite general, and can be applied to linear deriva- 
tions as well. The essential point is to break free 
from a generative straitjacket, relaxing the infer- 
ence rules for derivations by collecting constraints 
that are enforced at various points of the deriva- 
tion, including the end. 
M. Dalrymple, J. Lamping, F.C.N. Pereira, and 
V. Saraswat. 1993. LFG semantics via con- 
straints. In Proc. Sixth European A CL. Univer- 
sity of Utrecht. 
M. Dalrymple, V. Gupta, J. Lamping, and 
V. Saraswat. 1997. Relating resource-based se- 
mantics to categorial semantics. Mathematics 
of Language 5, Saarbriicken. 
Kees van Deemter. 1996. Towards a logic of am- 
biguous expressions. In K. van Deemter and 
S. Peters, editors, Semantic Ambiguity and Un- 
derspecification. CSLI Lecture Notes Number 
55, Stanford. 
Tim Fernando. 1997. Ambiguity under changing 
contexts. Linguistics and Philosophy, 20(6). 
Tim Fernando. In press. A modal logic for non- 
deterministic discourse processing. Journal of 
Logic, Language and Information. 
Jean-Yves Girard, Yves Lafont, and Paul Tay- 
lor. 1989. Proofs and Types. Cambridge Tracts 
in Theoretical Computer Science 7. Cambridge 
University Press. 
Per Martin-LSf. 1984. Intuitionistic Type Theory. 
Bibliopolis, Napoli. Notes by Giovanni Sambin 
of a series of lectures given in Padua, June 1980. 
Glyn V. Morrill. 1994. Type Logical Grammar. 
Kluwer Academic Publishers, Dordrecht. 
Aarne Ranta. 1994. Type-Theoretical Grammar. 
Oxford University Press, Oxford. 
References 
H. Alshawi and R. Crouch. 1992. Monotonic se- 
mantic interpretation. In Proc. 30th Annual 
Meeting of the Association for Computational 
Linguistics. 
J. Carbonell and P. Hayes. 1987. Natural lan- 
guage understanding. In S. Shapiro, D. Eck- 
roth, and G. Vallasi, editors, Encyclopedia of 
Artificial Intelligence. Wiley and Sons, New 
York. 
93 
