Lecomte and Retoré (2001) ^[1] introduce a formalism that modifies that core of the Lambek Calculus to allow for movement-like processes to be described without resort to the combinatorics of Combinatory categorial grammar. The formalism is presented in proof-theoretic terms. Differing only slightly in notation from Lecomte and Retoré (2001), we can define a minimalist grammar as a 3-tuple ${\displaystyle G=(C,F,L)}$ , where ${\displaystyle C}$  is a set of "categorial" features, ${\displaystyle F}$  is a set of "functional" features (which come in two flavors, "weak", denoted simply ${\displaystyle f}$ , and "strong", denoted ${\displaystyle f*}$ ), and ${\displaystyle L}$  is a set of lexical atoms, denoted as pairs ${\displaystyle w:t}$ , where ${\displaystyle w}$  is some phonological/orthographic content, and ${\displaystyle t}$  is a syntactic type defined recursively as follows:

all features in ${\displaystyle C}$  and ${\displaystyle F}$  are (atomic) types, and

if ${\displaystyle X}$  and ${\displaystyle Y}$  are types, so are ${\displaystyle X/Y}$ , ${\displaystyle X\backslash Y}$ , and ${\displaystyle X\circ Y}$ .

We can now define 6 inference rules:

${\displaystyle \vdash w:X}$ , for all ${\displaystyle w:X\in L}$ 

${\displaystyle w:X\vdash w:X}$ , for all ${\displaystyle w:X\notin L}$ 

${\displaystyle {\frac {\Gamma \vdash a:X/Y\qquad \Gamma '\vdash b:Y}{\Gamma ;\Gamma '\vdash ab:X}}[/E]}$ 

${\displaystyle {\frac {\Gamma '\vdash b:Y\qquad \Gamma \vdash a:X\backslash Y}{\Gamma ';\Gamma \vdash ba:X}}[\backslash E]}$ 

${\displaystyle {\frac {\Gamma ;\Gamma '\vdash \alpha }{\Gamma ,\Gamma '\vdash \alpha }}entropy}$ 

${\displaystyle {\frac {\Gamma \vdash a:X\circ Y\qquad \Delta ,b:X,c:Y,\Delta '\vdash d:Z}{\Delta ,\Gamma ,\Delta '\vdash d[b:=a,c:=a]:Z}}[\circ E]}$ 

The first rule merely makes it possible to use lexical items with no extra assumptions. The second rule is just a means of introducing assumptions into the derivation. The third and fourth rules just perform directional feature checking, combining the assumptions required to build the subparts that are being combined. The entropy rule presumably allows the ordered sequents to be broken up into unordered sequents. And finally, the last rule implements "movement" by means of assumption elimination.

The last rule can be given a number of different interpretations in order to fully mimic movement of the normal sort found in the Minimalist Program. The account given by Lecomte and Retoré (2001) is that if one of the product types is a strong functional feature, then the phonological/orthographic content associated with that type on the right is substituted with the content of the a, and the other is substituted with the empty string; whereas if neither is strong, then the phonological/orthographic content is substituted for the category feature, and the empty string is substituted for the weak functional feature. That is, we can rephrase the rule as two sub-rules as follows:

${\displaystyle {\frac {\Gamma \vdash a:X\circ Y^{*}\qquad \Delta ,b:X,c:Y^{*},\Delta '\vdash d:Z}{\Delta ,\Gamma ,\Delta '\vdash d[b:=\epsilon ,c:=a]:Z}}[\circ E_{strong}]}$  where ${\displaystyle X\in C,Y^{*}\in F}$ 

${\displaystyle {\frac {\Gamma \vdash a:X\circ Y\qquad \Delta ,b:X,c:Y,\Delta '\vdash d:Z}{\Delta ,\Gamma ,\Delta '\vdash d[b:=a,c:=\epsilon ]:Z}}[\circ E_{weak}]}$  where ${\displaystyle X\in C,Y\in F}$ 

Another alternative would be to construct pairs in the /E and \E steps, and use the ${\displaystyle \circ E}$  rule as given, substituting the phonological/orthographic content a into the highest of the substitution positions, and the empty string in the rest of the positions. This would be more in line with the Minimalist Program, given that multiple movements of an item are possible, where only the highest position is "spelled out".

As a simple example of this system, we can show how to generate the sentence who did John see with the following toy grammar:

Let ${\displaystyle G=(\{N,S\},\{W\},L)}$ , where L contains the following words:

${\displaystyle {\text{John}}:N\ }$ 

${\displaystyle {\text{see}}:(S\backslash N)/N}$ 

${\displaystyle {\text{did}}:(S\backslash W)/S}$ 

${\displaystyle {\text{who}}:N\circ W}$ 

The proof for the sentence who did John see is therefore:

${\displaystyle {\dfrac {\vdash {\text{who}}:N\circ W\quad {\dfrac {{\text{x}}:W\vdash {\text{x}}:W\quad {\dfrac {\vdash {\text{did}}:(S\backslash W)/S\quad {\dfrac {\vdash {\text{John}}:N\quad {\dfrac {{\text{y}}:N\vdash {\text{y}}:N\quad \vdash {\text{see}}:(S\backslash N)/N}{{\text{y}}:N\vdash {\text{see y}}:S\backslash N}}[/E]}{{\text{y}}:N\vdash {\text{John see y}}:S}}[\backslash E]}{{\text{y}}:N\vdash {\text{did John see y}}:S\backslash W}}[/E]}{{\text{x}}:W,{\text{y}}:N\vdash {\text{x did John see y}}:S}}[\backslash E]}{\vdash {\text{who did John see}}:S}}[\circ E]}$ 

• Harkema, H., 2001. "A characterization of minimalist languages", in: de Groote, P., Morrill, G., Retoré, C. (Eds.), Logical Aspects of Computational Linguistics (Lecture Notes in Artificial Intelligence, No. 2099). Springer, New York, pp. 193–211, doi:10.1007/3-540-48199-0_12
• Edward P. Stabler (2010). "After Government and Binding Theory". In Johan F.A.K. van Benthem; Alice ter Meulen (eds.). Handbook of Logic and Language (2nd ed.). Elsevier. pp. 395–414. ISBN 978-0-444-53727-0.