View source for Thompson's construction algorithm

{{Underlinked|date=November 2012}}
'''Pregroup grammar (PG)''' is a [[Formal grammar|grammar formalism]] intimately related to [[categorial grammar]]s. Much like categorial grammar (CG), PG is a kind of [[type logical grammar]]. Unlike CG, however, PG does not have a distinguished function type. Rather, PG uses inverse types combined with its monoidal operation.

== Definition of a pregroup ==

A pregroup is a [[partial order|partially ordered]] [[universal algebra|algebra]] <math>(A, 1, \cdot, -^l, -^r, \leq)</math> such that <math>(A, 1, \cdot)</math> is a [[monoid]], satisfying the following relations:

* <math>x^l \cdot x \leq 1 \qquad x \cdot x^r \leq 1</math> &nbsp;&nbsp;&nbsp;&nbsp;(contraction)

* <math>1 \leq x \cdot x^l \qquad 1 \leq x^r \cdot x</math> &nbsp;&nbsp;&nbsp;&nbsp;(expansion)

The contraction and expansion relations are sometimes called  [[Ajdukiewicz]] laws.

From this, it can be proven that the following equations hold:

* <math>1^l = 1 = 1^r</math>

* <math>x^{lr} = x = x^{rl}</math>

* <math>(x\cdot y)^l = y^l \cdot x^l \qquad (x\cdot y)^r = y^r \cdot x^r</math>

<math>x^l</math> and <math>x^r</math> are called the [[left adjoint|left]] and [[right adjoint]]s of ''x'', respectively.

The symbol <math>\cdot</math> and <math>\leq</math> are also written <math>\otimes</math> and <math>\to</math> respectively. In [[category theory]], pregroups are also known as [[compact closed category|(non-symmetric) compact closed (monoidal) categories]]. More typically, <math>x \cdot y</math> will just be represented by adjacency, i.e. as <math>xy</math>.

== Definition of a pregroup grammar ==

A pregroup grammar consists of a [[lexicon]] of words (and possibly [[morphemes]]) ''L'', a set of atomic types ''T'' which [[free object|freely generates]] a pregroup, and an relation <math>:</math> that relates words to types. In simple pregroup grammars, typing is a function that maps words to only one type each.

=== Examples ===

Some simple, intuitive examples using English as the language to model demonstrate the core principles behind pregroups and their use in linguistic domains.

Let ''L = {John, Mary, the, dog, cat, met, barked, at}'', let ''T = {N, S, N<sub>0</sub>}'', and let the following typing relation holds:

: <math>\text{John} : N \qquad \text{Mary} : N \qquad \text{the} : N \cdot N_0^l \qquad \text{dog} : N_0 \qquad cat : N_0</math>

: <math>met : N^r \cdot S \cdot N^l \qquad barked : N^r \cdot S \qquad at : S^r \cdot N^{rr} \cdot N^r \cdot S \cdot N^l</math>

A sentence ''S'' that has type ''T'' is said to be grammatical if <math>T \leq S</math>. We can prove this by use of a chain of <math>\leq</math>. For example, we can prove that <math>John\ met\ Mary : N \cdot N^r \cdot S \cdot N^l \cdot N</math> is grammatical by proving that <math>N \cdot N^r \cdot S \cdot N^l \cdot N \leq S</math>:

: <math>N \cdot N^r \cdot S \cdot N^l \cdot N ~\leq~ S \cdot N^l \cdot N ~\leq~ S</math>

