![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > On program equivalence in the probabilistic lambda calculus
On program equivalence in the probabilistic lambda calculusAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Anupam Das. We consider probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specific operational semantics. This notion has been studied with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven fully abstract with respect to the contextual equivalence in cbv but not in lazy cbn. We overcome this issue of cbn by relaxing the laziness constraint: we prove that PAB is fully abstract with respect to the standard head reduction contextual equivalence. The proof is based on the Leventis Separation Theorem, using probabilistic Nakajima trees as a tree-like representation of the contextual equivalence classes. Finally, we prove also that the inequality full abstraction fails, showing that the probabilistic applicative similarity is strictly contained in the contextual preorder. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsQuantitative Methods in Finance Seminar Analysis Seminar Analysis Reading SeminarOther talksHodge Theory: Connecting Algebra and Analysis The development of an optically pumped magnetometer based MEG system Ultrafast, all-optical, and highly efficient imaging of molecular chirality Modelling uncertainty in image analysis. Geometry of alternating projections in metric spaces with bounded curvature Quantum simulations using ultra cold ytterbium |