Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: dependent type theoretic methods in natural language semantics

Bottom of Page

1 to 26 of 26

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 28th 2015
    • (edited Oct 28th 2015)

    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.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 28th 2015
    • (edited Oct 28th 2015)

    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.

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

    • CommentRowNumber4.
    • CommentAuthorspitters
    • CommentTimeOct 29th 2015

    Added GF-HoTT as a worked example.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 29th 2015

    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.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 29th 2015

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

    • CommentRowNumber7.
    • CommentAuthorRodMcGuire
    • CommentTimeOct 29th 2015

    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.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeOct 29th 2015

    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.

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

    • CommentRowNumber10.
    • CommentAuthorJohn Dougherty
    • CommentTimeOct 30th 2015

    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.

    • CommentRowNumber11.
    • CommentAuthorspitters
    • CommentTimeOct 30th 2015

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

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

    • CommentRowNumber13.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeOct 30th 2015
    • (edited Oct 30th 2015)

    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.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 30th 2015

    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?

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 30th 2015

    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?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 30th 2015
    • (edited Oct 31st 2015)

    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_0 -operator (@0:γ 0→e)_0 : \gamma_0 \to e) is fed its left context cc (whose type is underspecified as γ 0\gamma_0 ) and returns an entity (of type ee) whom the pronoun refers to.

    (13) (λc)W((a 0:γ 0→e)(c))(\lambda c)W((a_0 : \gamma_0 \to e)(c))

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

    A:typeAtrue(a i:A):A\frac{A : type \;\; A true}{(a_i : A) : A}

    The (@ F) rule requires that a certain type (γ 0→e\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 aa in a couple of places.]

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

    • CommentRowNumber18.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 20th 2016
    • (edited Feb 20th 2016)

    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.

    • CommentRowNumber19.
    • CommentAuthorspitters
    • CommentTimeMay 26th 2017

    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.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 26th 2017

    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?

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2019

    I added some history.

    diff, v15, current

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2019

    Why are the links on this page not working to Göran Sundholm​?

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2019

    Maybe there is a unicode ambiguity in the background, as with the hyphen bug.

    In any case, I have now managed to “fix” the problem by giving Göran Sundholm​ a redirect which is a literal copy of the entry title, but with the Umlaut instead copy-and-pasted from Per Martin-Löf.

    While this makes no visually discernible difference, now the link from your entry works! and so I guess that the copy-and-pasting served to replace the unicode for the Umlaut.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2019

    Thanks!

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 9th 2019

    I’ll take some credit for the suggestion.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2019
    • (edited Dec 10th 2019)

    Er…

1 to 26 of 26

  1.