Embedding HTLCG into $\hbox {LCG}_\phi$

Abstract

A wide array of syntactic phenomena can be categorized as being either direction-sensitive (e.g. coordination) or direction-insensitive (quantification and medial extraction). In the realm of categorial grammar, many frameworks are engineered to handle one class of phenomena at the expense of the other. In particular, Lambek-inspired frameworks handle direction-sensitivity elegantly but struggle with cases of direction-insensitivity, whereas in linear grammars, the situation is just the opposite. One reasonably successful attempt to unify the insights of both types of grammar and allow for the analysis of direction-sensitive as well as direction-insensitive phenomena is hybrid type-logical categorial grammar (HTLCG), which augments the set of syntactic categories of an ordinary linear grammar with the directional slashes of a Lambek grammar. In this paper, the complementary nature of Lambek and linear grammars, with respect to direction-sensitive and direction-insensitive phenomena, is expounded on, as is the nature of how HTLCG attempts to reconcile the two systems. The paper further discusses an alternative to HTLCG—a linear grammar which adds Lambek-like capabilities by augmenting the string-combining (phenogrammatic) mechanism instead of the definition of syntactic categories (the tectogrammar). In particular, $\hbox {LCG}_\phi$ (linear categorial grammar with phenominators) adds a form of subtyping based on phenominators—a class of linear functions which specify various modes of (phenogrammatic) combination. Most importantly, an algorithm is provided for embedding HTLCG into $\hbox {LCG}_\phi$, thereby demonstrating that $\hbox {LCG}_\phi$ can handle direction-(in)sensitivity at least as well as HTLCG.

Appendices

Appendix

A Proof that $\textsf{pros2phen}$ and $\textsf{phen2pros}$ are Inverses

Theorem 1

For any HTLCG category Z, $\textsf{pros2phen}_Z$ and $\textsf{phen2pros}_Z$ are inverses.

Proof

The proof of Theorem 1 proceeds by induction on the structure of HTLCG categories (as given in (17) and (27)).

• Base Case: For any Lambek category L, prove that $\textsf{pros2phen}_L$ and $\textsf{phen2pros}_L$ are inverses.

 Let A be a PType and $\phi$ an A-phenominator, such that $\langle A,\phi \rangle =(\textsf{convert}\,L)$. Then, by the definitions given in (37) (repeated in (44)), we have the following:

$$\begin{aligned} \textsf{pros2phen}_L&= \iota _\phi \\ \textsf{phen2pros}_L&= \textsf{say}_\phi \end{aligned}$$

That these are inverses is already explicitly assumed, in Sect. 4.3.1.

• Inductive Case: For any HTLCG categories X and Y, prove that $\textsf{pros2phen}_{(Y\upharpoonright X)}$ and $\textsf{phen2pros}_{(Y\upharpoonright X)}$ are inverses.

  Inductive Hypothesis $\textsf{pros2phen}_X$ and $\textsf{phen2pros}_X$ are inverses, as are $\textsf{pros2phen}_Y$ and $\textsf{phen2pros}_Y$.

  Demonstrating that $\textsf{pros2phen}_{(Y\upharpoonright X)}$ and $\textsf{phen2pros}_{(Y\upharpoonright X)}$ are inverses requires showing that both of the following hold:⁵¹

  • 1. For any $f\mathbin {:}(\textsf{pros}\,X) \rightarrow (\textsf{pros}\,Y)$, $(\textsf{phen2pros}_{(Y\upharpoonright X)} (\textsf{pros2phen}_{(Y\upharpoonright X)}\,f))=f$.

  • 2. For any $g\mathbin {:}(\textsf{phen}\,X) \rightarrow (\textsf{phen}\,Y)$, $(\textsf{pros2phen}_{(Y\upharpoonright X)} (\textsf{phen2pros}_{(Y\upharpoonright X)}\,g))=g$.

  For the sake of brevity, only the first of these will be shown below, with the understanding that the proof of the second proceeds in a similar fashion. To begin with, assume an arbitrary $f\mathbin {:}{(\textsf{pros}\,X) \rightarrow (\textsf{pros}\,Y)}$. Applying the definitions of $\textsf{pros2phen}$ and $\textsf{phen2pros}$ given in (44), as well as $\beta$ -normalizing, gives us the following:⁵²

  $$\begin{aligned} (\textsf{phen2pros}&_{(Y\upharpoonright X)}\,(\textsf{pros2phen}_{(Y\upharpoonright X)}\,f))\\&=[\lambda g.\lambda v.\textsf{phen2pros}_Y\,(g\,(\textsf{pros2phen}_X\,v))](\textsf{pros2phen}_{(Y\upharpoonright X)}\,f)\\&=\lambda v.\textsf{phen2pros}_Y\,(\textsf{pros2phen}_{(Y\upharpoonright X)}\,f\,(\textsf{pros2phen}_X\,v))\\&=\lambda v.\textsf{phen2pros}_Y\left( \big [\lambda h.\lambda u.\textsf{pros2phen}_Y\,(h\,(\textsf{phen2pros}_X\,u))\big ]\right. \\&\quad \left. (f)(\textsf{pros2phen}_X\,v)\right) \\&=\lambda v.\textsf{phen2pros}_Y\\&\quad (\textsf{pros2phen}_Y\,(f\,(\textsf{phen2pros}_X\,(\textsf{pros2phen}_X\,v)))) \end{aligned}$$

  By the inductive hypothesis, we can further simplify as follows:

  $$\begin{aligned} (\textsf{phen2pros}_{(Y\upharpoonright X)}\,&(\textsf{pros2phen}_{(Y\upharpoonright X)}\,f))\\&=\lambda v.\textsf{phen2pros}_Y\,(\textsf{pros2phen}_Y\\&\quad (f\,(\textsf{phen2pros}_X\,(\textsf{pros2phen}_X\,v))))\\&=\lambda v.f\,(\textsf{phen2pros}_X\,(\textsf{pros2phen}_X\,v))\\&=\lambda v.f\,v\\&=f \end{aligned}$$

  Thus, we get that $(\textsf{phen2pros}_{(Y\upharpoonright X)}\,(\textsf{pros2phen}_{(Y\upharpoonright X)}\,f))$ is equal to f.

