Continuations
for Quantification

posted by Darryl on 27 Dec 2014

In this post, I'm going to talk about quantifiers. Not quantifiers as in the type theoretical quantifiers Pi and Sigma, but rather natural language quantifiers like "some", "all", "no", etc. One thing we need to do in implementing Language Engine is have a way of representing the meanings of these, and more specifically, the scope-taking properties that they have.

For simple sentences like "John saw Susan", it's easy to pretend like "John" and "Susan" just pick out some entities, perhaps like so:

[[John]] : Entity
[[John]] = john

[[Susan]] : Entity
[[Susan]] = susan

[[saw]] : Entity -> Entity -> Prop
[[saw]] = \x. \y. saw(y,x)

[[saw Susan]] : Entity -> Prop
[[saw Susan]] = \y. saw(y, susan)

[[John saw Susan]] : Prop
[[John saw Susan]] = saw(john, susan)

But this kind of analysis becomes tricky when we start considering sentences like "everyone saw Susan" or "John saw everyone". We might propose that subject quantifiers could be handled like so:

[[everyone]] : (Entity -> Prop) -> Prop
[[everyone]] = \p. forall x : Entity. p x

This would be perfectly able to combine with the verb phrase "saw Susan" on the above meaning assignment, to produce the intended meaning:

[[everyone saw Susan]] : Prop
[[everyone saw Susan]] = forall x : Entity. saw(x, susan)

But if we want to assign a meaning to object quantifiers in order to get a meaning for "John saw everyone", the assignment for subjects won't do. We need something different:

[[everyone]] : (Entity -> Entity -> Prop) -> Entity -> Prop
[[everyone]] = \p. \x. forall y : Entity. p x y

Now we can again get the intended meaning assignment:

[[saw everyone]] : Entity -> Prop
[[saw everyone]] = \x. forall y : Entity. saw(x,y)

[[John saw everyone]] : Prop
[[John saw everyone]] = forall y : Entity. saw(john, y)

But this comes with a heavy price to pay: every place that a quantifier can exist requires its own special version of the quantifier. What about "Stephen spoke to everyone" or "everyone's meal was flarn" or dozens of other examples? Each of this will require a different definition for "everyone".1 There are many ways to handle this, from introducing fancier syntax to letting the semantics compose in ways that aren't directly connected to the syntax. But what Language Engine does is use something called a continuation.

To start understanding what continuations are, let's abstract away from our examples a little bit. What we would like to do, ideally, is treat the meaning of "everyone" and "John" in similar ways. That is to say, abstractly we'd like something like this:

[[John ran]] = ran(john)

[[everyone ran]] = ran(something-involving-everyone)

Whatever this meaning is that we assign to "everyone ran", it needs to be equivalent using some mechanism to the one we want, i.e. forall x : Entity. ran(x). One way to do this is to make one the result of a transformation applied to the other, that is

  ran(something-involving-everyone)

= (by a magic transformation)

  forall x : Entity. ran(x)

If we could somehow perform the same transformation on other sorts of meanings, then we would have a solution:

  saw(something-involving-everyone, susan)

= (by a magic transformation)

  forall x : Entity. saw(x, susan)


  saw(john, something-involving-everyone)

= (by a magic transformation)

  forall y : Entity. saw(john, y)

This leads us to the concept of a continuation. Meanings such as these have a part-whole structure, and we can therefore view a whole, such as ran(john) as being a part john located in some context ran(_) (where the hole that john fills is indicated by the underscore). This context, ran(_), is called a continuation — in this case, a continuation for john. The choice of names comes from the idea that if you "start with" the part john, you can continue to build more structure by wrapping ran(_) around it.

A continuation is closely related to a function, in that, given any continuation K[_], you can construct the function \x. K[x] (provided x is not bound in the location of the hole). This very nearly gives us a solution: if we could pull out the continuation around something-involving-everyone and turn it into a function, and give it as an argument to the quantifier \p. forall x : Entity. p x, beta reduction would do the rest:

  (\p. forall x : Entity. p x) (\x. ran(x))

= (by beta-reduction multiple times)

  forall x : Entity. ran(x)



  (\p. forall x : Entity. p x) (\x. saw(x, susan))

= (by beta-reduction multiple times)

  forall x : Entity. saw(x, susan)
  
  
  
  (\p. forall y : Entity. p y) (\y. saw(john, y))
  
