![]() |
![]() |
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 listsOptimisation and Numerical Analysis Seminars Artificial Intelligence and Natural Computation seminars IRLab Seminars: Robotics, Computer Vision & AIOther talksThe tragic destiny of Mileva Marić Einstein An unobstructedness result for the coisotropic deformation problem Counting cycles in planar graphs Two-level spectral preconditioners for indefinite or non-symmetric problems Topological interfaces, phase transitions, and point-group symmetries – spinor Bose-Einstein condensates as topological-defect laboratories Width parameters and the maximum independent set problem |