Michael Moortgat
email: m.j.moortgat@uu.nl

Richard Moot
email: moot@labri.fr

Proofs nets and the categorial flow of information

The Lambek-Grishin calculus (LG) is a multiple-conclusion extension of Lambek's categorial type logic with dual families of fusion ('merge') and fission operations, and linear distributivity principles relating these two. Thanks to the distributivity principles, LG captures dependency patterns beyond context-free, both in syntax and semantics. In this paper we represent the information flow in categorial derivations in terms of a proof net graphical calculus. We study the correspondence between the composition graphs for these nets and the terms associated with focused sequent derivations.

Background, motivation

In this paper, we study LG, a type logic based on the generalization of Lambek's Syntactic Calculus proposed in Grishin (1983). The formula language of this

Algebraically, LG combines the residuated triple of (3) -fusion with its two residuals -with the dual residuated triple in (4): fission, left and right difference.

A  A ; from A  B and B  C infer A  C (2) A  C/B iff A ⌦ B  C iff B  A\C (3) B ; C  A iff C  B ⊕ A iff C ↵ A  B (4)
For the interaction between the fusion and fission families, we have the postulates of (5). 1 These postulates have come to be called linear distributivity principles (e.g. Cockett and Seely (1996)): linear, because they respect resources (no material gets copied).

(A ; B) ⌦ C  A ; (B ⌦ C) C ⌦ (B ↵ A)  (C ⌦ B) ↵ A C ⌦ (A ; B)  A ; (C ⌦ B)( B ↵ A) ⌦ C  (B ⌦ C) ↵ A (5)
LG is attractive for syntactic and for semantic reasons. Syntactically, the interaction principles of (5) bring expressivity beyond context-free. Moot (2007) gives an LG encoding of the adjunction operation of Tree Adjoining Grammar, the most restricted formalism in the mildly context-sensitive hierarchy Kallmeyer (2010); Moortgat (2009) has an LG grammar for MIX, according to Salvati (p.c.) an instance of a non-wellnested 2-MCFG. The upper bound for the syntactic expressivity of LG grammars in their full generality is open; see Melissen (2010) for discussion.

At the semantic level, LG derivations can be given an interpretation in the continuation-passing style. The CPS interpretation leads to a considerable simplification of the syntax/semantics interface: semantic scope construal can be obtained on the basis of simple first-order syntactic types, as shown in Bastenhof (2012) and discussed in §3.1.

Despite these attractions, working with the standard 'symbolic' presentations of LG involves rather formidable technical machinery. Our focus in this paper is on proof nets -an elegant graphical calculus that captures the essence of LG derivations without the bureaucracy of heavy symbol manipulation.

Display sequent calculus and proof nets

A sequent calculus for LG, in the 'display logic' style, can be found in Goré (1997). We present it in §2.1, using the notation of Moortgat (2009). In §2.2, we introduce the proof net graphical calculus, and show how it leads to a representation of LG derivations that is free of spurious ambiguities.

sLG: display sequent calculus

The characteristic feature of Display Logic is that for every logical connective, there is a corresponding structural connective, not just for conjunction and disjunction as in standard sequent calculus. We use the same symbols for the logical operations and their structural counterparts; structural operations are marked off by centerdots. Below the grammar for input (sequent left hand side), and output structures (sequent rhs). Atomic structures are formulas F .

I ::= F|I•⌦•I|I•↵•O|O•; •I O ::= F|O•⊕•O|I•\•O|O•/ •I (6)
Figures 1 and 2 then give the structural and logical rules of sLG. The (dual) residuation principles take the form of 'display postulates', so called because they allow any formula component of a structure to be displayed as the sole occupant of the sequent lhs or rhs. The logical rules apply to formulas thus displayed. The one-premise rules simply replace a logical connective by its structural counterpart; these rules are invertible. The non-invertible two-premise rules give expression to the monotonicity properties of the type-forming operations. The distributivity principles (5) appear in rule form here as G1 -G4 in the structural group.

A ) A Ax X ) AA ) Y X ) Y Cut X ) Z • / • Y X •⌦•Y ) Z rp Y ) X •\•Z rp Y • ; • Z ) X Z ) Y •⊕•X drp Z •↵•X ) Y drp X •⌦•Y ) Z •⊕•W Z • ; • X ) W • / • Y G1 X •⌦•Y ) Z •⊕•W Y •↵•W ) X •\•Z G3 X •⌦•Y ) Z •⊕•W Z • ; • Y ) X •\•W G2 X •⌦•Y ) Z •⊕•W X •↵•W ) Z • / • Y G4 Figure 1: sLG. Structural rules. A • $ • B ) Y A $ B ) Y $L $ 2 {⌦, ;, ↵} X ) A • # • B X ) A # B #R # 2 {⊕, /, \} X ) AY ) B X •⌦•Y ) A ⌦ B ⌦R A ) XB ) Y A ⊕ B ) X •⊕•Y ⊕L X ) AB ) Y A\B ) X •\•Y \L X ) AB ) Y X •↵•Y ) A ↵ B ↵R X ) AB ) Y B/A ) Y • / • X /L X ) AB ) Y Y • ; • X ) B ; A ;R Figure 2: sLG. Logical rules.
It is shown in Moortgat (2009) that the display sequent format sLG enjoys cut elimination and thus allows for decidable proof search. Still, there is room for improvement:

• spurious ambiguity: as with sequent calculi in general, one and the same matching of occurrences of atomic subformulae in a proof's axiom leaves may be obtained in different ways as a result of irrelevant rule permutations;

