On Completeness of Logical Relations for Monadic Types

Interesting properties of programs can be expressed using contextual equivalence. The latter is difficult to prove directly, hence (pre-)logical relations are often used as a tool to prove it. Whereas pre-logical relations are complete at all types, logical relations are only complete up to firstorder types. We propose a notion of contextual equivalence for Moggi's computational lambda calculus, and define pre-logical and logical relations for this calculus. Monads introduce new difficulties: in particular the usual proofs of completeness up to first-order types do not go through. We prove completeness up to first order for several of Moggi's monads. In the case of the non-determinism monad we obtain, as a corollary, completness of strong bisimulation w.r.t. contextual equivalence in lambda calculus with monadic non-determinism.

• Type: Conference
• Year: 2006
• Where: ASIAN
• Authors: Slawomir Lasota, David Nowak, Yu Zhang
• Keywords: Algorithms, ASIAN 2006, Contextual Equivalence, Lambda Calculus, Logical Relations