- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

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/panneReceived on Do Nov 05 1998 - 16:31:00 CET

*
This archive was generated by hypermail 2.3.0
: Mi Okt 21 2020 - 07:15:03 CEST
*