Dear all,
The starting example of Sebastian showing again (as my previous example did) that eta-expansion
has semantic consequences in presence of call-time choice (ctc) non-deterministic is very interesting
because it comes from a real classroom exercise and proves that a good understanding of
ctc is important in practice . This is true even in absence of HO and has been an old issue in our FLP community that comes
back to 1996 (in this sense I think that the discussion thread of the Curry
mailing list that started in January 23 1997 has still some value, at least for younger people).
I think that for a proper discussion of ctc and its properties is a good idea to
adopt adequate formalizations of it.
I refer to two of them that are valid
for functional logic programming with non-strict ctc-non-deterministic functions (Curry, Toy).
To keep things easier, we consider fhe first order case.
1. One is our CRWL framework, which gives a semantics to
programs (TRS, left linear, constructor based, extra variables allowed).
I skip details here, but the point is that in CRWL,
given a TRS R, any expression e
has a denotation [|e|] which is the set of all partial constructor terms
t such that t is an approximation to a possible value of e
(technically, this means that e -> t is provable in the proof calculus of CRWL).
Any expression
has at least \bottom in its denotation.
The distributibity laws of Sebastian become very easily provable facts in CRWL,
expressing the laws in terms of denotations (and assuming ? defined by x?y = x x?y = y):
(a) [| f (e ? e') |] = [| f e ? f e' |]
More generally
(b) [| C[ f (e ? e') ] |] = [| C[f e ? f e'] |]
and also
(c) [| C[ e ? e'] |] = [| C[e] ? C[e'] |]
All of them can be also obtained as consequences of the easy fact
that [| e ? e' |] = [|e|] U [|e'|] (U is here set union)
and the following general result,
that can be seen as a fundamental property of ctc:
(d) [| C[e] |] = \bigcup_{t \in [| e |]} [| C[t] |]
(bigcup expresses union of the family of sets indexed by the given subindex)
These results extend also to HO-CRWL (an existing HO extension of CRWL)
and therefore we have also:
[| (e ? e') e'' |] = [| e e'' ? e' e'' |]
2. In a recent paper
(
http://gpd.sip.ucm.es/fraguas/papers/PPDP07.pdf, to be presented in PPDP07)
we have worked out a textual presentation of term graph rewriting
based on local bindings of the form let x=e in e' (not necessarily normalized),
and we have given a natural set of reduction rules for them that turn out to be
a convenient rewrite notion for ctc (we call it let-rewriting in the paper),
as demonstrated by the strong equivalence results that we have obtained
for let-rewriting and CRWL.
One of these results is: for any program, expression e and total c-term t we have
e -> t in CRWL (i.e. t \in [| e |] ) iff e ->* t in let-rewriting.
Due to the previous distributivity laws for CRWL and this equivalence, we obtain
distributive laws for let-rewriting in the style of Sergio. For instance:
C[f (e ? e')] ->* t iff C[f e ? f e'] ->* t
where ->* means here let-rewriting.
Hoping all this can be useful to someone,
Paco
----- Mensaje original -----
De: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Fecha: Martes, Junio 19, 2007 6:21 pm
Asunto: Confused Students
A: curry_at_lists.RWTH-Aachen.DE
> 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
>
********************************
Francisco J. Lopez Fraguas
Dep. Sistemas Informaticos y Computacion
Fac. Informatica U. Complutense Madrid
Prof. Jose Garcia Santesmases s/n
28040 Madrid
Spain
fraguas_at_sip.ucm.es
Tel: +34 91 3947630
Fax: +34 91 3947529
********************************
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Jun 22 2007 - 08:51:20 CEST