# 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 ProofFebruary 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 GADTsJanuary 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 ApproachDecember 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. 1November 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 GrammarOctober 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 GreekSeptember 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 GreekMay 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 SymposiumMay 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.