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