by first using contraction on <math>N \cdot N^r</math> and then again on <math>N^l \cdot N</math>. A more convenient notation exists, however, that indicates contractions by connecting them with a drawn link between the contracting types (provided that the links are nested, i.e. don't cross). Words are also typically placed above their types to make the proof more intuitive. The same proof in this notation is simply

[[File:PregroupGrammar-Example-JohnMetMary.png|center|thumb]]

A more complex example proves that ''the dog barked at the cat'' is grammatical:

[[File:PregroupGrammar-Example-TheDogBarkedAtTheCat.png|center|thumb|upright=2]]

== Semantics of pregroup grammars ==

Because of the lack of function types in PG, the usual method of giving a semantics via the [[Lambda calculus|λ-calculus]] or via function denotations is not available in any obvious way. Instead, two different methods exist, one purely formal method that corresponds to the λ-calculus, and one denotational method analogous to (a fragment of) the tensor mathematics of [[quantum mechanics]].

=== Purely formal semantics ===

The purely formal semantics for PG consists of a logical language defined according to the following rules:

* Given a set of atomic terms ''T'' = {''a'', ''b'', ...} and atomic function symbols ''F = {f<sub>m</sub>, g<sub>n</sub>, ...}'' (where subscripts are meta-notational indicating arity), and variables ''x'', ''y'', ..., all constants, variables, and well-formed function applications are basic terms (a function application is well-formed when the function symbol is applied to the appropriate number of arguments, which can be drawn from the atomic terms, variables, or can be other basic terms)

* Any basic term is a term

* Given any variable ''x'', [''x''] is a term

* Given any terms ''m'' and ''n'', <math>m \cdot n</math> is a term

Some examples of terms are ''f''(''x''), ''g''(''a'',''h''(''x'',''y'')), <math>g(x,b) \cdot [x]</math>. A variable ''x'' is free in a term ''t'' if [''x''] does not appear in ''t'', and a term with no free variables is a closed term. Terms can be typed with pregroup types in the obvious manner.

The usual conventions regarding α conversion apply.

For a given language, we give an assignment ''I'' that maps typed words to typed closed terms in a way that respects the pregroup structure of the types. For the English fragment given above we might therefore have the following assignment (with the obvious, implicit set of atomic terms and function symbols):

: <math>I(John : N) = j : E</math>

: <math>I(Mary : N) = m : E</math>

: <math>I(the : N \cdot N_0^l) = \iota(p) \cdot [p] : E \cdot E_0^l</math>

: <math>I(dog : N_0) = dog : E_0</math>

: <math>I(cat : N_0) = cat : E_0</math>

: <math>I(met : N^r \cdot S \cdot N^l) = [x] \cdot met(x,y) \cdot [y] : E^r \cdot T \cdot E^l</math>

: <math>I(barked : N^r \cdot S) = [x] \cdot barked(x) : E^r \cdot T</math>

: <math>I(at : S^r \cdot N^{rr} \cdot N^r \cdot S \cdot N^l) = [x] \cdot y \cdot [y] \cdot at(x,z) \cdot [z] : T^r \cdot E^{rr} \cdot E^r \cdot T \cdot E^l</math>

where ''E'' is the type of entities in the domain, and ''T'' is the type of truth values.

Together with this core definition of the semantics of PG, we also have a reduction rules that are employed in parallel with the type reductions. Placing the syntactic types at the top and semantics below, we have

[[File:PregroupGrammar-LeftAdjointReduction.png|center|thumb|upright=1.5]]

[[File:PregroupGrammar-RightAdjointReduction.png|center|thumb|upright=1.5]]

For example, applying this to the types and semantics for the sentence <math>John\ met\ Mary : N \cdot (N^r \cdot S \cdot N^l) \cdot N</math> (emphasizing the link being reduced)

[[File:SemanticCalculation-JohnMetMary.png|center|thumb|upright=1.25]]

For the sentence <math>the\ dog\ barked\ at\ the\ cat : (N \cdot N_0^l) \cdot N_0 \cdot (N^r \cdot S) \cdot (S^r \cdot N^{rr} \cdot N^r \cdot S \cdot N^l) \cdot (N \cdot N_0^l) \cdot N_0</math>:

[[File:Pregroup-SemanticCalculation-TheDogBarkedAtTheCat.png|center|thumb|upright=2.5]]

== See also ==
* [[Compact closed category]]
* [[Lambek calculus]]

==References==
* {{cite journal|last=Lambek|first=Joachim|title=Pregroup grammars and Chomsky's earliest examples|journal=Journal of Logic, Language and Information|year=2008|volume=17|issue=2}}
* {{cite journal|last=Preller|first=Anna|title=Semantic pregroup grammars handle long distance dependencies in French|journal=Manuscript|year=2007}}
* Claudia Casadio (2004), [http://www.unich.it/~casadio/ricerca/slidescope.pdf Pregroup Grammar. Theory and Applications]

{{Reflist}}

[[Category:Grammar frameworks]]
[[Category:Semantics]]
[[Category:Type theory]]