Clairvoyance semantics and demand semantics are both pure and time-cost equivalent to lazy evaluation, offering alternatives to the stateful natural semantics of lazy evaluation for analyzing computation cost. Unfortunately, clairvoyance semantics is simple but hard to execute, and demand semantics is executable but complicated. In this paper, we propose a novel approach for unifying these two semantics using functional logic programming. We propose (1) a logical clairvoyance translation, which translates lazy functional programs to functional logic programs where the computation cost is reified, and (2) a logical demand translation, which is a simple extension to the logical clairvoyance translation. We prove that these two translations correctly implement clairvoyance and demand semantics respectively using Agda. We also conduct case studies on examples including insertion sort and Okasaki’s banker’s queue using Curry/KiCS2 to show how these translations can be used in practice.

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

Unifying Hindsight and Foresight

  • Nicholas Coltharp,
  • Steven Libby,
  • Laura Israel,
  • Yao Li

摘要

Clairvoyance semantics and demand semantics are both pure and time-cost equivalent to lazy evaluation, offering alternatives to the stateful natural semantics of lazy evaluation for analyzing computation cost. Unfortunately, clairvoyance semantics is simple but hard to execute, and demand semantics is executable but complicated. In this paper, we propose a novel approach for unifying these two semantics using functional logic programming. We propose (1) a logical clairvoyance translation, which translates lazy functional programs to functional logic programs where the computation cost is reified, and (2) a logical demand translation, which is a simple extension to the logical clairvoyance translation. We prove that these two translations correctly implement clairvoyance and demand semantics respectively using Agda. We also conduct case studies on examples including insertion sort and Okasaki’s banker’s queue using Curry/KiCS2 to show how these translations can be used in practice.