nach oben

Tipp

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory

verfasst von: Andreas Lochbihler

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen, um Zugang zu erhalten

Abstract

Aharoni et al. (J Combinat Theory, Ser B 101:1–17, 2010) 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.

Vorheriger Artikel A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Nächster Artikel A Formalization of Dedekind Domains and Class Groups of Global Fields

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

The record package achieves extensibility with structural subtyping by internally generalizing \(\alpha \ \textsf {graph}\) to \((\alpha , \beta )\ \textsf {graph-scheme}\), where \(\beta \) is the extension slot for further fields. For example, \(\beta \) is instantiated with the singleton type \(\textsf {unit}\) for \(\textsf {graph}\). All operations on \(\textsf {graph}\) are actually defined on \(\textsf {graph-scheme}\) so that they also work for all record extensions. We omit this technicality from the presentation.

Sack and Zhang set \(e_{i,j} = \infty \) if \(x_i \mathrel {R} y_j\), but the max-flow min-cut theorem handles only finite edge capacities. Their argument works unchanged for any value greater than 1, such as our choice of 2.

Sack and Zhang’s proof is formalized in the theory Rel_PMF_Characterisation in the accompanying AFP entry [25] version for Isabelle2016-1. The modified proof can be found in the theory Rel_PMF_Characterisation_MFMC in the version for Isabelle2021-1 of the same AFP entry.

Aharoni, R.: Menger’s theorem for graphs containing no infinite paths. Eur. J. Comb. 4, 201–204 (1983). https://doi.org/10.1016/S0195-6698(83)80012-2

Aharoni, R., Berger, E.: Menger’s theorem for infinite graphs. Invent. Math. 176(1), 1–62 (2009). https://doi.org/10.1007/s00222-008-0157-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). https://doi.org/10.1016/j.jctb.2010.08.002 MathSciNetCrossRefMATH

Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74, 568–589 (2009). https://doi.org/10.1016/j.scico.2007.09.002 MathSciNetCrossRefMATH

Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000). https://doi.org/10.1006/jcss.1999.1683 MathSciNetCrossRefMATH

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: https://doi.org/10.1007/978-3-540-24849-13

Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52, 123–153 (2014). https://doi.org/10.1007/s10817-013-9284-7 MathSciNetCrossRefMATH

Ballarin, C.: Exploring the structure of an algebra text with locales. J. Autom. Reason. 64, 1093–1121 (2020). https://doi.org/10.1007/s10817-019-09537-9 MathSciNetCrossRefMATH

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: https://doi.org/10.4230/LIPIcs.ICALP.2017.102

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). https://doi.org/10.1145/1480881.1480894

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: https://doi.org/10.1007/978-3-319-08970-67

12.

Bourbaki, N.: Sur le théorème de Zorn. Arch. Math. 2(6), 434–437 (1949) MathSciNetCrossRefMATH

13.

Deng, Y.: Semantics of Probabilistic Processes. Springer, Berlin (2014). https://doi.org/10.1007/978-3-662-45198-4 CrossRefMATH

14.

Desharnais, J.: Labelled Markov Processes. Ph.D. Thesis, McGill University (1999)

15.

Edmonds, J., Karp, R.M.: Theoretical improvements in algorithmic efficiency for network flow problems. J. ACM 19(2), 248–264 (1972). https://doi.org/10.1145/321694.321699 CrossRefMATH

16.

Ford, L.R., Fulkerson, D.R.: Maximal flow through a network. Can. J. Math. 8, 399–404 (1956). https://doi.org/10.4153/CJM-1956-045-5 MathSciNetCrossRefMATH

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: https://doi.org/10.1007/978-3-319-22102-113

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: https://doi.org/10.1007/978-3-319-03545-19

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, H.G.: Funktionen auf Produkträumen mit vorgegebenen Marginal-Funktionen. Math. Ann. 144, 323–344 (1961). https://doi.org/10.1007/BF01470505 MathSciNetCrossRefMATH

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). https://doi.org/10.1007/s10817-018-9464-6 MathSciNetCrossRefMATH

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: https://doi.org/10.1007/978-3-319-43144-414

23.

Lammich, P., Sefidgar, S.R.: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. J. Autom. Reason. 62, 261–280 (2019). https://doi.org/10.1007/s10817-017-9442-4 MathSciNetCrossRefMATH

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

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: https://doi.org/10.1007/978-3-662-49498-120

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: https://doi.org/10.4230/LIPIcs.ITP.2021.25

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)

30.

Lyons, R., Peres, Y.: Probability on Trees and Networks. Cambridge University Press, New York (2017). https://doi.org/10.1017/9781316672815 CrossRefMATH

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: https://doi.org/10.1007/BFb0055146

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: https://doi.org/10.5802/afst.1542

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: https://doi.org/10.1007/978-3-642-27940-926

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: https://doi.org/10.1007/978-3-319-22102-126

35.

Strassen, V.: The existence of probability measures with given marginals. Ann. Math. Stat. 36(2), 423–439 (1965). https://doi.org/10.1214/aoms/1177700153 MathSciNetCrossRefMATH

36.

Wiedijk, F.: The de Bruijn factor. https://www.cs.ru.nl/~freek/factor/factor.pdf (2000)

Titel: A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory
verfasst von: Andreas Lochbihler
Publikationsdatum: 15.01.2022
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-022-09616-4

Fachgebiete

Bücher

Zeitschriften

Weitere Formate

Jetzt Einzelzugang starten

Zugang für Unternehmen beantragen

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Fachgebiete Chevron down icon Chevron up icon

Bücher

Zeitschriften

Weitere Formate Chevron down icon Chevron up icon

Jetzt Einzelzugang starten

Zugang für Unternehmen beantragen

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2022

A Comprehensive Framework for Saturation Theorem Proving

From Specification to Testing: Semantics Engineering for Lua 5.2

Formalization of the Computational Theory of a Turing Complete Functional Language Model

A Formalization of Dedekind Domains and Class Groups of Global Fields

Tuple Interpretations for Termination of Term Rewriting

Theorem Proving as Constraint Solving with Coherent Logic

Premium Partner

Fachgebiete

Weitere Formate