I have moved this topic to a new thread.
>> By the way right now I think that you also have to use multisets if
>> you want to assign a denotational semantics to recursive let
>> expressions like they are implemented by Kics and PAKCS.
> Would nested set-based nondeterminism suffice?
I don't think so. In fact I was too eager when I suspected that
multisets would work. I only know that sets do not. There is a paper
called "Counterexamples to Simulation in Non-Deterministic Call-by-
Need Lambda-Calculi with letrec" (
http://www.ki.informatik.uni-frankfurt.de/papers/schauss/simcounter-IB38.pdf
). The authors consider a language which is quite similar to Curry.
Sadly they did not know Curry and use an imaginary language with
Haskell syntax for examples.
The authors present the following functions s1 and s2. These functions
yield the same results for all lists xs in a set-based semantics. Note
that we can replace seq by a simple function on lists as well.
s1 :: [Bool] -> [Bool]
s1 xs = False:seq xs [False] ? seq xs [False,True]
s1 :: [Bool] -> [Bool]
s2 xs = False:seq xs [False] ? False:seq xs [True] ? seq xs
[False,True]
If we use these functions in the context of a recursive let expression
the semantics of the resulting expressions differ.
s1rec = let xs = s1 xs in xs
s2rec = let xs = s2 xs in xs
We have head (tail s1rec) = False ? _|_ and head (tail s2rec) =
False ? True ? _|_. This demonstrates that there is no compositional
set-based denotational semantics for recursive let expressions. As
this example does only use flat non–determinism it also shows that a
model with non-flat set-based non–determinism does not work. If I now
think about it I would suspect that even a multiset approach does not
work.
Cheers, Jan
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 17 2010 - 13:51:45 CET