This paper explores two topics at once: the use of denotational semantics to bound the evaluation length of functional programs, and the semantics of strong (that is, possibly under abstractions) call-by-value evaluation. About the first, we analyze de Carvalho's seminal use of relational semantics for bounding the evaluation length of lambda-terms, starting from the presentation of the semantics as an intersection types system. We focus on the part of his work which is usually neglected in its many recent adaptations, despite being probably the conceptually deeper one: how to transfer the bounding power from the type system to the relational semantics itself. We dissect this result and re-understand it via the isolation of a simpler size representation property. About the second, we use relational semantics to develop a semantical study of strong call-by-value evaluation, which is both a delicate and neglected topic. We give a semantic characterization of terms normalizable with respect to strong evaluation, providing in particular the first result of adequacy with respect to strong call-by-value. Moreover, we extract bounds about strong evaluation from both the type systems and the relational semantics. Essentially, we use strong call-by-value to revisit de Carvalho's semantic bounds, and de Carvalho's technique to provide semantical foundations for strong call-by-value.

翻译：本文同时探讨两个主题：用指称语义界定函数式程序的求值长度，以及强（即可能在抽象层下进行）按值调用求值的语义学。针对第一个主题，我们分析了de Carvalho在关系语义学领域的基础性工作——通过将语义呈现为交集类型系统来界定λ-项的求值长度。我们聚焦于其研究中常被后续众多改编工作所忽视（尽管可能更具理论深度）的部分：如何将类型系统的界定能力迁移至关系语义本身。我们剖解了这一结果，并通过提炼出更简洁的规模表示性质来重新理解它。针对第二个主题，我们运用关系语义学对强按值调用求值（一项既微妙又鲜受关注的课题）展开语义研究。我们给出了强求值可归一化项的语义刻画，特别首次证明了针对强按值调用的适切性定理。此外，我们从类型系统和关系语义中同时提取了关于强求值的界。本质上，我们借助强按值调用重新审视de Carvalho的语义界理论，并运用de Carvalho的技术为强按值调用提供语义学基础。