Comments

Showing posts with label SMT. Show all posts
Showing posts with label SMT. Show all posts

Sunday, May 18, 2014

SMT III

Much as I enjoy the cut and thrust of debate about the discoveries of Generative Grammar and their significance for understanding FL, I am ready to change the topic, at least for a while. Before, doing so, let me urge those of you who have not been following the comment threads of my last two posts to dip into them. IMO, they are both (mostly) entertaining and actually insightful. I may be over-concluding here, but it looks to me that we have reached a kind of consensus in which almost everyone (there is one conspicuous exception, and I am sure regular readers can guess who this is) concurs that GG has made many serious empirical discoveries (what I dubbed "effects") that call for theoretical explanation.  With this consensus in hand, let’s return to the SMT.

In two previous posts (here and here), I outlined a version of the SMT that had several nice properties (or at least I thought them nice). First, empirically it linked work on syntax directly to work in psycho and vice versa, with results in each carrying clear(ish) consequences for work in the other. The SMT mediated this cross fertilization by endorsing a strong version of the transparency thesis wherein the performance systems used the principles, operations and representations of the competence systems to do what they do (and, this is important, do so well). I offered some illustrations of this two-way commerce and touted its virtues.

The second nice property of this version of the SMT is that it promises to deliver on the idea that grammars are evaluable wrt computational efficiency. Minimalists love to say that some property enhances or detracts from computational efficiency or adds or reduces computational complexity and our computational colleagues never tire from calling them/us out on this.[1] The SMT provides a credible sense in which grammars might be computationally efficient (CE). Grammars, operations, representations etc. are CE just in case transparently embedding them within performance systems allows these performance systems to be efficient. What’s ‘efficient’ mean? Parsers that parse fast are efficient. If these parsers are fast (i.e. efficient) (in part) because they embed grammars with certain specifiable properties then we can say that these grammars are CE. Ditto with acquisition. The SMT conjectures that we are efficient at acquiring our native Gs (in part) because UG has the properties it does. Thus, Gs and UGs are efficient to the degree that they explain why we are so good at doing (performing) what we do linguistically. Thus, given the SMT, Gs and UGs can be vicariously CE (VCE). I have been arguing that minimalists should endorse VCE as what they intend when claiming computational virtues for their minimalist proposals.

Say you buy this much. It would be useful to have a couple of paradigm examples of how to make the argument linking the properties of Gs and UG to CE in performance systems. Indeed, wouldn’t it be nice to have stories that take us from properties like, say, Extension, Cyclicity, and C-command to fast parsing and easy learnability. Fortunately, such illustrative examples exist. Let me bring a nice compact, short, and easily readable one to your attention. Berwick and Wexler (B&W) (here) provide a paradigm case of what I think we need. This paper was written in 1987 (the 80s really were a golden age for this sort of stuff, as Charles has noted), and sad to say, the wisdom it contains seems to have been almost entirely lost. In what follows I give a short précis of the B&W argument, highlighting what I take to be those features of the approach that it would behoove us to “rediscover” and use. It’s a perfect example of SMT reasoning.

B&W focuses on showing that c-command (CC) is “a linguistically-motivated restriction [that] can also be justified on computational grounds” (48)).  How do B&W show this? There are two prongs to the argument. First, B&W show how and under what conditions CC would enhance antecedence retrieval. The main result is that for trees that are as deep as they are wide the computational savings are a reduction in search time from N to log N (N = number of terminals) (48) when CC is transparently embedded in a Marcus Parser (M-Par).[2]

B&W then show that CC follows from a particular property of M-Pars, which B&W dub “constituency completeness” (55). What is this? It is the assumption that “the “interior” of any phrase attached to a node on the active node stack…[is] opaque to further access” (55). More specifically, “once a phrase has been completely built” it is “attached as a single, opaque object to its proper dominating phrase…Crucially, this means that the … [node] now acts as a single, opaque unit…[that will not be]…accessible to syntactic analysis.” As B&W note, “this restriction is simply the core notion of c-command once again” (50).

Constituent Completeness has an analogue within current syntax. It is effectively the Extension Condition (EC). EC states that once a constituent is built it cannot be further reconfigured (i.e tampered with). Furthermore, as several have noted, there is a tight connection between EC and CC, at least for some class of dependencies.[3] It is interesting to see these connections foreshadowed in B&W. Note that the B&W discussion in the current theoretical context lends credence to the idea that EC promotes CE via its relation to CC and M-Pars rapid parsing.

