Quantitative logics for equivalence of effectful programs. (English) Zbl 07515965
König, Barbara (ed.), Proceedings of the 35th conference on the mathematical foundations of programming semantics, MFPS XXXV, London, UK, June 4–7, 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 347, 281-301 (2019).
Summary: In order to reason about effects, we can define quantitative formulas to describe behavioural aspects of effectful programs. These formulas can for example express probabilities that (or sets of correct starting states for which) a program satisfies a property. Fundamental to this approach is the notion of quantitative modality, which is used to lift a property on values to a property on computations. Taking all formulas together, we say that two terms are equivalent if they satisfy all formulas to the same quantitative degree. Under sufficient conditions on the quantitative modalities, this equivalence is equal to a notion of Abramsky’s applicative bisimilarity, and is moreover a congruence. We investigate these results in the context of Levy’s call-by-push-value with general recursion and algebraic effects. For example, the results apply to (combinations of) nondeterministic choice, probabilistic choice, global store, and error.
For the entire collection see [Zbl 1428.68030].
For the entire collection see [Zbl 1428.68030].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
| 68Q55 | Semantics in the theory of computing |
Keywords:
quantitative logic; program equivalence; algebraic effects; behavioural equivalence; applicative bisimilarity; modalities; call-by-push-value; probability; nondeterminism; global store; effect combinationsReferences:
| [1] | Abramsky, Samson, The lazy λ-calculus, Research Topics in Functional Programming, 65-117 (1990) |
| [2] | Arnold, André; Nivat, Maurice, Metric interpretations of infinite trees and semantics of non deterministic recursive programs, Theoretical Computer Science, 11, 2, 181-205 (1980) · Zbl 0427.68022 |
| [3] | Dal Lago, Ugo; Gavazzo, Francesco; Blain Levy, Paul, Effectful applicative bisimilarity: Monads, relators, and Howe’s method, (Logic in Computer Science (2017)), 1-12 · Zbl 1458.68130 |
| [4] | Escardó, Martín Hötzel, A metric model of PCF, (Workshop on Realizability Semantics and Applications (1999)) · Zbl 0921.54010 |
| [5] | Felleisen, Matthias; Friedman, Daniel P., Control operators, the SECD-machine, and the lambda-calculus, (Formal Description of Programming Concepts (1986)), 193-217 |
| [6] | Fiore, Marcelo; Staton, Sam, Substitution, jumps, and algebraic effects, (Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14 (2014), ACM: ACM New York, NY, USA), 41:1-41:10 · Zbl 1401.68039 |
| [7] | Gavazzo, Francesco, Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances, (Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018)), 452-461 · Zbl 1497.68092 |
| [8] | Hasuo, Ichiro, Generic weakest precondition semantics from monads enriched with order, Theor. Comput. Sci., 604, C, 2-29 (November 2015) · Zbl 1330.68046 |
| [9] | Hennessy, Matthew; Milner, Robin, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), 32, 1, 137-161 (1985) · Zbl 0629.68021 |
| [10] | Howe, Douglas J., Equality in lazy computation systems, (Proc. 4th IEEE Symposium on Logic in Computer Science (1989)), 198-203 · Zbl 0716.68065 |
| [11] | Howe, Douglas J., Proving congruence of bisimulation in functional programming languages, Information and Computation, 124, 2, 103-112 (1996) · Zbl 0853.68073 |
| [12] | Hyland, Martin; Plotkin, Gordon; Power, John, Combining effects: Sum and tensor, Theor. Comput. Sci., 357, 1, 70-99 (July 2006) · Zbl 1096.68088 |
| [13] | Johann, Patricia; Simpson, Alex; Voigtländer, Janis, A generic operational metatheory for algebraic effects, Logic in Computer Science, 209-218 (2010) |
| [14] | Kozen, Dexter, Probabilistic PDL, Journal of Computer and System Sciences, 30, 162-178 (1985) · Zbl 0575.03013 |
| [15] | Lassen, Søren Bøgh, Relational Reasoning about Functions and Nondeterminism (1998), BRICS, PhD thesis |
| [16] | Blain Levy, Paul (2001), University of London, Call-By-Push-Value. PhD thesis |
| [17] | Blain Levy, Paul, Call-by-push-value: Decomposing call-by-value and call-by-name, Higher-Order and Symbolic Computation, 19, 4, 377-414 (2006) · Zbl 1112.68025 |
| [18] | Blain Levy, Paul, Similarity quotients as final coalgebras, Lecture Note in Computer Science, 6604, 27-41 (2011) · Zbl 1326.68193 |
| [19] | Lopez, Aliaume; Simpson, Alex, Basic operational preorders for algebraic effects in general, and for combined probability and nondeterminism in particular, (27th EACSL Annual Conference on Computer Science Logic, CSL 2018. 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK (2018)), 29:1-29:17 · Zbl 1528.68204 |
| [20] | Mardare, Radu; Panangaden, Prakash; Plotkin, Gordon D., Quantitative algebraic reasoning, (Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016 (2016)), 700-709 · Zbl 1391.68021 |
| [21] | McIver, Annabelle; Morgan, Carroll, Abstraction, Refinement And Proof For Probabilistic Systems, Monographs in Computer Science (2004), SpringerVerlag · Zbl 1069.68039 |
| [22] | Moggi, Eugenio, Notions of computation and monads, Information and Computation, 93, 1, 55-92 (1991) · Zbl 0723.68073 |
| [23] | Moggi, Eugenio, A general semantics for evaluation logic, (9th LICS (1994)), 353-362 |
| [24] | Pitts, Andrew M., Evaluation logic, (Proceedings of 4th Higher Order Workshop (1991)), 162-189 |
| [25] | Plotkin, Gordon, LCF considered as a programming language, Theoretical Computer Science, 5, 3, 223-255 (1977) · Zbl 0369.68006 |
| [26] | Plotkin, Gordon, Adequacy for infinitary algebraic effects, (Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO’09 (2009), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 1-2 · Zbl 0986.68055 |
| [27] | Plotkin, Gordon; Power, John, Adequacy for algebraic effects, (Foundations of Software Science and Computation Structures (2001)), 1-24 · Zbl 0986.68055 |
| [28] | Plotkin, Gordon; Pretnar, Matija, A logic for algebraic effects, (23rd Symposium on Logic in Computer Science (2008)), 118-129, 07 |
| [29] | Simpson, Alex; Voorneveld, Niels, Behavioural equivalence via modalities for algebraic effects, (Programming Languages and Systems - 27th European Symposium on Programming (2018)), 300-326 · Zbl 1418.68066 |
| [30] | Thijs, Albert Marchienus, Simulation and fixpoint semantics (1996), University of Groningen, PhD thesis |
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.
