This page links to some proofs and discussion supplementing Eisner (1996), "Efficient Normal-Form Parsing for Combinatory Categorial Grammar."
Frederick Hoyt requested the proofs in March 2008, pointing out
that I had never posted them on cmp-lg. Below is my email
response.
The 3 attachments containing the actual proofs can be found at the
URL http://cs.jhu.edu/~jason/papers/eisner.acl96-proof/.
(You'll have to cut-and-paste that URL into your browser. I
didn't make it clickable because I thought maybe it shouldn't be
indexed by search engines ... it seemed better if people instead
find this page first.)
From: Jason Eisner Date: Sat, Mar 1, 2008 at 5:30 PM Subject: Re: Hoyt - UT-Austin: Proofs for Eisner (1996) To: Frederick Hoyt Cc: Jason Baldridge On Fri, Feb 29, 2008 at 1:30 PM, Frederick Hoyt wrote: > My name is Fred Hoyt, and I am a PhD candidate working with Jason > Baldridge at UT-Austin. > > I am writing regarding your 1996 paper on normal-form parsing > constraints in combinatory categorial grammar. In your paper, you > refer the reader interested in detailed proofs for you theorems to > the compling archives. I have looked there, and found only the paper > itself. Additional Google searches have not brought them to light. > > Could I impose upon your time long enough to direct me to where I > might find the proofs? Dear Fred (and hi Jason!), Thanks for your interest. This certainly takes me back ... I think I must have had some intention to improve the style of the proof or further extend the results before posting it to cmp-lg -- evidently I never did, for which apologies. (In partial defense, the version that I *submitted* to ACL'96 only asserted the existence of the proof without promising to post it, so at least it wasn't accepted under false pretenses.) In all these years, you're the first person to ever ask about it! Glad you're working on this or related issues. I attach three items that should tell you what you need to know. The first is a term project paper with a proof for the generalized FC and BC combinators. It is dated spring 1993, but since I didn't actually start grad school until fall 1993 and the timestamp on the .tex file is 5/16/1994, I think it should say spring 1994! I got around to turning this into an ACL submission about 1.5 years later, around 1/10/1996. The second is a text file dated 4/29/1996, showing how to extend that proof to also handle the S combinator. (At least, I hope it completes that job. If it doesn't, let me know and I will look for other notes on the subject.) This extension wasn't in the ACL submission; I worked it out for the camera-ready version around 5/2/1996. The third appears to be a draft of the thing I was going to post to cmp-lg. The .tex file was last edited on 6/23/1996. Now, after these writings, I spent some time (a couple of weeks, I think) working on trying to extend the theorems to handle the T combinator as well -- i.e., productive type-raising of arbitrary constituents. Even conjecturing a correct theorem was difficult (I have a specific memory of wrestling with it while visiting my girlfriend in Chicago, and I don't think I got a conjecture that withstood testing). But I seemed to be moving in a direction that might have yielded a more elegant (less "syntactic") proof of the ACL'96 theorems as well as extending to handle the T combinator. I had a sense that this direction was connected to proof nets, and figured I ought to learn about them, but Girard's paper didn't seem like the best place to start. Ultimately I got distracted by other work that I was doing at the time (on statistical CF and dependency parsing) and let the further CCG work lapse. I probably do still have my paper notes from that time if you're interested in picking this up. It's work that ought to be done, assuming no one else has done it. BTW, I also have a couple of old Prolog files that do normal-form CCG parsing, if these are of any use to you. I suppose I wrote them as a sanity check. -cheers, jason p.s. Interestingly, a normal-form parsing problem popped up again in my recent work. NF parsing is needed with Eisner & Tromble (2006). A few months back, I derived a non-trivial normal-form algorithm for the quadratic-time-searchable neighborhood that we proposed at one point in that paper; as a check, Roy Tromble verified it experimentally for n <= 8. We should probably have sent that work to ACL'08 ...