Since all possible shapes of HTLCG categories have been accounted for, we can conclude that $\textsf{pros2phen}_Z$ and $\textsf{phen2pros}_Z$ are inverses for any HTLCG category Z. $\square$

B Working Through Select Translations

Since there are a lot of intricate moving parts involved in the translations of HTLCG signs into $\hbox {LCG}_\phi$, it will be instructive to see how they work together to get from point A to point B in a few of the examples from Sect. 5.4. It will be a useful exercise for the interested reader to work through the remaining examples to confirm the outputs are correct. Since the translation of signs require many moving parts, the relevant definitions are repeated in (45) to (49) below:

• Example 1. $\text {slept}\,;\,\text {NP}\backslash \text {S}$ We’ll begin with a fairly simple sign—that of the intransitive verb slept. To translate the HTLCG sign for slept into an LCG$_\phi$ sign, we begin by plugging the HTLCG sign into the $\textsf{Hyb2LCG}$ function (as defined in (49)), as follows:

  $$\begin{aligned}{} & {} {(\textsf{Hyb2LCG}\;(\text {slept};\text {NP}\backslash \text {S}))}\\{} & {} \quad ={{(\textsf{pros2phen}_{(\text {NP}\backslash \text {S})}\,\text {slept})}\mathbin {:}{(\textsf{phen}\,(\text {NP}\backslash \text {S}))};(\text {NP}\backslash \text {S})'} \end{aligned}$$

  From here, we’ll proceed from right to left (which corresponds to increasing complexity) to simplify the complex expressions on the right-hand side of the above equation.

  • Step 1 The Category: By the definition of the category mapping given in (45), the tecto simplifies as follows:

    

  • Step 2 The Phenotype: The definition of $\textsf{phen}$ given in (36b) yields the following for the type of the phenoterm in the above translation:

    $$\begin{aligned}{(\textsf{phen}\,(\text {NP}\backslash \text {S}))}={(\texttt {let }{\langle A,\phi \rangle }\mathbin {\texttt {:=}}{(\textsf{convert}\,(\text {NP}\backslash \text {S}))}{} \texttt { in }A_\phi )} \end{aligned}$$

    By the definition of $\textsf{convert}$ given in (48) (using the shorthands defined in (46)), we get:

    

    Since both NP and S are atomic categories, the output of $\textsf{convert}$ is the same for both: $\langle \textsf{s},\textsf{i}\rangle$. Substituting this in for $\langle B,\beta \rangle$ and $\langle C,\gamma \rangle$ in the above expression yields ${(\textsf{convert}\,(\text {NP}\backslash \text {S}))}={\langle \textsf{s}_{\textsf{i}}\rightarrow \textsf{s}_{\textsf{i}},\textsf{i}\backslash \textsf{i}\rangle }$. Thus, for the phenotype, we get:

    

  • Step 3 The Phenoterm: Working with just $\textsf{pros2phen}$ alone first, we have the following:

    $$\begin{aligned}{\textsf{pros2phen}_{(\text {NP}\backslash \text {S})}}={(\texttt {let }{\langle A,\phi \rangle }\mathbin {\texttt {:=}}{(\textsf{convert}\,(\text {NP}\backslash \text {S}))}{} \texttt { in }\iota _\phi )}\end{aligned}$$

    As demonstrated above, we have ${(\textsf{convert}\,(\text {NP}\backslash \text {S}))}={\langle \textsf{s}_{\textsf{i}}\rightarrow \textsf{s}_{\textsf{i}},\textsf{i}\backslash \textsf{i}\rangle }$; therefore, we have that ${\textsf{pros2phen}_{(\text {NP}\backslash \text {S})}}={\iota _{(\textsf{i}\backslash \textsf{i})}}={\iota _{\textsf{iv}}}$. From this, we get that the phenoterm for the translated sign is:

    

  • Step 4 The Result: Putting all of the above simplifications together, we get that the translation of the HTLCG sign for slept into LCG$_\phi$ should be:

    

• Example 2. $\text {and};((\text {NP}\backslash \text {S})\backslash (\text {NP}\backslash \text {S}))/(\text {NP}\backslash \text {S})$ A somewhat more complex sign is that of ordinary VP (i.e. NP$\backslash$S) conjunction in HTLCG. Once again we begin by plugging the sign into the $\textsf{Hyb2LCG}$ function, yielding the following:

  $$\begin{aligned} {(\textsf{Hyb2LCG}\;(\text {and};(\text {VP}\backslash \text {VP})/\text {VP}))}={}&{{(\textsf{pros2phen}_{((\text {VP}\backslash \text {VP})/\text {VP})}\,\text {and})}}\\&:{\textsf{phen}\,((\text {VP}\backslash \text {VP})/\text {VP})} \\&;((\text {VP}\backslash \text {VP})/\text {VP})' \end{aligned}$$

  Once again, the reductions will be addressed from right to left.

  • Step 1 The Category: Using the category mapping defined in (45) again, along with identifying ${\text {VP}'}={(\text {NP}\backslash \text {S})'}={\text {NP}\multimap \text {S}}$, the tecto for the translated sign is:

    

  • Step 2 The Phenotype: Applying the definition of $\textsf{phen}$ to the present HTLCG category yields the following:

    

    The next step is to use $\textsf{convert}$ on $(\text {VP}\backslash \text {VP})/\text {VP}$. This yields the following:

    

    The output of $\textsf{convert}$ on VP is exactly what we saw in the translation of slept: $\langle \textsf{s}_{\textsf{i}}\rightarrow \textsf{s}_{\textsf{i}},\textsf{iv}\rangle$. For $(\textsf{convert}\,(\text {VP}\backslash \text {VP}))$, we have the following:

    

    Plugging this back in to $(\textsf{convert}\,((\text {VP}\backslash \text {VP})/\text {VP}))$ gives us:

    

    Finally, using this we obtain the phenotype for the translated sign:⁵³

    

  • Step 3 The Phenoterm: Since we are dealing once again with a sign whose category is a Lambek category, computing the phenoterm of the translated sign is fairly similar to the result for slept:

    

  • Step 4 The Result: Putting all of these pieces together gives us the following translated sign:⁵⁴

    

• Example 3. ${(\lambda \phi .\phi \cdot \text {slept})};{\text {S}\upharpoonright \text {NP}}$ To see how the algorithm works with vertical slashes, consider the “unslanted” version of the entry for slept. The unsimplified output of the translation of this sign into LCG$_\phi$ is the following:

  $$\begin{aligned}&(\textsf{Hyb2LCG}\,({(\lambda \phi .\phi \cdot \text {slept})};{\text {S}\upharpoonright \text {NP}}))\\&{}\quad ={{(\textsf{pros2phen}_{(\text {S}\upharpoonright \text {NP})}\,(\lambda \phi .\phi \cdot \text {slept}))}\mathbin {:}{(\textsf{phen}\,(\text {S}\upharpoonright \text {NP}))};{(\text {S}\upharpoonright \text {NP})'}} \end{aligned}$$

  The simplifications of the various components will again be addressed from right to left.

  • Step 1 The Category: Applying the category mapping gives the following output:

    

    Notice that the resulting tecto here is precisely the same as the one in the first example—both entries for slept are mapped to a sign whose tectogrammatic information says that they combine with an NP to result in an S. Of course, this is to be expected in the maintaining of a strict pheno/tecto distinction—what both signs combine with (i.e. an NP) and what is the result (an S) ought to be the same for both; however, how the two signs combine with their arguments (concatenation on the left in the previous case, function application in the present one) will be reflected solely in phenogrammatic component of the signs.

  • Step 2 The Phenotype: Since we are dealing with a category lacking any real directional information (since there are no Lambek slashes), the output of $\textsf{phen}$ will be fairly simple:

    

    This last step comes from the fact that both NP and S are atomic categories, as we saw earlier.

  • Step 3 The Phenoterm: In contrast to the phenotype associated with this sign, obtaining the phenoterm is somewhat more involved. Fleshing out this particular instance of $\textsf{pros2phen}$ before applying it to the HTLCG sign’s phenoterm yields the following:

    $$\begin{aligned} {\textsf{pros2phen}_{(\text {S}\upharpoonright \text {NP})}}&={\lambda f\!:\!{(\textsf{pros}\,\text {NP}) \rightarrow (\textsf{pros}\,\text {S})}.\lambda u\!:\!{(\textsf{phen}\,\text {NP})}.}\\&{\textsf{pros2phen}_{\text {S}}\,(f\,(\textsf{phen2pros}_{\text {NP}}\,u))}\\&={\lambda f\!:\!{\textsf{s}\rightarrow \textsf{s}}.\lambda u\!:\!\textsf{s}_{\textsf{i}}.\textsf{pros2phen}_{\text {S}}\,(f\,(\textsf{phen2pros}_{\text {NP}}\,u))}\\&={\lambda f\!:\!{\textsf{s}\rightarrow \textsf{s}}.\lambda u\!:\!\textsf{s}_{\textsf{i}}.\iota _{\textsf{i}}\,(f\,(\textsf{say}_{\textsf{i}}\,u))} \end{aligned}$$

    The last step of the above reduction comes from the base clauses of the definitions of $\textsf{pros2phen}$ and $\textsf{phen2pros}$ along with the fact that the output of $\textsf{convert}$ applied to both NP and S is the pair $\langle \textsf{s},\textsf{i}\rangle$. Applying this expression (with the variable types being suppressed) to the original HTLCG sign’s phenoterm gives us the following phenoterm for the translated sign:

    

    The interesting result we get from applying $\textsf{pros2phen}_{(\text {S}\upharpoonright \text {NP})}$ to $(\lambda \phi .\phi \cdot \text {slept})$ is that the final result is an instance of a phenominator ($\textsf{i}\backslash \textsf{i}$, aka $\textsf{iv}$) applied to some string support (slept). More importantly, the phenominator in question is exactly the one we were dealing with in the original entry for slept. Of course, this outcome is a consequence of the “shape” of the original HTLCG pheno expression—for other potential $\textsf{s}\rightarrow \textsf{s}$ functions, such as $(\lambda \phi .\text {David}\cdot \text {ate}\cdot \phi )$ or $(\lambda \phi .\text {John}\cdot \text {gave}\cdot \phi \cdot \text {to}\cdot \text {Mary})$, the result of applying $\textsf{pros2phen}_{(\text {S}\upharpoonright \text {NP})}$ to these would yield $\textsf{s}_{\textsf{i}}\rightarrow \textsf{s}_{\textsf{i}}$ functions that are not under the image of the $\textsf{iv}$ phenominator.

  • Step 4 The Result: Having simplified all of the above expressions, we can write the translated sign as the following:

    

• Example 4. $(\lambda \sigma .\lambda \sigma '.\lambda \phi .(\sigma \,\phi )\cdot \text {and}\cdot (\sigma '\,\textsf{e}));(\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)$

  Stepping up the difficulty somewhat, we have the gapping operator found in Kubota and Levine (2012). As was the case in Sect. 5.4.2 above, this entry is schematized over Lambek categories L; furthermore, let A be a PType and $\varphi$ be an A-phenominator such that ${\langle A,\varphi \rangle }={(\textsf{convert}\,L)}$ (therefore, ${{(\textsf{phen}\,L)}={A_{\varphi }}}$). With this in mind, applying the $\textsf{Hyb2LCG}$ function to the sign yields the following:

  $$\begin{aligned}&{\left( \textsf{Hyb2LCG}\;\Big ((\lambda \sigma .\lambda \sigma '.\lambda \phi .(\sigma \,\phi )\cdot \text {and}\cdot (\sigma '\,\textsf{e}));(\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\Big )\right) } \\&={\big (\textsf{pros2phen}_{((\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L))}\,(\lambda \sigma .\lambda \sigma '.\lambda \phi .(\sigma \,\phi )\cdot \text {and}\cdot (\sigma '\,\textsf{e}))\big )}\\&{}\mathbin {:}{\textsf{phen}\,((\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L))}\\&{}\mathbin {;}{\big ((\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\big )'} \end{aligned}$$

  As with the other examples, simplifications will proceed from right to left.

  • Step 1 The Category: Since the vertical slash is for HTLCG what the linear implication is for LCG$_\phi$, the category translation is fairly straightforward:

    

  • Step 2 The Phenotype: Since the syntactic category for the HTLCG sign doesn’t contain any Lambek slashes, obtaining the PType for the translated sign is also fairly simple:

    

  • Step 3 The Phenoterm: Since this sign has vertical slashes in its category, and therefore has a functional pheno component in HTLCG, the LCG$_\phi$ phenoterm will be far more complicated than those of the previous examples. Partially expanding out the use of $\textsf{pros2phen}$ yields the following:

    

    Thus, the result of $\textsf{pros2phen}_{((\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L)\upharpoonright (\text {S}\upharpoonright L))}$ is a function which takes the original pheno expression and returns a function which takes the direction-encoded arguments, converts them into expressions the original can take (by way of $\textsf{phen2pros}$), then feeds these converted expressions to the original term. In the present case, this gives us the following:

    

    The only remaining unsimplified expressions here are two instances of $\textsf{phen2pros}_{(\text {S}\upharpoonright L)}$. By the definition given in (44b), this function is:

    $$\begin{aligned} {\textsf{phen2pros}_{(\text {S}\upharpoonright L)}}&={\lambda m\!:\!{(\textsf{phen}\,L) \rightarrow (\textsf{phen}\,\text {S})}.\lambda v\!:\!\textsf{pros}\,L.}\\&\textsf{phen2pros}_{\text {S}}\,(m\,(\textsf{pros2phen}_L\,v))\\&={\lambda m\!:\!A_{\varphi } \rightarrow \textsf{s}_{\textsf{i}}.\lambda v\!:\!\textsf{s}.\textsf{say}_{\textsf{i}}\,(m\,(\iota _{\varphi }\,v))} \end{aligned}$$

    Plugging this in to the overall expression and simplifying gives us the following:

    

    Note that the last simplification comes from the fact stated in Sect. 4.3.1 that instances of $\iota$ and $\textsf{say}$ of the same phenominator ($\varphi$ in this case) are inverses.

  • Step 4 The Result: Putting everything together gives us the fully simplified translated sign:

    

C Proof of the Embedding

Theorem 2

For any HTLCG lexicon ${\mathcal {L}}$ and sequent $\Sigma$, if $\Sigma$ is derivable in HTLCG with respect to lexicon ${\mathcal {L}}$, then $\textrm{Tr}[\Sigma ]$ is derivable in $\hbox {LCG}_\phi$ with respect to lexicon ${\mathcal {L}}'$. (as defined in (40), repeated as (50) below)

Once again, a reminder of the definitions of the relevant functions:

Fig. 4

Rules for HTLCG

Fig. 5

Rules for $\hbox {LCG}_\phi$

Proof

The proof of Theorem 2 proceeds by induction on the structure of proofs in HTLCG.

• Case 1 Hyp: The simplest case is an HTLCG sequent derived by the Hyp axiom. In HTLCG, we have the following, for some HTLCG category A and variable ${x}\mathbin {:}{\textsf{pros}\,A}$ (independent of the choice of lexicon):

  

  Therefore, the goal is to show that $\text {Tr}[x;A\vdash _Hx;A]$ is derivable in $\hbox {LCG}_\phi$ (again, independent of the particular lexicon). Applying the definition of $\text {Tr}[-]$ in (51), we get the following:

  $$\begin{aligned} \begin{aligned} \text {Tr}[x;A\vdash _Hx;A]&= \{x;A\}'\vdash _\phi (\textsf{Hyb2LCG}\,((x)';A)) \\&= \{({y'}\mathbin {:}{\textsf{phen}\,B};B')\,\mid \,(y;B)\!\!\in \!\!\{x;A\}\}\vdash _\phi \\&{\left( \textsf{pros2phen}_A\,(x[{y}\mapsto {(\textsf{phen2pros}_B\,y')}])_{(y;B)\in \{x;A\}}\right) }\\&:{\textsf{phen}\,A};A' \\&= {x'}\mathbin {:}{\textsf{phen}\,A};A'\vdash _\phi {\left( \textsf{pros2phen}_A\,(x[{x}\mapsto {(\textsf{phen2pros}_A\,x')}])\right) }\\&:{\textsf{phen}\,A};A' \\&= {x'}\mathbin {:}{\textsf{phen}\,A};A'\vdash _\phi {(\textsf{pros2phen}_A\,(\textsf{phen2pros}_A\,x'))}\mathbin {:}{\textsf{phen}\,A};A' \\&= {x'}\mathbin {:}{\textsf{phen}\,A};A'\vdash _\phi {x'}\mathbin {:}{\textsf{phen}\,A};A' \end{aligned} \end{aligned}$$

  Note that the simplification in the last step comes from the fact stated in Sect. 5.2 (and proved in Appendix A) that $\textsf{pros2phen}_X$ and $\textsf{phen2pros}_X$ are inverses for any HTLCG category X.⁵⁵ Thus, it should be clear that $\text {Tr}[x;A\vdash _Hx;A]$ is in fact derivable in $\hbox {LCG}_\phi$ using $\hbox {LCG}_\phi$’s Hyp rule:

  

• Case 2 Lex: The next simplest situation is an HTLCG sequent which comes from the lexicon ${\mathcal {L}}$. Such a case would be as follows, for some HTLCG category A and (closed) term ${u}\mathbin {:}{\textsf{pros}\,A}$:

  

  In this case, the goal is to prove that $\text {Tr}[\vdash _Hu;A]$ is derivable in $\hbox {LCG}_\phi$ with respect to the translated lexicon ${\mathcal {L}}'$, under the assumption that $(u;A)\!\!\in \!\! {\mathcal {L}}$. Once again, applying the definition of sequent translation from (51), we get the following:

  $$\begin{aligned} \begin{aligned} \text {Tr}[\vdash _Hu;A]&= \emptyset '\vdash _\phi (\textsf{Hyb2LCG}\,((u)';A)) \\&= \{{y'}\mathbin {:}{\textsf{phen}\,B};B'\,\mid \,(y;B){\in } \emptyset \}\\&\quad \vdash _\phi \left( \textsf{Hyb2LCG}\,\left( (u[{y}\mapsto {(\textsf{phen2pros}_B\,y')}])_{(y;B)\in \emptyset };A\right) \right) \\&= \emptyset \vdash _\phi (\textsf{Hyb2LCG}\,(u;A)) \\&=\, \vdash _\phi {(\textsf{pros2phen}_A\,u)}\mathbin {:}{\textsf{phen}\,A};A' \end{aligned} \end{aligned}$$

  Thus, the goal is to show that $\left( {(\textsf{pros2phen}_A\,u)}\mathbin {:}{\textsf{phen}\,A};A'\right)$ is derivable in $\hbox {LCG}_\phi$ with respect to the lexicon ${\mathcal {L}}'$ with an empty context. Notice that this sign is simply the sign translation of (u; A) (as seen in line 3 of the above reduction). Since $(u;A)\!\!\in \!\!{\mathcal {L}}$ is already assumed, by the definition of ${\mathcal {L}}'$ we have that the sign $\left( {(\textsf{pros2phen}_A\,u)}\mathbin {:}{\textsf{phen}\,A};A'\right)$ is in ${\mathcal {L}}'$, and therefore the desired sequent is derivable by means of $\hbox {LCG}_\phi$’s Lex rule:

  

At this point, we see that the base axioms of HTLCG (i.e. Hyp and Lex) correspond exactly to the equivalent axioms of $\hbox {LCG}_\phi$. This bodes well for the validity of the theorem in general. The remaining cases to consider are the rules for HTLCG’s three connectives, which come with the inductive hypothesis that for any HTLCG sequent $\Sigma$ which is a premise to one of the rules, $\text {Tr}[\Sigma ]$ is already known to be derivable in $\hbox {LCG}_\phi$. We’ll first consider the rules for the vertical slash, as these should correspond to the linear implication rules of $\hbox {LCG}_\phi$.

• Case 3 $\upharpoonright$I: For the case of $\upharpoonright$I, we have the following situation, for any HTLCG context $\varGamma$, categories A and B, variable ${x}\mathbin {:}{\textsf{pros}\,A}$ such that $x\not \in \text {FV}(\varGamma )$, and term ${u[x]}\mathbin {:}{\textsf{pros}\,B}$:

  

  Therefore, the goal is to show that $\text {Tr}[\varGamma \vdash _H(\lambda x.u[x]);B\upharpoonright A]$ is derivable in $\hbox {LCG}_\phi$, with the inductive hypothesis that $\text {Tr}[\varGamma ,x;A\vdash _Hu[x];B]$ already is. The evaluation of these translated sequents is provided below, with $\varGamma '$ defined as the set ${\{({y'}\mathbin {:}{\textsf{phen}\,B};B')\,\mid \,(y;B)\!\!\in \!\! \varGamma \}}$ and for any expression ${t}\mathbin {:}{\textsf{pros}\,A}$ such that t is free for x in u, we have ${u'[t]}\mathbin {:=}{(u[t][{y}\mapsto {(\textsf{phen2pros}_B\,y')}])_{(y;B)\in \varGamma }}$:

  

  From these, we see that the goal is to show that, given $\varGamma ',x';A'\vdash _\phi V;B'$, we can derive the sequent $\varGamma '\vdash _\phi (\lambda x'.V);A'\multimap B'$ in $\hbox {LCG}_\phi$ (supressing types in the pheno and abbreviating ${(\textsf{pros2phen}_B\,(u'[\textsf{phen2pros}_A\,x']))}$ as V). It should be clear that this is indeed possible by means of linear implication introduction:

  

• Case 4 $\upharpoonright$E: The scenario for $\upharpoonright$E is the following, for any disjoint HTLCG contexts $\varGamma$ and $\varDelta$ , categories A and B, and terms ${f}\mathbin {:}{(\textsf{pros}\,A) \rightarrow (\textsf{pros}\,B)}$ and ${u}\mathbin {:}{\textsf{pros}\,A}$:

  

  Therefore, the goal is to prove that $\text {Tr}[\varGamma ,\varDelta \vdash _H(f\,u);B]$ is derivable in $\hbox {LCG}_\phi$, with the inductive hypothesis that both $\text {Tr}[\varGamma \vdash _Hf;B\upharpoonright A]$ and $\text {Tr}[\varDelta \vdash _Hu;A]$ are already known to be so derivable. The evaluation of these translations are provided below, with $\varGamma '$ defined similarly to the definition given for the $\upharpoonright$I case, $\varDelta '$ defined similarly, and $f'$ and $u'$ defined similarly to the definition of $u'[x]$ in the $\upharpoonright$I case, relativized to $\varGamma$ and $\varDelta$, respectively:

  $$\begin{aligned} \begin{aligned} \text {Tr}[\varGamma \vdash _Hf;B\upharpoonright A]&= \varGamma '\vdash _\phi \left( \textsf{Hyb2LCG}\,(f';B\upharpoonright A)\right) \\&= \varGamma '\vdash _\phi {(\textsf{pros2phen}_{(B\upharpoonright A)}\,f')}\mathbin {:}{(\textsf{phen}\,A) \rightarrow (\textsf{phen}\,B)};A'\multimap B' \\&= \varGamma '\vdash _\phi {\left( \lambda v.\textsf{pros2phen}_B\,(f'\,(\textsf{phen2pros}_A\,v))\right) }\\&{}\mathbin {:}{(\textsf{phen}\,A) \rightarrow (\textsf{phen}\,B)};A'\multimap B' \\ \text {Tr}[\varDelta \vdash _Hu;A]&= \varDelta '\vdash _\phi \left( \textsf{Hyb2LCG}\,(u';A)\right) \\&= \varDelta '\vdash _\phi {(\textsf{pros2phen}_A\,u')}\mathbin {:}{\textsf{phen}\,A};A' \\ \text {Tr}[\varGamma ,\varDelta \vdash _H(f\,u);B]&= (\varGamma ,\varDelta )'\vdash _\phi \left( \textsf{Hyb2LCG}\,((f\,u)';B)\right) \\&= \varGamma ',\varDelta '\vdash _\phi \left( \textsf{pros2phen}_B\right. \\&\left. \left( (f\,u)[{y}\mapsto {(\textsf{phen2pros}_C\,y')}]\right) _{(y;C)\in \varGamma \cup \varDelta }\right) \\&{}\mathbin {:}{\textsf{phen}\,B};B' \\&= \varGamma ',\varDelta '\vdash _\phi {\left( \textsf{pros2phen}_B\,(f'\,u')\right) }\mathbin {:}{\textsf{phen}\,B};B' \end{aligned} \end{aligned}$$

  Note that, in the last translation, the moves from $(\varGamma ,\varDelta )'$ to $(\varGamma ',\varDelta ')$ and from ${\big ((f\,u)[{y}\mapsto {(\textsf{phen2pros}_C\,y')}]\big )_{(y;C)\in \varGamma \cup \varDelta }}$ to ${(f'\,u')}$ are licit due to the assumptions that the free variables in $\varGamma$ and $\varDelta$, f and $\varDelta$, and u and $\varGamma$ are all disjoint. Thus, the goal is to show that the sequent ${\varGamma ',\varDelta '\vdash _\phi \big (\textsf{pros2phen}_B\,(f'\,u')\big );B'}$ is derivable in $\hbox {LCG}_\phi$, on the assumption that both ${\varGamma '\vdash _\phi (\textsf{pros2phen}_{(B\upharpoonright A)}\,f');A'\multimap B'}$ and ${\varDelta '\vdash _\phi (\textsf{pros2phen}_A\,u');A'}$ are. That this is in fact the case can be seen from the derivation below (with types of the pheno terms supressed to save space):

  

  Similarly to what we saw in the Hyp case, $\textsf{phen2pros}_A$ and $\textsf{pros2phen}_A$ are inverses, which justifies the simplification in the last step of the derivation. As a result of this simplification, we see that we do indeed get that the desired sequent is derivable given the premises.

Just as the axioms of HTLCG correspond to the axioms of $\hbox {LCG}_\phi$, so too do the vertical slash rules in HTLCG correspond to the linear implication rules of $\hbox {LCG}_\phi$. The remaining four rules—those for the Lambek slashes—are different, however; $\hbox {LCG}_\phi$ doesn’t have any singular rules which correspond to these. As such, these cases are the crucial ones for showing that the embedding does in fact hold. The proofs for the forward slash rules are provided below, with the understanding that the backslash cases can be demonstrated similarly.

For the following cases, let $\varGamma$ and $\varDelta$ once again be arbitrary disjoint HTLCG contexts, with the corresponding $\hbox {LCG}_\phi$ contexts $\varGamma '$ and $\varDelta '$ defined as before. Furthermore, let L and M be arbitrary Lambek categories (since the directional slashed rules only apply to these), such that ${\langle A,\varphi \rangle }\mathbin {:=}{(\textsf{convert}\,L)}$ and ${\langle B,\psi \rangle }\mathbin {:=}{(\textsf{convert}\,M)}$ (therefore ${(\textsf{phen}\,L)}={A_{\varphi }}$ and ${(\textsf{phen}\,M)}={B_\psi }$). Additionally, let x be a variable over the type $\textsf{s}$ such that $x\not \in \text {FV}(\varGamma )$, and s and t be terms of type $\textsf{s}$ where ${s',t'}\mathbin {:}{\textsf{s}}$ are defined relative to $\varGamma$ and $\varDelta$ , respectively, similarly to $f'$ and $u'$ above.

• Case 5 /I: With /I, we have the following situation, assuming $x\not \in \text {FV}(s)$:

  

  Therefore, the goal is to show that $\text {Tr}[\varGamma \vdash _Hs;M/L]$ is derivable in $\hbox {LCG}_\phi$, on the assumption that $\text {Tr}[\varGamma ,x;L\vdash _Hs\cdot x;M]$ is. The evaluation of these sequents is given below:

  $$\begin{aligned} \begin{aligned} \text {Tr}[\varGamma ,x;L\vdash _Hs\cdot x;M]&= (\varGamma ,x;L)'\vdash _\phi \left( \textsf{Hyb2LCG}\,\left( (s\cdot x)';M\right) \right) \\&= \varGamma ',{x'}\mathbin {:}{\textsf{phen}\,L};L'\vdash _\phi \!\!\left( \textsf{Hyb2LCG}\,\left( (s'{\cdot }(\textsf{phen2pros}_L\,x'));M\right) \right) \\&= \varGamma ',{x'}\mathbin {:}{A_{\varphi }};L'\vdash _\phi {\left( \textsf{pros2phen}_M\,(s'\cdot (\textsf{phen2pros}_L\,x')\right) }\\&:{\textsf{phen}\,M};M' \\&= \varGamma ',{x'}\mathbin {:}{A_{\varphi }};L'\vdash _\phi {\left( \iota _\psi \,\left( s'\cdot (\textsf{say}_{\varphi }\,x')\right) \right) }\mathbin {:}{B_\psi };M' \\&\\ \text {Tr}[\varGamma \vdash _Hs;M/L]&= \varGamma '\vdash _\phi \left( \textsf{Hyb2LCG}\,(s';M/L)\right) \\&= \varGamma '\vdash _\phi {\left( \textsf{pros2phen}_{(M/L)}\,s'\right) }\mathbin {:}{\textsf{phen}\,(M/L)};(M/L)' \\&= \varGamma '\vdash _\phi {(\iota _{(\psi /\varphi )}\,s')}\mathbin {:}{B_\psi /A_{\varphi }};L'\multimap M' \end{aligned} \end{aligned}$$

  Recall that for Lambek categories, $\textsf{pros2phen}$ and $\textsf{phen2pros}$ yield the corresponding instances of $\iota$ and $\textsf{say}$, respectively. Also, recall from Sect. 5 that $B_\psi /A_{\varphi }$ is a shorthand for the fine-grained $\textsc {PType}$ $(A_{\varphi } \rightarrow B_\psi )_{(\psi /\varphi )}$. Keeping those facts in mind, the goal here is to show, given that ${\varGamma ',{x'}\mathbin {:}{A_{\varphi }};L'\vdash _\phi (\iota _\psi \,(s'\cdot (\textsf{say}_{\varphi }\,x')));M'}$ is derivable, that ${\varGamma '\vdash _\phi (\iota _{(\psi /\varphi )}\,s');L'\multimap M'}$ is as well. That this is in fact the case can be seen as follows:

  

  As this derivation demonstrates, what is a single inference rule in HTLCG gets factored into two separate steps in $\hbox {LCG}_\phi$; first, the assumption is discharged by the usual means of linear implication introduction (note that the corresponding move of $\upharpoonright$I would be licensed in HTLCG as well), then the resulting phenoterm is refined by means of a phenominator introduction rule (specifically $\psi /\varphi$ I). The crucial piece here is the third line of the above proof—the recognition that the pheno term obtained from the use of $\multimap$ I is under the image of the $\psi /\varphi$ phenominator (with string support $s'$). This bears a striking resemblence to the ‘slanting’ lemmas of HTLCG—the move from a vertically-slashed sign to a Lambek-slashed sign is only licensed in particular cases, allowing for the encoding of the direction-specific information just in those cases where it applies.

• Case 6 /E: The situation we find ourselves in for /E is the following:

  

  For this final case, the goal is to show that $\text {Tr}[\varGamma ,\varDelta \vdash _Hs\cdot t;M]$ is derivable in $\hbox {LCG}_\phi$, under the assumption that both ${\text {Tr}[\varGamma \vdash _Hs;M/L]}$ and ${\text {Tr}[\varDelta \vdash _Ht;L]}$ are derivable. The evaluation of these sequents is provided below:

  $$\begin{aligned} \begin{aligned} \text {Tr}[\varGamma \vdash _Hs;M/L]&= \varGamma '\vdash _\phi \left( \textsf{Hyb2LCG}\,(s';M/L)\right) \\&= \varGamma '\vdash _\phi {(\iota _{(\psi /\varphi )}\;s')}\mathbin {:}{B_\psi /A_{\varphi }};L'\multimap M' \\&\\ \text {Tr}[\varDelta \vdash _Ht;L]&= \varDelta '\vdash _\phi \left( \textsf{Hyb2LCG}\,(t';L)\right) \\&= \varDelta '\vdash _\phi {(\iota _{\varphi }\;t')}\mathbin {:}{A_{\varphi }};L' \\&\\ \text {Tr}[\varGamma ,\varDelta \vdash _Hs\cdot t;M]&= (\varGamma ,\varDelta )'\vdash _\phi \left( \textsf{Hyb2LCG}\,\left( (s\cdot t)';M\right) \right) \\&= (\varGamma ,\varDelta )'\vdash _\phi {(\iota _\psi \;(s\cdot t)')}\mathbin {:}{B_\psi };M' \\&= \varGamma ',\varDelta '\vdash _\phi {(\iota _\psi \;(s'\cdot t'))}\mathbin {:}{B_\psi };M' \end{aligned} \end{aligned}$$

  The proof that we in fact can derive ${\varGamma ',\varDelta '\vdash _\phi (\iota _\psi \;(s'\cdot t'));M'}$ given ${\varGamma '\vdash _\phi (\iota _{(\psi /\varphi )}\;s');L'\multimap M'}$ and ${\varDelta '\vdash _\phi (\iota _{\varphi }\;t');L'}$ proceeds as follows:

  

  Similar to what we saw with the /I case, in the move to $\hbox {LCG}_\phi$, /E also gets factored into two steps. The first step is to use the phenominator elimination rule ($\psi /\varphi$ E) to turn the functor sign’s phenoterm into a function.⁵⁶ Just as there is a parallel between the use of phenominator introduction in $\hbox {LCG}_\phi$ and ‘slanting’ in HTLCG, so too is there a parallel between the use of the phenominator elimination here and ‘unslanting’ in HTLCG—some of the directional information in the functor sign is lost, yielding a sign with a functional phenogrammatic component. Once this functional pheno is obtained, the second step is to use linear implication elimination to combine the two signs, giving us the sign to be derived.

Since every rule in an HTLCG can be simulated in a corresponding $\hbox {LCG}_\phi$, we can conclude that HTLCG can in fact be faithfully embedded in $\hbox {LCG}_\phi$, without loss of any combinatorial information. $\square$