Demand Analysis with Partial Predicates

TL;DR

This paper presents a unified semantic framework for demand analysis using partial predicates, offering new insights into its relation with other analyses, and introduces innovative methods including set constraint-based analysis and program transformation for implementation.

Contribution

It introduces a concise, unified semantic framework for demand analysis with partial predicates, relating it to other analyses and proposing new implementation techniques.

Findings

Demand analysis can be formalized using partial predicates in a semantic framework.

A set constraint-based analysis was derived using program transformation ideas.

Program transformation can be used to perform demand analysis in complex property domains.

Abstract

In order to alleviate the inefficiencies caused by the interaction of the logic and functional sides, integrated languages may take advantage of \emph{demand} information -- i.e. knowing in advance which computations are needed and, to which extent, in a particular context. This work studies \emph{demand analysis} -- which is closely related to \emph{backwards strictness analysis} -- in a semantic framework of \emph{partial predicates}, which in turn are constructive realizations of ideals in a domain. This will allow us to give a concise, unified presentation of demand analysis, to relate it to other analyses based on abstract interpretation or strictness logics, some hints for the implementation, and, more important, to prove the soundness of our analysis based on \emph{demand equations}. There are also some innovative results. One of them is that a set constraint-based analysis has been derived in a stepwise manner using ideas taken from the area of program transformation. The other one is the possibility of using program transformation itself to perform the analysis, specially in those domains of properties where algorithms based on constraint solving are too weak.