Abstract
Convex sets appear in various mathematical theories, and are used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets in vector spaces, we formalize in Coq an intrinsic axiomatization of convex sets, namely convex spaces, based on an operation taking barycenters of points. A convex space corresponds to a specific type that does not refer to a surrounding vector space. This simplifies the definitions of functions on it. We show applications including the convexity of information-theoretic functions defined over types of distributions. We also show how convex spaces are embedded in conical spaces, which are abstract real cones, and use the embedding as an effective device to ease calculations.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The support of a probability distribution d is the set \(\{i \mid d_i > 0\}\).
- 2.
This way of restricting the domain of functions in their properties rather than in the definitions is a design choice often found in Coq. It makes it possible for functions such as the logarithm to be composable without being careful about their domains and ranges, and leads to a clean separation between definitions and properties of functions in the formalization.
References
Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11(1), 43–76 (2018)
Affeldt, R., Garrigue, J., Nowak, D., Saikawa, T.: A trustful monad for axiomatic reasoning with probability and nondeterminism, March 2020, https://arxiv.org/abs/2003.09993
Affeldt, R., et al.: Monadic equational reasoning in Coq (2019). https://github.com/affeldt-aist/monae/, Coq scripts
Affeldt, R., Garrigue, J., Saikawa, T.: Examples of formal proofs about data compression. In: International Symposium on Information Theory and Its Applications (ISITA 2018), Singapore, 28–31 October 2018, pp. 665–669. IEICE, IEEE Xplore, October 2018
Affeldt, R., Garrigue, J., Saikawa, T.: Reasoning with conditional probabilities and joint distributions in Coq. Computer Software (2020, to appear). Japan Society for Software Science and Technology. https://staff.aist.go.jp/reynald.affeldt/documents/cproba_preprint.pdf
Affeldt, R., Hagiwara, M., Sénizergues, J.: Formalization of Shannon’s theorems. J. Autom. Reason. 53(1), 63–103 (2014)
Affeldt, R., Nowak, D., Saikawa, T.: A hierarchy of monadic effects for program verification using equational reasoning. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 226–254. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33636-3_9
Beaulieu, G.: Probabilistic completion of nondeterministic models. Ph.D. thesis, University of Ottawa (2008)
Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_11
Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 85, pp. 23:1–23:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https://doi.org/10.4230/LIPIcs.CONCUR.2017.23
Cheung, K.H.: Distributive interaction of algebraic effects. Ph.D. thesis, University of Oxford (2017)
Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. Wiley, Hoboken (2006)
Flood, J.: Semiconvex geometry. J. Aust. Math. Soc. 30(4), 496–510 (1981). https://doi.org/10.1017/S1446788700017973
Fritz, T.: Convex spaces I: Definition and examples (2015). https://arxiv.org/abs/0903.5522, First version: 2009
Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_23
van Heerdt, G., Hsu, J., Ouaknine, J., Silva, A.: Convex language semantics for nondeterministic probabilistic automata. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 472–492. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02508-3_25
Infotheo: A Coq formalization of information theory and linear error-correcting codes (2020). https://github.com/affeldt-aist/infotheo/, Coq scripts
Infotheo: probability/convex_choice.v. In: [17] (2020), Coq scripts
Jacobs, B.: Convexity, duality and effects. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 1–19. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15240-5_1
Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp. 186–195, June 1989. https://doi.org/10.1109/LICS.1989.39173
Keimel, K., Plotkin, G.: Mixed powerdomains for probability and nondeterminism. Log. Meth. Comput. Sci. 13, December 2016. https://doi.org/10.23638/LMCS-13(1:2)2017
Keimel, K., Plotkin, G.D.: Predicate transformers for extended probability and non-determinism. Math. Struct. Comput. Sci. 19(3), 501–539 (2009). https://doi.org/10.1017/S0960129509007555
Kirch, O.: Bereiche und Bewertungen. Master’s thesis, Technischen Hochschule Darmstadt (1993)
Mahboubi, A., Tassi, E.: Canonical structures for the working coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19–34. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_5
Neumann, W.D.: On the quasivariety of convex subsets of affine spaces. Archiv der Mathematik 21, 11–16 (1970)
Semadini, Z.: Banach Spaces of Continuous Functions. PWN (1971)
Stone, M.H.: Postulates for the barycentric calculus. Ann. Mat. Pura Appl. 29(1), 25–30 (1949)
Świrszcz, T.: Monadic functors and convexity. Bulletin de l’Académie polonaise des sciences. Série des sciences mathématiques, astronomiques et physiques 22(1) (1974)
The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2019). https://coq.inria.fr. Version 8.11.0
Tix, R., Keimel, K., Plotkin, G.: Semantic domains for combining probability and non-determinism. Electron. Notes Theor. Comput. Sci. 222, 3–99 (2009). https://doi.org/10.1016/j.entcs.2009.01.002
Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87–113 (2006)
Acknowledgments
We acknowledge the support of the JSPS KAKENHI Grant Number 18H03204. We also thank Shinya Katsumata for his comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Affeldt, R., Garrigue, J., Saikawa, T. (2020). Formal Adventures in Convex and Conical Spaces. In: Benzmüller, C., Miller, B. (eds) Intelligent Computer Mathematics. CICM 2020. Lecture Notes in Computer Science(), vol 12236. Springer, Cham. https://doi.org/10.1007/978-3-030-53518-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-53518-6_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-53517-9
Online ISBN: 978-3-030-53518-6
eBook Packages: Computer ScienceComputer Science (R0)