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

From: Juan Rodriguez Hortala <juanrh_at_fdi.ucm.es>

Date: Mon, 31 Aug 2009 15:03:59 +0200

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

Date: Mon, 31 Aug 2009 15:03:59 +0200

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/curryReceived on Mo Aug 31 2009 - 16:00:45 CEST

*
This archive was generated by hypermail 2.3.0
: Mo Okt 26 2020 - 07:15:04 CET
*