Hi list.
I think I have not explained our proposals correctly, because in fact we
already allow to declare sharing at the level of variables. You can do
it in the first of our two proposals for mixing call-time and run-time
choice in the same language.
== Run-time based proposal ==
More information in: [1]
https://gpd.sip.ucm.es/trac/gpd/wiki/GpdSystems/RtToy#Run-timechoicebasedvariant
We extend first order term rewriting with a let primitive to express
sharing, so we manipulate the same kind of let expressions of [2] "A
Simple Rewrite Notion for Call-time Choice Semantics"
(
http://portal.acm.org/citation.cfm?doid=1273920.1273947), but the
underlaying semantics is very different. Consider the program:
{{
X ? Y -> X
X ? Y -> Y
pair(X) -> (X, X)
}}
Under the rewriting notion of [2], that I will call ct-let-rewriting,
the step 'pair(0?1) -> (0?1, 0?1)' is not allowed, and the derivation
'pair(0?1) -> let X = 0 ? 1 in pair(X) -> let X = 0 ? 1 in (X, X)' must
be performed in order to get (the equivalent to) a head normal form.
Then in ct-let-rewriting let bindings are introduced during the
computations and a call-time choice semantic as expressed in CRWL, the
Launchbury-style calculus and the graph rewriting of Echahed is obtained.
On the other hand, with the rewriting notion of [1], that I will call
rt-let-rewriting, the step 'pair(0?1) -> (0?1, 0?1)' is perfectly
allowed, and the only sharing you have is the one that you specify with
let bindings, in the program or in the expressions to evaluate. Although
some lets are introduced by computations, those do not introduce more
sharing as they are added for subexpressions of expressions which where
already shared.
So, __we indicate sharing at the level of variables__. If you can share
variables then you can share particular arguments of functions, by
sharing each of its variables. For example for the function g1 defined by:
g1(X,Y) -> let Z = X in (Z, Z, Y, Y)
you have that g1(0?1,0?1) can be reduced to (0, 0, 0, 1) but not to (0,
1, 0, 1): the first argument is shared but it is not the case for the
second. You can do it also for arguments with more complex patterns, or
do it for all the arguments. In [1] we call this language with lets "the
core language" and propose to annotate the functions as ct or rt. Only
for ct functions, we perform a simple transformation introducing one let
in the right-hand side of each program rule for each variable in the
left hand side of the rule. We also have a formal proof that this
transformation leads to call-time choice.
The moral is: if you can share variables you can have call-time choice
for particular arguments of functions (sharing each variable of the
corresponding argument in each program rule for that functions) and then
you can have call-time choice for functions. We think that the
discipline of expressing the call-time choice behavior at the level of
functions --- either at the level of call-time choice functions or at
the level of call-time choice arguments --- helps to improve the
readability of the code.
Anyway our prototype in [1] implements just the core language, not the
function annotations, and it does it by extending Toy, by tweaking the
suspension mechanism. Therefore we are in a HO context. Instead of using
lets we use where, as this construction was already present in the
syntax of Toy. We could express the original problem Wolfgang proposed
as follows:
{{
infixr 5 //
X // Y = X
X // Y = Y
data arb' A = arb' A
arb'' (arb' F) = G where G=F
inst'Arb'Bool = arb' arb'Bool
arb'Bool = false // true
arbP2' Da Db = (arb'' Da, arb'' Db)
arbL2' Da = [arb'' Da, arb'' Da]
g1 = arbL2' (inst'Arb'Bool)
}}
Here we assume a translation to core where all functions had been
annotated as call-time except arbP2' and arbL2'. That is why a where
binding is added to the right-hand side of the rule for arb''. The
prototype behaves as follows:
Toy> g1 == V
{ V -> [ false, false ] }
Elapsed time: 0 ms.
sol.1, more solutions (y/n/d/a) [y]?
{ V -> [ false, true ] }
Elapsed time: 0 ms.
sol.2, more solutions (y/n/d/a) [y]?
{ V -> [ true, false ] }
Elapsed time: 0 ms.
sol.3, more solutions (y/n/d/a) [y]?
{ V -> [ true, true ] }
Elapsed time: 0 ms.
sol.4, more solutions (y/n/d/a) [y]?
no
Elapsed time: 0 ms.
== Call-time based proposal ==
More information in: [2]
https://gpd.sip.ucm.es/trac/gpd/wiki/GpdSystems/RtToy#Call-timechoicebasedvariant
Here we have another core language, where we assume that we can annotate
the function symbols with a ^rt mark, so they are treated like
constructor symbols for the call-time choice mechanism. That is, any
expression containing just variables, constructor symbols and ^rt-marked
functions symbols can be freely copied: in other words, can be unshared.
Appart from that ^rt mark we have a regular call-time choice FLP language.
Our implementation in Toy, also based in some tweaking of suspensions,
provides a primitive rt/1 that puts the ^rt mark in every function
symbols appearing in its only arguments. We can also use this prototype
to implement Wolfgang's example:
{{
infixr 5 //
X // Y = X
X // Y = Y
data arb' A = arb' A
arb'' (arb' F) = F
inst'Arb'Bool = arb' (rt arb'Bool)
arb'Bool = false // true
arbP2' Da Db = (arb'' Da, arb'' Db)
arbL2' Da = [arb'' Da, arb'' Da]
g1 = arbL2' inst'Arb'Bool
}}
Note the use of the primitive rt in the definition of inst'Arb'Bool.
There you can also find the only use of the constructor arb', appart
from its use in a pattern in the definition of arb'', so it is pretty
close to treating it as a rt-constructor in the spirit of Wolfgang's
proposal. The prototype behaves as follows:
Toy> g1 == V
{ V -> [ false, false ] }
Elapsed time: 0 ms.
sol.1, more solutions (y/n/d/a) [y]?
{ V -> [ false, true ] }
Elapsed time: 0 ms.
sol.2, more solutions (y/n/d/a) [y]?
{ V -> [ true, false ] }
Elapsed time: 0 ms.
sol.3, more solutions (y/n/d/a) [y]?
{ V -> [ true, true ] }
Elapsed time: 0 ms.
sol.4, more solutions (y/n/d/a) [y]?
no
Elapsed time: 0 ms.
We could also add another function to see how sharing interacts with this:
{{
tShar [X, Y] = (X, X, Y, Y)
g1tShar = tShar g1
}}
The prototype behaves as follows:
Toy> g1tShar == V
{ V -> (false, false, false, false) }
Elapsed time: 0 ms.
sol.1, more solutions (y/n/d/a) [y]?
{ V -> (false, false, true, true) }
Elapsed time: 0 ms.
sol.2, more solutions (y/n/d/a) [y]?
{ V -> (true, true, false, false) }
Elapsed time: 0 ms.
sol.3, more solutions (y/n/d/a) [y]?
{ V -> (true, true, true, true) }
Elapsed time: 0 ms.
sol.4, more solutions (y/n/d/a) [y]?
no
Elapsed time: 0 ms.
We still have sharing of X and Y in tShar, as expected in a call-time
choice framework.
In conclusion
- Two possible designs: in a run-time choice environment you only
need a let primitive that expresses sharing, and in a call-time choice
enviroment, a ^rt mark to destroy sharing.
- The call-time choice based approach maybe could be used to
implement Wolfgang's proposal.
- This can be achieved by tweaking suspensions, although that will
cause a lot of reevaluation, that maybe could be avoided by using
sharing accross non-determinism in KICS style.
- Later you can add some sugar to express sharing at the level of
function arguments, or functions, to get programs more easy to understand.
- We think that the run-time choice based approach is more
expressive, for example, how could you express the following program in
the call-time choice based approach?
f X = (Y,X) where Y=X % X is used once shared and once unshared
g (X,Y) = (X,X,Y,Y)
g(f(coin)) can be reduced to (0,0,0,1),
(0,0,0,1),...,(1,1,0,0),(1,1,0,1),...,(1,1,1,1) but not to (0,1,0,0)
This is a quite artificial example but anyway the ^rt marks in an
expression do not grant a full run-time choice behaviour for that,
because new function symbols appearing during the evaluation of that
expresssion are not obligued to have the ^rt mark too.
Greetings,
Juan
--
------------------------------------------------------------------------
Juan Rodríguez Hortalá
Grupo de Programación Declarativa / Declarative Programming Group
E-Mail : juanrh_at_fdi.ucm.es
Home Page: http://gpd.sip.ucm.es/juanrh/
Tel: + 34 913947646
Despacho / Office: 220 (2ª planta / 2nd floor)
Dept. Sistemas Informáticos y Computación / Department of Computer
Systems and Computing
Universidad Complutense de Madrid
Facultad de Informática
C/ Profesor José García Santesmases, s/n
E - 28040 Madrid. Spain
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Aug 31 2009 - 16:00:45 CEST