INDY Partial Evaluator

INDY v1.8

Integrated Narrowing-Driven specialization system

A Partial Evaluator for Functional Logic Programs

The system INDY is a rather concise implementation of the narrowing-driven partial evaluator originally introduced in [AFV96]. It implements the different instances of the algorithm which have been presented in [AFV98] (based on innermost narrowing), [AFJV97] (based on lazy narrowing), and [AHLV98] (based on needed narrowing), as well as the control improvements of [AAFJV98]. It is written in SICStus Prolog and is publicly available.

In contrast to the approach usually taken with pure functional languages, INDY uses the unification-based computation mechanism of narrowing for specialization. This coincides with the usual execution mechanism of functional logic languages, which allows us to deal with expressions containing partial information by means of logical variables and unification in a natural way, as well as to consider efficient evaluation strategies and include a deterministic simplification phase.

INDY is parametric w.r.t. the narrowing strategy which is used for the automatic construction of (finite) narrowing trees. The specializer also performs a post-processing renaming phase which allows us to automatically fulfill the independence condition as well as to avoid the restriction to specialize only patterns. This renaming technique can be found in [AFJV97]. The inclusion of primitive function symbols (and, in particular, the conjunctive operator) in input calls poses specific control problems that require an special treatment in order to achieve a good specialization (see [AAFJV98] ).

The user can adapt the following settings:

Unfolding rule: one of the following three strategies can be selected to control the construction of the local trees:

emb_goal: the nonembedding unfolding rule, which uses the homeomorphic embedding ordering to stop the construction of the narrowing trees;

emb_redex: this unfolding rule uses a dynamic narrowing selection strategy to determine the set of positions to be unfolded by a don't-care selection within a conjunction. It implements the dependency_clash test of [AAFJV98] using homeomorphic embedding on comparable ancestors of selected redexes to ensure finiteness;

comp_redex: it differs from emb_redex in that comp_redex uses a simpler definition of dependency_clash based on comparable ancestors of selected redexes as a whistle;

depthk: a depth-k bound strategy, which expands derivations down to the depth-k frontier of the tree.

Narrowing strategy: the default option is needed narrowing; otherwise, the user can select a lazy (call-by-name) narrowing strategy or an innermost (call-by-value) narrowing strategy.

Normalization: when it is switched on, normalization of the goal is performed between narrowing steps. There exists the possibility to use only a subset of the program rules for normalization. This distinction is useful when non-terminating programs are considered, since the (possibly empty) terminating subset of the program rules can be safely used for simplification.

Splitting: by setting the splitting strategy on, the partition of expressions containing primitive function symbols is allowed (in order to avoid unnecessary generalization).

A detailed user manual describing the system and the use of INDY is available.

You can get the INDY system here (30k).

ELP

GPLIS

DSIC

UPV

Last update Nov 98 # gvidal (at) dsic (dot) upv (dot) es