On program equivalence in the probabilistic lambda calculus

Add to your list(s) Download to your calendar using vCal

• Gianluca Curzi (University of Birmingham)
• Friday 23 October 2020, 13:45-15:30
• https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09.

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:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience
• https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09

Note that ex-directory lists are not shown.