Sangiorgi's normal form bisimilarity is call-by-name, identifies all the call-by-name meaningless terms, and rests on open terms in its definition. The literature contains a normal form bisimilarity for the call-by-value $\lambda$-calculus, Lassen's enf bisimilarity, which validates all of Moggi's monadic laws. The starting point of this work is the observation that enf bisimilarity is not the call-by-value equivalent of Sangiorgi's, because it does not identify the call-by-value meaningless terms. The issue has to do with open terms. We then develop a new call-by-value normal form bisimilarity, deemed net bisimilarity, by exploiting an existing formalism for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity identifies meaningless terms but it does not validate Moggi's laws. Moreover, there is no easy way to merge them. To better understand the situation, we provide a detailed analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard's call-by-value relational semantics.

翻译：桑吉奥吉的范式互模拟是按名调用的，它识别了所有按名调用无意义的项，并在其定义中依赖于开放项。文献中包含一种按值调用λ-演算的范式互模拟，即拉森的enf互模拟，它验证了莫吉的所有单子定律。这项工作的起点是观察到enf互模拟并非桑吉奥吉互模拟的按值调用等价物，因为它不识别按值调用无意义的项。问题与开放项有关。然后，我们通过利用一种处理按值调用中开放项的现有形式主义，开发了一种新的按值调用范式互模拟，称为net互模拟。结果表明，enf和net互模拟是不可比较的，因为net互模拟识别无意义项，但不验证莫吉定律。此外，没有简单的方法将它们合并。为了更好地理解这一情况，我们提供了对丰富多样的可能按值调用范式互模拟的详细分析，并将它们与埃哈德的按值调用关系语义联系起来。