Encapsulated search does not encapsulate (all) non-determinism

From: Wolfgang Lux <lux_at_wi.uni-muenster.de>
Date: Tue, 08 Jan 2002 15:36:17 +0100

Dear colleagues,

I'd like to wish you a happy new year and let you share an interesting
experience I had with the encapsulated search.

The encapsulated search was introduced into Curry in order to encapsulate
non-deterministic computations and allow to use different search strategies.
However, in the presence of sharing not all non-determinism can be
encapsulated. Consider the following simple program:

  coin = 0
  coin = 1

  main = findall (\x -> x=:=y) where y = coin

where findall computes and unpacks all solutions of a search goal with a depth
first strategy. In a system based on pure term rewriting, evaluating the goal
main would yield the list [0,1].

In Curry we must not evaluate the non-local shared application for y inside
the encapsulated search but must evaluate it in the global search space. This
is similar to a non-local variable which must not be bound inside an
encapsulated search. Thus, the non-determinism in the function coin
``escapes'' from the encapsulated search and we get two solutions for the
goal main, namely [0] and [1].

A slight variation of the main function shows better why we must not evaluate
non-local applications in an encapsulated search:

  main' = filter (/= y) (findall (\x -> x=:=y)) where y = coin

The only sensible solution I can think of is two times the empty list.

Maybe this was already obvious to you, but the report is totally ignorant
about this. IMHO it should at least include a comment about this (writing
down a semantics seems quite tricky and is impossible in the framework
used by appendix D as there is no explicit notion of sharing).

This problem can also creep in if you are used to higher-order programming.
For instance the following program will not compute a list of all solutions
for the function coin but -- like the initial example -- compute both
solutions non-deterministically (except if you expect the compiler to
perform some global sharing analysis and detect that the first argument of
the function same is never going to be shared).

  coin = 0
  coin = 1

  main = findall (same coin)
  same x y = x =:= y


Wolfgang Lux				  Phone: +49-251-83-38263
Institut fuer Wirtschaftinformatik	    FAX: +49-251-83-38259
Universitaet Muenster		      Email: wlux_at_uni-muenster.de
curry mailing list
Received on Di Jan 08 2002 - 17:47:52 CET

This archive was generated by hypermail 2.3.0 : So Jul 05 2020 - 07:15:03 CEST