Confused Students

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

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:09 CEST