Suspending in or-nodes

From: Sven Panne <Sven.Panne_at_informatik.uni-muenchen.de>
Date: Thu, 05 Nov 1998 16:27:03 +0100

Perhaps someone on this list can enlighten me a little bit: It's not
clear to me why an entire disjunction must suspend when one disjunct
suspends. Reading Michael Hanus' POPL97 paper
(http://www-i2.informatik.rwth-aachen.de/~hanus/publications/papers/POPL97.dvi.Z)
didn't help me either. :-( Example 3.5 in this paper is supposed to
show the reason for this, but it is not "real Curry" (no definitions
for /\ and the = with a dot). There are at least two readings, so which
one was intended? Here the first one:

--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--

-- und is called /\ in the paper
-- Definitional tree:
-- or(branch(und x1 x2, 1, rigid, rule(und True x2 = x2))
-- branch(und x1 x2, 2, rigid, rule(und x1 True = x1)))

und :: Bool -> Bool -> Bool;
und eval rigid;
und True x = x;
und x True = x;


data T = A | B;

-- eq is called = with a dot in the paper and polymorphic

eq :: T -> T -> Bool;
eq eval flex;
eq A A = True;
eq A B = False;
eq B A = False;
eq B B = True;


-- Intended definitional tree for p (hack below):
-- or(branch(p x1 x2, 1, rigid, rule(p A x2 = True))
-- branch(p x1 x2, 2, flex, rule(p x1 B = True)))

p :: T -> T -> Bool;
p x y = isA x;
p x y = isB y;

isA :: T -> Bool;
isA eval rigid;
isA A = True;

isB :: T -> Bool;
isB eval flex;
isB B = True;

-- critical goal:
goal x = und (p x x) (eq x A);

--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--

As the current Curry version does not allow the specification of
definitional trees anymore, I had to resort to the (hopefully
equivalent) isA/isB-hack. And here the second reading:

--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--

data T = A | B;

-- Intended definitional tree for p (hack below):
-- or(branch(p x1 x2, 1, rigid, rule(p A x2 = {}))
-- branch(p x1 x2, 2, flex, rule(p x1 B = {})))

p :: T -> T -> Constraint;
p x y = isA x;
p x y = isB y;

isA :: T -> Constraint;
isA eval rigid;
isA A = {};

isB :: T -> Constraint;
isB eval flex;
isB B = {};

-- critical goal:
goal x = {p x x, x = A};

--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--SNIP--

If I read the operational semantics given in the Curry report
correctly, there is no way how substitutions from one disjunct can
affect the other one, so what's the problem?

Of course things get incomplete when you simply commit to the
non-suspending disjunct and forget about the suspending one. Simply
keep the latter one as it is, as flexible branches similarly keep
suspending RHSs.

Hopefully not writing complete nonsense, :-}
   Sven

-- 
Sven Panne                                        Tel.: +49/89/2178-2235
LMU, Institut fuer Informatik                     FAX : +49/89/2178-2211
LFE Programmier- und Modellierungssprachen              Oettingenstr. 67
mailto:sven.panne_at_informatik.uni-muenchen.de            D-80538 Muenchen
http://www.pms.informatik.uni-muenchen.de/mitarbeiter/panne

Received on Do Nov 05 1998 - 16:31:00 CET