• no parsing: backward chaining sequent proof search requires the structure of the formulas making up the end sequent to be given in advance; for genuine LG parsing, one would like this structure to be computed as the outcome of the deduction process;

• display equivalences represent alternative views on one and the same structure: one would like to have a proof format where there is no need for the explicit structural manipulations of the display postulates.

The proof net approach to be discussed below removes these problematic aspects.

Proof nets

Proof nets are a graphical way of representing proofs, introduced first for linear logic Girard (1987). The proof nets for LG we present in this section are a simple extension of the proof nets for the multimodal Lambek calculus of Moot and Puite (2002). A proof structure is a (hyper)graph where the vertices are labeled by formulas and the edges connect these formulas. 2 The hyperedges correspond to the logical rules, linking the active formulas and the main formula of the rule and keeping track of whether one is dealing with a non-invertible two-premise rule or with an invertible one-premise rule. We'll call these tensor and cotensor links respectively.

Definition 2.1. A link is a tuple ht, p, c, mi where

• t is the type of the link -tensor or cotensor

• p is the list of premises of the link,

• c is the list of conclusions of the link,

• m, the main vertex/formula of the link, is either a member of p, a member of c or the constant "nil".

In case m is a member of p we speak of a left link (corresponding to the left rules of the sequent calculus, where the main formula of the link occurs in the antecedent) and in case m is a member of c we speak of a right link.

Graphically, links are displayed as shown below. A central node links together the premises and conclusions of the link; when we need to refer to the connections between the central node and the vertices, we will call them its tentacles.

The interior of this central node is white for a tensor link and black for a cotensor link. The premises are drawn, in left-to-right order, above the central node and the conclusions, also in left-to-right order, are drawn below it. The main formula of cotensor links is drawn with an arrow towards it; the main formula of a tensor link can only be determined by inspection of the formulas.

P 1 ••• P m C 1 ••• C n tensor rule P 1 ••• P m C 1 ••• C n
cotensor rule (right rule)

P 1 ••• P m C 1 ••• C n cotensor rule (left rule)
Figure 3 shows the links for LG. The links for the fission connectives are updown symmetric versions of the links for the fusion connectives.

Definition 2.2. A proof structure hS, Li is a finite set of formula occurrences S and a set of links L from those shown in Figure 3 such that

• each formula is at most once the premise of a link,

• each formula is at most once the conclusion of a link.

Formulas which are not the conclusion of any link are called the hypotheses of the proof structure. Formulas which are not the premise of any link are called the conclusions of the proof structure.

We will say that a proof structure with hypotheses H 1 ,...,H m and conclusions

C 1 ,...,C n is a proof structure of H 1 ,...,H m ) C 1 ,...C n .
Example 1. Figure 4 shows the hypothesis unfolding of (s ↵ s) ; np and the conclusion unfolding of s / (np \ s). Both are obtained by simple application of the rules of Figure 3 until we reach the atomic subformulas.

Though the figure satisfies the condition on proof structures (connectedness is not a requirement), it is a proof structure of (s↵s);np, s, s, np ) s/(np\s), s, s, np.

We obtain a proof structure of (s ↵ s) ; np ) s / (np \ s) by identifying atomic formulas. 3 In this case, we choose to identify the top s of the left subgraph Fusion connectives -hypothesis Due to the graphical constraints of writing these proof nets on the planewe want to draw the np \ s node below the cotensor link at the bottom of the figure, since it is a conclusion of this link, but would have to draw the figure on a cylinder to make this work -we need to use curved tentacles connect the minor premise of (co-)implication links to the rest of the proof structure.

[L/] A A / B B [L⌦] A ⌦ B A B [L\] A B B \ A Fusion connectives -conclusion [R/] A A / B B [R⌦] A ⌦ B A B [R\] A B B \ A Fission connectives -hypothesis [L↵] A A ↵ B B [L⊕] A ⊕ B A B [L;] A B B ; A Fission connectives -conclusion [R↵] A A ↵ B B [R⊕] A ⊕ B A B [R;] A B B ; A
Definition 2.3. An abstract proof structure hV, L, h, ci is a set of vertices V, a set of (unlabeled) links L and two functions h and c, such that

• each formula is at most once the premise of a link,

• each formula is at most once the conclusion of a link,

• h and c are functions from the hypotheses resp. conclusions of the abstract proof structure to formulas Note that the abstract proof structure corresponding to a two formula sequent

A ) B has only a single vertex v, with h(v) = A and c(v) = B.
The transformation from proof structure to abstract proof structure is a forgetful mapping: we transform a proof structure into an abstract proof structure by erasing all formula information on the internal vertices. Visually, we remove the formula labels from the graph and replace them by simple vertices (⇧). We indicate the results of the functions h and c above (resp. below) the vertices (for the hypotheses and conclusions respectively). As a result, we have to following four types of vertices in an abstract proof structure.

⇧⇧⇧⇧ A B A B

internal hypothesis conclusion both

Example 2. Figure 5 shows (on the right) the transformation of the proof structure on its left into an abstract proof structure.

Definition 2.4. A tree is an acyclic, connected abstract proof structure which does not contain any cotensor links.

The trees of Definition 2.4 correspond to sequents in a rather direct way. In fact, they have the pleasant property of "compiling away" the display rules of the sequent calculus. Or, in other words, trees represent a class of sequents which is equivalent up to the display postulates.

Definition 2.5. Given an abstract proof structure A, we say that A contracts in one step to A 0 , written A ! A 0 iff A 0 is obtained from A by replacing one of the subgraphs of the form shown in Figures 6 and7 by a single vertex.

