Abstract
We present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators, \(B|_{A}\) (restriction, a strengthening of implication) and \({\mathbf {\downdownarrows }}(B)\) (total concurrency). The source of the extraction are formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy’s amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb.
Chapter PDF
Similar content being viewed by others
References
Abramsky, S.: Proofs as processes. Theoretical Computer Science 135(1), 5–9 (Apr 1992). https://doi.org/10.1016/0304-3975(94)00103-0
Apt, K., Olderog, E.: Fifty years of Hoare’s logic. Formal Aspects of Computing 31, 751 – 807 (2019). https://doi.org/10.1007/s00165-019-00501-3
Berger, U.: CFP (concurrent fixed point logic) repository, https://github.com/ujberger/cfp
Berger, U.: From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods in Comput. Sci. 7(1), 1–24 (2011). https://doi.org/10.2168/LMCS-7(1:8)2011
Berger, U.: Extracting Non-Deterministic Concurrent Programs. In: Talbot, J.M., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, pp. 26:1–26:21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2016). https://doi.org/10.4230/LIPIcs.CSL.2016.26
Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M.: Minlog - a tool for program extraction for supporting algebra and coalgebra. In: CALCO-Tools. Lecture Notes in Computer Science, vol. 6859, pp. 393–399. Springer (2011). https://doi.org/10.1007/978-3-642-22944-2_29
Berger, U., Petrovska, O.: Optimized program extraction for induction and coinduction. In: CiE 2018: Sailing Routes in the World of Computation. LNCS, vol. 10936, pp. 70–80. Springer Verlag, Berlin, Heidelberg, New York (2018). https://doi.org/10.1007/978-3-319-94418-0_7
Berger, U., Petrovska, O., Tsuiki, H.: Prawf: An interactive proof system for program extraction. In: Anselmo, M., Vedova, G., Manea, F., Pauly, A. (eds.) Beyond the Horizon of Computability - 16th Conference on Computability in Europe, CiE 2020. Lecture Notes in Computer Science, vol. 12098, pp. 137–148. Springer (2020). https://doi.org/10.1007/978-3-030-51466-2_12
Berger, U., Seisenberger, M.: Proofs, programs, processes. Theory of Computing Systems 51(3), 213–329 (2012). https://doi.org/10.1007/s00224-011-9325-8
Berger, U., Seisenberger, M., Spreen, D., Tsuiki, H.: Concurrent Gaussian elimination. To appear (2022)
Berger, U., Tsuiki, H.: Extracting total amb programs from proofs (2021), https://arxiv.org/abs/2104.14669
Berger, U., Tsuiki, H.: Intuitionistic fixed point logic. Annals of Pure and Applied Logic 172(3), 102903 (2021). https://doi.org/10.1016/j.apal.2020.102903
Brookes, S.: A semantics for concurrent separation logic. Theoretical Computer Science 375, 227–370 (2007). https://doi.org/10.1016/j.tcs.2006.12.034
Broy, M.: A theory for nondeterminism, parallelism, communication, and concurrency. Theoretical Computer Science 45, 1 – 61 (1986). https://doi.org/10.1016/0304-3975(86)90040-X
Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Mathematical Structures in Computer Science 26, 367–423 (2016). https://doi.org/10.1017/S0960129514000218
Carayol, A., Hirschkoff, D., Sangiorgi, D.: On the representation of mccarthy’s amb in the \(\pi \)-calculus. Theoretical Computer Science 330(3), 439 – 473 (2005). https://doi.org/10.1016/j.tcs.2004.10.005, expressiveness in Concurrency
Clinger, W., Halpern, C.: Alternative semantics for McCarthy’s amb. In: Brookes S.D., Roscoe A.W., W.G. (ed.) Seminar on Concurrency. CONCURRENCY 1984. Lecture Notes in Computer Science, vol. 197. Springer (1985). https://doi.org/10.1007/3-540-15670-4_22
Di Gianantonio, P.: An abstract data type for real numbers. Theoretical Computer Science 221(1-2), 295–326 (1999). https://doi.org/10.1016/S0304-3975(99)00036-5
Du Bois, A., Pointon, R., Loidl, H.W., Trinder, P.: Implementing declarative parallel bottom-avoiding choice. In: 14th Symposium on Computer Architecture and High Performance Computing (SBAC-PAD 2002), 28-30 October 2002, Vitoria, Espirito Santo, Brazil. pp. 82–92. IEEE Computer Society (2002). https://doi.org/10.1109/CAHPC.2002.1180763
Escardo, M.H.: PCF extended with real numbers. Theoretical Computer Science 162, 79–115 (1996). https://doi.org/10.1016/0304-3975(95)00250-2
Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices and Domains, Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press (2003)
Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press (1980)
Hughes, J., Moran, A.: A semantics for locally bottom-avoiding choice. In: Launchbury, J., Sansom, P.M. (eds.) Functional Programming, Glasgow 1992, Proceedings of the 1992 Glasgow Workshop on Functional Programming, Ayr, Scotland, UK, 6-8 July 1992. pp. 102–112. Workshops in Computing, Springer (1992). https://doi.org/10.1007/978-1-4471-3215-8_9
Hughes, J., O’Donnell, J.: Expressing and reasoning about non-deterministic functional programs. In: Davis, K., Hughes, J. (eds.) Functional Programming, Proceedings of the 1989 Glasgow Workshop, 21-23 August 1989, Fraserburgh, Scotland, UK. pp. 308–328. Workshops in Computing, Springer (1989)
Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up. Journal of Functional Programming 28, 1–73 (2018). https://doi.org/10.1017/S0956796818000151
Kouzapas, D., Nobuko, Y., Hu, R., Honda, K.: On asynchronous eventful session semantics. Mathematical Structures in Computer Science 26, 303–364 (2016). https://doi.org/10.1017/S096012951400019X
Lassen, S.B.: Normal Form Simulation for McCarthy’s Amb. Electronic Notes in Theoretical Computer Science 155, 445 – 465 (2006). https://doi.org/10.1016/j.entcs.2005.11.068, proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)
Lassen, S.B., Moran, A.: Unique Fixed Point Induction for McCarthy’s Amb. In: Kutylowski, M., Pacholski, L., Wierzbicki, T. (eds.) Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS’99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1672, pp. 198–208. Springer (1999). https://doi.org/10.1007/3-540-48340-3_18
Levy, P.B.: Amb breaks Well-Pointedness, Ground Amb doesn’t. Electronic Notes in Theoretical Computer Science 173, 221 – 239 (2007). https://doi.org/10.1016/j.entcs.2007.02.036, proceedings of the 23rd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII)
Luckhardt, H.: A fundamental effect in computations on real numbers. Theoretical Computer Science 5(3), 321–324 (1977). https://doi.org/10.1016/0304-3975(77)90048-2
Mamouras, K.: Synthesis of strategies and the hoare logic of angelic nondeterminism. In: Pitts, A.M. (ed.) Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015. Lecture Notes in Computer Science, vol. 9034, pp. 25–40. Springer (2015). https://doi.org/10.1007/978-3-662-46678-0_2
McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, Studies in Logic and the Foundations of Mathematics, vol. 35, pp. 33 – 70. Elsevier (1963). https://doi.org/10.1016/S0049-237X(08)72018-4
Moran, A., Sands, D., Carlsson, M.: Erratic fudgets: a semantic theory for an embedded coordination language. Science of Computer Programming 46(1), 99 – 135 (2003). https://doi.org/10.1016/S0167-6423(02)00088-6, special Issue on Coordination Languages and Architectures
O’Hearn, P.: Resources, concurrency, and local reasoning. Theoretical Computer Science 375(1), 271–307 (2007). https://doi.org/10.1016/j.tcs.2006.12.035
Pierce, B.C.: Types and Programming Languages. The MIT Press (2002)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55–74. LICS ’02, IEEE Computer Society, Washington, DC, USA (2002). https://doi.org/10.1109/LICS.2002.1029817
Sabel, D., Schmidt-Schauss, M.: A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations. Mathematical Structures in Computer Science 18(3), 501–553 (2008). https://doi.org/10.1017/S0960129508006774
Schwichtenberg, H.: Minlog. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. pp. 151–157. No. 3600 in Lecture Notes in Artificial Intell. (2006). https://doi.org/10.1016/j.jlap.2004.07.005
Schwichtenberg, H., Wainer, S.S.: Proofs and Computations. Cambridge University Press (2012)
Sondergard, H., Sestoft, P.: Non-determinism in Functional Languages. The Computer Journal 35(5), 514–523 (1992). https://doi.org/10.1093/comjnl/35.5.514
Spreen, D.: Computing with continuous objects: a uniform co-inductive approach. Mathematical Structures in Computer Science 31(2), 144–192 (2021). https://doi.org/10.1017/S0960129521000116
Tsuiki, H.: Real number computation through Gray code embedding. Theoretical Computer Science 284(2), 467–485 (2002). https://doi.org/10.1016/S0304-3975(01)00104-9
Tsuiki, H.: Real number computation with committed choice logic programming languages. J. Log. Algebr. Program. 64(1), 61–84 (2005). https://doi.org/10.1016/j.jlap.2004.07.005
Wadler, P.: Propositions as sessions. Journal of Functional Programming 24, 384–418 (2014). https://doi.org/10.1017/S095679681400001X
Wadler, P.: Propositions as types. Communications of the ACM 58(12), 75–84 (2014). https://doi.org/10.1145/2699407
Weihrauch, K.: Computable Analysis. Springer (2000)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Berger, U., Tsuiki, H. (2022). Extracting total Amb programs from proofs. In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. Springer, Cham. https://doi.org/10.1007/978-3-030-99336-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-99336-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99335-1
Online ISBN: 978-3-030-99336-8
eBook Packages: Computer ScienceComputer Science (R0)