We start by de ning the notion of Howe's extension, a construction extending a ?-term V-open relation to a compatible and substitutive ?-term V-relation. 2. For any a ? V if ?, x : s ? |= v a ? ? H (u, z) : ? is derivable, 2015. ,
, The proof is by induction on the derivation of the judgments: J ?, x : s ? |= ? a ? ? H (e, f ) : ? J ?
x : s ? v ? (x, u) : ? ?, x : s ? |= v a ? ? H (x, u) : ? (H-var), so that s ? 1 and J is ?, x : s ? |= v a ? ? H (x, u) : ? . We have to prove a ?s ? ( v ? H ( , w )) ? ? v ? H ( , u[w/x]) : ? . Since ? is value substitutive, from ?, x : s ? |= v a ? ? H (x, u) : ? we infer a ? ? v ? (w, u[w/x]) : ? . Moreover, since ? H is an open ?-term V-relation (and thus closed under weakening), We have two subcases to consider. 1.1 J has been inferred via an instance of rule (H-var) from premises: a ? ? ,
,
, 2 J has been inferred via an instance of rule (H-var) from premises: a ? ?, : r ?
, u) : ? . We have to prove a ? s ? (? v ? H ( , w )) ? ?, : r ? v ? H ( , u[w/x]) : ? . As V is integral and ? is value-substitutive, we have: a ? s ? (? v ? H ( , w )) ? a ? ?, J is ?
, Suppose J has been inferred via an instance of rule (H-let) from premises: ?, x : s ? |= ? a ? ? H (e, e ) : ? (12.1)
,
, x : s ? ) ? (?, x : r ? ) ? H (let = e in f , ) : ? . (12.3) so that is: (p ? 1) · ? ? ?, x : (p?1) ·s ?r ? |= ? (p ? 1)(a) ? b ? c ? ? H
, First of all we observe that since ? H is re exive, we can assume n = m. In fact, if e.g. n = m + l, then we can 'complete' (? H ) (m) as follows: (? H ) (m) = (? H ) (m) ·I · · · · I l -times ? (? H ) (m) · ? H · · · · ? H l -times = (? H ) (n)
, The base case is trivial. Let us turn on the inductive step. We have to prove: (s ? 1) ? e (? ? H (e, e ) : ? ) ? (? (? H ) (n) (e , e ) : ? ) ? f (?, x : s ? ? H ( f , f ) : ? ) ? (?, x : s ? (? H ) (n) ( f , f ) : ? ) ? c
, ) : ? ) ? (?, x : s ? (? H ) (n) ( f , f ) : ? ) ? c, i.e. (s ? 1) ? (? ? H (e, e ) : ? ) ? (?, x : s ? ? H ( f , f ) : ? ) ? (s ? 1) ? (? (? H
x : s ? (? H ) (n) ( f , f ) : ? ) ? c ,
, We can now apply compatibility of ? H plus the induction hypothesis, thus reducing the thesis to: (s ? 1) · ? ? ? ? H (let x = e in f
, ? (s ? 1) · ? ? ? (? H ) T (let x = e in f , let x = e in f ) : ? ) ? c
, We can now conclude the thesis by very de nition of (? H ) T . To prove point 2 we have to show (? H ) T ? ((? H ) T ) ? . For that it is su cient to show ? H ? ((? H ) T ) ? . That amounts to prove that for all computations ? e, e : ? and values ? v , and for any a ? V such that ? |= ? a ? ? H (e, e ) : ? is derivable we have a ? ? (? H ) T (e, e ) : ? (and similarity for ? v , : ? ). The proof is by induction on the derivation of ? |= ? a ? ? H
, If any CBE in ? is nitely continuous, Theorem 17
One inequality follows from Lemma 41 as follows: ? ? ? H ? (? ) T . For the other inequality, we rely on the coinduction proof principle associated with ? , meaning that it is su cient to prove that ((? ) H ) T is a symmetric applicative simulation (with respect to ?). Symmetry is given by Lemma 45. From Lemma 43 (Key Lemma) we know that ? H is an applicative simulation distance. Since the identity ?-term V-relation is an applicative simulation distance, and the composition of applicative simulation distances is itself an applicative simulation distance (see Proposition 30), Lemma 45 we know that (? H ) T is compatible. Therefore, it is su cient to prove ,
, We conclude this chapter by noticing that we can rely on Theorem 17 to come up with concrete notions of compatible applicative bisimilarity distance. For instance, we obtain a compatible pseudometric for for P-Fuzz (observe that CBEs are indeed nitely continuous)
normal form bisimilarity has been mainly investigated for call-by-name languages, due to its equivalence with Lévy-Longo tree equivalence, and for the so-called classical theory of ?-calculus (Barendregt, 1984), due to its equivalence with Böhm tree equivalence. To the best of the author's knowledge, no abstract account of normal form bisimilarity in the context of languages with algebraic e ects has been given so far. However, there are some works on speci c e ectful extensions of Böhm trees, notably the work of de Liguoro and Piperno on nondeterministic Böhm trees, de ned are proved using our abstract Howe's method. Applicative bisimilarity has also been investigated for languages with non-algebraic e ects, notably for languages with control operators (Biernacki & Lenglet, 1993. ,
, Similar in spirit to our approach, the work of Katsumata and Sato (Katsumata & Sato, 2013) (as well as (Katsumata, 2013)) analyses monadic lifting of relations in the context of -lifting
Concerning program metrics, several works have been done in the past years on quantitative reasoning in the context of programming language semantics. In particular, several authors have used (cartesian) categories of ultrametric spaces as a foundation for denotational semantics of both concurrent, Another piece of work which is related to ours is due to Johann, 1980. ,
2017) is a denotational version of the so-called metric preservation (Reed & Pierce, 2010) (whose original proof requires a suitable step-indexed metric logical relation). Corollary 6 is the operational counterpart of such result generalised to arbitrary algebraic e ects. A di erent but deeply related line of research has been recently proposed in, where coinductive, operationally-based distances have been studied for probabilistic ?-References Abramsky, pp.65-117, 1990. ,
Research topics in functional programming, pp.65-116, 1990. ,
Domain theory, Handbook of logic in computer science, pp.1-168, 1994. ,
Full abstraction in the lazy lambda calculus, Inf. Comput, vol.105, issue.2, pp.159-267, 1993. ,
An indexed model of recursive types for foundational proof-carrying code, ACM Trans. Program. Lang. Syst, vol.23, issue.5, pp.657-683, 2001. ,
Metric interpretations of in nite trees and semantics of non deterministic recursive programs, Theor. Comput. Sci, vol.11, pp.181-205, 1980. ,
Report on the algorithmic language algol 60, Commun. ACM, vol.3, issue.5, pp.299-314, 1960. ,
Behavioral metrics via functor lifting, Proc. of FSTTCS, pp.403-415, 2014. ,
Towards trace metrics via functor lifting, Proc. of CALCO 2015, pp.35-49, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01285298
The lambda calculus: its syntax and semantics, 1984. ,
Relational algebras, Lect. Notes Math, vol.137, pp.39-55, 1970. ,
Programming with algebraic e ects and handlers, J. Log. Algebr. Meth. Program, vol.84, issue.1, pp.108-123, 2015. ,
Monads and e ects, Applied semantics, international summer school, APPSEM, advanced lectures, pp.42-122, 2000. ,
Applicative bisimilarities for call-by-name and call-by-value ?µcalculus, Electr. Notes Theor. Comput. Sci, vol.308, pp.49-64, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01080960
Proving soundness of extensional normal-form bisimilarities, Electr. Notes Theor. Comput. Sci, vol.336, pp.41-56, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01650000
, Handle with care: relational interpretation of algebraic e ects and handlers. PACMPL, 2(POPL), vol.8, p.30, 2018.
Step-indexed logical relations for probability, Proc. of FOSSACS 2015, pp.279-294, 2015. ,
Alcune proprietà delle forme ??-normali del ?k-calcolo. Pubblicazioni dell'Istituto per le Applicazioni del Calcolo, p.696, 1968. ,
E ekt: Extensible algebraic e ects in scala (short paper), Proceedings of the 8th acm sigplan international symposium on scala, pp.67-72, 2017. ,
A core quantitative coe ect calculus, Proc. of ESOP, pp.351-370, 2014. ,
Some algebraic laws for spans (and their connections with multirelations), Electronic Notes in Theoretical Computer Science, vol.44, issue.3, pp.175-193, 2001. ,
Bicategories of spans and relations, Journal of Pure and Applied Algebra, vol.33, issue.3, pp.259-267, 1984. ,
A semantical and operational account of call-by-value solvability, Foundations of software science and computation structures -17th international conference, FOSSACS 2014, held as part of the european joint conferences on theory and practice of software, pp.103-118, 2014. ,
The calculi of lambda conversion. (am-6) (annals of mathematics studies), 1985. ,
, Wasserstein metric and subordination, vol.189, 2008.
From lax monad extensions to topological theories, vol.46, pp.99-123, 2014. ,
On probabilistic applicative bisimulation and call-by-value lambdacalculi, Proc. of ESOP, pp.209-228, 2014. ,
Metric reasoning about lambda-terms: The a ne case, Proc. of LICS, pp.633-644, 2015. ,
Metric reasoning about lambda-terms: The general case, Proc. of ESOP 2017, pp.341-367, 2017. ,
Contextual equivalence for probabilistic programs with continuous random variables and scoring, Proceedings of ESOP 2017, pp.368-392, 2017. ,
On coinductive equivalences for higher-order probabilistic functional programs, Proc. of POPL, pp.297-308, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01091573
Probabilistic operational semantics for the lambda calculus, RAIRO -Theor. Inf. and Applic, vol.46, issue.3, pp.413-450, 2012. ,
Introduction to lattices and order, 1990. ,
Testing equivalence for processes, Automata, languages and programming, 10th colloquium, pp.548-560, 1983. ,
A semantic account of metric preservation, Proc. of POPL 2017, pp.545-556, 2017. ,
Denotational semantics of concurrency, Stoc, pp.153-158, 1982. ,
Non deterministic extensions of untyped lambda-calculus, Inf. Comput, vol.122, issue.2, pp.149-177, 1995. ,
Course in general linguistics: Translated by wade baskin. edited by perry meisel and haun saussy, 2011. ,
Bisimulation for probabilistic transition systems: A coalgebraic approach, Automata, languages and programming, 24th international colloquium, icalp'97, pp.460-470, 1997. ,
Concurrent system programming with e ect handlers, Trends in functional programming -18th international symposium, pp.98-117, 2017. ,
The theory of di erence: Readings in contemporary continental thought. State University of, 2001. ,
Behavioural pseudometrics for nondeterministic probabilistic systems, Proc. of SETTA 2016, pp.67-84, 2016. ,
Eager functions as processes, Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, pp.364-373, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01917255
Di erential privacy, Automata, languages and programming, pp.1-12, 2006. ,
A metric model of pcf, Workshop on realizability semantics and applications, 1999. ,
The revised report on the syntactic theories of sequential control and state, Theor. Comput. Sci, vol.103, issue.2, pp.235-271, 1992. ,
Programming languages: Principles and paradigms, Proc. of ICFP 2016, pp.476-489, 2010. ,
Compositional bisimulation metric reasoning with probabilistic process calculi, Logical Methods in Computer Science, vol.12, issue.4, 2016. ,
Bounded linear logic: A modular approach to polynomial-time computability, Theor. Comput. Sci, vol.97, pp.1-66, 1992. ,
Initial algebra semantics and continuous algebras, J. ACM, vol.24, issue.1, pp.68-95, 1977. ,
A tutorial on co-induction and functional programming, Workshops in computing, pp.78-95, 1994. ,
Logical relations for monadic types, Mathematical Structures in Computer Science, vol.18, issue.6, pp.1169-1217, 2008. ,
Generic trace semantics via coinduction, Logical Methods in Computer Science, vol.3, issue.4, 2007. ,
Grundzüge der mengenlehre, 1949. ,
Structural induction and coinduction in a brational setting, Inf. Comput, vol.145, issue.2, pp.107-152, 1998. ,
A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications, vol.3, pp.113-151, 2015. ,
Topological theories and closed objects, Adv. Math, vol.215, pp.789-824, 2007. ,
Convergence and quantale-enriched categories. Categories and General Algebraic Structures with Applications, vol.9, pp.77-138, 2018. ,
Monoidal topology. a categorical approach to order, metric, and topology, 2014. ,
Dynamic probabilistic systems, 2007. ,
Proving congruence of bisimulation in functional programming languages, Inf. Comput, vol.124, issue.2, pp.103-112, 1996. ,
Simulations in coalgebra, Theor. Comput. Sci, vol.327, issue.1-2, pp.71-108, 2004. ,
Combining algebraic e ects with continuations, Theor. Comput. Sci, vol.375, issue.1-3, pp.20-40, 2007. ,
Combining e ects: Sum and tensor, Theor. Comput. Sci, vol.357, issue.1-3, pp.70-99, 2006. ,
The category theoretic understanding of universal algebra: Lawvere theories and monads, Electr. Notes Theor. Comput. Sci, vol.172, pp.437-458, 2007. ,
, Introduction to coalgebra: Towards mathematics of states and observation, vol.59, 2016.
Trace semantics via determinization, Coalgebraic methods in computer science -11th international workshop, vol.2012, pp.109-129, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-01539887
, Set theory, 1997.
A generic operational metatheory for algebraic e ects, Proc. of LICS 2010, pp.209-218, 2010. ,
Relating computational e ects by -lifting, Inf. Comput, vol.222, pp.228-246, 2013. ,
Preorders on monads and coalgebraic simulations, Foundations of software science and computation structures -16th international conference, FOSSACS 2013, held as part of the european joint conferences on theory and practice of software, pp.145-160, 2013. ,
Basic concepts of enriched category theory, Reprints in Theory and Applications of Categories, pp.1-136, 2005. ,
Strong functors and monoidal monads, Archiv der Mathematik, issue.23, pp.113-120, 1972. ,
Discrete in nite transportation problems, Discrete Applied Mathematics, issue.58, pp.19-33, 1995. ,
From applicative to environmental bisimulation, Electr. Notes Theor. Comput. Sci, vol.276, pp.215-235, 2011. ,
Relation lifting, a survey, J. Log. Algebr. Meth. Program, vol.85, issue.4, pp.475-499, 2016. ,
Correspondence between ALGOL 60 and church's lambda-notation: part I, Commun. ACM, vol.8, issue.2, pp.89-101, 1965. ,
A correspondence between ALGOL 60 and church's lambda-notations: Part II, Commun. ACM, vol.8, issue.3, pp.158-167, 1965. ,
Bisimulation through probabilistic testing, Proceedings of POPL 1989, pp.344-352, 1989. ,
Relational reasoning about contexts, Higher order operational techniques in semantics, pp.91-136, 1998. ,
Relational reasoning about functions and nondeterminism (Unpublished doctoral dissertation), 1998. ,
Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context, Electr. Notes Theor. Comput. Sci, vol.20, pp.346-374, 1999. ,
Eager normal form bisimulation, Proceedings of LICS 2005, pp.345-354, 2005. ,
Head normal form bisimulation for pairs and the \lambda\mu-calculus, Proceedings of LICS, pp.297-306, 2006. ,
Normal form simulation for mccarthy's amb, Electr. Notes Theor. Comput. Sci, vol.155, pp.445-465, 2006. ,
Metric spaces, generalized logic, and closed categories, Rend. Sem. Mat. Fis. Milano, vol.43, pp.135-166, 1973. ,
Functorial Semantics of Algebraic Theories. Reprints in Theory and Applications of Categories, vol.4, pp.1-121, 2004. ,
Implementing algebraic e ects in c, Programming languages and systems, pp.339-363, 2017. ,
Probabilistic lambda-theories (Unpublished doctoral dissertation), 2016. ,
Probabilistic böhm trees and probabilistic separation, Proc. of lics, 2018. ,
An algebraic interpretation of the lambda beta -calculus and a labeled lambda -calculus, Lambda-calculus and computer science theory, proceedings of the symposium, pp.147-165, 1975. ,
In nitary howe's method, Electr. Notes Theor. Comput. Sci, vol.164, issue.1, pp.85-104, 2006. ,
Similarity quotients as nal coalgebras, Proc. of FOSSACS 2011, vol.6604, pp.27-41, 2011. ,
Modelling environments in call-by-value programming languages, Inf. Comput, vol.185, issue.2, pp.182-210, 2003. ,
Amb breaks well-pointedness, ground amb doesn't. Electronic Notes in Theoretical Computer Science, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, vol.173, pp.221-239, 2007. ,
Set-theoretical models of lambda calculus: Theories, expansions, isomorphisms, Annals of Pure and Applied Logic, vol.24, pp.153-188, 1983. ,
Basic operational preorders for algebraic e ects in general, and for combined probability and nondeterminism in particular, 27th EACSL annual conference on computer science logic, CSL 2018, vol.29, pp.1-29, 2018. ,
Categories for the working mathematician, 1971. ,
A triple theoretic construction of compact algebras, Seminar on triples and categorical homology theory, pp.91-118, 1969. ,
Taut monads and t0-spaces, Theor. Comput. Sci, vol.275, issue.1-2, pp.79-109, 2002. ,
Call-by-name, call-by-value, call-by-need and the linear lambda calculus, Theor. Comput. Sci, vol.228, issue.1-2, pp.175-210, 1999. ,
Equivalence in functional languages with e ects, J. Funct. Program, vol.1, issue.3, pp.287-327, 1991. ,
Triangulating context lemmas, Proceedings of the 7th acm sigplan international conference on certi ed programs and proofs, pp.102-114, 2018. ,
Fully abstract models of typed lambda-calculi, Theor. Comput. Sci, vol.4, issue.1, pp.1-22, 1977. ,
Communication and concurrency, 1989. ,
Functions as processes, Mathematical Structures in Computer Science, vol.2, issue.2, pp.119-141, 1992. ,
URL : https://hal.archives-ouvertes.fr/inria-00075405
Co-induction in relational semantics, Theor. Comput. Sci, vol.87, issue.1, pp.209-220, 1991. ,
De nition of standard ML, 1990. ,
Computational lambda-calculus and monads, Proc. of LICS 1989, pp.14-23, 1989. ,
Notions of computation and monads, Inf. Comput, vol.93, issue.1, pp.55-92, 1991. ,
Lambda calculus models of programming languages (Unpublished doctoral dissertation), 1969. ,
, , 2000.
The lazy lambda calculus: An investigation into the foundations of functional programming, 1988. ,
Non-determinism in a functional setting, Proc. of LICS 1993, pp.275-286, 1993. ,
Concurrency and automata on in nite sequences, Theoretical computer science, pp.167-183, 1981. ,
Coe ects: a calculus of context-dependent computation, Proc. of ICFP, pp.123-135, 2014. ,
Howe's method for higher-order languages, Advanced topics in bisimulation and coinduction, vol.52, pp.197-232, 2011. ,
Lambda-de nability and logical relations, 1973. ,
Call-by-name, call-by-value and the lambda-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975. ,
Lcf considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977. ,
Adequacy for algebraic e ects, Proc. of FOSSACS, pp.1-24, 2001. ,
Notions of computation determine monads, Proc. of FOSSACS, pp.342-356, 2002. ,
Algebraic operations and generic e ects, Applied Categorical Structures, vol.11, issue.1, pp.69-94, 2003. ,
Handling algebraic e ects, Logical Methods in Computer Science, vol.9, issue.4, 2013. ,
Enhancements of the bisimulation proof method, Advanced Topics in Bisimulation and Coinduction, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00909391
An introduction to algebraic e ects and handlers, Electr. Notes Theor. Comput. Sci, vol.319, pp.19-35, 2015. ,
Finite automata and their decision problems, IBM Journal of Research and Development, vol.3, issue.2, pp.114-125, 1959. ,
Distance makes the types grow stronger: a calculus for di erential privacy, Proc. of ICFP 2010, pp.157-168, 2010. ,
Types, abstraction and parametric polymorphism, IFIP congress, pp.513-523, 1983. ,
Quantales and their applications, Longman Scienti c & Technical, 1990. ,
Elements of generalized ultrametric domain theory, Theor. Comput. Sci, vol.170, issue.1-2, pp.349-381, 1996. ,
Universal coalgebra: a theory of systems, Theor. Comput. Sci, vol.249, issue.1, pp.3-80, 2000. ,
Improvement theory and its applications, Higher Order Operational Techniques in Semantics, pp.275-306, 1998. ,
The lazy lambda calculus in a concurrency scenario (extended abstract), Proceedings of the seventh annual symposium on logic in computer science (LICS '92), pp.102-109, 1992. ,
A theory of bisimulation for the pi-calculus, CONCUR '93, 4th international conference on concurrency theory, pp.127-142, 1993. ,
The lazy lambda calculus in a concurrency scenario, Inf. Comput, vol.111, issue.1, pp.120-153, 1994. ,
Introduction to bisimulation and coinduction, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00907026
Environmental bisimulations for higher-order languages, ACM Trans. Program. Lang. Syst, vol.33, issue.1, p.69, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-01337665
Environmental bisimulations for probabilistic higher-order languages, Proceedings of POPL 2016, pp.595-607, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01337665
The ? -calculus -a theory of mobile processes, 2001. ,
Theory of linear and integer programming, 1986. ,
Reasoning about sequential functions via logical relations, Applications of categories in computer science, vol.177, pp.258-269, 1992. ,
Behavioural equivalence via modalities for algebraic e ects, Proc. of ESOP, pp.300-326, 2018. ,
Counterexamples in topology, 1995. ,
A complete, co-inductive syntactic theory of sequential control and state, Proceedings of POPL 2007, pp.161-172, 2007. ,
Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, vol.13, pp.11-49, 2000. ,
The existence of probability measures with given marginals, Ann. Math. Statist, vol.36, issue.2, pp.423-439, 1965. ,
A lattice-theoretical xpoint theorem and its applications, Paci c J. Math, vol.5, issue.2, pp.285-309, 1955. ,
Simulation and xpoint semantics, 1996. ,
Computability and ?-de nability, The Journal of Symbolic Logic, vol.2, issue.4, pp.153-163, 1937. ,
Domain theory, testing and simulation for labelled markov processes, Theor. Comput. Sci, vol.333, issue.1-2, pp.171-197, 2005. ,
Word and object, 1964. ,
Topology via logic, 1996. ,
Optimal transport: Old and new, 2008. ,
Metrics for di erential privacy in concurrent systems, Formal techniques for distributed objects, components, and systems -34th IFIP WG 6.1 international conference, pp.199-215, 2014. ,