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 ...