We propose a simple model of turn-taking in an information state based approach to dialogue using TTR (Type Theory with Records). The information state (dialogue gameboard) contains an agenda formulated as a list of speech event types that the dialogue participant plans to realize. A novel aspect of the proposal is that the agenda also includes types of events that intuitively should be carried out by an interlocutor. We argue that all dialogue events should be regarded as events jointly carried out by the dialogue participants and that this yields a simple formal method for representing turn-taking in a formal treatment of dialogue.
In the literature on TTR (Type Theory with Records), see Cooper and Ginzburg (2015) for a recent introduction, a connection is made between the notion of judgement in type theory (judging that an object or event is of a certain type) and perception, that is, perception involves classifying something as being of a certain type. We will describe this in this section. As we interact with our environment we not only perceive objects but also create new objects of certain types. Performing an action is creating an event of a particular type. A plan is a list of types which we hope to realize in this way. Thus we obtain a simple theory of action based on type theoretic ideas, which we will describe in Section 2. In Section 3 we will consider how coordinated action can be modelled in terms of games in this framework. We will see in Section 4 that this type theoretical view of action leads naturally to a notion of joint action and that this is important in order to obtain a theory of coordinated action. Finally, in Section 5, we will apply this view of action to turn taking in dialogue.
TTR is a type theory which takes many ideas
from Martin-Lo¨f type theory
A judgement can be thought of as an action which an agent carries out, for example, when an object is presented to its perceptual apparatus. Cooper (2014; Cooper (in prep) calls it a kind of type act (meant as a parallel to speech act) and presents a simple theory of action based on types. Basically, there are three things that you can do with types: (i) judge an object to be of a type (ii) wonder whether an object is of a type (iii) create a new object of a type. The third of these is important for this paper. Since we have types of situations (including events) we can regard actions as involving the creation of a situation of a certain type. Consider a particular boy, b and a particular dog, d. The type of situation in which b hugs d can be represented in TTR as a ptype (a type constructed from a predicate and appropriate arguments), ‘hug(b,d)’. It is no accident that the notation for this situation type is the same as that for a logical formula corresponding to a proposition. In this kind of type theory, types can serve as propositions (the “propositions as types” slogan1). When considered as propositions, they are true if there is something of the type and false if there is nothing of the type. Thus if b creates a situation of the type ‘hug(b,d)’, then b has guaranteed that the type is “true”. 3
Let us consider a slightly more complicated kind of situation. Suppose we have a human and a dog playing the game of fetch, where the human picks up a stick and throws it, the dog runs after the stick and brings it back to the human. This involves a string of events2 which could be regarded as witnesses for ptypes in TTR. If T1; : : : ; Tn are types, then T1_ : : : _Tn is a type whose witnesses are strings a1 : : : an such that ai : Ti for 1 i n. Thus a game of fetch between a human, a, and a dog, b, involving a stick, c could be characterized as having the type: pick up(a,c)_attract attention(a,b)_throw(a,c)_ run after(b,c)_pick up(b,c)_return(b,c,a) For technical reasons that will become apparent below we will use record types containing these ptypes instead of the simple ptypes: he:pick up(a,c)i_he:attract attention(a,b)i_ he:throw(a,c)i_he:run after(b,c)i_ he:pick up(b,c)i_he:return(b,c,a)i 1See Wadler (2015) for an account of the origins of this slogan from the perspective of computer science and Ranta (1994) for a discussion of its relevance for linguistic semantics
2The idea of events as strings come from work by Tim Fernando, most recently presented in Fernando (2015). This gives us a label ‘e’ which we can use as a pointer to pick out the individual subevents. A record, he=si, would be of type he:pick up(a,c)i just in case s:pick up(a,c). We can think of a record as modelling a situation with one or more facts which hold in it. Witnesses for record types may contain more facts than those required by the type. Thus "ee0==ss0# would also be a witness of this record type just in case the object, s, in the field labelled by ‘e’ is of the appropriate type. Fields with labels not mentioned in the type are ignored.
One aspect of coordination between the human and the dog is that they both realize that the game they are playing has this type. For each type in the string an event of that type has to be created and this has to be carried out in the appropriate order, of course. One way to do this is to think of the rules of the game as a collection of update functions addressing an agenda in the agents’ information state. An agenda is a list of types (that is, it is of type ‘[Type]’) which the agent plans to realize in order. An update function can come in one of two forms. The first form will map an information state of a given type to a new type which can then be used to compute a type for the new information state. The second form will map an information state of a given type and an event of a given type to a new type which can be used to compute a type for the new information state. The type of information state we are using here is hagenda:[RecType]i, that is the type of records which have a field labelled ‘agenda’ which contains a list of record types. (RecType is the type of record types and [RecType] is the type of lists of record types.) We can restrict the type of information states to be one where the agenda is required to be some specific list, L, by using a manifest field: hagenda=L:[RecType]i, the type of information states whose ‘agenda’-field contains the list, L.
The two forms of update function are illustrated with respect to the fetch game below.
r:hagenda=[]:[RecType]i .
hagenda=[he:pick up(a,c)i]:[RecType]i This function maps a state with an empty agenda to the type of states where the agenda contains a sole member the type of situation where a picks up c.
r:hagenda=[he:pick up(a,c)i]:[RecType]i . e: he:pick up(a,c)i .
hagenda=[he:attract attention(a,b)i]:[RecType]i
This function maps a state with the event type “a
picks up c” on the agenda and an event where a
picks up c to the type of state which has the type
“a attracts b’s attention” on the agenda. Such
functions can be used by an agent to predict what type
of information state could be licensed on the
basis of the agent’s current information state and,
in the case of the second function, also an
external event of a given type. The idea is that, if
f is such a function of type Ti ! RecType (or
Ti ! Te ! RecType) and r : Ti0 is the
current information state where Ti0 is a subtype of Ti
(and also e : Te0, where Te0 is a subtype of Te), the
type of the next information state is licensed to be
Ti0 ^. f (r) (or Ti0 ^. f (r)(e)). ‘ ^. ’ is the
operation of asymmetric merge
other-info:T with
hagenda=[he:attract attention(a,b)i]:[RecType]i is "agenda=[he:attract attention(a,b)i]:[RecType]# other-info:T
An important word in the characterization of update above is licensed. Actions are licensed by previous events of the appropriate type as specified by the game. There is, of course, no necessary inference that such an action will occur or even that the type will appear on anybody’s agenda. We can at any point decide to stop playing the game. What we can infer is that if we stop in the middle we will not have completed the game and that certain actions are necessary if we are to create an instance of the game type we have in mind. In this way the kind of inferencing that is involved here is enthymematic in the sense of Breitholtz (2014a), Breitholtz (2014b).
In Section 3 we have said something about what it might mean for agents to be coordinated on the type of the game they are playing and how they might update their agendas on the basis of previous events considered as events in a particular instance of the game. But we have said nothing about which event types go on which agent’s agenda. At first blush it seems there is a clear division of duties between the human and the dog in the game of fetch. The human has to pick up the stick, attract the dog’s attention and throw the stick. The dog has to run after it and bring it back to the human. Therefore it might appear that the first three types should, at the appropriate point in the game, appear on the human’s agenda and the other two types, again at an appropriate point in the game, appear on the dog’s agenda.
But let us think about this a little more carefully before we develop a formal treatment which involves the different types arriving on the appropriate agenda. Suppose the human picks up the stick and tries to realize the event type of attracting the dog’s attention. But the dog is facing the other way gnawing on a bone. The human perhaps calls to the dog but gets no response. Perhaps the human walks around the dog so that she is in the dog’s line of sight. The dog turns around taking the bone and faces away from the human. The game cannot continue. The dog has to make a contribution to the realization of the type ‘attract attention(a,b)’, look at the stick, and look excited, bark or jump up and down or something. The agent who realizes the type is not just the intuitive “first argument” to the predicate. The dog has to give some kind of feed-back that it is up for the game.
Consider another scenario, a little further on in the game. The stick has been thrown and the dog has run after it and has it in its mouth but then discovers that the human has disappeared. How can the dog realize the type ‘return(b,c,a)’ if a has wandered off somewhere and is nowhere to be seen? No, the human has to contribute to the realization of this type by at least staying close enough to the dog and in the dog’s line of sight when it turns round, quite possibly also by encouraging the dog and looking like she expects the stick to be brought back to her.
These actions are joint actions in the sense of Clark (1996), even if one of the agents is active and the other is fairly passive. Realizing the situation types in a game for two agents is not something that you can do on your own. The technical conclusion I would draw from this is that the types associated with the game are entered onto both agents’ agendas as the appropriate juncture in the game as specified by the update functions. Then even if there are types where you don’t have to make any kind of active contribution to realizing the type at least there will be a mechanism for causing you to wait until the type on the agenda has been realized before moving on and updating the agenda with a new type. This is known as turn taking. 5
I have dwelt at length on the non-linguistic example of the game of fetch because I believe that the basic strategies of coordination, including turntaking, in dialogue are really the same strategies needed by collaborating agents even without language. The event types involved are very different, involving types of speech events which on an evolutionary scale are extremely specialized and even arcane, but I would like to suggest that the basic turn-taking mechanism which enables coordination in speech is built on the kind of cognitive abilities and strategies necessary for coordinating agents independent of whether they have language or not. This is one reason that it seems important to embed a formal theory of language in a general formal theory of action.
In the literature involving gameboards of the
kind Ginzburg has proposed
We have suggested a simple notion of turn taking as a kind of coordination between information states in agents both in linguistic and nonlinguistic games and we have emphasized the importance of embedding a formal theory of language in a formal theory of action. It seems on this view that almost any speech act is a kind of joint action, albeit in many cases with a “leading” actor and a “supporting” actor.