Internal vs external reducibility type

[xekoukou]

We currently have a type that determines the conditions under which a system/actor is reducible.

We need to split this type into two types, to account for internal vs external reducibility. The first occurs between the components of the system, while the other requires the environment to have a specific shape.

[xekoukou]

Let us assume that we use scope to split the reducibility type into inner and external. It seems that there might be cases that would force us to scope the two systems once again. Will we have inner1 and inner2?

It seems to me that since we scope things on two different secrets, then inner1 and inner2 do not interact, thus simply putting them in parallel would be acceptable. inner1 && inner2.

But I need to prove a theorem for this. To show that scope checking all secrets at the same time or one at a time creates reducibility types that are equivalent.

[xekoukou]

The reducibility type is used to inform us of the same of the environment, that would allow the system to always reduce. The inner type has no environment, thus its information is useless, all we need to know is whether it reduces on itself or not.

[xekoukou]

At the moment , I am preserving the info on the internal type, and I expect it will be truncated when I define equality. I have to define the subtyping relations if I have any change to remove this information. The subtyping rules are those that will inform us of its reducibility, thus it will allow us to truncate. We need to know if it reduces or not.

[xekoukou]

Now that I have defined what it means for something to be self reducible, I believe that I can replace the internal type with the self- reducibility proposition.