1
$\begingroup$

Working in the untyped lambda-calculus, I'm asked to give two terms that are equivalent in call-by-name semantics but not in call-by-value.

Call $\text{fls} = \lambda x. \lambda y. y$ and $\Omega = (\lambda x. x x) (\lambda x. x x)$ . I was proposed to look at these terms:

$\text{fls} (\lambda x. \Omega)$ which in both semantics reduces to $\lambda y. y$

$\text{fls} (\lambda x. \Omega x)$ which in call-by-name reduces to $\lambda y. y$ but in call-by-value "diverges evaluating the argument to $\text{fls}$".

I don't see how these diverges except if I assume $\text{eta}$-conversion which was not assumed in my course. On top of that, I don't see how one can diverge and evaluate the argment to $\text{fls}$. Does this make sense to you?

Aside

I proposed the terms $(\lambda f. \Omega)$ and $(\lambda t. \lambda f. t) \Omega$ I think this is a valid example...

The notion of equivalence:

The notion of equivalence that I'm using is behavioral equivalence (see Pierce's TAPL book for details). The definition says that for any sequence of values to which my terms are applied I should have the same observation: either the two results diverge or the results don't diverge.

A separate notion is that of call-by-value or call-by-name which are some standard evaluation strategies for lambda terms.

$\endgroup$
  • $\begingroup$ Can you give the formal definitions of "equivalence in call-by-name" and "equivalence in call-by-value" used in your class/book? That will make the question more self contained. $\endgroup$ – Jake Nov 12 '19 at 17:16
  • $\begingroup$ @Jake I added some detail at the end of the question. Hope is better now $\endgroup$ – Rodrigo Nov 12 '19 at 17:19
  • $\begingroup$ $\lambda x. (\Omega x)$ is in normal form, however, $(\lambda x. \Omega) x$ is not in normal form. The latter term diverges while the former term does not. You may want to clarify the parenthesization of the term. $fls(\lambda 𝑥. \Omega 𝑥)$ seems to be non-diverging in both CBV and CBN strategies. $\endgroup$ – Apoorv Ingle Nov 12 '19 at 18:37
  • $\begingroup$ I guess the simplest example would be to take $(\lambda x.\lambda y.y) \Omega$ and $\lambda y.y$. They both normalize the the latter in call-by-name, but the former diverges in call-by-value. $\endgroup$ – Rodolphe Lepigre Nov 12 '19 at 19:37
  • $\begingroup$ @RodolpheLepigre does my proposal in "aside" section make sense to you? $\endgroup$ – Rodrigo Nov 12 '19 at 21:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.