TL;DR
This paper analyzes pull-tabbing, an evaluation method for functional logic programming, proving its correctness and formal properties, and highlighting its advantages over other non-deterministic choice handling techniques.
Contribution
It formally defines the pull-tab transformation, characterizes applicable programs, and proves the correctness of extended computations, advancing understanding of this evaluation approach.
Findings
Pull-tabbing avoids irrevocable non-deterministic choices.
The transformation is correct for a specific class of programs.
Pull-tabbing does not require upfront cloning of large contexts.
Abstract
Pull-tabbing is an evaluation approach for functional logic computations, based on a graph transformation recently proposed, which avoids making irrevocable non-deterministic choices that would jeopardize the completeness of computations. In contrast to other approaches with this property, it does not require an upfront cloning of a possibly large portion of the choice's context. We formally define the pull-tab transformation, characterize the class of programs for which the transformation is intended, extend the computations in these programs to include the transformation, and prove the correctness of the extended computations.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.