B&W observe that Constituent Completeness (aka, EC) has another pleasant consequence. It’s pivotal in making M-Pars fast. How so? First M-Pars is a species of Bounded Context Parsers (BCP). BCPs (and hence M-Pars) are fast because they move forward by “examining strictly literal contexts around the current locus of parsing” (55).  Thus, parsing decisions can only consult “the local environment of the parse.” To implement this, such local environments must be represented in the very same code that linguists use in describing syntactic objects:

…[a] decision will be made by consulting he local environment of the parse – the S and VP nodes, with the attached verb, and the three input buffer items. Further these items are recorded exactly as written by the linguist – as the nodes S, NP, VP, V and so forth. No “additional” coding is carried out. It this literal use of the parse tree context that distinguishes bounded context parsing…

Thus, Constituent Completeness (viz. EC) “effectively limits the left-hand parsing context that is available…[and] is a necessary requirement for such a parser to work” (55).

In other words, something very like EC contributes to making BCPs/M-Pars fast. Additionally, Constituent Completeness and the transparency assumption together motivate the Berwick and Weinberg proposal that something very like bounded cyclic derivations are necessary for efficient parsing given the relation between bounded left contexts and fast parsing. Every grammatical theory since the mid 80s has included some way of representing bounded cycles (i.e. either phases + PIC or Barriers+Subjacency or Bounding nodes + subjacency). Indeed, as you all know, Berwick and Weinberg argued that Subjacency was sufficient to provide bounded left contexts of the kind their parser required to operate quickly.  In sum, the B&W paper shows how EC (in the guise of Constituent Completeness) and something like bounded domains of computation (phases/subjacent domain) in the context of a M-Parser together can conspire to yield fast parsing. If so, this supports the view that something like EC and phases are computationally efficient. Wow!!

B&W doesn’t stop here. It goes on to speculate about the relation between fast parsing and easy learnability. Wexler and Culicover showed that grammars that have the BDE property (bounded degree of error) can be learned on the basis of degree 2 data.[4] It is possible that BDE and BCP are closely related. Berwick (here) showed that one can derive BDE from BCP and that both properties rely on something like EC and bounded domains of computation (which, to repeat, something like phase/subjacency theory would provide). B&W suggest that BDE might in turn imply BCE, which, if correct, would further support the idea that notions like EC and phases are CE. Indeed, should it prove possible to prove that Gs are easily learned iff they are quickly parsed and that both quick learning and speedy parsing leverage specific properties of G and UG like EC, phases/subjacency, CC etc. then we will have taken a big step in vindicating the SMT.

Let me end with two last comments on B&W.

First, one of the key features of the paper is the proposal to take M-Pars/BCPs as proxy models for efficient parsing and to then study what enables them to be so good. What B&W finds is that part of what makes them good are the data structures they use with the particular properties they encode. Thus, the choice to study M-Pars/BCPs is the choice to study parsers (and maybe BDE learners) “grounded in particular linguistic theories” (58).  As B&W note, this approach is quite unlike what one finds in formal learning theory or “the general results obtained from the parsability of formal languages” (58). B&W starts from a consideration of a narrower class of languages that are “already known to be linguistically relevant” (59). The aim, as B&W sees it, is to evaluate the impact on computations that the data structures we know to be operative in natural language Gs and UG have. As B&W puts it, what the paper develops is a model for studying “the interactions between data structures and algorithms…[as a way] to develop more computationally based linguistic theory” (51). In other words, it offers an interesting and concrete way of understanding the current minimalist interest in CE.

Second, as B&W stresses again and again, this is not the “last word” on the topic (53). But, to my eyes it is a very good first word. In contrast to many computational approaches to parsing and learning, it takes linguistic theory seriously and considers its implications for performance. Let me quote B&W:

…what we want to illustrate here is not the final result but the method of study. We can assess the relative strengths of parsability and learnability in this case, but only because we have advanced specific models for each. These characterizations are still quite specific, being grounded in particular linguistic theories. The results are therefore quite unlike the formal learning theories of Gold (1967), or more recently, of Osherson, Stob and Weinstein (1982) nor are they like the general results obtained from the analysis of the parsability of formal languages. Rather, they hold of a narrower class of languages that are already known to be linguistically relevant. In this respect, what the theories lose in terms of invariance over changes in linguistic theories, they gain in terms of specificity.[5] (58-9)

