Abstract
Ambiguous notation is a powerful tool developed to deal with the complexity of mathematics without sacrificing clarity or conciseness. In the mechanized parsing of ambiguous terms, a disambiguation algorithm can be used to provide the system with the intelligence necessary to select valid interpretations for the overloaded symbols received in input.
Disambiguation works by means of an incremental analysis of the input term, progressively discarding all invalid interpretations. As a result, if the input term cannot be disambiguated, many errors will be produced, only a handful of which are truly meaningful to the user.
In this paper, we improve the existing technique to classify disambiguation errors by introducing a new heuristic to sort errors from the most meaningful to the least, showing that it can be implemented in a natural way in the existing disambiguation algorithm. We also describe a neat interface to present disambiguation errors to the user, suitable for the use in interactive theorem proving applications.
The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.
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
Preview
Unable to display preview. Download preview PDF.
References
Asperti, A., Ricciotti, W.: A Web Interface for Matita. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 417–421. Springer, Heidelberg (2012)
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: A bi-directional refinement algorithm for the calculus of (co)inductive constructions. LMCS 8(1) (2012)
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011)
Geuvers, H., Jojgov, G.I.: Open Proofs and Open Terms: A Basis for Interactive Logic. In: Bradfield, J.C. (ed.) CSL 2002. LNCS, vol. 2471, pp. 537–552. Springer, Heidelberg (2002)
Hage, J., Heeren, B.: Heuristics for Type Error Discovery and Recovery. In: Horváth, Z., Zsók, V., Butterfield, A. (eds.) IFL 2006. LNCS, vol. 4449, pp. 199–216. Springer, Heidelberg (2007)
Jun, Y., Michaelson, G., Trinder, P.: Explaining polymorphic types. Comput. J. 45(4), 436–452 (2002)
Muñoz, C.: A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory. PhD thesis, INRIA (November 1997)
Rittri, M.: Finding the source of type errors interactively. Technical report, Department of Computer Science, Chalmers University of Technology, Sweden (1993)
Sacerdoti Coen, C., Zacchiroli, S.: Efficient Ambiguous Parsing of Mathematical Formulae. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 347–362. Springer, Heidelberg (2004)
Sacerdoti Coen, C., Zacchiroli, S.: Spurious disambiguation errors and how to get rid of them. Journal of Mathematics in Computer Science, Special Issue on MKM 2, 355–378 (2008)
Stuckey, P.J., Sulzmann, M., Wazny, J.: Improving type error diagnosis. In: Proceedings of 2004 ACM SIGPLAN Haskell Workshop, Haskell 2004, pp. 80–91. ACM, New York (2004)
Wenzel, M.: Type Classes and Overloading in Higher-Order Logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997)
Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asperti, A., Ricciotti, W. (2012). Rating Disambiguation Errors. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-35308-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35307-9
Online ISBN: 978-3-642-35308-6
eBook Packages: Computer ScienceComputer Science (R0)