H ⇧ C
H represents the result of the function h for the indicated node (relevant only in case this node is a hypothesis of the abstract proof structure). Similarly, C represents the formula assigned by the function c to the indicated node.

[R/]

⇧ H ⇧ ⇧ ⇧ C [L⌦] ⇧ C ⇧ ⇧ H ⇧ [R\] ⇧ H ⇧ ⇧ ⇧ C Figure 6: Contractions -Lambek connectives [L↵] ⇧ ⇧ C ⇧ H ⇧ [R⊕] ⇧ C ⇧ ⇧ H ⇧ [L;] ⇧ ⇧ C ⇧ H ⇧ Figure 7: Contractions -Grishin connectives
Given an abstract proof structure A we say that A contracts to an abstract proof structure A 0 if there is a sequence of zero or more one step contractions from A to A 0 .

When we say that a proof structure P contracts to an abstract proof structure A 0 we will mean that the underlying abstract proof structure A of P contracts to A 0 .

To obtain expressivity beyond context-free, we are interested in LG with added interaction principles. Figures 8 and9 give the additional rewrite rules on abstract proof structures that correspond to the rule form of Grishin's distributivity laws.

Definition 2.6. A proof structure P is a proof net iff its underlying abstract proof structure A converts to a tree using the contractions of Figures 6 and 7 and the

X ⇧ ⇧ ⇧ V Y ⇧ ⇧ W ⇧ ⇧ W ⇧ V X ⇧ Y ⇧ Y ⇧ ⇧ W ⇧ X ⇧ ⇧ V G1 G3 Figure 8: Grishin interactions I -"mixed associativity" Y ⇧ ⇧ ⇧ V X ⇧ ⇧ W ⇧ ⇧ W ⇧ V X ⇧ Y ⇧ X ⇧ ⇧ W ⇧ Y ⇧ ⇧ V G2 G4
Figure 9: Grishin interactions II -"mixed commutativity" structural rules of Figures 8 and9.

Theorem 1. A proof structure P is a proof net -that is, P converts to a tree T -iff there is a sequent proof of T.

The proof is an easy adaptation of the proof of Moot and Puite (2002). A detailed proof can be found in Moot (2007).

Example 3. We show that the proof structure of Figure 5 is a proof net by contracting it to a tree. Starting with rule (G1), the two cotensor links can be contracted in any order. Figure 10 shows a complete sequence.

Example 4. For a second example (to be taken up again when we discuss focused proof search in §3) we turn to Figure 11 which shows the lexical proof structures for a generalized quantifier noun phrase, a transitive verb, a determiner and a lexical noun.