Thus, it offers a concrete way of motivating actually proposed principles of FL/UG on computational grounds. In other words, it offers a concrete way of exploring the SMT. Not bad for a 1987 paper that has long been ignored. It’s time to go back to the future.




[1] I still fondly recall a day in Potsdam several years ago when Greg Kobele suggested in the question period after a talk I gave that any minimalist claims to computational efficiency are unfounded (actually, he implied worse, BS being what sprang to my mind). At any rate, Greg was right to push. The SMT posts are an attempt to respond.
[2] For trees that are not “perfectly balanced” (i.e. not as deep as wide) the computational savings decline until they go to zero in simple left branching sentences.
[3] Epstein has noted this connection. Hornstein 2009 discusses it ad nauseum and it forms the basis of his argument that all relations mediated by CC should be reduced to movement. This includes pronominal binding. This unification of binding with movement is still very controversial (i.e. only Kayne, Sandiway Fong, me and a couple of other crazies think it possible) and cannot be considered as even nearly settled. This said, the connections to B&W are intriguing.
[4] Like real time parsing, I suspect degree 2 is too lax a standard. We likely want something stricter, something along the lines of Lightfoot’s degree 0+ (main clauses plue a little bit).
[5] This is important. Most formal work on language quite deliberately abstract away from what linguists would consider the core phenomenon of interest: the structure of Gs and UG. They results are general because they are not G/UG dependent. But this is precisely what makes them the wrong way for investigating G/UG properties and for exploring the SMT.

There is a counter argument, that by going specific one is committing hostages to the caprice of theory. There are days where I would sympathize with this. However, as I’ve not yet gone tired of repeating, the rate of real theoretical change within GG is far slower than generally believed. For example, as I noted in the main body of the post, modern theory is often closely related to old proposals (e.g. phases/subjacency or CC/EC). This means that theory change is not quite as radical as often advertised and so the effects of going specific not nearly as baleful as often feared.  This said, I need not be so categorical. General results are not to be pooh-poohed just because they are general. However, as regards the SMT, to the degree that formal results are not based in grammatically specific concepts, to that degree they will not be useful for SMT purposes. So, if you are interested in the SMT, B&W is the right way to go.

An aside: the branch of CS that that B&W take to be of relevance to their discussion is compiler theory, a branch of CS which gets its hand dirty with the nitty gritty details.

Monday, May 5, 2014

What has the SMT done for you lately?

A recent post (here) illustrated how the SMT provided a unified framework for various kinds of research into the structure of FL. In particular I reviewed some work showing how certain recent findings concerning online parsing followed were parsers to transparently embed grammars as the SMT would require. The flow of argument in the work described goes from results in syntax to consequences for online measures of incremental parsing complexity. In other words, this is a case where SMT, given some properties of the grammar, makes claims about some property of the interface. Here’s a question: can we reverse the direction of argument? Can we find cases where the SMT does grammatically useful work, in that some property of the interface makes a claim about what grammars must look like?  In other words, where the argument moves from some property of the interfaces to some claims about the right theory of grammar? 

Before offering some illustrations, let me note that the first kind of argument is nothing to sneeze at if you are interested in discovering the structure of FL (and who isn’t interested in this?). Why? Because the kind of evidence that comes from things like the filled gap effect and the plausibility effect are different from the kind of data that acceptability (under an interpretation) judgments provide. And, as every intro philo of science course will tell you, the best support for a theory comes from different kinds of data all pointing to the same conclusion (this is called consilience (a term Whewell invented)). Consequently, finding online data that supports conclusions garnered from acceptability data is interesting even if one is mainly interested in competence theories.

This said, for purely selfish reasons, it would still be nice to have examples of arguments going in the other direction as well: implications for grammatical theory from psycho considerations. I have three concrete(ish) examples to offer as models; one that I have talked about before (here) based on the work by Pietroski, Lidz, Hunter and Halberda (PLHH), but would like to remind you of, one on how to understand binding domains based on work by Dave Kush (here), and one that is entirely self-serving (i.e. based on some work I did on non-obligatory control) (here ch. 6).

