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

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

### Towards Univalent Observational Type Theory: First StepsJuly 7, 2013

Last week I proposed a way to embed non-canonical equality proofs in a type theory in such a way as to force that they are eliminated prior to evaluation. This approach has a few problems. Today, I shall reformulate equality internally after the manner of Altenkirch, McBride et al,1 and again shy away from the problem of computing congruence or substitution over functions, which is quite a bit more difficult.2

### Terms Indexed by Canonicity Admit Coercion Across IsomorphismJune 30, 2013

Let $$\mathcal{U}$$ be an impredicative universe defined as follows with an empty set, a unit set, a boolean set, non-dependent functions, products, and some notion of equality which we will elaborate upon later:

\begin{align*} \mathcal{U} &:\equiv \{\text{Set}, \mathbf{0}, \mathbf{1}, \mathbf{2}, \cdot\to\cdot, \cdot\otimes\cdot, \cdot\cong\cdot \} \end{align*}

$$\mathcal{U}$$ is embedded in Martin-Löf Type Theory with UIP and given with the following translation:

\begin{align*} ⟦\text{Set}⟧ &\mapsto \color{blue}{\text{Set}}\\ ⟦\mathbf{0}⟧, ⟦\mathbf{1}⟧, ⟦\mathbf{2}⟧ &\mapsto \color{blue}{\bot}, \color{blue}{\top}, \color{blue}{\text{Bool}}\\ ⟦A\, \to\, B⟧, ⟦A\, \otimes\, B⟧ &\mapsto \color{blue}{\prod_{x : ⟦A⟧} ⟦B⟧}, \color{blue}{\sum_{x : ⟦A⟧} ⟦B⟧}\\ ⟦A\, \cong\, B⟧ &\mapsto \color{blue}{⟦A⟧ \equiv ⟦B⟧}\\ \end{align*}

We define $$\mathcal{U}$$ together with a term language, and in a particularly egregious abuse of notation, conflate the interpreting functions $$⟦\cdot⟧$$ for the two.

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

### A Survey of Phrase Projectivity in the AntigoneApril 28, 2013

In this paper, I demonstrate how, and to what degree, phrase projectivity corresponds with register and meter in Sophocles’s Antigone, by developing a quantitative metric $$\wp$$ for projectivity and comparing it across lyrics, trimeters and anapaests using the data provided by the Perseus Ancient Greek Dependency Treebank. In the appendices, the formal algorithm for the computations done herein is developed in Haskell.