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