= (by beta-reduction multiple times)

  forall y : Entity. saw(john, y)

Well, from here it's relatively easy to define the transformation we want, and what something-involving-everyone should be. First, we just need to give some fixed syntax for something-involving-everyone. In principle we could just make up a new symbol just for "everyone", but we want to support other quantifiers too, so instead, we'll create a new syntactic wrapper around quantifier means like so:

if you have
  Q : (Entity -> Prop) -> Prop
then you can form
  shift{ Q } : Entity

Now our sentences have the meanings

[[everyone ran]] = ran(shift{ \p. forall x : Entity. p x })

[[everyone saw Susan]] = saw(shift{ \p. forall x : Entity. p x}, susan)

[[John saw everyone]] = saw(john, shift{ \p. forall x : Entity. p x})

And the transformation, called a continuation passing style (CPS) transform, can be defined in terms of shift and its continuation like so:

if you have
  K[shift{ Q }]
such that x is not bound in the hole in K[_]
transform it to
  Q (\x. K[x])

Each of our sentence meanings now transforms relatively directly:

  ran(shift{ \p. forall x : Entity. p x})

= (by CPS-transform, where K[_] = ran(_))

  (\p. forall x : Entity. p x) (\x. ran(x))

= (by beta-reduction multiple times)

  forall x : Entity. ran(x)
  
  
  
  saw(shift{ \p. forall x : Entity. p x }, susan)
  
= (by CPS-transform, where K[_] = saw(_, susan))

  (\p. forall x : Entity. p x) (\x. saw(x, susan))
  
= (by beta-reduction multiple times)

  forall x : Entity. saw(x, susan)
  
  
  
  saw(john, shift{ \p. forall y : Entity. p y })
  
= (by CPS-transform, where K[_] = saw(john, _))

  (\p. forall y : Entity. p y) (\y. saw(john, y))
  
= (by beta-reduction multiple times)

  forall y : Entity. saw(john, y)

The particular implementation algorithm for this sort of continuation can vary by preferred style. There's also a question of where the CPS-transform moves things to, as there are potentially many different "landing sites" that will work. In another post, I'll discuss a few options.

If you have comments or questions, get it touch. I'm @psygnisfive on Twitter, augur on freenode (in #languagengine and #haskell). Here's the HN thread if you prefer that mode, and also the Reddit thread.

Notes

1 The word "to" can be given a variety of possible meanings, but let's suppose we give it the following meaning:

[[to]] : Entity -> Prop -> Prop
[[to]] = \x. \p. directed(p,x)

The intention here being that directed(p,x) indicates that the proposition p is directed in some sense at entity x. We might prefer events for this, but that's a complication we can ignore for now.

Doing this, we get the meaning of "Stephen spoke to Susan" to be

[[Stephen spoke to Susan]] = directed(spoke(stephen), susan)

If we now wanted to define "everyone" to work in the position of "Susan" here, we could give the following definition:

[[everyone]] : (Entity -> Prop -> Prop) -> Prop -> Prop
[[everyone]] = \f. \p. forall x : Entity. f x p

Which gives "Stephen spoke to everyone" the meaning

  [[Stephen spoke to everyone]]

= (by definitions)

  (\f. \p. forall x : Entity. f p x)
    (\x. \p. directed(p,x))
    spoke(stephen)
  
= (by beta-reduction multiple times)

  forall x : Entity. directed(spoke(stephen), x)

To capture "everyone's meal was flarn" we'd need something like this for the meaning of the possessive "'s":

[['s]] : (Entity -> Prop) -> Entity -> Entity
[['s]] = \p. \x. poss(x,p)

Where poss(x,p) just is that thing which p holds of, such that it belongs to x. For example, poss(john,hat) is that thing which is a hat, and which belongs to John.

Now we can define "everyone":

[[everyone]] : (Entity -> Entity) -> (Entity -> Prop) -> Prop
[[everyone]] = \f. \p. forall x : Entity. p (f x)

Which now gives the sentence the meaning

  [[everyone's meal was flarn]]

= (by definitions)

  (\f. \p. forall x : Entity. p (f x))
    (\x. poss(x,meal))
    (\x. was(x, flarn))

= (by beta-reduction multiple times)

  forall x : Entity. was(poss(x,meal), flarn)