nach oben

Journal of Automated Reasoning

Erschienen in:

15.01.2022

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

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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 haben noch keine Lizenz? 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 Wissensvorsprung sichern!

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 Wissensvorsprung sichern!

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 Wissensvorsprung sichern!

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.002MathSciNetCrossRefMATH

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.002MathSciNetCrossRefMATH

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.1683MathSciNetCrossRefMATH

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-7MathSciNetCrossRefMATH

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-9MathSciNetCrossRefMATH

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-4CrossRefMATH

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.321699CrossRefMATH

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-5MathSciNetCrossRefMATH

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/BF01470505MathSciNetCrossRefMATH

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-6MathSciNetCrossRefMATH

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-4MathSciNetCrossRefMATH

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/9781316672815CrossRefMATH

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/1177700153MathSciNetCrossRefMATH

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

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? 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 Formalization of Dedekind Domains and Class Groups of Global Fields

Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

Faster Linear Unification Algorithm

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic

A Formalization of the Smith Normal Form in Higher-Order Logic

Verifying Whiley Programs with Boogie