Before proceeding, let me emphasize that the examples are meant to be illustrative of the logic of the SMT. I do actually think that the cited arguments are pretty compelling (of course I LOVE the third one). However, my point here is not to defend their truth but to outline their logic and how this relates to SMT reasoning. Being motivated by the SMT does not imply that an account is true. But given minimalist interests, it is an interesting property for an account to have. This out of the way, let’s consider some cases.

First PLHH’s argument concerning the meaning of ‘most.’ The argument is that there is a privileged representational format for the meaning of ‘most.’ It’s meaning is (1c) and not the truth functionally equivalent (1a) or (1b):

            (1) Three possible meanings for ‘most.’
a.     [{x: D (x)}, [x: Y (x)}] iff some some set s, s Ì {X: D(x)} and OneToOne [s, {x: Y (x)}]
                        b.   |{x: D (x) & Y (x)}| > {x: D (x) & - Y (x)}|
c.     |{x: D (x) & Y (x)}| > |{ x: D (x)}| - |{x: D(x) & Y (x)}|

Why (1c)? Because that’s the one that speakers use when evaluating the quantities of dot arrays when visually presented. And if one assumes that the products of well-designed grammars (e.g. meanings) are transparently used by the interfaces, i.e. if one assumes that the SMT is true, then the fact that the visual system uses representations like (1c) in preference to those in (1a,b) even when the others could be used is evidence that this is what ‘most’ means. In other words, given the SMT and the fact that (1c) is used (and used very efficiently and quickly (see the experiments)) implies that (1c) is the linguistic meaning of ‘most.’

Consider a second case with similar logic. In his thesis and in recent presentations (here), Dave Kush observes that speakers respect c-command restrictions when parsing sentences that involve quantificational binding. More specifically, in parsing sentences like (2a,b), speakers look for antecedents only within the c-command domain (CCD) of the bound pronoun. While parsing, speakers reliably distinguish cases like (2a), where the antecedent c-commands the bound pronoun, from those like (2b), where it doesn’t.

            (2) a. Kathi didn’t think that any janitor1 liked his job when he1 had to clean up
                  b. Kathi didn’t think that any janitor1 liked his job but he1 had to clean up       

Parsing sensitivity to CCDs is further buttressed by the difference found in the online parsing of Strong vs Weak Crossover (S/WCO) effects. Kush provides evidence that incremental parsing respects the former, which invokes CCDs, but not the latter, which does not.[[1]] As Kush notes, this fits well with earlier work on the binding of reflexives and reciprocals. Kush adds some Hindi data on reciprocals to earlier work by Dillon and Sturt on reflexives to ground this conclusion. Taking these various results together, Kush concludes, very reasonably IMO, that online parsing is sensitive to the c-command relations that bound expressions have wrt to their antecedents.

The conclusion, then, is that incremental parsing computes CCDs in real time. Based on this established fact, Kush then asks a second very interesting follow up question: how is this condition implemented in human parsers. He notes the following problem. Human memory architecture appears to be content addressable. He notes that this makes coding CCDs with such an architecture difficult.[[2]] However, the data clearly indicate that we code something like CCDs and do so online quickly. So how is this done? Kush suggests that we do not actually code for CCDs but for something that does similar work, something very like clausemates, the restriction that did the heavy lifting in previous incarnations of syntactic theory. Howard Lasnik and Ben Bruening have recently argued for a return to something like this (Bruening has proposed “phase-command” rather than c-command as the operative condition). Interestingly, as Kush shows, these alternatives to c-command can be made to comfortably fit with the kinds of content addressable memory architectures humans seems we have. Conclusion: our competence grammars use something like clause/phase command conditions rather than CCDs as the relevant primitive relations relevant to binding. Note that the direction of argument goes from online parsing facts plus facts about human memory architecture to claims about the primitive relations in the competence grammar. What’s of interest here is how the SMT is critical in licensing the argument form. Whether Kush is right or not about the conclusion he draws is, of course, important. But IMO, this mere factual issue it is not nearly as interesting as the argument form itself.

