Software engineer, dilettante type theorist, syntactician, and philologist. Student of Ancient Greek, Sumerian, Hittite, Akkadian, Latin, Old English and German.

I’m currently banging my head against a combinatory categorial grammar model for Ancient Greek, which will help us generate word order for Greek compositionally with minimal incidental structure.

To those of us without a background in topology, it may have initially been surprising that the unit circle \(S^1\) is not contractible. In this post, I’ll outline a homotopy type-theoretic proof for why this is in fact the case.

It is well known that generalized algebraic data types (a sort of phase-locked inductive family) suffice in languages like Haskell^{1} and OCaml to be used as a deductive system for intuitionistic logic. I’ll demonstrate how type-level axioms can be given and used in Standard ML, using only signatures and functors.

The issue of verbs which appear to take multiple arguments has long been a sticking point for Chomskyan grammarians, with various proposals having taken shape. Here, I’ll describe current approaches in transformational grammar, and demonstrate another approach in Multi-Modal Combinatorial Categorial Grammar. Finally, I’ll discuss the pros and cons of each approach.

As I read Bell’s *A Primer of Smooth Infinitesimal Analysis*, I thought it would be useful for me to write down my workings of the exercises as I went. The proofs are in the language of Intuitionistic Type Theory; according to common practice, I will sometimes omit arguments from application which can easily be inferred from the others.

Baldridge’s Multi-Modal extension of Steedman’s CCG attempts to account for variation in rule applicability entirely within the lexicon, by annotating slash types (function arrows) with modalities, which license different combining rules: \(\bullet\) licenses only simple application, \(\diamond\) simple application and harmonic composition/substitution, \(\times\) simple application and permuting composition/substitution, and \(\star\) licenses all rules. I demonstrate that further refinement is needed in order to have a grammar which suffices for the most basic hyperbata of Ancient Greek (and Latin).

Within a type-theoretic grammar, we must eventually deal with the issue of argument-ordering in languages which have (relatively) free word order. One approach, considered unsatisfactory, is to provide multiple categorial types for a word, giving the different orders in which it may accept its arguments; this is embeddable within a minimal CCG calculus. Another is to make copious use of the type raising operator combined with composition to construct mountains of unsatisfied clauses: this is less than optimal, however, given that the type raising operator itself is problematic for reasons outside the scope of this short exposition. So today, I shall present two different modest extensions to CCG which address this issue, namely *something old* and *something new*.

This is the first in a series I intend to write in regard to the syntax of Ancient Greek hyperbaton, and what can be done about it formally using a combinatory categorial grammar^{1}. We will begin with a pathological example of \(Y_1\) hyperbaton from Sophocles’ *Trachinian Women*:

τὴν Εὐρυτείαν οἶσθα δῆτα παρθένον;

the-*acc* of-Eurytus-*acc* know-*2.sing* of-course girl-*acc*

“You of course know the daughter of Eurytus…?” (*Trachinian Women*, l. 1219)

The six speeches of the *Symposium* may be divided into two sets: on the one hand, there is Phaedrus’s speech and those which are derivative of his, and on the other hand, there are the novel speeches; and these are the ones which reject the previous approaches and propose unique theories of Eros.

All posts…