A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. (English) Zbl 1512.05165
Summary: R. Aharoni et al. [J. Comb. Theory, Ser. B 101, No. 1, 1–17 (2011; Zbl 1221.05186)] proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a flow and a cut such that the flow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source and the sink is finite. This proof is based on the max-flow min-cut theorem for finite networks. As a use case, we formalize a characterization theorem for relation lifting on discrete probability distributions and two of its applications.
MSC:
| 05C21 | Flows in graphs |
| 05C63 | Infinite graphs |
| 60E05 | Probability distributions: general theory |
| 68V20 | Formalization of mathematics in connection with theorem provers |
Citations:
Zbl 1221.05186Software:
Transfer; Zoo Probabilistic Systems; MFMC_Countable; Isabelle/HOL; Archive Formal Proofs; Probabilistic_While; Lifting; Edmonds-Karp; LocalesReferences:
| [1] | Aharoni, R.: Menger’s theorem for graphs containing no infinite paths. Eur. J. Comb. 4, 201-204 (1983). doi:10.1016/S0195-6698(83)80012-2 · Zbl 0525.05043 |
| [2] | Aharoni, R., Berger, E.: Menger’s theorem for infinite graphs. Invent. Math. 176(1), 1-62 (2009). doi:10.1007/s00222-008-0157-3 · Zbl 1216.05092 |
| [3] | Aharoni, R.; Berger, E.; Georgakopoulos, A.; Perlstein, A.; Sprüssel, P., The max-flow min-cut theorem for countable networks, J. Combinat. Theory, Ser. B, 101, 1-17 (2010) · Zbl 1221.05186 · doi:10.1016/j.jctb.2010.08.002 |
| [4] | Audebaud, P.; Paulin-Mohring, C., Proofs of randomized algorithms in Coq, Sci. Comput. Program., 74, 568-589 (2009) · Zbl 1178.68667 · doi:10.1016/j.scico.2007.09.002 |
| [5] | Baier, C.; Engelen, B.; Majster-Cederbaum, M., Deciding bisimilarity and similarity for probabilistic processes, J. Comput. Syst. Sci., 60, 1, 187-231 (2000) · Zbl 1073.68690 · doi:10.1006/jcss.1999.1683 |
| [6] | Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani F. (Eds.) TYPES 2003, LNCS, vol. 3085, pp. 34-50. Springer (2004). doi: doi:10.1007/978-3-540-24849-13 · Zbl 1100.68615 |
| [7] | Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 123-153 (2014) · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7 |
| [8] | Ballarin, C., Exploring the structure of an algebra text with locales, J. Autom. Reason., 64, 1093-1121 (2020) · Zbl 1468.68277 · doi:10.1007/s10817-019-09537-9 |
| [9] | Barthe, G., Espitau, T., Hsu, J., Sato, T., Strub, P.Y.: *-liftings for differential privacy. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl A. (Eds.) ICALP 2017, LIPIcs, vol. 80, pp. 102:1-102:12. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). doi: doi:10.4230/LIPIcs.ICALP.2017.102 · Zbl 1442.68100 |
| [10] | Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal Certification of Code-based Cryptographic Proofs. In: POPL 2009, pp. 90-101. ACM (2009). doi:10.1145/1480881.1480894 · Zbl 1315.68081 |
| [11] | Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: ITP 2014, LNCS, vol. 8558, pp. 93-110. Springer (2014). doi: doi:10.1007/978-3-319-08970-67 · Zbl 1416.68151 |
| [12] | Bourbaki, N., Sur le théorème de Zorn, Arch. Math., 2, 6, 434-437 (1949) · Zbl 0045.32902 · doi:10.1007/BF02036949 |
| [13] | Deng, Y., Semantics of Probabilistic Processes (2014), Berlin: Springer, Berlin · Zbl 1315.68002 · doi:10.1007/978-3-662-45198-4 |
| [14] | Desharnais, J.: Labelled Markov Processes. Ph.D. Thesis, McGill University (1999) |
| [15] | Edmonds, J.; Karp, RM, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM, 19, 2, 248-264 (1972) · Zbl 0318.90024 · doi:10.1145/321694.321699 |
| [16] | Ford, LR; Fulkerson, DR, Maximal flow through a network, Can. J. Math., 8, 399-404 (1956) · Zbl 0073.40203 · doi:10.4153/CJM-1956-045-5 |
| [17] | Hölzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang X. (Eds.) ITP 2015, LNCS, vol. 9236, pp. 203-220. Springer (2015). doi: doi:10.1007/978-3-319-22102-113 · Zbl 1465.68199 |
| [18] | Huffman, B., Kunčar, O.: Lifting and Transfer: A modular design for quotients in Isabelle/HOL. In: CPP 2013, LNCS, vol. 8307, pp. 131-146. Springer (2013). doi: doi:10.1007/978-3-319-03545-19 · Zbl 1426.68284 |
| [19] | Immler, F.: Generic construction of probability spaces for paths of stochastic processes in Isabelle/HOL. Master’s thesis, Fakultät für Informatik, Technische Universität München (2012) |
| [20] | Kellerer, HG, Funktionen auf Produkträumen mit vorgegebenen Marginal-Funktionen, Math. Ann., 144, 323-344 (1961) · Zbl 0129.03402 · doi:10.1007/BF01470505 |
| [21] | Kunčar, O.; Popescu, A., From types to sets by local type definition in higher-order logic, J. Autom. Reason., 62, 237-260 (2019) · Zbl 1468.68295 · doi:10.1007/s10817-018-9464-6 |
| [22] | Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: J.C. Blanchette, S. Merz (eds.) ITP 2016, LNCS, vol. 9807, pp. 219-234. Springer (2016). doi: doi:10.1007/978-3-319-43144-414 · Zbl 1468.68327 |
| [23] | Lammich, P.; Sefidgar, SR, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, J. Autom. Reason., 62, 261-280 (2019) · Zbl 1468.68328 · doi:10.1007/s10817-017-9442-4 |
| [24] | Lee, G.: Correctnesss of Ford-Fulkerson’s maximum flow algorithm. Formal. Math. 13(2), 305-314 (2005). https://fm.mizar.org/2005-13/pdf13-2/glib_005.pdf |
| [25] | Lochbihler, A.: A formal proof of the max-flow min-cut theorem for countable networks. Archive of Formal Proofs (2016). http://www.isa-afp.org/entries/MFMC_Countable.shtml, Formal proof development · Zbl 07699442 |
| [26] | Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher-order logic. In: P. Thiemann (ed.) ESOP 2016, LNCS, vol. 9632, pp. 503-531. Springer (2016). doi: doi:10.1007/978-3-662-49498-120 · Zbl 1335.68033 |
| [27] | Lochbihler, A.: Probabilistic while loop. Archive of Formal Proofs (2017). https://isa-afp.org/entries/Probabilistic_While.html, Formal proof development |
| [28] | Lochbihler, A.: A mechanized proof of the max-flow min-cut theorem for countable networks. In: Cohen, L., Kaliszyk C. (Eds.) ITP 2021, LIPIcs, vol. 193, pp. 25:1-25:18 (2021). doi: doi:10.4230/LIPIcs.ITP.2021.25 · Zbl 07699442 |
| [29] | Lochbihler, A.: A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. http://www.andreas-lochbihler.de/pub/lochbihler-mfmc.pdf (2021) · Zbl 07699442 |
| [30] | Lyons, R.; Peres, Y., Probability on Trees and Networks (2017), New York: Cambridge University Press, New York · Zbl 1376.05002 · doi:10.1017/9781316672815 |
| [31] | Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Grundy, J., Newey M. (Eds.) TPHOLs 1998, LNCS, vol. 1479, pp. 349-366. Springer (1998). doi: doi:10.1007/BFb0055146 · Zbl 0927.03026 |
| [32] | Sabot, C., Tournier, L.: Random walks in Dirichlet environment: an overview. Annales de la Faculté des sciences de Toulouse: Mathématiques Ser. 6, 26(2), 463-509 (2017). doi: doi:10.5802/afst.1542 · Zbl 1369.60074 |
| [33] | Sack, J., Zhang, L.: A general framework for probabilistic characterizing formulae. In: Kuncak, V., Rybalchenko, A. (Eds.) VMCAI 2012, LNCS, vol. 7148, pp. 396-411. Springer (2012). doi: doi:10.1007/978-3-642-27940-926 · Zbl 1326.68176 |
| [34] | Smolka, G., Schäfer, S., Doczkal, C.: Transfinite constructions in classical type theory. In: Urban, C., Zhang, X., (Eds.) ITP 2015, LNCS, vol. 9236, pp. 391-404. Springer (2015). doi: doi:10.1007/978-3-319-22102-126 · Zbl 1465.03057 |
| [35] | Strassen, V., The existence of probability measures with given marginals, Ann. Math. Stat., 36, 2, 423-439 (1965) · Zbl 0135.18701 · doi:10.1214/aoms/1177700153 |
| [36] | Wiedijk, F.: The de Bruijn factor. https://www.cs.ru.nl/ freek/factor/factor.pdf (2000) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
