Abstract

A couple years ago, in order to handle scrambling in Japanese, I introduced a new calculus for the semantic side of CCG derivations. This simple calculus is easy to describe and it can also be used to formalize keyword-arguments in programming languages, to justify notational shorthands in category theory, and numerous other things I keep stumbling upon. The calculus ties together a number of disparate threads in theoretical linguistics, type theory, logic, and category theory; and seems therefore worthy of future study. But one nagging question is: is it a nice place to do work? Does the calculus have the properties we usually desire from computational formalisms, like confluence and strong normalization?

This summer I worked on answering these questions. Some have been answered in the affirmative. Others remain open, due to limitations in our usual techniques for solving them— and perhaps due to limitations in our understanding of the phenomena in question. This talk relays some of that exploration.