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

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Tue, 19 Jun 2007 18:17:12 +0200

Dear Friends of Curry!

Consider the following exercise: In Curry, directed graphs can be

represented as (non-deterministic) successor relation of

type Graph a = a -> a

For example, the graph {(1,2),(1,3),(2,4),(3,4)} can be represented

as operation

succ :: Graph Int

succ 1 = 2; succ 1 = 3; succ 2 = 4; succ 3 = 4

Define operations "undir :: Graph a -> Graph a" and "path :: Graph a -

* > a -> a -> [a]" that compute an undirected graph from a directed
*

one and a path between two given nodes, respectively. One possibility

to solve this exercise is

inv, undir :: Graph a -> Graph a

inv g x | x =:= g y = y where y free

undir g x = g x

undir g x = inv g x

path :: Graph a -> a -> a -> [a]

path g x y | (y:ys) =:= search g [x] = reverse (y:ys) where ys free

search :: Graph a -> [a] -> [a]

search _ xs = xs

search g xs | not (x `elem` xs) = search g (x:xs) where x = g (head

xs) -- no cycles in path

With this definitions, the expression

path (undir succ) 2 3

non-deterministically evaluates to [2,1,3] or [2,4,3] like one would

expect. Many students, however, come up with a slightly different

definition of undir (In a first try, I wrote this myself):

undir g = g

undir g = inv g

With this definition, the expression above has no result rather than

two. Instead of an undirected graph, path is applied to the graph

succ and its inverse non-deterministically due to call-time choice.

The other day, Paco showed us that eta-expansion is incorrect in

presence of non-determinism:

g x = 0

h x = 1

fcoin = g

fcoin = h -- fcoin is a 'functional coin'

The above example differs in that there is nothing a Haskell

programmer would consider a constant, but I admit that it's a minor

difference. My reason to post this example is: I consider it a nice

little program that shows that Curry programmers need to be aware of

the rule Bernd once called the essential property of call-time choice:

f (x?y) = f x ? f y

With this in mind, you soon recognize that

path (undir succ)

should be different from

path (succ ? inv succ)

which is equivalent to

path succ ? path (inv succ)

according to the rule above. I think, only with this rule in mind you

get a clue why the two definitions of undir have different meanings

although they only differ w.r.t. eta-expansion.

I'm looking forward to explaining this to my students ;)

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Jun 20 2007 - 08:56:24 CEST

Date: Tue, 19 Jun 2007 18:17:12 +0200

Dear Friends of Curry!

Consider the following exercise: In Curry, directed graphs can be

represented as (non-deterministic) successor relation of

type Graph a = a -> a

For example, the graph {(1,2),(1,3),(2,4),(3,4)} can be represented

as operation

succ :: Graph Int

succ 1 = 2; succ 1 = 3; succ 2 = 4; succ 3 = 4

Define operations "undir :: Graph a -> Graph a" and "path :: Graph a -

one and a path between two given nodes, respectively. One possibility

to solve this exercise is

inv, undir :: Graph a -> Graph a

inv g x | x =:= g y = y where y free

undir g x = g x

undir g x = inv g x

path :: Graph a -> a -> a -> [a]

path g x y | (y:ys) =:= search g [x] = reverse (y:ys) where ys free

search :: Graph a -> [a] -> [a]

search _ xs = xs

search g xs | not (x `elem` xs) = search g (x:xs) where x = g (head

xs) -- no cycles in path

With this definitions, the expression

path (undir succ) 2 3

non-deterministically evaluates to [2,1,3] or [2,4,3] like one would

expect. Many students, however, come up with a slightly different

definition of undir (In a first try, I wrote this myself):

undir g = g

undir g = inv g

With this definition, the expression above has no result rather than

two. Instead of an undirected graph, path is applied to the graph

succ and its inverse non-deterministically due to call-time choice.

The other day, Paco showed us that eta-expansion is incorrect in

presence of non-determinism:

g x = 0

h x = 1

fcoin = g

fcoin = h -- fcoin is a 'functional coin'

The above example differs in that there is nothing a Haskell

programmer would consider a constant, but I admit that it's a minor

difference. My reason to post this example is: I consider it a nice

little program that shows that Curry programmers need to be aware of

the rule Bernd once called the essential property of call-time choice:

f (x?y) = f x ? f y

With this in mind, you soon recognize that

path (undir succ)

should be different from

path (succ ? inv succ)

which is equivalent to

path succ ? path (inv succ)

according to the rule above. I think, only with this rule in mind you

get a clue why the two definitions of undir have different meanings

although they only differ w.r.t. eta-expansion.

I'm looking forward to explaining this to my students ;)

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Jun 20 2007 - 08:56:24 CEST

*
This archive was generated by hypermail 2.3.0
: Mo Feb 06 2023 - 07:15:09 CET
*