Liveness and reducibility

[xekoukou]

We have defined the reducibility type that describes the type of the environment that is required so that the actor would be reducible.

At the same time, the actor could reduce internally without any interaction with the environment.

If the actors, can be reducible externally an infinite amount of times, then a liveness property would mean that there is a natural namber n after which it reduces externally.

All actors should have this live property. What conditions should be set to the environment , so that the actor is infinitely reducible????

[xekoukou]

We could encode liveness in the composition && operator by saying that after n turns, if the reducibility type guarantees external (between the two) reducibility , then we reduce externally for this step.

If after n turns, we cant guarantee reduction, we wait till we do.

Maybe n should be an N + infinite, so that we disable liveness when we do not want to use it.

Does this have the same semantics with the previous definition?

[xekoukou]

If we are provided a sequence of abstract numbers, then we could very easiliy define liveness in the && (parallel) operator, as discussed above. That liveness though is between the two systems A , B which are composed. Which means that the order of parallel composition will change the liveness guarantess we are providing. (A && B) && C is not equal to A && (B && C).

The reason is that we have defined liveness between the two systems. Is there a way to solve this problem?

[xekoukou]

We need to have a stream of natural numbers for each system, and then when we compose two systems, to take the minimum of the two.

It needs more thought, but I think this fixes the problem, and it makes more semantically clear.

This number n tells us that a system A will prioritize interaction with its environment after n steps.