Thanks, Bas. I’m still hoping to be (one of) the first to get something about the homotopy of HoTT meets natural language into print in the form of the equivariant definite description idea here. Two to-and-fros to a referee already. Third time lucky.

I know some people here…

Where are you?

]]>Slides on Copredication in Homotopy Type Theory: A homotopical approach to formal semantics of natural languages haven’t read it yet, but I know some people here are interested in this direction.

]]>I happened to remember that I never replied to #13 and #14, my apologies!

Regarding #13: thanks very much, I was not aware of this work!

Regarding #14: such an example would indeed be impressive! But my main point was not so much to do with the scope of examples, as with the approach one takes. What I was getting at is that I would like to see things turned on their head: rather than saying “here is a nice example, let us translate it into dependent type theory using some rough guiding principles”, I would like to see a formal theory of semantics in dependent type theory, which we then test on specific examples. One of the main points of Montague’s work (and thus almost all work on semantics by linguists since the 1970s) is to take exactly this step: here is a famous quote regarding the difference between his approach to expressing natural language statements in logic and the ’naïve’ one, the latter being the one that I feel is being taken when dependent type theory is discussed here on the nForum and at the n-café.

It should be emphasized that this is not a matter of vague intuition, as in elementary logic courses, but an assertion to which we have assigned exact significance.

Regarding Montague’s work, I think the standard reference is to *Formal philosophy*, which contains all of his most important works.

Re #15, what I understand is that the distinction between traditional categorial grammar and type-logical grammar is roughly analogous to the distinction between proof theory and type theory, with the connotation that the latter is supposed to be more general, or at least more flexible. So in categorial grammar you show that sentences are well-formed by building derivations of sequents in little substructural proof systems, whereas in type-logical grammar you do the same by building derivations of typing judgments in little substructural type systems.

The term “type-logical grammar” is newer, I think it might have been introduced by Morrill (1994), drawing inspiration from an older essay by van Benthem (1983) which is said to have revived interest in Lambek’s work by showing how to extract lambda terms as meanings for syntactic derivations. I don’t think the distinction categorial grammar vs type-logical grammar is very rigid, though, and approaches like Philippe de Groote’s abstract categorial grammars blur the distinction.

]]>John #10, thanks. So another thing to explore, whether that work makes contact with Bekki’s ideas. From the reference in #2:

Anaphora and presupposition triggers are represented by @-operators that take the left context that is passed to a dynamic proposition that contains them. The representation for “He whistled” is (13), where the @$_0$ -operator (@$_0 : \gamma_0 \to e)$ is fed its left context $c$ (whose type is underspeciﬁed as $\gamma_0$ ) and returns an entity (of type $e$) whom the pronoun refers to.

(13) $(\lambda c)W((a_0 : \gamma_0 \to e)(c))$

@-operators have the following formation rule (@ F).

$\frac{A : type \;\; A true}{(a_i : A) : A}$The (@ F) rule requires that a certain type ($\gamma_0 \to e$), in the case of (13)) is inhabited, which is the presupposition triggered by the @-operator. There is no introduction or elimination rule for @-operators.

[How does @ work in Latex? I’ve used $a$ in a couple of places.]

]]>I shifted some material on categorial grammar/typelogical grammar from linguistics to the page categorial grammar. Does anyone know how these terms, categorial grammar/typelogical grammar, are related? Synonyms?

]]>Re #9, that sounds like an interesting proposal. I agree that there is excessive focus on limited examples – farmers always seem to be beating their donkeys. If we could nail a piece of, say, Jane Austen, I’d be suitable impressed:

Mr. Collins was not left long to the silent contemplation of his successful love; for Mrs. Bennet, having dawdled about in the vestibule to watch for the end of the conference, no sooner saw Elizabeth open the door and with quick step pass her towards the staircase, than she entered the breakfast-room and congratulated both him and herself in warm terms on the happy prospect of their nearer connection. Mr. Collins received and returned these felicitations with equal pleasure, and then proceeded to relate the particulars of their interview with the result of which he trusted he had every reason to be satisfied, since the refusal which his cousin had steadfastly given him would naturally flow from her bashful modesty and the genuine delicacy of her character.

I’ve started a page Montague grammar. Is there any particular salient piece of writing to indicate there?

]]>Richard #9: in case you are not already familiar with it, you might have a look at Chris Barker and Chung-chieh Shan’s work, and in particular their recent book *Continuations and Natural Language*. Again, their work is not about dependent type theory per se, nor is it expressed in categorical language, but they take one aspect which is implicit in Montague’s analysis of quantification (namely, the concept of continuation semantics) and try to turn that into a general account of many different natural language phenomena.

