[m-dev.] Proposal: sequence quantification

Peter Schachte schachte at cs.mu.OZ.AU
Wed Jan 3 11:49:29 AEDT 2001


We propose a specialized form of quantification that fills the roles
of the map/fold/filter higher order predicates (and all their
combinations) in a flexible and convenient way.

================================================================

In Mercury, we can write:

	all [X] ( q(X) => p(X) )

which states that every X that satisfies q also satisfies p.  For
example:

	all [X] ( member(X, List) => X = 0 )

would check that every element of List is 0.  Unfortunately, we cannot
use this to generate List.  In Mercury, universal quantification is
turned into negation, so it cannot bind variables.  This example would
be translated to

	\+ ( member(X, List), \+ X = 0 )

so it cannot nondeterministically generate lists of 0's.  A more
interesting case is

	all [I] ( between(1, 10, I) => index1(List, I, I) )

which checks that List is the list [1,2,3,4,5,6,7,8,9,10] (assume
between(X,Y,Z) has the semantics X =< Z, Z =< Y, and has a mode
between(in, in, out) is nondet).  Again, sadly, this cannot be used to
generate List.

The problem is the translation to negation (backtracking); the
solution is instead to translate to iteration.  This was proposed by
Jonas Barklund and Johan Bevemyr under the name "bounded
quantification."  The above examples included numbers and lists;
Barklund and Bevemyr were particularly interested in arrays.  In fact,
any finitely enumerable set can be used.  The idea is to include a
specification of the range of the quantified variable in the
quantification, so it can be implemented iteratively.

By subtly restricting what we can quantify over, we can make bounded
quantification still more useful.  If we restrict ourselves to
quantifying over *sequences*, we can use a rich algebra of operations
on sequences to extend the expressiveness of bounded quantification.

The syntax we propose for sequence quantification is:

	for Var in Sequence :: Goal

where Goal will usually contain Var.  Logically, this means

	all [Var] ( member(Var,Sequence) => Goal ).

Operationally, it is implemented as iteration over Sequence in order,
binding a fresh instance of Var to each element of Sequence in turn
and executing Goal.

