[Prev][Next][Index][Thread]

[riecke@THEORY.LCS.MIT.EDU: Counterexample Albert mentioned]

Date: Fri, 24 Jun 88 14:35:19 edt
From: Jon Riecke <riecke@THEORY.LCS.MIT.EDU>
To: summer-logic@theory.LCS.MIT.EDU
Subject: Counterexample Albert mentioned


  At the last meeting of the logic seminar at MIT, we continued
discussing Ong's abstract on the lazy lambda calculus.  Ong notes (in
Section 2.3) that one can simulate the (untyped) call-by-value lambda
calculus in his call-by-name calculus with convergence testing
operator C.  More precisely,

THM 1: (Ong) M halts in call-by-value  iff  the translation of M, Mbar, halts
under call-by-name (with C).

  Albert conjectured that the translation does NOT preserve
call-by-value observational congruences, and I have verified the conjecture.
First, let "obsv" denote the observational congruence relation in call-by-value,
and "obsnC" denote observational congruence in Ong's call-by-name language with
convergence testing.  Then

THM 2: There are terms M, N where M obsv N, but where Mbar and Nbar
are not obsnC.

PROOF: Consider the terms
        M = \x.\y. y x
        N = \x.\y. y (\z. x z) 
In this case, 
        M obsv N
(proved using Moggi's partial lambda calculus, whose rules are sound
for call-by-value.)  Using Ong's translation,
        Mbar = \x.\y. (C x) (y x)
        Nbar = \x.\y. (C (\z. (C z) (x z))) (y (\z. (C z) (x z)))
Now let P2 = \a.\b.b, the projection on the second argument.  
Using the context
        D[ ] = [ ] P2 (\f.f Omega)
we can show that
        D[Mbar] ->> (C P2) ((\f.f Omega) P2)
                ->> (P2 Omega)
                ->> \b.b
whereas
        D[Nbar] ->> (\f.f Omega) (\z. (C z) (P2 z))
                ->> (C Omega) (P2 Omega)
which diverges.  Thus, Mbar and Nbar are not obsnC.
END-OF-PROOF


REMARK:  One may ask if the converse holds, namely does
        Mbar obsnC Nbar implies M obsv N hold?  
In fact, this is a corollary of Theorem 1; if M and N were
call-by-value distinguishable, that context would distinguish Mbar and
Nbar, by Theorem 1.


-Jon



---------------------------------------------------------------
Date: Fri, 24 Jun 88 16:45:16 edt
From: Albert R. Meyer <meyer@THEORY.LCS.MIT.EDU>
To: riecke@THEORY.LCS.MIT.EDU
Cc: summer-logic@theory.LCS.MIT.EDU
In-Reply-To: Jon Riecke's message of Fri, 24 Jun 88 14:35:19 edt <8806241835.AA11144@LOON.LCS.MIT.EDU>
Subject: Counterexample Albert mentioned

One can also ask whether there can be ANY effective translation, ()^, such
that M obsnC N iff M^ obsv N^.  Likewise for a translation in the opposite
direction.

Regards, A.

P.S.  How about cc'ing this stuff to TYPES?