Useful evaluation is an optimised evaluation mechanism for functional programming languages, introduced by Accattoli and Dal Lago. The key to useful evaluation is to represent programs with sharing and to implement substitution of terms only when this contributes to the progress of the computation. Initially defined in the framework of call-by-name, useful evaluation has since been extended to call-by-value. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them. In this work, we define useful call-by-value evaluation inductively, proceeding in two stages. First, we refine the well-known Value Substitution Calculus, so the substitution operation becomes linear, yielding the \(\textsc {lcbv} \) calculus. The two calculi are observationally equivalent. We then further refine \(\textsc {lcbv} \) by restricting linear substitution only when it contributes to the progress of the computation, yielding the \(\textsc {ucbv} \) strategy. This new substitution notion is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we formally show that the resulting \(\textsc {ucbv} \) is a sound and complete implementation of \(\textsc {lcbv} \) , optimised to implement useful evaluation. As a further contribution, we show that the \(\textsc {ucbv} \) strategy can be implemented by an existing lower-level abstract machine called GLAMoUr with polynomial overhead in time. This entails, as a corollary, that \(\textsc {ucbv} \) is time-invariant, i.e., that the number of reduction steps to normal form in \(\textsc {ucbv} \) can be used as a measure of time complexity. Our \(\textsc {ucbv} \) strategy is part of the preliminary work required to develop semantic interpretations of useful evaluation, for which its inductive formulation is more suitable than the (non-inductive) existing ones.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Fresh Inductive Approach to Useful Call-by-Value

  • Pablo Barenbaum,
  • Delia Kesner,
  • Mariana Milicich

摘要

Useful evaluation is an optimised evaluation mechanism for functional programming languages, introduced by Accattoli and Dal Lago. The key to useful evaluation is to represent programs with sharing and to implement substitution of terms only when this contributes to the progress of the computation. Initially defined in the framework of call-by-name, useful evaluation has since been extended to call-by-value. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them. In this work, we define useful call-by-value evaluation inductively, proceeding in two stages. First, we refine the well-known Value Substitution Calculus, so the substitution operation becomes linear, yielding the \(\textsc {lcbv} \) calculus. The two calculi are observationally equivalent. We then further refine \(\textsc {lcbv} \) by restricting linear substitution only when it contributes to the progress of the computation, yielding the \(\textsc {ucbv} \) strategy. This new substitution notion is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we formally show that the resulting \(\textsc {ucbv} \) is a sound and complete implementation of \(\textsc {lcbv} \) , optimised to implement useful evaluation. As a further contribution, we show that the \(\textsc {ucbv} \) strategy can be implemented by an existing lower-level abstract machine called GLAMoUr with polynomial overhead in time. This entails, as a corollary, that \(\textsc {ucbv} \) is time-invariant, i.e., that the number of reduction steps to normal form in \(\textsc {ucbv} \) can be used as a measure of time complexity. Our \(\textsc {ucbv} \) strategy is part of the preliminary work required to develop semantic interpretations of useful evaluation, for which its inductive formulation is more suitable than the (non-inductive) existing ones.