This facility becomes much more powerful when sequences are modified
and combined.  The most useful operation on sequences we will consider
is zip (as in Haskell, not Mercury's list__zip).  Zip combines two or
more sequences to create a single sequence of tuples.  We will shortly
present some syntactic sugar which removes the need for an explicit
zip operation, so we will not go into details about zip, except to
point out that zip requires all its arguments, as well as its value,
to be sequences of the same length.  Zip allows us to iterate over
multiple sequences in lock step.  For example,

	for {P,S} in zip(Preds, Succs) :: S = P + 1

states that Succs is a sequence each of whose elements is one greater
than the corresponding element of Preds, and both sequences have the
same length.

Since it is likely to be very common to iterate over multiple
sequences, we support a more convenient syntax.  The above example
could also be written as

	for P in Preds as S in Succs :: S = P + 1

This is equivalent to

	list__map((pred(P::in,S::out) is semidet :- S = P + 1), Preds, Succs)

except that it generalizes to mapping over more than two sequences
without having to write new mapping predicates, and doesn't require
mode annotations.  Also, the quantifier version handles more modes
than list__map has declared.  This is an important point:  the above
example can be used to compute the successors from the predecessors or
vice-versa.  This permits the predicate that includes this sequence
quantification to be used in multiple modes.

Another example using this syntax:

	for _ in List as _ in 1..Len :: true

Here, 1..Len specifies the obvious arithmetic sequence, so this
example specifies that the length of List is Len.  In the mode where
List is supplied and Len is not, we are generating part of the
sequence 1..Len (namely, Len) in the quantification.  The makes use of
the fact that the `as' operator insists that the sequences involved be
of the same length.

These examples relate corresponding elements of different sequences,
but do not allow information to be communicated between different
sequence elements.  A simple trick can provide that facility.
Consider the predicate diag/3:

	diag(Fin, Fin, []).
	diag(Ini, Fin, [{Ini,Nxt}|Rest]) :-
		diag(Nxt, Fin, Rest).

This predicate holds for any list of pairs for which the first part of
the first element (if there is one) is Ini, and the second part of the
last element (if there is one) is Fin, and for every i between 2 and
the length of the list, the second part of element i-1 is identical to
the first part of elemnt i.  diag/3 does not put any constraints on
the relationship between the two parts of any pair in the list.

The logic of this predicate is what we need, but unfortunately
Mercury's mode system will not allow this predicate to be used to
generate its third argument, as we need.  However, our actual
implementation will not be in terms of diag/3, so this is not
important.  Diag/3 is introduced only to explain the semantics.
We can, for example, use this predicate together with sequence
quantification to sum a sequence as follows:

	diag(0, Sum, D), for E in List as {S0,S} in D :: S = S0 + E

Again, this construct seems important enough to warrant some special
syntax; the follow goal is equivalent to the one above:

	for E in List as S initially 0 finally Sum :: next S = S + E

Here the `next' prefix operator must be followed by a variable name;
together this term specifies the second part of the pair, while the
unadorned variable specifies the first part.  The `S initially 0
finally Sum' construct is equivalent to `{S,next S} in D' where
`diag(0, Sum, D)' holds, and `next S' is just a funny variable name.

Generally the quantified goal will compute `next S' from S in some
way, but it need not.  For example, one could find the last element of
a sequence like this:

	for E in Sequence as Curr initially no finally yes(LastElt) ::
		next Curr = yes(E)

This will bind LastElt to the last element of Sequence, or fail if
Sequence is empty.

There are several ways to create sequences from other sequences,
extending the capabilities of sequence quantification.  The simplest
of these is concatenation, which is performed with the `followed_by'
operator:

	for E in List1 followed_by List2 as S in Result :: S = E + 1

This makes Result a list of the successors of the elements of List1
followed by those of List2.

A more useful operation is filtering, performed by the `when' operator:

	for E in List when E > 0 as R in Result :: E = R

This says that Result is the elements of List which are greater than
0.  This is equivalent to a call to list__filter.  A more interesting
example is:

	for P in List when P > 0 
	 as N in List when N < 0 
         as S in Result 
	 :: S = P + N

which says that Result is the sequence of sums of the corresponding
positive and negative elements of List.  The `when' operator employs a
bit of syntactic sugar:  `E in List when E > 0' is equivalent to `E in
filter(List, (pred(X::in) is semidet :- X > 0))', but easier to write.

Similar are `while' and `until', which take the front of a sequence up
to but not including the first element for which a condition fails
(succeeds).  For example:

	for E in List while E >= 0 as S initially 0 finally Sum 
		:: next S = S + E

or equivalently,

	for E in List until E < 0 as S initially 0 finally Sum 
		:: next S = S + E

which sum the elements of List up to the first negative element.
Nonnegative elements of List following the first negative one are not
summed.  Again, this construct is syntactic sugar for a simple
higher-order sequence operation which takes the front of the sequence.

Similarly, the `once' operator drops the front of the sequence up to
the point that a predicate holds, for example:

	for E in List once E >= 0 as S initially 0 finally Sum 
		:: next S = S + E

would sum all the elements of List beginning with the first
nonnegative one.

Of course, users can write their own sequence operations.

It was intended that sequence quantification be implemented on a
sequence type class.  Unfortunately, it appears that constructor
classes are needed, and Mercury does not yet support them.  Therefore,
we propose to initially implement sequence quantification only for
lists.  This is a shame, but the generalization to sequences should be
straightforward once constructor classes are supported.

There are a few small issues of syntax to be considered, but (since
syntax issues are so divisive) I'll address them later.

-- 
Peter Schachte <schachte at cs.mu.OZ.AU>  A billion here, a couple of billion
http://www.cs.mu.oz.au/~schachte/      there -- first thing you know it adds
Phone:  +61 3 8344 9166                up to be real money.
Fax:    +61 3 9348 1184                -- Senator Everett McKinley Dirksen 
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------



More information about the developers mailing list