Abstract
In this paper, we present an extension to Martin-Löf’s Intuitionistic Type Theory which gives natural solutions to problems in pragmatics, such as pronominal reference and presupposition. Our approach also gives a simple account of donkey anaphora without resorting to exotic scope extension of the sort used in Discourse Representation Theory and Dynamic Semantics, thanks to the proof-relevant nature of type theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In this paper, we opt to use the notation (x: A) × B and (x: A) → B in place of the more common \(\Sigma x: A.B\) and \(\Pi x: A.B\), respectively, in order to emphasize that these are merely dependent versions of pairs and functions. This notation was first invented in the Nuprl System (Constable et al. 1986).
- 2.
From a formalistic perspective, the elaboration is all that is needed to justify the rule.
References
Allen, S., Bickford, M., Constable, R., Eaton, R., Kreitz, C., Lorigo, L., Moran, E.: Innovations in computational type theory using Nuprl. J. Appl. Log. 4(4), 428–469 (2006). Towards Computer Aided Mathematics
Bekki, D.: Representing anaphora with dependent types. In: Asher, N., Soloviev, S. (eds.) Logical Aspects of Computational Linguistics. Lecture Notes in Computer Science, vol. 8535, pp. 14–29. Springer, Berlin/Heidelberg (2014)
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986)
Coquand, T., Jaber, G.: A computational interpretation of forcing in type theory. In: Dybjer, P., Lindström, S., Palmgren, E., Sundholm, G. (eds.) Epistemology Versus Ontology, Logic, Epistemology, and the Unity of Science, vol. 27, pp. 203–213. Springer, Dordrecht (2012)
Devriese, D., Piessens, F.: On the bright side of type classes: instance arguments in Agda. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP’11, pp. 143–155. ACM, New York (2011)
Harper, R., Licata, D.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4–5), 613–673 (2007)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)
Howe, D.: On computational open-endedness in Martin-Löf’s type theory. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science (LICS’91), Amsterdam, pp. 162–172 (1991)
Marlow, S.: Haskell 2010 Language Report (2010). https://www.haskell.org/definition/ haskell2010.pdf
Martin-Löf, P.: Constructive mathematics and computer programming. In: Cohen, L.J., Łoś, J., Pfeiffer, H., Podewski, K.P. (eds.) Logic, Methodology and Philosophy of Science VI. Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979. Studies in Logic and the Foundations of Mathematics, vol. 104, pp. 153–175. North-Holland (1982)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)
Martin-Löf, P.: Analytic and synthetic judgements in type theory. In: Parrini, P. (ed.) Kant and Contemporary Epistemology. The University of Western Ontario Series in Philosophy of Science, vol. 54, pp. 87–99. Springer, Dordrecht (1994)
Martin-Löf, P.: On the meanings of the logical constants and the justifications of the logical laws. Nord. J. Philos. Log. 1(1), 11–60 (1996)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Trans. Comput. Log. 9(3), 23:1–23:49 (2008)
Pfenning, F.: Logical frameworks—a brief introduction. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliability. NATO Science Series, vol. 62, pp. 137–166. Springer, Dordrecht (2002)
Rahli, V., Bickford, M.: A nominal exploration of intuitionism. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (2016)
Ranta, A.: Type-Theoretical Grammar. Oxford University Press, Oxford (1994)
Sundholm, G.: Proof theory and meaning. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic. Synthese Library, vol. 166, pp. 471–506. Springer, Dordrecht (1986)
Sundholm, G.: Constructive recursive functions, Church’s thesis, and Brouwer’s theory of the creating subject: afterthoughts on a parisian joint session. In: Dubucs, J., Bourdeau, M. (eds.) Constructivity and Computability in Historical and Philosophical Perspective, Logic, Epistemology, and the Unity of Science, vol. 34, pp. 1–35. Springer, Dordrecht (2014)
van Atten, M.: Brouwer Meets Husserl: On the Phenomenology of Choice Sequences. Springer, Dordrecht (2007)
Acknowledgements
The second author thanks Mark Bickford, Bob Harper and Bob Constable for illuminating discussions on choice sequences, Church’s Thesis, and computational open-endedness. We thank our reviewers for their constructive feedback and references to related work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
McAdams, D., Sterling, J. (2016). Dependent Types for Pragmatics. In: Redmond, J., Pombo Martins, O., Nepomuceno Fernández, Á. (eds) Epistemology, Knowledge and the Impact of Interaction. Logic, Epistemology, and the Unity of Science, vol 38. Springer, Cham. https://doi.org/10.1007/978-3-319-26506-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-26506-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26504-9
Online ISBN: 978-3-319-26506-3
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)