Differential Logical Relations, Part I: The Simply-Typed Case (Track B: Automata, Logic, Semantics, and Theory of Programming)
We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category.
Logical Relations
lambda-Calculus
Program Equivalence
Semantics
Theory of computation~Lambda calculus
111:1-111:14
Track B: Automata, Logic, Semantics, and Theory of Programming
The authors are partially supported by the ERC Consolidator Grant DLV-818616 DIAPASoN, as well as by the ANR projects 14CE250005 ELICA and 16CE250011 REPAS.
https://arxiv.org/abs/1904.12137
Ugo
Dal Lago
Ugo Dal Lago
University of Bologna, Italy
INRIA Sophia Antipolis, France
Francesco
Gavazzo
Francesco Gavazzo
IMDEA Software Institute, Spain
Akira
Yoshimizu
Akira Yoshimizu
INRIA Sophia Antipolis, France
10.4230/LIPIcs.ICALP.2019.111
S. Abramsky. The Lazy Lambda Calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-117. Addison Wesley, 1990.
Samson Abramsky. Abstract Interpretation, Logical Relations and Kan Extensions. J. Log. Comput., 1(1):5-40, 1990.
Mario Alvarez-Picallo and C.-H. Luke Ong. Change Actions: Models of Generalised Differentiation. In Proc. of FOSSACS 2019, pages 45-61, 2019.
A. Arnold and M. Nivat. Metric Interpretations of Infinite Trees and Semantics of non Deterministic Recursive Programs. Theor. Comput. Sci., 11:181-205, 1980.
C. Baier and M.E. Majster-Cederbaum. Denotational Semantics in the CPO and Metric Approach. Theor. Comput. Sci., 135(2):171-220, 1994.
Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. Programming language techniques for differential privacy. SIGLOG News, 3(1):34-53, 2016.
Michael A. Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial Metric Spaces. The American Mathematical Monthly, 116(8):708-718, 2009.
Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation. In Proc. of PLDI, pages 145-155, 2014.
Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized Bisimulation Metrics. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, pages 32-46, 2014.
Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning about λ-Terms: The Affine Case. In Proc. of LICS 2015, pages 633-644, 2015.
Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About λ-Terms: The General Case. In Proc. of ESOP 2017, pages 341-367, 2017.
Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential Logical Relations, Part I: The Simply-Typed Case (Extended Version), 2018. URL: http://arxiv.org/abs/1904.12137.
http://arxiv.org/abs/1904.12137
A.A. de Amorim, M. Gaboardi, J. Hsu, S. Katsumata, and I. Cherigui. A semantic account of metric preservation. In Proc. of POPL 2017, pages 545-556, 2017.
J.W. de Bakker and J.I. Zucker. Denotational Semantics of Concurrency. In STOC, pages 153-158, 1982.
Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323-354, 2004.
M.H. Escardo. A metric model of PCF. In Workshop on Realizability Semantics and Applications, 1999.
Francesco Gavazzo. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. In Proc. of LICS 2018, pages 452-461, 2018.
D. Hofmann, G.J. Seal, and W. Tholen, editors. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology. Number 153 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2014.
F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43:135-166, 1973.
John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
Sparsh Mittal. A Survey of Techniques for Approximate Computing. ACM Comput. Surv., 48(4), 2016.
J. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1969.
Gordon D. Plotkin. Lambda-Definability and Logical Relations. Memorandum SAI-RM-4, University of Edinburgh, 1973.
J. Reed and B.C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP 2010, pages 157-168, 2010.
K.I. Rosenthal. Quantales and their applications. Pitman research notes in mathematics series. Longman Scientific &Technical, 1990.
Dana Scott. Outline of a mathematical theory of computation. Technical Report PRG02, OUCL, November 1970.
Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages. Technical Report PRG06, OUCL, August 1971.
F. Van Breugel. An introduction to metric semantics: operational and denotational models for programming and specification languages. Theor. Comput. Sci., 258(1-2):1-98, 2001.
F. Van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115-142, 2005.
Franck van Breugel and James Worrell. Towards Quantitative Verification of Probabilistic Transition Systems. In Proc. of ICALP 2001, pages 421-432, 2001.
Edwin M. Westbrook and Swarat Chaudhuri. A Semantics for Approximate Program Transformations. CoRR, abs/1304.5531, 2013. URL: http://arxiv.org/abs/1304.5531.
http://arxiv.org/abs/1304.5531
Lili Xu, Konstantinos Chatzikokolakis, and Huimin Lin. Metrics for Differential Privacy in Concurrent Systems. In Proc. of FORTE 2014, pages 199-215, 2014.
Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode