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

From: Jan Christiansen <jac_at_informatik.uni-kiel.de>

Date: Fri, 17 Dec 2010 13:42:10 +0100

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 Fri Dec 17 2010 - 13:51:45 CET

Date: Fri, 17 Dec 2010 13:42:10 +0100

I have moved this topic to a new thread.

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 Fri Dec 17 2010 - 13:51:45 CET

*
This archive was generated by hypermail 2.3.0
: Thu Nov 14 2019 - 07:15:07 CET
*