Previous Page
Strategies Specification
Non-Deterministic Computations
Rules Specifications
Modularity and parameterization
Next Page

ELAN - Non-deterministic Computations

In order to illustrate these constructions, let us write a program that computes the images by a given function f of every element occurring in an input list. Lists are defined in the following module, where the empty list is denoted by nil and the concatenation operator by . :
module list
sort Element List; end
operators global
a : Element;
b : Element;
c : Element;
nil : List;
@.@ : (Element List) List;

The list composed of elements a and b is thus represented by the term a.b.nil. Given a function f(@): (Element) Element, we define map-f(@): (List) Element by the following rewrite rules where element and list are respectively local variables of sort Element and List.
[head] map-f(element.list) => f(element) end
[tail] map-f(element.list) => map-f(list) end

Then we introduce a constant strategy operator mapStrat defined by the following strategy rule
[] mapStrat => iterate*(dc one(tail));dc one(head) end

mapStrat applied on map-f(a.b.c.nil) returns successively f(a), then f(b) and finally f(c). If f is defined as the identity on Element, we get a strategy called listExtract that extracts all elements of a list. This illustrates how the notion of strategy can be used to compute a set of normal forms without using explicitly a notion of set.