winterkoninkje: shadowcrane (clean) (Default)

For all you local folks, I'll be giving a talk about my dissertation on November 5th at 4:00–5:00 in Ballantine Hall 011. For those who've heard me give talks about it before, not much has changed since NLCS 2013. But the majority of current CL/NLP, PL, and logic folks haven't seen the talk, so do feel free to stop by.

Abstract: Many natural languages allow scrambling of constituents, or so-called "free word order". However, most syntactic formalisms are designed for English first and foremost. They assume that word order is rigidly fixed, and consequently these formalisms cannot handle languages like Latin, German, Russian, or Japanese. In this talk I introduce a new calculus —the chiastic lambda-calculus— which allows us to capture both the freedoms and the restrictions of constituent scrambling in Japanese. In addition to capturing these syntactic facts about free word order, the chiastic lambda-calculus also captures semantic issues that arise in Japanese verbal morphology. Moreover, chiastic lambda-calculus can be used to capture numerous non-linguistic phenomena, such as: justifying notational shorthands in category theory, providing a strong type theory for programming languages with keyword-arguments, and exploring metatheoretical issues around the duality between procedures and values.

Edit 2014.11.05: The slides from the talk are now up.

winterkoninkje: shadowcrane (clean) (Default)

Until recently I've been using semantic for typesetting my deduction rules and deduction proofs. But in writing the last few papers I've become acutely aware of its limitations: in particular, it offers no way to do dotted or doubled inference lines. After looking around for a while I found bussproofs; and I don't think I'll ever look back.

The semantic package is solid enough, and follows the traditional structural/nested style of macros. At first I was quite dubious of bussproofs' stack-machine style of macros, but after typing up a few proofs in it, I'm convinced. Because you don't have all the nested braces, it's much easier to restructure, clean up, or copypaste chunks of proofs. It's a bit verbose, all told, but that's easy enough to remedy by writing your own layer of macros on top of it. The one downside to bussproofs (compared to semantic) is that it doesn't support arbitrarily many premisses, and it doesn't allow vertical orientation of premisses. So if your typing rules are complex enough, you may need to stick with semantic; but for doing proofs in basic logics, or for doing CCG derivations, bussproofs is where it's at.

winterkoninkje: shadowcrane (clean) (Default)
So it looks like I'll be giving a talk at NASSLLI next week. It's a 30min talk, which seems rather short coming from CLSP's hour-long NLP seminars, though apparently it counts as long from a conference timeline. The Midwest Theory Day talks were also half an hour and nobody got much beyond their background material, which seems ludicrous as a means of disseminating new research. Oh well.

The talk is on a new semantic logic for handling constrained free word order in CCG. The logic is based on lambda calculus extended with something like a type system, though the extension is orthogonal to most type systems. Outside of CCG and linguistics, the logic seems like it would be helpful for typing the free ordering of keyword arguments or for capturing certain kinds of staged computation. I'm (re)writing up the paper this summer, so hopefully I'll be able to point y'all at a publication early next year. If you're interested and in the area you should stop by. Lots of other interesting things at NASSLLI this year too.
RSS Atom

March 2017



Page generated 30 Mar 2017 12:42 pm
Powered by Dreamwidth Studios