Jonathan Sterling.

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.

The Circle Is Not Contractible: A Short Proof February 1, 2014

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.

Standard ML as a Proof System, without GADTs January 4, 2014

It is well known that generalized algebraic data types (a sort of phase-locked inductive family) suffice in languages like Haskell1 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.

Ditransitives & Datives Without Movement: A Multi-Modal Approach December 14, 2013

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.

A Primer of Smooth Infinitesimal Analysis: Some Exercises from Ch. 1 November 7, 2013

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.

Hyperbaton & Resource Sensitivity in Combinatory Categorial Grammar October 26, 2013

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

Proof-Relevant MCCG: an approach to scrambling in Ancient Greek September 2, 2013

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.

Combinatory Categorial Grammar for Ancient Greek May 20, 2013

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

Derivative and Novel Speeches in Plato’s Symposium May 19, 2013

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…