Let me end with a third example, one from some of my own work. As some of you may know, I have done some work on Control phenomena. With many colleagues (thx Jairo, Cedric, Masha, Alex), I have argued that there exists a theory of control, the Movement Theory of Control (MTC), that has pretty good empirical coverage and can effectively be derived given certain central tenets of the Minimalist Program (MP). In particular, once one eliminates D-structure in toto and treats Move as a species of Merge then the MTC is all but inevitable. None of this means to say that the MTC is empirically correct, but it does mean that it is a deeply minimalist theory. I would go further (and indeed I have) and argue that the MTC is the only deeply minimalist theory of control and if something like it is incorrect then either MP is wrong (at least for this area of grammar) or control phenomena are not part of FL (here’s a good place to wave hands about properties of the interface). Why do I mention this? Because the MTC is a theory of obligatory control (OC) and, as we all know, this is not the end of the control menagerie. There is non-obligatory control (NOC) as well. What does the MTC have to say about this?

Well, not that much actually.[[3]] Here’s what MTCers have said: it’s the by-product of having a pro in a subject position rather than a PRO (viz. an “A-trace”). And this proposal creates problems for the MTC. How?

Well, to get the data to fall out right any theory of control must assume that given a choice between an OC and an NOC configuration, grammars prefer OC.[[4]] In the context of the MTC this translates into saying that grammars prefer OC style movement to pro binding. Let’s call this a preference for Move over Bind. This sets up the problem. Here it is.

