This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the lambda-calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the lambda-calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard's call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists. We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value.

翻译：本文为λ-演算中强（即可能在抽象下进行的）按值调用求值提供了理论基础。近期，Accattoli等人针对λ-演算提出了一种按值调用强求值形式——外部策略，并证明了其时间合理性。此处，我们利用语义工具，即Ehrhard提出的按值调用多类型（交类型的一种变体）来研究外部策略。研究表明，当项可被所谓的收缩多类型定型时，外部策略恰好终止，这模仿了强按名调用类似结果。此外，在无类型设定中，外部策略是规范化的，即只要范式存在，它就能到达范式。我们还考虑了Biernacka等人证明时间合理的按扩展值调用强求值方法。结果表明这两种方法并不等价：某些项可能通过外部策略发散，但对按扩展值调用策略却是终止的。