Consider the sentence 'everyone likes the teacher'. In the unfocused sequent calculus sLG, the sequent (np proofs, depending on the order of application of the introduction rules for the five occurrences of the logical connectives involved: ⌦ (once), / (three times), \ (once). Figure 12 gives, on the left, the single possible identification of n and np formulas that gives rise to a proof net with the lexical entries in the desired order. The corresponding abstract proof structure is given in the middle. This abstract proof structure allows us to apply a contraction directly, as shown on the right.

/ n) ⌦ n, (np \ s) / np, np / n, n ) s has at least seven ⇧ ⇧ ⇧ ⇧ ⇧ (
The table below summarizes the correspondence between proof nets and sequent proofs. The invertible one-premise rules correspond to both a link and a contraction and the interaction rules are invisible in the proof structure, appearing only in the conversion sequence.

(np / n) ⌦ n np / n n np np \ s s (np \ s) / np np np / n n (np/n)⌦n ⇧ ⇧ ⇧ ⇧ ⇧ ⇧ s (np\s)/np ⇧ ⇧ np/n ⇧ n ⇧ (np/n)⌦n ⇧ ⇧ ⇧ s (np\s)/np ⇧ ⇧ np/n ⇧ n ⇧ L⌦ Figure 12: (np / n) ⌦ n, (np \ s) / np,
With a bit of extra effort in the sequentialization proof (and the exclusion of cuts on axioms) we can show that these correspondences are 1-to-1, that is each axiomatic formula in a proof net corresponds to exactly one axiom rule in the sequent proof, each non-invertible two-premise rule corresponds to exactly one link in the proof net and each invertible one-premise rule to exactly one link in the proof net and exactly one contraction in its conversion sequence.

Summing up, the proof net approach offers the following benefits in comparison to sequent proof search.

• Parsing. Whereas for sequent proof search the structure of the sequent has to be given, the contraction sequence that identifies a proof structure as a proof net actually computes this structure.

• Removal of spurious ambiguity. Proof nets, like (product-free) natural deduction, have different proof objects only for proofs of a judgement which differ essentially. The combinatorial possibilities for such readings, which are obtained by finding a complete matching of the premise and conclusion atomic formulas, can easily be enumerated for a given sequence of formulas.

• Display rules compiled away. The tensor trees associated with wellformed proof nets represent a class of sequents which is equivalent up to the display postulates.

Proof nets and focused display calculus

The spurious non-determinism of naive backward-chaining proof search can also be addressed within the sequent calculus itself, by introducing an appropriate notion of 'normal' derivations. In §3.1, we introduce fLG, a focused version of the sequent calculus for LG. In §3.2, we then study how to interpret focused derivations from a proof net perspective.

fLG: focused display calculus

The strategy of focusing has been well-studied in the context of linear logic, starting with the work of Andreoli Andreoli (2001). It is based on the distinction between asynchronous and synchronous non-atomic formulas. The introduction rule for the main connective of an asynchronous formula is invertible; it is noninvertible for the synchronous formulas. Backward chaining focused proof search starts with an asynchronous phase where invertible rules are applied deterministically until no more candidate formulas remain. At that point, a non-deterministic choice for a synchronous formula must be made: this formula is put 'in focus', and decomposed in its subformulae by means of non-invertible rules until no more non-invertible rules are applicable, at which point one reenters an asynchronous phase. The main result of Andreoli ( 2001) is that focused proofs are complete for linear logic.

Focused proof search for the Lambek-Grishin calculus has been studied by Bastenhof ( 2011) who uses a one-sided presentation of the calculus. In this section, we implement his focusing regime in the context of the two-sided sequent format of Bernardi and Moortgat (2010). We proceed in two steps.

First we introduce fLG, the focused version of the sequent calculus of §2.1. fLG makes a distinction between focused and unfocused judgements, and has a set of inference rules to switch between these two. fLG comes with a term language that is in Curry-Howard correspondence with its derivations. This term language is a directional refinement of the λµe µ language of Curien and Herbelin (2000).

The second step is to give a constructive interpretation for LG derivations by means of a continuation-passing-style translation: a mapping d•e that sends derivations of the multiple-conclusion source logic to (natural deduction) proofs in a fragment of single-conclusion intuitionistic Linear Logic MILL (in the categorial terminology: LP). For the translation of Bastenhof ( 2011) that we follow here, the target fragment has linear products and negation A ? , i.e. a restricted form of linear implication A (?, where ? is a distinguished atomic type, the response type. Focused source derivations then can be shown to correspond to distinct normal natural deduction proofs in the target calculus.

!

For the linguistic illustrations in §3.2, we compose the CPS translation d•e with a second mapping • `, that establishes the connection with Montague-style semantic representations. This mapping sends the linear constructs to their intuitionistic counterparts, and allows non-linear meaning recipes for the translation of the lexical constants.

fLG: proofs and terms

In the Curry-Howard proofs-as-programs tradition, we set up fLG starting from a term language for which the sequent logic then provides the type system. The term language encodes the logical steps of a derivation (left and right introduction rules, and the new set of left and right (de)focusing rules, to be introduced below); structural rules (residuation, distributivity) leave no trace in the proof terms.

Sequent structures, as in §2.1, are built out of formulas. Input formulas now are labeled with variables x, y, z,..., output formulas with covariables ↵, β, γ, . . ..

To implement the focusing regime, we allow sequents to have one displayed formula in focus. Writing the focused formula in a box, fLG will have to deal with three types of judgements: sequents with no formula in focus (we'll call these structural), and sequents with a succedent or antecedent formula in focus.

X `YX `A

A `Y

Corresponding to the types of sequents, the term language has three types of expressions: commands, values and contexts respectively. For commands, we use the metavariables c, C, for values v, V, for contexts e, E. The typing rules below provide the motivation for the subclassification.

v ::= µ↵.C | V ; V ::= x | v 1 ⌦ v 2 | v ↵ e | e ;
C ::= c | xy z .C | x β z .C | β x z .C | ↵β γ .C | x β γ .C | β x γ .C (7)
Typing rules To enforce the alternation between asynchronous and synchronous phases of focused proof search, formulas are associated with a polarity: positive for non-atomic formulas with invertible left introduction rule: A ⌦ B, A ↵ B, B ; A; negative for non-atomic formulas with invertible right introduction rule: A ⊕ B, A\B, B/A. For atomic formulas, one can fix an arbitrary polarity. Different choices lead to different prooftheoretic behaviour (and to different interpretations, once we turn to the CPS translation). We will assume that atoms are assigned a bias (positive or negative) in the lexicon. Below the typing rules for fLG (restricting attention to the cut-free system).

(Co-)Axiom, (de)focusing First we have the focused version of the axiomatic sequents, and rules for focusing and defocusing which are new with respect to the unfocused presentation of §2.1. There is a polarity restriction on the formula A in these rules: the boxed formula has to be negative for CoAx, µ, e µ ⇤ ; for Ax, e µ, µ ⇤ it has to be positive. In the (Co-)Axiom cases, A can be required to be atomic.

x : A `x : A Ax ↵ : A `↵ : A CoAx X `V : A hV ↵i :(X `↵ : A) µ ⇤ E : A `X hx ⇠ Ei :(x : A `X) e µ ⇤ C :(x : A `X) e µx.C : A `X e µ C :(X `↵ : A) X `µ↵.C : A µ (8)
From a backward-chaining perspective, the µ, e µ rules remove the focus from a focused succedent or antecedent formula. The result is an unfocused premise sequent, the domain of applicability of the invertible rules, i.e. one enters the asynchronous phase. From the same perspective, the rules µ ⇤ , e µ ⇤ place a succedent or antecedent formula in focus, shifting control to the non-invertible rules of the synchronous phase. The µ ⇤ , e µ ⇤ rules are in fact instances of Cut where one of the premises is axiomatic.

Invertible rules

The term language makes a distinction between simple commands c (the image of the focusing rules e µ ⇤ ,µ ⇤ : hx ⇠ Ei, hV ↵i) from extended commands C. The latter start with a sequence of invertible rewrite rules replacing a logical connective by its structural counterpart. We impose the requirement that in the asynchronous phase all formulas to which an invertible rule is applicable are indeed decomposed.

C :(x : A •⌦•y : B `X) xy z .C :(z : A ⌦ B `X) ⌦L C :(X `↵ : A •⊕•β : B) ↵β γ .C :(X `γ : A ⊕ B) ⊕R C :(x : A •↵•β : B `X) x β z .C :(z : A ↵ B `X) ↵L C :(X `x : A •\•β : B) x β γ .C :(X `γ : A\B) \R C :(β : B • ; • x : A `X) β x z .C :(z : B ; A `X) ;L C :(X `β : B • / • x : A) β x γ .C :(X `γ : B/A) /R (9)
Non-invertible rules When a positive (negative) formula has been brought into focus in the succedent (antecedent), one is committed to transfer the focus to its subformulae.

e 1 : B `Ye 2 : A `X e 1 ⊕ e 2 : B ⊕ A `Y •⊕•X ⊕L X `v1 : A Y `v2 : B X •⌦•Y `v1 ⌦ v 2 : A ⌦ B ⌦R X `v : A e : B `Y v\e : A\B `X •\•Y \L X `v : A e : B `Y X •↵•Y `v ↵ e : A ↵ B ↵R e : B `YX `v : A e/v : B/A `Y • / • X /L e : B `YX `v : A Y • ; • X `e ; v : B ; A ;R (10)
Derived inference rules: focus shifting To highlight the correspondence with the algorithm for proof net construction to be discussed in §2.2, we will use a derived rule format for shifting between a conclusion and premise focused formula. A branch from (e µ ⇤ ) via a sequence (possibly empty) of structural rules and rewrite rules to (µ) is compiled in a derived inference rule with the e µ ⇤ restrictions on A and the µ restrictions on B.

E : A `Y hx ⇠ Ei :(x : A `Y) e µ ⇤ . . . (res, distr, rewrite) . . . (÷)hx ⇠ Ei :(X `β : B) X `µβ.(÷)hx ⇠ Ei : B µ { E : A `Y X `µβ.(÷)hx ⇠ Ei : B ↵
For the combinations of µ ⇤ , e µ ⇤ and µ, e µ, this results in the focus shifting rules below. We leave it to the reader to add the terms.

A `Y X `B ↵ X 0 `A X `B * + X `A B `Y ⌦ A `Y0 B `Y ( ) (11)
Example 5. We illustrate the effect of the focusing regime with some alternative ways of assigning a polarity bias to atomic formulas with a simple Subject-Transitive Verb-Object sentence. Examples with lexical material filled in would be 'everyone seeks/finds a unicorn'.

(np/n ⌦ n) •⌦•((np\s)/np •⌦•(np/n •⌦•n)) `s (12)
For the Object we have a Determiner-Noun combination. For the Subject, we take a product type (np/n)⌦n, so that we have a chance to illustrate the working of the asynchronous phase of the derivation. In the discussion of Figure 12, we saw that (12) has multiple proofs in the unfocused sequent calculus, but only one proof net, i.e. one way of matching the premise and conclusion atoms.

What about the focused calculus fLG? Before answering this question, we have to decide on the polarization of the atomic types. Suppose we give them uniform negative bias. There is only one focused proof then, with proof term (13): 'goal driven', top-down, to use parsing terminology. In the proof term, we write tv for the transitive verb; det for the object determiner; noun for the object common noun; subj for the subject noun phrase.

µβ.( yz subj .h tv ⇠ ((Q \ β) / Q 0 ) i) with Q : µγ.h y ⇠ (γ / µγ 0 .h z ⇠ γ 0 i)i , Q 0 : µ↵.h det ⇠ (↵ / µ↵ 0 .h noun ⇠ ↵ 0 i)i (13)
As an alternative, suppose basic type s keeps its negative bias, resetting the sentence continuation for each clausal domain, but the other basic types are assigned positive bias. We now have two focused derivations: 'data driven', bottom-up. To make sense of this difference, we will have to look at the CPS translation of these proofs, to be introduced below.

µ↵.(

x 0 z subj .h x 0 ⇠ (e µx.h det ⇠ (e µy.h tv ⇠ ((x \ ↵) / y) i / noun) i / z) i) (14)
((x \ ↵) / y) i / z) i / noun) i) (15)
CPS translation Let us turn then to the translation that associates the proofs of the multiple-conclusion source logic fLG with a constructive interpretation, i.e. a linear lambda term of the target logic MILL/LP. CPS translations for LG were introduced in Bernardi and Moortgat (2007;2010), who adapt the call-byvalue and call-by-name regimes of Curien and Herbelin (2000) to a directional environment. The translation of Bastenhof (2011) (following Girard (1991)) is an improvement in that it avoids the 'administrative redexes' of the earlier approaches: the image of LG source derivations, under the mapping from Bastenhof (2011) that we present below, are normal LP terms.

The target language, on the type level, has the same atoms as the source language, and in addition a distinguished atom ?, the response type. Complex types are linear products -⌦-and a defined negation A ? .

= A (?. The CPS translation d•e maps fLG source types, sequents and their proof terms to the target types and terms in Curry-Howard correspondence with normal natural deduction proofs.

Types For positive atoms, dpe = p, for negative atoms dpe = p ? . For complex types, the value of d•e depends on the polarities of the subtypes as shown in Table 1.

Terms The action of d•e on terms is given in ( 16). We write e x, e ↵ for the target variables corresponding to source x,↵. The (de)focusing rules correspond to application/abstraction in the target language. Non-invertible (two premise) rules are mapped to linear pair terms; invertible rewrite rules to the matching deconstructor, the case construct (', , ⇠ metavariables for the the (co)variables involved).

Proof nets and focusing

We saw in §3.1 that fLG may allow multiple derivations from one and the same set of (co)axiom judgements. These derivations would be identified under the proof net perspective of §2.2. To establish the correspondence with fLG derivations, we introduce term-labeled proof nets, and show how a proof term can be read off from the composition graph associated with a net.

Our approach is comparable to the algorithm of de Groote and Retoré (1996), which computes a linear lambda term from a traversal of the dynamic graph associated with a proof net for a derivation in the Lambek calculus L. For singleconclusion L, the term associated with a given proof net is unique; in the case of multiple-conclusion LG the term computation algorithm may associate more than one term with a proof net. These multiple results will then be shown to correspond to the derivational ambiguity of focused proof search.

Reduction tree

In order to analyse the structure of a conversion sequence in more detail, we introduce the notion of a proof net component: Definition 3.1. Given a proof net P,acomponent C of P is a maximal subnet of P containing only tensor links.

From a proof net, we can obtain its components by simply erasing all cotensor links. The components will be the connected components (in the graphtheoretic sense) of the resulting graph. To simplify the following discussion, unless otherwise indicated, we will use the word component to refer only to components containing at least one tensor link.

When P is a proof net (and therefore converts to a tensor tree using a sequence ⇢ of conversions and contractions) the components of P can bee seen as a parallel representation of the synchronous phases in sequent proof search. In ⇢, all interaction rules operate in one component C, the cotensor rules and the corresponding contractions join two different components (though the component connected to the main vertex can be trivial here). When multiple cotensor links have both active tentacles attached to a single component (Figure 10 shows an example), we apply all contractions simultaneously, repeating this process until no further contractions apply.

So instead of seeing ⇢ as a sequence of reductions, we can see it as a rooted tree of reductions: the initial components are its leaves (synchronous phases) and the contractions, which join components, are its branches (the branches from the active components to their parents correspond to asynchronous phases) and the final tree -a single component -is its root (we will see an example in Figure 19 below). Note that this same observation is essential to the cut elimination proof of Moot and Puite (2002).

Nets and term labeling When assigning a term label to a proof net, our algorithms will assign labels to larger and larger subnets of a given proof net, until we have computed a term for the complete proof net. Like in the sequent calculus, we distinguish between subnets which are commands, contexts and values. Figure 13 shows how we will distinguish these visually: the main formula of a subnet is drawn white, other formulas are drawn in light gray, values are drawn inside a rectangle, contexts inside an oval.

Figure 14 gives the term-labeled version of the proof net links corresponding to the logical rules of the sequent calculus. The flow of information is shown by the arrows: information flow is always from the active formulas to the main formula of a link, and as a consequence the complex term can be assigned either to a conclusion or to a premise of the link. This is the crucial difference with term labeling for the single-conclusion Lambek calculus, where the complex term is always assigned to a conclusion. The cotensor rules, operating on commands, indicate the prefix for the command corresponding to the term assignment for the rule (we will see later how commands are formed).

The proof term of an LG derivation is computed on the basis of the composition graph associated with its proof net.

Definition 3.2. Given a proof net P, the associated composition graph cg(P) is obtained as follows. (a) follow an unvisited command link attached to a previously calculated maximal subnet, forming a correct command subnet; like before, we restrict to active subnets which do not contain (or allow us to reach through an axiom) the main formula of a negative link; (b) for each negative link with both active formulas attached to the current command subnet, pass to the main formula of the negative link, forming a new command, repeat this step until no such negative links remain attached; (c) follow a µ or e µ link to a new vertex, forming a larger value or context subnet and replacing the variable previously assigned to the newly visited vertex by the µ value or e µ context.

The algorithm stays quite close to the focused derivations of the previous section: the maximal subnets of step 1 are rooted versions of the components we have used before, with the directions of the arrows potentially splitting components into multiple rooted components (Figure 18 will give an example) and the asynchronous phases, which consisted of one or more contractions for cotensor links, will now consist of a passage through a command link, followed by zero or more cotensor links, followed by either a µ or a e µ link, the result being a new, larger subnet. The term assignment algorithm is a way to enumerate the non-equivalent proof terms of a net. Given that these terms are isomorphic to focused sequent proofs, it is no coincidence that the computation of the proof terms looks a lot like the sequentialisation algorithm.4

Lemma 1. If P is a proof net (with a pairing of command and µ/e µ links) and v is a term calculated for P using this pairing then there is a sequent proof π which is assigned v

  logic is given in (1).A, B ::= p | atoms: s, np,...A ⌦ B | B\A | A/B | product, left vs right division A ⊕ B | A ↵ B | B ; A coproduct, right vs left difference (1)

Figure 3 :Figure 5 :

 35 Figure 3: Links for proof structures of the Lambek-Grishin calculus

Figure 10 :Figure 11 :

 1011 Figure 10: Reducing the abstract proof structure of Figure 5 to a tree.

  v e ::= e µx.C | E ; E ::= ↵ | e 1 ⊕ e 2 | v\e | e/v c ::= hx ⇠ Ei|hV ↵i

(

  co)var dxe = e x ; d↵e = e ↵ linear application dhx ⇠ Eie = (e x dEe);dhV ↵ie = (e ↵ dVe) linear abstraction de µx.Ce = λe x.dCe ; dµ↵.Ce = λe ↵.dCe linear pair d'# e = hd'e, d ei (# 2 {⌦, /, \, ⊕, ↵, ;}) case d ' ⇠ .Ce = case e ⇠ of he ', e i.dCe (16) Sequents For sequent hypotheses/conclusions, we have pol(A) dx : Aed ↵ : Ae + e x : dAe e ↵ : dAe ? -e x : dAe ? e ↵ : dAe (17)

  d(13)e = λ e β.(case subj `of he y,e zi.(tv `hhλe γ.(e y he γ, λe γ 0 .(e z e γ 0 )i), e βi,λe ↵.(det `he ↵, λe ↵ 0 .(noun `e ↵ 0 )i)i)) d(13)e `= λc.(8 λx.(() (person x)) (c ((needs λw.(9 λy.((^(unicorn y)) (wy)))) x)))) d(14)e = λe ↵.(case subj `of he x 0 ,e zi.(e x 0 hλe x.(det `hλe y.(tv `hhe x, e ↵i, e yi), noun `i),e zi)) d(14)e `= λc.(8 λx.(() (person x)) (9 λy.((^(unicorn y)) (c ((likes y) x)))))) d(15)e = λe ↵.(case subj `of he x 0 ,e zi.(det `hλe y.(e x 0 hλe x.(tv `hhe x, e ↵i, e yi),e zi), noun `i)) d(15)e `= λc.(9 λy.((^(unicorn y)) (8 λx.(() (person x)) (c ((likes y) x))))))

Figure 13 :

 13 Figure 13: Proof nets with term labels: commands, context and values

Figure 16 :

 16 Figure 14: LG links with term labeling

Table 1 :

 1 CPS translation: non-atomic types

	pol(•)
	AB		dA ⌦ Be	dA/Be	dB\Ae	dA ⊕ Be	dA ↵ Be	dB ; Ae
	--dAe ? ⌦dBe ?	dAe⌦dBe ?	dBe ? ⌦dAe	dAe⌦dBe	dAe ? ⌦dBe	dBe⌦dAe ?
	-+	dAe ? ⌦dBe	dAe⌦dBe	dBe⌦dAe	dAe⌦dBe ?	dAe ? ⌦dBe ? dBe ? ⌦dAe ?
	+ -	dAe⌦dBe ?	dAe ? ⌦dBe ? dBe ? ⌦dAe ?	dAe ? ⌦dBe	dAe⌦dBe	dBe⌦dAe
	++		dAe⌦dBe	dAe ? ⌦dBe	dBe⌦dAe ?	dAe ? ⌦dBe ?	dAe⌦dBe ?	dBe ? ⌦dAe
	µ↵.(	x 0 z subj	.

h det ⇠ (e µy.h x 0 ⇠ (e µx.h tv ⇠

Table 1

 1 For the lexical constants of the illustration, Table2gives • `translations compatible with the typing. In Table3, these lexical recipes are substituted for the parameters of the CPS translation.

	then specifies how the translation extends to sequents (replace logical
	connectives by their structural counterparts, and target ⌦ by the comma for
	multiset union).
	dC :(X `Y)e = dXe, dYe`L P dCe :?
	l X `v : A	m	= dXe`L P dve : dAe	(18)
	l	e : A	`Ym	= dYe`L P dee : dAe ?
	Illustrations We return to our sample derivations. In (19) one finds the CPS
	image of the source types for transitive verb and determiner under the different
	assignments of bias to the atomic subformulas, and the composition with • `,
	assuming np `= e (entities), s `=? `= t (truth values) and n `= e ! t (sets of

Table 3 :

 3 Compositional translations

There is a second set, with the inequalities reversed, which we'll not discuss here.

In what follows we will often speak of formula occurrences (or simply formulas if there is no possibility of confusion) instead of vertices labeled by formulas.

This node identification corresponds to the "axiom links" of linear logic proof nets.

The connection between proof net sequentialisation and focusing for linear logic is explored inAndreoli and Maieli (1999)

1. all vertices of P with formula label A are expanded into axiom links: edges connecting two vertices with formula label A; all links are replaced by the corresponding links of Figure 14;

2. all vertices in this new structure are assigned atomic terms of the correct type (variable or covariable) and the terms for the tensor rules are propagated from the active formulas to the main formula;

3. all axiom links connecting terms of the same type (value or context) are collapsed.

Figure 15 gives an example of the composition graph associated with a net. In all, the expansion stage gives rise to four types of axiom links, depending on the type of the term assigned to the A premise and the A conclusion. These cases are summarized in Figure 16. The substitution links are collapsed in the final stage of the construction of the composition graph (shown on the right of Figure 15; the command and µ/e µ cases are the ones that remain.

Given the composition graph cg(P) associated with a proof net P, we compute terms for it as follows.

1. we compute all maximal subnets of cg(P), which consist of a set of tensor links with a single main formula, marking all these links as visited;


A.-H Olivier

A Marin

A Crétual

J Pettré

Minimal predicted distance: a kinematic cue to investigate collision avoidance between walkers

Keywords: Interaction, collision avoidance, locomotion, distance, anticipatory locomotor control

Introduction

Collision-free navigation requires avoiding static and moving obstacles as well as other humans. Previous studies focused on the avoidance of static [START_REF] Jansen | Human locomotion through a multiple obstacle environment: strategy changes as a result of visual field limitation[END_REF][START_REF] Vallis | Locomotor adjustments for circumvention of an obstacle in the travel path[END_REF] or passive moving obstacles such as a mannequin [START_REF] Cinelli | Travel path conditions dictate the manner in which individuals avoid collisions[END_REF][START_REF] Gérin-Lajoie | The negociation of stationary and moving obstructions during walking: anticipatory locomotor adaptations and preservation of personal space[END_REF]. Collision avoidance between human walkers was only studied in a frontal task to investigate the influence of gender and height on the lateral deviation and clearance distance [START_REF] Van Basten | Exploiting motion capture to enhance avoidance behaviour in games[END_REF]. Our objective was to identify the conditions that lead to avoidance manoeuvres in locomotor trajectories of two walkers. Based on the assumption of a reciprocal interaction, we suggested a mutual variable, the Minimum Predicted Distance (MPD), which emphasises the risk of collision and describes the general collision avoidance behaviour.

Methods

30 participants volunteered for this experiment (11♀, 19♂). For each of the 420 trials recorded, 2 participants stood at the corners of the 15m side length experimental area (Figure 1A). Their task was to walk to the opposite corner. By synchronizing their start signals, we provoked situations of potential collisions on orthogonal trajectories. The variability in natural speeds and reaction times actually changed the exact conditions of the kinematics of interactions, thereby allowing us to study their influence. Occluding walls (2m high by 3m long) between corners prevented participants from seeing each other before reaching their natural speeds. The time when participants can see each other was denoted 'tsee'. The time when the distance between participants was minimal ('dmin') was denoted 'tcross'. 3D kinematics were recorded using 12 Vicon MX-40 cameras at a sampling rate of 120Hz. We approximated participant's motion as the one of their mid-shoulders and applied a Butterworth lowpass filter (0.5Hz cut-off frequency) to average out the higher frequency stepping oscillations. Collision avoidance interaction can obviously only occur between tsee and tcross so we temporally normalized all the data between these two instants. At each instant t, if no motion adaption was performed by walkers, we can predict their future trajectories as linear extrapolations of their current states:

) ( ) ( ) ( ) , ( 1 1 1 , t V t u t P u t P pred   
where u is a time parameter, P 1 (t) the current position and V 1 (t) the current velocity vector of participant #1. tests were used to determine differences between values of MPD at several instants of the interaction.

Results and Discussion

Minimum distance 'dmin' was 1.09m (±0.47) and ranged from 0.41 to 3.48m. MPD(tsee) ranged from 0 to 3.81m. We subdivided the dataset in 10 groups of 42 trials according to ascending MPD(tsee) values. For each group, we computed ) (t MPD (Fig. 2A). When MPD(tsee) was lower than 1m (groups 1 to 6), the set of MPD(tcross) values for each group was significantly higher than MPD(tsee) (T 1 =0, T 2 =0, T 3 =0, T 4 =0, T 5 =72, T 6 =125; df=41, p<0.01). When MPD(tsee) ranged from 1 to 1.5m, there was no significant difference between the sets of MPD(tcross) and MPD(tsee) (p>0.05). When MPD(tsee) was higher than 1.5m, MPD(tcross) was significantly smaller than MPD(tsee) (T 9 =208, T =56; df=41, p<0.05). These first results show that walkers adapted their trajectories to increase MPD(t) when MPD(tsee) was lower than 1m, i.e., when future collision is predicted by MPD(tsee). These results corroborate previous observations on the preservation of the personal space during interactions [START_REF] Gérin-Lajoie | The negociation of stationary and moving obstructions during walking: anticipatory locomotor adaptations and preservation of personal space[END_REF], but also reveal human ability to accurately predict future crossing distance. For all trials with MPD(tsee)<1m, we computed the overall mean ) (t MPD (Fig. 2B). We then observed three successive phases in time with respect to the sign of its time derivative ) ( ' t MPD . First, the observation phase was between t0% to t7%: ) (t MPD was constant (p>0.05). Second, the reaction phase was from t7% to t79%: ) ( ' t MPD was positive and ) (t MPD significantly increased up to 0.88m±0.22 (T=258, df=263, p<0.01). Third, the regulation phase was from t79% to t100%: ) ( ' t MPD was negative and ) (t MPD slightly decreased to dmin=0.84m ±0.19, ranging from 0.41 to 1.48m (T=-4648, df=263, p<0.01). This second set of results shows that MPD(t) captures the temporal structure of interaction (observation, reaction and regulation) and that collision avoidance is anticipated. Indeed, the reaction phase ended 0.8s before crossing which indicates that collision avoidance is solved in advance. MPD(t) is then maintained at constant value during the regulation phase. The duration of this phase (0.8s) is close to the duration of a stride. This can be related to the one-stride interval necessary to allow a walker to successfully implement adaptive strategies [START_REF] Patla | Understanding the role of vision in the control of human locomotion[END_REF].

Conclusion

We concluded that walkers are able to accurately predict crossing distances and to react accordingly. We also concluded that avoidance is performed with anticipation, i.e., maneuvers are ended time before interaction ended. However, our analysis focused on the mutual aspects of interaction. Future work is still required to investigate the nature of each walker reactions to avoid collisions.

Figure 1 :

 1 Figure 1: A) Experimental set-up. B) Minimum Predicted Distance over the interaction phase. We then introduced the Minimal Predicted Distance (MPD). At each instant t, MPD(t) represented the distance at which participants would meet if they did not perform motion adaptation after this instant: ) , ( ) , ( min arg ) (1 , 2 , u t P u t P t MPD pred pred u  

Figure 2

 2 Figure 2: A) ) (t MPD for 10 groups of ascending MPD(tsee) values. B) ) (t MPD (±SD) for all trials where MPD(tsee)<1m.

Acknowledgments

This study was funded by the French ANR PSIROB Locanthrope project and the European FP7-ICT-2009C Tango Project (n° 249858).