On Type-Theoretical Formalization of Situation Semantics
DOI:
https://doi.org/10.47850/RL.2021.2.3.32-41Keywords:
situation semantics, type theory, functional languagesAbstract
Situation semantics is an effective instrument for analysing semantical aspects of natural languages with
explicit dependence on contexts, like referential opacity of belief contexts etc. Making use of type-theoretical approaches not
only makes its formalism more practical in many ways, but also facilitates its migration to computer systems, specifically, the
formalization in functional programming languages. The article deals with a prototype of the type theoretical language of
situation semantics, implemented on the basis of the language Racket. It decribes principal approaches, methods of solving
some problems of formal semantics as well as issues that need to be addressed.
References
Barwise, J. and Perry, J. (1983). Situations and Attitudes. MIT Press.
Bertot, Y. and Castéran, P. (2004). Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. XXV, 472 p. DOI: 10.1007/978-3-662-07964-5.
Cooper, R. (2005). Austinian Truth, Attitudes and Type Theory. Research on Language and Computation. Vol. 3. no. 2. pp. 333-362. DOI: 10.1007/s11168-006-0002-z.
Cooper, R. (2017). Adapting Type Theory with Records for Natural Language Semantics. In Chatzikyriakidis, S. and Luo, Z. (eds.). Modern Perspectives in Type-Theoretical Semantics. Studies in Linguistics and Philosophy 98. Springer International Publishing. pp. 71-94. DOI: 10.1007/978-3-319-
-3_4.
Cooper, R. and Ginzburg, J. (2015). Type Theory with Records for Natural Language Semantics. In Lappin, S. and Fox, C. (eds.). The Handbook of Contemporary Semantic Theory. Blackwell Handbooks in Linguistics. Wiley. pp. 376-407. DOI: 10.1002/9781118882139.ch12.
Lambek, J. and Scott, P. J. (1986). Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics 7. Cambridge. Cambridge University Press.
Martin-Löf, P. (1987). Truth of a Proposition, Evidence of a Judgement, Validity of a Proof. Synthese. Vol. 73. pp. 407-420. DOI: 10.1007/BF00484985.
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, Heijen, The Netherlands, May 2008, Revised Lectures. Lecture Notes in Computer Science 5832 : Theoretical Computer
Science and General Issues. Berlin, Heidelberg. Springer-Verlag Berlin Heidelberg. pp. 230-266. DOI: 10.1007/978-3-642-04652-0_5.
Paulin-Mohring, C. (2015). Introduction to the Calculus of Inductive Constructions. In Paleo, B. W. and Delahaye, D. (eds.). All about Proofs, Proofs for All. Studies in Logic (Mathematical logic and foundations) 55. [Online]. Available at: https://hal.inria.fr/hal-01094195 (Accessed: 30 July 2021).
Pierce, B. C. (2002). Types and Programming Languages. Cambridge. The MIT Press. 648 p.
Quine, W. V. O. (1956). Quantifiers and Propositional Attitudes. Journal of Philosophy. Vol. 53. no. 5. pp. 177-187.
Ranta, A. (1994). Type-theoretical grammar. Indices 1. Clarendon Press. 226 p.
Ranta, A. (2011). Grammatical Framework. Programming with Multilingual Grammars. CSLI studies in computational linguistics. CSLI Publications, Center for the Study of Language and Information. XII, 331 p.
Rossberg, A. (Aug. 2015). 1ML – core and modules united (F-ing first-class modules). ACM SIGPLAN Notices. Vol. 50. pp. 35-47. DOI: 10.1145/2858949.2784738.
Salmon, N. U. (1986). Frege’s Puzzle. Cambridge, Mass. Bradford Books/The MIT Press. 195 p.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
https://oc.philosophy.nsc.ru/remote.php/webdav/%D0%94%D0%BE%D0%B3%D0%BE%D0%B2%D0%BE%D1%80%20%D1%81%20%D0%B0%D0%B2%D1%82%D0%BE%D1%80%D0%BE%D0%BC%20RL-%D0%BF%D1%80%D0%B0%D0%B2.doc
