Монадные вычисления в теоретико-типовой семантике

Олег Анатольевич Доманов

doi:10.47850/RL.2023.4.4.70-81

Авторы

Олег Анатольевич Доманов Институт философии и права СО РАН (г. Новосибирск)

DOI:

https://doi.org/10.47850/RL.2023.4.4.70-81

Ключевые слова:

семантика, естественный язык, теория типов, монады, вычисления, Agda

Аннотация

Монада является теоретико-категорной конструкцией, которую возможно понимать как
абстракцию вычисления [Moggi, 1991]. Это вычисление, результатом которого является не просто вычисляемая
величина, а эта величина с дополнительной структурой. Так понятая, монада успешно применяется в последние
годы в семантике естественного языка в рамках формализма Монтегю. Данная статья посвящена применению
монадных вычислений в теоретико-типовой семантике [Ranta, 1994]. На нескольких примерах демонстрируется
применение монад, а также аппликативных функторов, для учёта различных контекстов, управления порядком
применения кванторов, формализации представления мнений (belief reports). Формализация проводится
в функциональном языке Agda

Биография автора

Олег Анатольевич Доманов, Институт философии и права СО РАН (г. Новосибирск)

кандидат философских наук, доцент, старший научный сотрудник

Библиографические ссылки

Agda Documentation (2023). Available at: https://agda.readthedocs.io/ (Accessed: 10 July 2023).

Asudeh, A. (2014). Monads: Some Linguistic Applications. Available at: http://www.sas.rochester.edu/lin/sites/asudeh/handouts/asudeh-se-lfg13.pdf (Accessed: 10 July 2023).

Asudeh, A. and Giorgolo, G. (2020). Enriched Meanings. Natural Language Semantics with Category Theory. Oxford. OUP. 179 p.

Barker, C. (2002). Continuations and the nature of quantification. Natural Language Semantics. Vol. 10. no. 3. pp. 211-242.

Barker, C. and Shan, C.-c. (2014). Continuations and Natural Language. Oxford. OUP. 230 p.

Luo, Z. (1994). Computation and Reasoning. A Type Theory for Computer Science. Oxford. OUP. 228 p.

Martin-Löf, P. (1984). An Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Napoli. Bibliopolis. 91 p.

Moggi, E. (1991). Notions of computation and monads. Information and Computation. Vol. 93. no. 1. pp. 55-92. DOI: 10.1016/0890-5401(91)90052-4.

Montague, R. (1974). Formal Philosophy. Selected Papers of Richard Montague. Thomason, R. H. (ed.). With an intro. by Thomason, R. H. New Haven and London. Yale University Press. 369 p.

Norell, U. (2009). Dependently Typed Programming in Agda. In Koopman, P., Plasmeijer, R., and Swierstra, D. (eds.). Advanced Functional Programming: 6th International School, AFP 2008. Berlin, Heidelberg. Springer-Verlag. pp. 230-266. DOI: 10.1007/978-3-642-04652-0_5.

Ranta, A. (1994). Type-theoretical grammar. Clarendon Press. 226 p.

Wadler, P. L. (1994). Monads and composable continuations. Lisp and Symbolic Computation. Vol. 7. no. 1. pp. 39-56.