The MTC explains cases like (3a) on the assumption that the gap in the lowest clause is a product of movement (i.e. an “A-trace”). But what prevents a representation like (3b) with a pro in place of the trace thereby licensing the indicated unavailable interpretation? Nothing, and this is a problem.

            (3) a. John1 expects Mary2 to regret PRO2/*1 shaving himself1
                  b. John1 expects Mary2 to regret pro1 shaving himself1

The SMT provides a possible solution (this is elaborated in detail here ch. 6). Given the SMT, parsers respect the distinctions grammars make. Thus, parsers must also prefer treating ecs as A-traces rather than pros if they can. So, in parsing a sentence like (4) the parser prefers treating the ec as an A-trace/Copy rather than a pro. But if so, this A-trace must find a (very) local antecedent. Mary fits the bill, John cannot (it would violate minimality).

            (4) John expects Mary to regret ec shaving himself

Given this line of reasoning, (3b) above is not a possible parse of the indicated sentence and so the sentence is judged unacceptable. Note that this account relies on the SMT: the parser must cleave to the contours the grammar lays out. Thus, given the grammatical preference for Move over Bind we cannot parse the ec in (4) as a pro and so the structure in (3b) is in principle unavailable to the parser.

Note that this logic only applies to phonetically null pronouns. The parser need not decide on the status of a phonetically overt pronoun, hence the acceptability of (5) with the same binding relations we were considering in (3b):

            (5) John1 expects Mary to regret him1 shaving himself1

I don’t expect anyone to believe this analysis (well, not as stated here. Once you read the details you will no doubt be persuaded). Indeed, I have had a hard time convincing very many that the MTC is on the right track at all. But, for the nonce I just want to note that the logic deployed above illustrates another use of SMT reasoning. Let’s review.

Given the SMT, there are strong ties between what parsers do and what grammars prescribe. One can argue from the properties of one to those of the other given the transparency assumptions characteristic of the SMT. In this case, we can use it to argue that though there is nothing grammatically wrong with (3b) it is, given the MTC and the grammatical preference for Move over Bind, inherently unparsable, hence unacceptable under the indicated interpretation.

I have reviewed three instances of SMT reasoning where claims about processing have implications for the competence theory. We have already reviewed arguments that move from competence grammars to interface properties. As is evident (I hope), the SMT has interesting implications for the relationship between the properties of performance systems and competence theories. This should not come as a surprise. We have every reason to think that there is an intimate connection between the shapes of data structures and the algorithms that use them efficiently (see Marr or Gallistel and King on this topic). The SMT operationalizes this truism in the domain of language. Of course, whether the SMT is true is an entirely different issue. Maybe it is, maybe it isn’t. Maybe FL’s data structures are well designed, maybe not. However, for the first time in my linguistic life, I am starting to see how the SMT might function in providing interesting arguments to probe the structure of FL. It seems that at least one version of the SMT has empirical clout and licenses interesting inferences about the structure of performance systems given the properties of competence systems AND vice versa, the structure of competence systems given the properties of performance systems. This version of the SMT further provides a way of understanding minimalist claims about the computational efficiency of grammatical formalisms that make computational sense.[[5]]  Of course, this may all be wrong (though not wrong-headed), but it is novel (at least to me) and very very exciting.

Last point and I sign off: The above outlines one version of the SMT. There are various interpretations around. I have no idea whether this version is exactly what Chomsky has been proposing (I suspect that it is in the same intellectual region, but I don’t really care if my exegesis is correct). I like this interpretation for I can make sense of it and because it has a pedigree within Generative Grammar (which I will discuss in a proximate future post). Some don’t seem to like it because it does not make the SMT obviously false or incoherent (you know who you are). The above version of the SMT relies on treating it as an empirical thesis (albeit a very abstract one) about good design. Good design is indexed by various empirical properties: fast parsing and easy learning being conspicuous examples. Whether the FL design is “optimal” (whatever that might mean) is less interesting to me than the question of how/whether our very efficient linguistic performance systems are as good as they are because they exploit FL’s basic properties. It seems to be a fact that we are very good at language processing/production and acquisition. Some might think that how we do these things so well (and why) calls for an explanation. One explanation, the one that I have urged that we investigate (partly because I believe we have some non-trivial evidence bearing on the questions already), is that part of what makes us good at what we do is that the data-structures that Gs generate (our linguistic knowledge) have the properties they have. In short: why are we fast parsers and good acquirers? Because grammars embody principles like c-command, subjacency, Extension etc. That folks is the SMT! And that folks is a very interesting conjecture that we are just now beginning to study in a non-trivial manner. And that folks is called progress. Yessss!



[1] This raises the interesting question of how to model WCO if one accepts the SMT. Why don’t we find WCO effects in online measures like the ones that pop out for SCO?
[2] Actually the argument is more involved: if we model this feature about human memory in something like an Act-R framework (this is based on implementations of this idea by Rick Lewis) then coding c-command into the system proves to be very difficult.
[3] Well, it does say that NOC must occur where movement is prohibited, say into islands:
(i)             John said that [ ec kissing Mary] would upset Bill
Thus, the ec in (i) is not the product of movement, so not a case of OC, and thus must be a case of NOC.
[4] Were both equally optional NOC would render OC effects invisible as the latter’s observable properties are a proper subset of the former’s.
[5] I will go into this in more detail in a post that I am working on.

Sunday, February 9, 2014

Where Chris Collins enters the fray

Chris sent me this longish response to some of what has appeared in the blog. In the hope of getting him to become a regularish participant in the ongoing discussions I here post his "Response to Norbert." I feel that he let me off lightly, actually. But this said, I think that I can still finds some points to disagree with. I will restrict these to the comments section and hand the floor over to him. Thx Chris.

*****

Response to Norbert

I read with interest Norbert’s recent post on formalization: “Formalization and Falsification in Generative Grammar”. Here I write some preliminary comments on his post.  I have not read other relevant posts in this sprawling blog, which I am only now learning how to navigate. So some of what I say may be redundant. 

For me the quote by Frege in the Begriffsschrift (pg. 6 of the book “Frege and Godel”) indicates what is important when he analogizes the “ideography” (basically first and second order predicate calculus) to a microscope: “But as soon as scientific goals demand great sharpness of resolution, the eye proves to be insufficient. The microscope, on the other hand, is perfectly suited to precisely such goals, but that is just why it is useless for all others.” Similarly, formalization in syntax is a tool that needs to be employed when needed. It not an absolute necessity and there are many ways of going about things (as I discuss below). By citing Frege, I am in no way claiming that we should aim at the same level of formalization that Frege did.

There is an important connection with the ideas of Rob Chametzky (posted by Norbert) in another place on this blog. As we have seen, Rob divides up theorizing into meta-theoretical, theoretical and analytical.  Analytical work, according to Chametzky is: “concerned with investigating the (phenomena of the) domain in question. It deploys and tests concepts and architecture developed in theoretical work, allowing for both understanding of the domain and sharpening of the theoretical concepts.” It is clear that more than 90% of all linguistics work (maybe 99%) is analytical, and that there is a paucity of true theoretical work.

A good example of analytical work would be Chomsky’s “On Wh-Movement”, which is one of the most beautiful and important papers in the field. Chomsky proposes the wh-diagnostics and relentlessly subjects a series of constructions to those diagnostics uncovering many interesting patterns and facts. The consequence that all these various constructions can be reduced to the single rule of “wh-movement” is a huge advanced, allowing one insight into UG. Ultimately, this paper lead to the Move-Alpha framework, and indirectly to Merge (the simplest and most general operation yet).
However, “On Wh-Movement” is what I would call “semi-formal”. It has semi-formal statements of various conditions and principles, and also lots of assumptions are left implicit. As a consequence it has the hallmark property of semi-formal work: there are no theorems and no proofs. Formalization is stating a theory clearly and formally enough that one can establish conclusively (i.e., with a proof) the relations between various aspects of the theory and between claims of the theory and claims of alternative theories.

Certainly, it would have been a waste of time to fully formalize “On Wh-Movement”. It would have expanded the text 10-20 fold at least, and added nothing. This is something that I think Pullum completely missed in his 1989 paper on formalization. The semi-formal nature of syntactic theory, also found in such classics as “Infinite Syntax” by Ross and “On Raising” by Postal, has led to a huge explosion of knowledge that people outside of linguistics/syntax cannot really understand (hence all the lame discussion out there on the internet and Facebook about what the real accomplishments of generative grammar have been), in part because syntacticians are not very good popularizers.
Theoretical work, according to Rob is:  “is concerned with developing and investigating primitives, derived concepts and architecture within a particular domain of inquiry.” There are many good examples of this kind of work in the minimalist literature. I would say Uriagereka’s original work on multi-spell-out qualifies and so does Epstein’s work on c-command, amongst others.

My feeling is that theoretical work (in Chametzky’s sense) is the natural place for formalization in linguistic theory. The reason is that it is possible, using formal assumptions to show clearly the relationship between various concepts, assumptions, operations and principles. For example, it should be possible to show, from formal work, that things like the NTC and Extension condition should really be thought of as theorems proved on the basis of assumptions about UG.  Since NTC and Extension condition are theorems, they can actually be eliminated from UG. And from this, one can wonder if that program can be extended to the full range of what syntacticians normally think about as constraints.
In this, I agree with Norbert who states: “It can lay bare what the conceptual dependencies between our basic concepts are.” Furthermore, as my previous paragraph makes clear, this mode of reasoning is particularly important for pushing the SMT forward. How can we know, with certainty, how some concept/principle/mechanism fits into the SMT? We can formalize and see if we can prove relations between our assumptions about the SMT and the various concepts/principles/mechanisms. Using the ruthless tools of definition, proof and theorem, we can gradually whittle away at UG, until we have the bare essence. I am sure that there are many surprises in store for us. Given the fundamental, abstract and subtle nature of the elements involved, such formalization is probably a necessity, if we want to avoid falling into a muddle of unclear conclusions.

A related reason for formalization (in addition to clearly stating/proving relationships between concepts and assumptions) is that it allows one to clarify murky areas. One of the biggest such areas nowadays is whether syntactic dependencies make use of chains, multi-dominance structures or something else entirely (maybe nothing else). Chomsky’s papers, including his recent ones, make references to chains at many points. But other recent work invokes multi-dominance. What are the differences and relations between these theories and are either of them really necessary? What assumptions about UG does multi-dominance or chains entail? I am afraid that without formalization it will be impossible to answer these questions. I am investigating these questions in my seminar this semester.
These questions about syntactic dependencies interact closely with TransferPF (Spell-Out) and TransferLF, which to my knowledge, have not only not been formalized but not even stated in an explicit manner. Investigating the question of whether multi-dominance, chains or some something else entirely (perhaps nothing else) is needed to model human language syntax will require a concomitant formalization of TransferPF and TransferLF, since these are the functions that make use of the structures formed by Merge.

Minimalist syntax calls for formalization in a way that previous syntactic theories did not. First, the nature of the basic operations is simple enough (e.g., Merge) to make formalization a real possibility. The baroque and varied nature of “transformations” in the “On Wh-Movement” framework and preceding work made the prospect for a full formalization more daunting.

Second, the nature of the concepts involved in minimalism, because of their simplicity and generality (e.g., copies, occurrences), are just too fundamental and subtle and abstract to resolve by talking through them in an informal or semi-formal way. With formalization we can hope to state things in such a way to make clear conceptual and empirical properties of the various proposals, and compare and evaluate them. In fact, I have recently being doing a lot of this with my colleagues, because only recently (by helping to write Collins and Stabler 2012) have I seen what the issues are.
So, in the spirit of Frege, formalization should be a tool for ordinary working syntacticians to clarify their ideas and examine them empirically and conceptually.