David #5: a parent page makes sense, perhaps as a section within the linguistics article. I see there’s already a long list of “related concepts” at the bottom of that article, so that could be expanded by interested parties into a more detailed overview.

]]>Rod, #7, yes that seems about right. I hope I did not claim HoTT was used for NLP.

]]>Re: implicit generalization (#2 and #8). In Coq, implicit generalization is basically syntactic sugar. It was mainly implemented by Amokrane Saïbi, and the theory behind it forms chapters 4 and 5 of his thesis. There, he writes (in very rough translation)

The implicit calculus is to be considered an informal language, allowing one to approximate the usual notation of mathematics (and of programming languages), thus avoiding having to write large terms in the explicit calculus. The idea is that… certain information about the type may be omitted and reconstructed by a type-inference algorithm.

So implicit generalization in Coq is not part of the type system, but a feature of the specification language. However, Alexandre Miquel has a paper on including an implicit dependent product alongside the usual pi-types as an extension to the type theory. One interesting feature of this implicit dependent product is the subtyping it allows. I only just found this paper now while poking around online, though, so I don’t know what’s become of the theory.

]]>A comment in passing!

A lot of the work that has been done (by Ranta and others) on the use of dependent type theory in linguistics, very interesting though it is, has a similar feel to me as the discussions that take place on the forum and on the n-café every now and then on this: one picks out pieces of natural language, various themes of the study of syntactics and semantics in linguistics, and offers a suggestion for an expression in dependent type theory, but one does not attempt to pin down a rigorous formal theory of semantics that reasonably captures a fragment (an interesting one, naturally!) of a particular natural language. In this way, I feel that the work of Ranta et al. and that of the discussions here actually differs quite significantly from that which characterises ’semantics’ as a field of study within linguistics, post-Montague.

If I might offer a suggestion, something that would be of great interest to me at least would be to go through some of the pioneering original papers of Montague (or presentations of Montague work in other texts), and try to understand those (in an equally formal and rigorous way) using dependent type theory, Ranta et al’s work, etc. Of course the field of semantics has evolved since then, but there should be still be more than enough to grapple with there.

I am myself interested in, and working on when I find the opportunity, a formal theory of semantics using category theory, but this is of a very different flavour, and takes a different point of departure.

]]>Re: #2, I don’t know. It seems likely to me that most type theorists regard it as part of the “sugar” that a proof assistant adds on top, rather than part of the formal system itself.

]]>As far as I can tell, http://www.grammaticalframework.org/~aarne/gf-hott/ has nothing to do with HOTT or dependent type theory being used in linguistics.

Instead it is about parsing an example English text about HOTT into enough of a logical representation that it can generate the corresponding text in French. The logical representation: http://www.grammaticalframework.org/~aarne/gf-hott/ltestLogic.txt.

While that representation may encode dependent type concepts they are only used as uninterpreted templates for parsing and generation.

GF seems in part to be a kitchen sink geared mainly towards parsing, generation, and translation.

Wikipedia: Grammatical_Framework seems like a good overview. There it is stated there that

]]>Typologically, GF is a functional programming language. Mathematically, it is a type-theoretic formal system (a logical framework to be precise) based on Martin-Löf’s intuitionistic type theory, with additional judgments tailored specifically to the domain of linguistics.

Re #4, Bas could you tell us in a couple of lines what Grammatical Framework is trying to achieve?

]]>They look like interesting links. Thanks for those!

Re organisation of pages, I would quite like to keep the dependent type approach on its own, but I don’t know how much blurring of the lines there is out there.

Do you think there could be a parent page, say, on all logical and category theoretic approaches to natural language? Then would there be a natural division into the different systems?

There’s no doubt material already about on nLab. I see we have categorial grammar. linguistics, context-free grammar.

]]>Added GF-HoTT as a worked example.

]]>Would you like this page to also include references to people trying to use type theory in a broader sense (without necessarily emphasizing the dependent aspect) to understand natural language? If so, we might include a link to Chris Barker and Jim Pryor’s recent seminar at NYU, What Philosophers and Linguists Can Learn From Theoretical Computer Science But Didn’t Know To Ask, and to Oleg Kiselyov and Chung-chieh Shan’s NASSLLI/ESSLLI course Lambda: the ultimate syntax-semantics interface.

]]>The idea of ’implicit generalization’ in Coq that Mike mentioned here, does it have a formalization? I ask since Dependent Type Semantics approach is to extend MLTT with an @-operator, which deals with underspecified contexts, see section 3 of ’Representing Anaphora with Dependent Types’ Springer.

On p. 91 of ’Resolving Modal Anaphora in Dependent Type Semantics’ Springer we even see an aspect of our analysis of ’Have you left of beating your wife?’, where we discussed the presupposition that this used to happen. In this case, somebody stopping smoking is seen to presuppose that they used to smoke.

]]>I thought this should be better developed, and it is. Following the work of Sundholm and Ranta, several people are trying to use dependent type theory to understand natural language. This involves a range of things philosophers care about: anaphora, polysemy, modality, factivity, etc.

It should be interesting to bring this work into contact with the work here on dependent type theory in mathematics and physics. Already I see an overlap in the analysis of modality via a type of worlds, between us here and them in Resolving Modal Anaphora in Dependent Type Semantics on p. 89.

So I’ve started a page dependent type theoretic methods in natural language semantics to list references, and later results.

]]>