2020/04/27 by Gianluca Curzi, Curzi, Gianluca, Michele Pagani +1
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2004.12891
openalex publication_date 2020/04/27 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28
We consider the probabilistic applicative bisimilarity (PAB), a coinductive\nrelation comparing the applicative behaviour of probabilistic untyped lambda\nterms according to a specific operational semantics. This notion has been\nstudied with respect to the two standard parameter passing policies,\ncall-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not\nreducing within the body of a function. In particular, PAB has been proven to\nbe fully abstract with respect to the contextual equivalence in cbv but not in\nlazy cbn. We overcome this issue of cbn by relaxing the laziness constraint: we\nprove that PAB is fully abstract with respect to the standard head reduction\ncontextual equivalence. Our proof is based on the Leventis Separation Theorem,\nusing probabilistic Nakajima trees as a tree-like representation of the\ncontextual equivalence classes. Finally, we prove also that the inequality full\nabstraction fails, showing that the probabilistic applicative similarity is\nstrictly contained in the contextual preorder.\n