— The original motivation for studying extrusive posets was to study capabilities. Speaking colloquially a capability is a ‘thing’ that an ‘agent’ is able to do.
For instance, many companies and organizations stratify employees into various levels of security clearance, where different clearance levels grant access to different pieces of information, locations, or people. We might model this by considering each atomic piece of granted access to be a capability, and associate to each security clearance a set of these capabilities.
Similar ‘permissions systems’ show up in software: unix has permissions on files, as well as a distinction between ‘normal’ and ‘super’ users; many applications with user accounts distinguish between normal and administrative accounts; many software ‘plugins’ or ‘extensions’ systems, such as browser addons, come with notions plugin permissions. All of these could be modelled by treating each ‘power level’ as having a set of ‘capabilities’.
Even at the level of software implementation we can still find this pattern. Effects systems can be considered as granting pieces of code capabilities, as can mutable vs immutable references and perhaps even Rust’s lifetimes system.
— In some cases, certain sets of capabilities can be used to ‘emulate’ other capabilities.
For instance, my smartphone allows me to admit and revoke permissions to/from apps as I please. At any point I may allow or disallow an app from accessing my phone’s location and/or internet and I may also allow/disallow sending of notifications. If I disallow an app from accessing my location but allow it to access the internet, it may1 still be able to glean my location by performing an IP address lookup. Hence, the internet capability may be used to emulate the location capability.
Depending on the details of the phone
In such cases, we say that the system of capabilities exhibits overlap or redundancy. Overlap is what makes the study of capabilities interesting. Let’s say we have some set K of capabilities (such as K={internet,location,notifications}). There are some questions that naturally arise:
What is the
minimal subset
k⊆K of capabilities that is at
least as powerful as some fixed subset
k0⊆K?
If I, an app user, want to give an app both internet and location access, what’s the smallest
set of capabilities that would in principle suffice?
Can some fixed subset
k⊆K be used to emulate some fixed capability
κ∈K?
If I, an app user, grant my app all capabilities in
k, will I in principle also be inadvertently granting the app access to
κ?
How many ‘different’ combinations of capabilities
k⊆K are there, where by “different” we mean that they cannot emulate each other? (ie, at
least one cannot be emulated by the other)
This example is the original example that birthed the study of capabilities!
For another exhibition of this example, see
hereIs it a read reference? If we have the reference, are we able to read the current state of the referenced data?
Is it a write reference? If we have the reference, are we able to overwrite the data it references?
Is it an
update reference? If we have the reference, are we able to apply a pure
function to the current value of the data it references?
We can make the semantics of the capabilities more precise, at
least to the users who are familiar with Haskell. We offer the following phrasing of references. A
reference type is a
type Ref :: Type -> Type; it respectively has the
read,
write, and
update capabilities if it admits
functions of the following signatures which do the right thing:
read :: Ref a -> IO a
write :: a -> Ref a -> IO ()
update :: (a -> a) -> Ref a -> IO ()
In Haskell (see the previous footnote), we have the following to
witness that
update is at
least as powerful as
write:
update :: (a -> a) -> Ref a -> IO ()
write :: a -> Ref a -> IO ()
write value ref = update (const value) ref
and the following to
witness that
read+
write is at
least as powerful as
update:
read :: Ref a -> IO a
write :: a -> Ref a -> IO ()
update :: (a -> a) -> Ref a -> IO ()
update f ref = do
value <- read ref
let value' = f value
write value' ref
As promised, we will now dig into the question: how many different combinations of the capabilities K={read,write,update} are there, where by “different” we mean that they cannot emulate each other? To answer this, we start by writing down every combination of K={read,write,update}:
Doing so requires knowing that the
diagram denotes a
preorder, which we haven’t established so far but is true.
Notation 〈🌷 1, flat-tail arrows〉 If
f:A→B is a
function, we may write
a⟼fb
for
f(a)=b. Further, we may go so far to consider
f as a (
partial one-to-one) relation on
A∪B. Usually when we do this we will have
dom(f)=cod(f), so we will be considering
f:A→A as a (one-to-one) relation on
A2.
Notation 〈🌷 2, bullet notation〉 When using flat-tail arrows we may write dots for unnamed values, so that
a⟼f∙⟼g∙⟼hb
means
(∃x y)(f(a)=x∧g(x)=y∧h(y)=b); ie,
(h∘g∘f)(a)=b.
Definition / Notation. 〈🌷 3, arrows〉 If
⇝ is a relation over
A2, we can consider it as a (small, thin)
category C with
Ob(C)=A and where
∃!r∈HomC(a,b)⟺a⇝b
We will freely identify
set-relation pairs
(A,⇝) with their associated
categories and use this to talk about “arrows”
r:a⇝b when convenient or otherwise appropriate.
Definitions. 〈🌷 4, closures of relations〉 Let
⇝⊆A2 be a binary relation. Then...
Its
reflexive closure is
⇝ plus all identities; that is,
⇝∪{(a,a):a∈A}. Equivalently, this is the
minimal superset of
⇝ which is reflexive.
Its
symmetric closure is
⇝ plus all reversals; that is,
⇝∪{(b,a):a⇝b}. Equivalently, this is the
minimal superset of
⇝ which is symmetric. We can think of the symmetric
closure of
⇝ as ‘modifying
⇝ to not care about direction’
Its
transitive closure is the relation of nonempty
⇝-paths; that is,
{(a,b):exists a sequence a⇝∙⇝∙⇝⋯⇝b}. Equivalently, this is the
minimal superset of
⇝ which is
transitive.
Taking a reflexive
closure commutes both with taking
transitive and symmetric closures, but taking
transitive and symmetric closures do not commute. We adopt the convention that a relation’s
transitive, symmetric closure and its
symmetric, transitive closure are both
defined to be the
transitive closure of its symmetric
closure. This relation relates two elements
a and
b exactly when there is a path of elements between them where adjacent elements are related in either direction by
⇝. (To contrast, the symmetric
closure of the
transitive closure of
⇝ relates
a and
b when there is a
⇝-path going from
a to
b or a
⇝-path going from
b to
a.)
In general relation closures will be denoted by subscripting the relation with any combination of
tr,
re, and
sym depending on the
closure being taken. Abiding by the convention above, if both
tr and
sym are present we mean to take the symmetric
closure first. Hence
⇝sym,re
denotes the reflexive, symmetric
closure of
⇝.
As a special case we use
⇝⊵ to denote the
transitive, reflexive
closure of
⇝. This relates two elements
a and
b exactly when exists a possibly-empty
⇝-path between them. This is also called the
path relation over
⇝.
Definition Say
⇝ is a relation over
P(K). For each arrow
r:a⇝b let
pfm(r)pfm(r):P(K)→P(K):A↦{A∪bAA⊇aelse
Here one should think of K as a set of capabilities, such as K={read,write,update} and ⇝ as the relation telling us what capabilities can be transformed into other capabilities; in the example we have {read,write}⇝{update} and {update}⇝{write}.
The function pfm takes an arrow r:a⇝b and tells us what would happen if we actually performed the transformation signified by r: on supersets A⊇a we would get b ‘for free’, and on non-supsersets A⊉a we would do nothing.
Notation We will allow ourselves to freely identify arrows
r:a⇝b with the
function pfm(r), and accordingly instead of writing
A⟼pfm(r)B
may simply write
A⟼rB
or
even, by the fact that at each tuple
(a,b)∈⇝ is witnessed by exactly one arrow
r:a⇝b, may just write
A⟼a⇝bB
Remark A⟼a⇝bB⟺(A=B)∨(A⊇a∧A∪b=B)
Notation We write
A⟼⇝B
to mean that there exists some arrow
r:a⇝b so that
A⟼rB
Terminology A single arrow
A⟼a⇝bB is called a
performance, and a sequence of arrows
A⟼a1⇝b1∙⟼a2⇝b2⋯⟼an⇝bnB
may be called called a
performance path.
Again thinking of K as a set of capabilities and ⇝ as a witness to capability transformations, the relation ⟼⇝ tells us what sets of capabilities can be transformed by performances of ⇝ to what other sets. Note that A⟼⇝B is only true if one can turn A into B in a single performance; cases where multiple performances are required to transform A to B are not included in ⟼⇝.
Definition Say
⇝ is a relation over
P(K) for some
K. Define the
induced preorder ⟨⇝⟩ as follows. For
A,B⊆K we have that
A⟨⇝⟩B iff exists parallel sequences
{an},
{bn},
{An} so that
a1⇝b1,a2⇝b2,…,an⇝bnand
A⟼a1⇝b1A1⟼a2⇝b2A2⟼a3⇝b3⋯⟼an⇝bnAn⊇B
We have that A⟨⇝⟩B if there is a sequence of performances which we can apply to A to produce a supserset of B. Essentially, A⟨⇝⟩B if A is at least as powerful as B.
This is the relation we are most interested in studying, since it is what tells us most directly the power relationships between sets of capabilities.
Definition For
⇝⊆K2, the
induced preorder-set In(⇝) is
(P(K),⟨⇝⟩).
Definition For
⇝⊆K2, the
induced poset Ind(⇝) is
(A,[⇝]):=(P(K),⟨⇝⟩)/≅ where
≅ is
isomorphism.
Remark A⟨⇝⟩B if and only if A⟼⇝⊵∙⊇B
Proposition 〈🌷 5, lifting lemma〉 For
⇝⊆P(K)2 and
A,B⊆K,
Proof Say
A⊇A′⟼⇝⊵B. Then we have a performance path going from
A′ to
B. Since
A⊇A′, then those same performances may be applied to
A; the result will be some superset of
B.
Proposition 〈🌷 6〉 For any relation
⇝, the induced
preorder ⟨⇝⟩ is indeed a
preorder.
Reflexivity — always
A⊇A and hence always
A⟨⇝⟩A
Transitivity — Comes from repeated application of the
〈🌷 5, lifting lemma〉.
Say
X⟨⇝⟩Y⟨⇝⟩Z. Then we have a sequence of performances taking
X to a supserset
X′ of
Y and a sequence of performances taking
Y to a supserset
Y′ of
Z. By applying the performances in the second sequence to
X′ instead of
Y, we obtain a sequence of performances taking
X′ to a superset
X′′ of
Z (we have lifted the performance sequence). Then by composing this with the existing sequence taking
X to
X′, we obtain a sequence of performances taking
X to a supserset
X′′ of
Z; that is, we obtain a
witness to X⟨⇝⟩Z.
In the name of cool
diagrams, let’s see this as a cool
diagram.
On the left we have the performance sequence taking
X to a superset
Xn of
Y. Below we have the performance sequence taking
Y to a superset
Yk of
Z.
We then repeatedly apply the
〈🌷 5, lifting lemma〉 lifting lemma to ‘lift’ this second performance to compose with the first. In more detail ...
Then since
Xn⊇Y we note that the transformation
y1⇝y1′ which when performed to
Y produces
Y1 can instead be performed to
Xn to produce some
Xn+1⊇Y1. Repeating this we can ‘lift’ the path of performances
Y⟼⇝⊵Yk into one
Xn⟼⇝⊵Xn+k⊇Yk. And since
Yk⊇Z then this acts as
witness to X⟨⇝⟩Z.
One very neat thing to note here is that the arrows
⟹ can be interpreted as logical implication; it is literally true, for instance, that
Y⟼y1⇝y1′Y′⟹Xn⟼y1⇝y1′∙
because we know that
Xn⊇Y
Remark This proof of transitivity also serves as justification that if we had
defined ⟨⇝⟩ by allowing
⊇ at any point along the path (instead of at just the end), we would end up constructing the same relation.
Observation If
A⊆B, then
B⟨⇝⟩A regardless of choice of
⇝.
Corrolary 〈🌷 7〉 For any
⇝ over
P(K), then
poset (P(K),⊇) homomorphs into
Ind(⇝) since if
A⊇B then
A⟨⇝⟩B so
[A]≅[⇝][B]≅.
Example 〈🌷 8〉 Let
K={1,2,3} and let
⇝=∅. Then
In(⇝) and
Ind(⇝) are both
isomorphic to
Example 〈🌷 9〉 Let
K={1,2,x} and let
2⇝1. Then
In(⇝) is
and
Ind(⇝) is
isomorphic to
Example 〈🌷 10〉 Let
K={a,b,c,d} and let
cd⇝a,b⇝ac,ac⇝d. Then
In(⇝) is
and
Ind(⇝) is
isomorphic to (assuming no mistakes made by me):
Worth noting how small the final
poset is in comparison to the
preorder! The
preorder has
2∣K∣=16 vertices but the induced
poset has only
7.
Observation 〈🌷 11〉 Say we have
⇝ and say we construct
⇝′⊇⇝ by adding arrows which are either transitively redundant (ie, of the form
a⇝′c when already exists
a⇝b⇝c for some
b) or reflexively redundant (ie, of the form
a⇝′a). Since performance sequences through
⇝′ are the same as those through
⇝, then
In(⇝′)=In(⇝)
Hence the construction
In(−) is invariant over
transitive and reflexive
closure of its input
⇝. In other words,
In(−) should really be thought of as a mapping
In(−):Preorder(K)→Poset(K)
instead of
In(−):Relation(K)→Poset(K)
although one can regard it either way
Definition 〈🌷 12〉 An arrow
r:A⟨⇝⟩B is called
downwards if
A⊇B, and called
upwards if
A⟼⇝⊵B.
Note that
A⟨⇝⟩B iff A⟼⇝⊵∙⊇B. Accordingly, every arrow
r:A⟨⇝⟩B can be decomposed into an upward arrow
u and downward arrow
d so that
Au⟼⇝⊵A′d⊇B
for some
A′. This decomposition is not necessarily
unique, but fixing
A′ induces
unique u,d since
⟨⇝⟩ viewed as a
category is thin.
Definition 〈🌷 13〉 The
downwards part of
⟨⇝⟩ is the collection of downwards arrows in
⟨⇝⟩. Likewise, the
upwards part of
⟨⇝⟩ is the collection of upwards arrows in
⟨⇝⟩.
Observation 〈🌷 14〉 For some
⇝, some arrows in
⟨⇝⟩ are neither upwards nor downwards.
Observation Say we have an arrow
r:A⟨⇝⟩B. If
r is upwards and not the identity, then
B=A∪k for some nonempty
k and hence
B⊋A. On the other hand, if
r is downwards and not the identity, then
B⊊A. Hence, the only arrows which are both upwards and downwards are the identities.
The upshot of this is that by looking at the upwards and downards arrows in
⟨⇝⟩ we are creating a well-behaved decomposition of
⟨⇝⟩. It is well-behaved in two ways:
Except for identities, arrows are at most one of upwards and downwards
(The identities are a non-issue because both the the downwards and upwards part of
⟨⇝⟩ are reflexive, so there is no question of “where an identity came from”)
Definition If
⇝ is a relation over
P(K), and if
s⊆K, then the
translation
trs(⇝)is the relation
⇝′ given by
⇝′={(a∪s,b∪s):s⊆K,a⇝b}
and the
extrusion exta(⇝) is
exta(⇝)=⇝∪tra(⇝)
Remark Translations and extrusions could be easily generalized to any relation over a semigroup by replacing
∪ with the semigroup
operation. This will not be useful for us, though, so we won’t bother.
Remark The
terms ‘translate’ and ‘extrude’ are most ordinarily used in the context of an infinite
n-dimensional
space; in this context, translations and extrusions of a shape are ‘rigid’ in the sense that they do not map any two distinct
parts of the shape into the same place. This is not the case for the translations and extrusions we use here, as is exemplified by the following:
Example Let
⇝ denote the relation
Then the translation
tr{a}(⇝) is
Note how while
⇝ has three arrows,
tr{a} has only two; this demonstrates how translation is not ‘lossless’. The extrusion
ext{a}(⇝) is
Remark Neither translations nor extrusions generally preserve transitivity. Translations also do not generally preserve reflexivity. Consider for instance
Due to limitations of my tooling, I’m sadly unable to draw identity arrows on these
diagrams. The input relation is supposed to have all identities, and the output relation has some subset of those. Then:
Transitivity is not preserved because
even though the input relation is
transitive, its image is not, as the image has
a→ab→abc but not
a→abc
Reflexivity is not preserved because the output relation does not have any of
∅→∅,
b→b,
c→c, or
bc→bc.
If the
operation tr{a} is swapped out with
ext{a} we obtain an example of extrusions not preserving transitivity.
Proposition 〈🌷 15, extrusions commute〉 Extrusions commute
Proof Let
K be a
set, let
a,b⊆K, and let
⇝ be a relation over
P(K).
Note that
Xextb(exta(⇝))Y if and only if one of the following four cases hold:
X(X∪a)(X∪b)(X∪a∪b)⇝Y⇝(Y∪a)⇝(Y∪b)⇝(Y∪a∪b)
and likewise
Xexta(extb(⇝))Y if and only if one of the following hold
X(X∪b)(X∪a)(X∪b∪a)⇝Y⇝(Y∪b)⇝(Y∪a)⇝(Y∪b∪a)
These two conditions are the same, and hence extrusions commute.
Proposition 〈🌷 16, translations commute〉 Translations commute
Proof
⟺⟺⟺Xtrb(tra(⇝))Y(X∪a∪b)⇝(Y∪a∪b)(X∪b∪a)⇝(Y∪b∪a)Xtra(trb(⇝))Y
Definition If
⇝ is a relation over
P(K) then we define
X⇝∪Y⟺defX⇝∙⟼−∪XY
equivalently,
⇝∪={(X,X∪Y):X⇝Y}
equivalently,
We think of ⇝ as telling us what capabilities can be transformed into other capabilities. Under this interpretation the ⇝ relation is in some sense ‘lossy’, in that if a⇝b the ‘transformation’ of a to b ‘loses’ a.
In practice when performing transformations we would want to keep a around, so that if we have the capability a then we’d transform it into ab. This is what ⇝∪ is: we perform a transformation but keep the capabilities we already have.
Note that ⇝∪ is similar to ⟼⇝, except that the latter performs transformations on any set and the former only performs transformations on those sets in dom(⇝).
More explicitly, say we know that X⟼k⇝k′Y, and let k⋆=k′∪k (so that k⇝∪k⋆). Then we know that k⊆X is a set of capabilities in X; let R=X∖k be what’s left over. Then we know that Y=k⋆∪R.
The point is that what we’re doing here is “shifting” the relation k⇝∪k⋆ by any “context” R. The operation of translation is exactly shifting, and extrusion is optional shifting. So we should expect that ⟼⇝ is exactly ⇝∪ extruded along all “basis vectors” (singleton sets); and that is indeed what we find, as follows.
Picture An illustration of what I mean by “context”
I think I’d need to learn TikZ-cd to do this, so we’
re going back to the basics instead: plaintext
X ~> Y
├───>
= =
a a
b b
c c
… …
┐ ┌
q │ ∪ │ q
r │ ~> │ r
s │ │ s
┘ │ t
└
… …
x x
y y
z z
ok, so what the hell is this supposed to be saying
I’ve assumed we have some
sets X,Y so that
X⟼⇝Y. I’ve
split X up into
X={a,b,c,…}⊔{q,r,s,…}⊔{…,x,y,z}. The first and final items of this decomposition are intended to compose the ‘context’
R. The point is that
only the middle part is actually what’s relevant to
⟼⇝. The mapping
X⟼⇝Y can be seen as taking place on this middle part
only, with the context
R ‘surrounding’ the transformation but not taking part or affecting it in any way.
Definition The
full extrusion of a relation
⇝ over
P(K) is the relation where
Xfullext(⇝)Y iff exists
k⊆K so that
Equivalently,
fullext(⇝)=fullext(⇝)=fullext(⇝)={(a∪k,b∪k):a⇝b,k⊆K}(◯k∈Kext{k})(⇝)(◯k⊆Ktrk)(⇝)(1)(2)(3)
If you’ll excuse the inattention, won’t give
full proofs of these equivalencies (they are not all that complex). But we will say a few words:
(1) is
equivalent to the diagrammatic definition essentially by definition; one can consider
(1) to be a symbolic expression of the definition of
fullext.
(2) is
equivalent to
(1) with a little algebra, and
(3) to
(2) with a little more.
Proposition We have one more
equivalence. Note that if
s⊆u then
u∪k=u∪(k∖s). Then we get:
fullext(⇝)={(a∪k,b∪k)={(a∪(k∖a∩b),b∪(k∖a∩b))={(a∪k,b∪k):a⇝b,k⊆K}:a⇝b,k⊆K}:a⇝b,k⊆K∖a∩b}
This equivalence reduces the number of k⊆K we need to compute in order to compute a full extension, which will be useful later.
Proposition fullext(⇝∪)=⟼⇝ for any relation
⇝ over
P(K)
Traditional-style proof
(⇒)Say that
Xfullext(⇝∪)Y. Then we have some
set k⊆K by which we’ve translated
⇝∪ along to relate
X and
Y; that is, exists
X0,Y0 so that
X0⇝∪Y0 and
X=X0∪k and
Y=Y0∪k.
Since
X0⇝∪Y0 then exists
X0′ so that
X0⇝X0′ and
X0′∪X0=Y0.
Note that since
X=X0∪k and
Y=Y0∪k=X0′∪X0∪k then we know
Y=X∪X0′.
Hence
X0⇝X0′ and
X⊇X0 and
Y=X∪X0; in other words,
X⟼X0⇝X0′Y.
(⇐)Say that
X⟼⇝Y. Then exists some
X0⊆X and
X0′⊆K so that
X⟼X0⇝X0′Y.
Hence
X0⇝X0′. By letting
Y0=X0∪X0′ we get
X0⇝∪Y0.
Then choosing
k=X we get that
X=X0∪k and
Y=Y0∪k; that is,
Xfullext(⇝∪)Y.
Diagrammatic proof
(⇒)Say that
Xfullext(⇝∪)Y. Then exists
X0,X0′,k⊆K so that
There’s a number of moving
parts here, but all we’
re doing is unravelling the definitions of
(−)∪ and
fullext.
Noting that
X=X0∪k and
Y=X0′∪X0∪k we conclude that
Y=X∪X0′ and hence
ie,
X⟼X0⇝X0′Y
(⇐)Say that
X⟼⇝Y. Then exists some
X0,Y0⊆K so that
by choosing
k=X we get
in other words,
Xfullext(⇝∪)Y.
Remark We just showed that
⟼⇝=fullext(⇝∪). One reason this might be at
least a little bit surprising is that
⟼⇝ is
transitive, but extrusions in general do not preserve transitivity: so perhaps it’s surprising that this image under a
full extrusion (which is just many extrusions) is
transitive.
Proposition Say
A⟼⇝⊵B. Then
B is the result of applying a sequence of performances to
A, and so
B⊇A. Then by reflexivity of
⟼⇝⊵ and
⊇ we get
A⟼⇝⊵B⊇Band
B⟼⇝⊵B⊇AThat is,
A⟨⇝⟩BandB⟨⇝⟩A
and hence
A≅⟨⇝⟩B. In other words, every upwards arrow
r:A⟼⇝⊵B induces an
isomorphism in
In(⇝);
A⟼⇝⊵B⟹A≅⟨⇝⟩B
Remark The converse does not hold. A good counterexample is
⇝={(ab,cx),(bc,ay)}; then we have
Thus
ab≅bc despite not being related by
⟼⇝⊵.
However, a weakening of the converse does hold if we assume some extra structure on the input relation ⇝. Requiring extra structure sounds suspicious: what if we want to work with a ⇝ which does not exhibit this structure? There is a way to transform any given ⇝ into one which exhibits this stricture without affecting the ‘meaning’ of ⇝ as capability transformations; ie, without affecting the induced preorder.
The extra structure is this:
Definition 〈🌷 17, graduality〉 Call a relation
⇝⊆P(K)2 gradual if whenever
a⇝b we know
∣b∣≤1.
If ⇝ is to be interpreted as a set of capability replacements, requiring that ⇝ is gradual is asking that each replacement produces at most one capaiblity. This sounds like a restriction on the capability replacements we are able to work with, but it isn’t really, because if ever we have s⇝{a,b,c} we can split it up into s⇝{a} and s⇝{b} and s⇝{c}, which is ‘the same’ set of replacements in a different form8. This canonical ‘gradualification’ is expressed as the following construction:
There’s an argument to be made here, I think, that capability replacements should be expressed as a relation
⇝⊆P(K)×K instead of
⇝⊆P(K)×P(K); ie, we require by definition that all replacements are gradual.
Definition 〈🌷 18, gradient〉 Given
⇝⊆P(K)2, its
gradient grad(⇝) is the relation
grad(⇝)={(a,b):(∃B)(a⇝B⊇b),∣b∣≤1}
That is,
Xgrad(⇝)Y if and only if ∣Y∣≤1 and
X⇝Y′ for some superset
Y′⊇Y.
The following proposition justifies that taking the gradient of a relation ‘does not change it’ as far as we are concerned:
Proposition In(⇝)=In(grad(⇝))
Proof No
The reason for interest in graduality is the following property:
Proposition 〈🌷 19, shrinking lemma〉 If
⇝ is gradual and
A⟼⇝⊵A′⊇B then
A⟼⇝⊵A∪B.
The antecedent here is that
A⟨⇝⟩B by some
witness A′, and the consequent is that also
A⟨⇝⟩B by the smallest possible sufficient
witness A∪B. This is some kind of a ‘shrinking condition’.
Proof Take
⇝ gradual and
A⟼⇝⊵A′⊇B. Then we have a sequence of performances taking
A to some superset
A′ of
B. Since
⇝ is gradual, then each performance adds at most one element. By omitting performances which add elements
e for which
e∈/B (ie, unnecessary performances), we construct a smaller sequence of performances which takes
A to
A∪B. Hence
A⟼⇝⊵A∪B.
And now finally we get to the punchline, which is the weakened converse from before:
Proposition Say
⇝ is gradual and
A≅⟨⇝⟩B. Then
A and
B are related by the symmetric,
transitive closure of
⟼⇝.
Stronger If
⇝ is gradual, then
A≅⟨⇝⟩B exactly when A,B⟼⇝⊵A∪B
Proof Say we know
A≅⟨⇝⟩B. Then for some
A′,B′ we have
since
⇝ is gradual then we may
〈🌷 19, shrink〉 it to conclude that
A⟼⇝⊵A∪B and likewise for
B, giving:
which entails in particular that
which implies that
A⟼⇝⊵⊴B.
Proposition If
⇝ is gradual, then
⟼⇝ is a symmetric,
transitive reduction of
≅⟨⇝⟩.
Proof We have already shown the following two facts:
If
A⟼⇝⊵B then
A≅⟨⇝⟩B
If
A≅⟨⇝⟩B then
A⟼⇝⊵⊴B, as long as
⇝ is gradual
Together we get that if
⇝ is gradual then
≅⟨⇝⟩ is
equivalent to
⟼⇝⊵⊴
(⇒)Assume
⇝ is gradual, and say
A≅⟨⇝⟩B. Then by (2) we have that
A and
B are related by
⟼⇝⊵⊴
(⇐)Assume
⇝ is gradual, and say
A and
B are related by the symmetric,
transitive closure of
⟼⇝. Then we have a path
A≈X1≈X2≈⋯≈Xn≈B
where
≈ is the symmetric
closure of
⟼⇝. We can treat each
≈ as a length-one path and then invoke (1) to induce an
isomorphism for each, so this becomes
A≅X1≅X2≅⋯≅Xn≅B
and hence we get that
A≅⟨⇝⟩B.
Prop For
⇝⊆P(K)2, we have that if
a≅⟨⇝⟩b and
c≅a∪b then
c≅a∪b≅a≅b.
Proof (Conversational) Say
a≅b and
c≅a∪b. We will show that
c≅a, which is sufficient by
isomorphism composition.
First we show that
c⟨⇝⟩a. Since
c≅a∪b then in particular
c⟨⇝⟩a∪b, meaning we have a performance path
p from
c to a superset of
a∪b. But since
a∪b is itself a supserset of
a, then
p also acts as a performance path from
c to a superset of
a; that is,
p:c⟨⇝⟩a. Done!
Now we show that
a⟨⇝⟩c. Since
a≅b then we have a performance path
p1 from
a to some superset
a′ of
b. Since
a′ is the result of performances, then we know
a′ is also a superset of
a; hence,
a′⊇a∪b. Then since
c≅a∪b then we have a performance path
p2 from
a∪b to a superset of
c. Altogether we get
By the lifting lemma this becomes simply
a⟼⇝⊵∙⊇c, which is to say
a⟨⇝⟩c. Now we are done.
Proof (Diagrammatic). Say
a≅b and
c≅a∪b. Then we have
for some
a′. Here the two embedded bowtie
diagrams come from the assumed
isomorphisms. Dashed arrows are drawn on top and are also true. The fact that
a′⊇a∪b holds is because we know
a′⊇b and we also know that
a′⊇a since know that
a′ is the caboose of a performance train starting at
a.
As subdiagrams we have both of the following
The former
diagram entails that
c⟼⇝⊵∙⊇a, which means that
c⟨⇝⟩a. The latter
diagram reorganizes to
which by the lifting lemma means that
a⟼⇝⊵∙⊇c, meaning that
a⟨⇝⟩c.
Hence
c⟨⇝⟩a⟨⇝⟩c, so
c≅a. Composing with the already-given
isomorphisms a≅b and
c≅a∪b we get that
c≅a≅b≅a∪b
as desired.
Corrolary By applying the previous proposition to the assignment
c=a∪b we get that if
a≅b then
a∪b≅a≅b; that is,
classes of
⟨⇝⟩-
isomorphism are
closed under union.
Proposition 〈🌷 20〉 The following
equivalences fall out:
⟺⟺⟺X≅⟨⇝⟩YX≅⟨grad(⇝)⟩YX(⟼grad(⇝))⊵⊴YXfullext(grad(⇝)∪)⊵⊴Y⟨−⟩ is invariant over grad(−)property of graduality⟼→=fullext(→∪)
In other words, the
full extension of
grad(⇝)∪ is a symmetric,
transitive reduction of
⟨⇝⟩-
isomorphism.
This may seem like a bizarre result, but in fact this result has been the point of all the work we’ve done so far. Because while I don’t necessarily know how to efficiently compute ≅⟨⇝⟩, I can give an efficient computation for fullext(grad(⇝)∪)⊵⊴!
Namely...
Algorithm 〈🌷 21〉 Computing
⇝↦grad(⇝)∪
Iterate over arrows
a⇝b and then over elements
b0∈b; for each add to
grad(⇝)∪ one pair
(a,a∪{b0}).
Algorithm 〈🌷 22〉 Computing
⇝↦fullext(⇝)⊵⊴
Given a relation
⇝⊆P(K)2, we want to compute
fullext(⇝)⊵⊴. We give two algorithms to do this. The first is simpler and easier to verify as correct, and the second incrementally improves upon the first in
terms of efficiency but at the cost of complexity.
The first algorithm proceeds as follows
(nb — want to ensure typing consistency — lowercase are subset of
K, upper are
set of subset, so on)
We claim that after performing this procedure,
C will be exactly
classes of
fullext(⇝)⊵⊴
To this algorithm we make the following modifications:
Omit singletons
{k} from
C — if we find that
k∈/C∈C for all
C then we know we should
act as if
{k}∈C
Note that if some
s⊆K is never computed on line (5) as
a∪k or
b∪k, then by the end of the algorithm it will not be a member of any
class C∈C. We need to explicitly add these singletons back into
C in at the end of the algorithm
9.
We do it at the end rather than the beginning to keep
C small during the main part of the algorithm for the sake of efficiency
These
sets s are exactly those which are not computed as
a∪k or
b∪k; ie, those for which there is no pair
k⊆K and
c∈fld(⇝) for which
s=c∪k. In other words,
s is not a superset of an element of
fld(⇝): ie,
¬(s⊇∙∈fld(⇝)).
We can enumerate such
sets efficiently by performing a search through
P(K), emitting each
s⊆K as its encountered but abandoning the current branch as soon as it is a superset of something in
fld(⇝). In more detail, we can perform the following algorithm:
Remark. Each
set a∈fld(⇝) will prune multiple branches. This suggests that this algorithm is not the most efficient possible implementation of the target
function. However, the algorithm gets us away from best-case
2n time, and that’s good enough for me.
Line (4) need only iterate over
k⊆K∖a∩b as per a proposition
Recall that
equivalence classes of
⟨⇝⟩ are
closed under (
nonempty10) union. Hence storing unions in collections
C∈C is in some sense redundant — if we know
c,c′∈C then there’s no point in also explicitly storing
c∪c′ in
C as well. To this end we ought to represent elements
C∈C as some
minimal subcollection of ‘generators’
G⊆C whose
closure under union is exactly
C.
That is, an
equivalence class E of
⟨⇝⟩ contains all unions of the form
e1∪e2∪⋯∪en∣ei∈E
which are
nonempty; ie, where
n≥1. The empty union produces
∅, which is in exactly one
equivalence class of
⟨⇝⟩, not all of them.
Unfortunately having to work with closures under
nonempty union is slightly more annoying than working with closures under possibly-empty unions. Oh, well.
We detail how this works later; for now it is sufficient to make a few assumptions. We assume existence of some
class cSet (for “
closed set”) whose elements, called
c-
sets, are used to give efficient representations for
∪-
closed sets. We also assume existence of mappings
Set(−)s⟵−⋅−⟶(−)ccSet
We think of
(−)c as taking the
∪-
closure of a
set but
representing the result efficiently as a
c-
set instead of as a
set, and we think of
(−)s as taking a
c-
set representation of a
closed set and realizing it as a
set in the ‘usual’ way.
We also assume existence of operations
∈c:Set×cSet→{0,1} and
∪c:cSet2→cSet which work as expected; specifically, such that:
This modification is not ‘a priori’ safe to make to the algorithm: making this change may result in a subset
k⊆K showing up in multiple
classes C1,C2∈C; accordingly we amend lines (6) and (7) to search for and then
operator over
all C1,C2 containing
a∪k and
b∪k (rather than searching for the
unique C1,C2).
This modification will only cause more
class merges than before; none will be omitted. And since each merge will be consistent with
⟨⇝⟩ still, we retain correctness.
Modifications (1) and (3) mean that we avoid using
2n space in the general case, which is good. We will still be both
2n time and
space in the worst cases, but this is likely unavoidable.
Applying these modifications produces the following algorithm. The
M column annotates algorithm instructions with which modifications are relevant to them, if any
Algorithm (C) Computing
⇝↦Ind(⇝)
By
〈🌷 20〉 we have that
≅⟨⇝⟩=fullext(grad(⇝)∪)⊵⊴
Algorithm
〈🌷 21〉 gives a way to compute
grad(⇝)∪ from
⇝, and algorithm
〈🌷 22〉 gives a way to then compute
fullext(grad(⇝)∪)⊵⊴.
The result of algorithm (B) will give us
≅⟨⇝⟩-
isomorphism classes, which are exactly the elements of
Ind(⇝). What remains is to compute this
poset's relation,
[⇝]. We know that
[A][⇝][B]⟺def(∀a∈[A],b∈[B])(a⟨⇝⟩b)⟺(∃a∈[A],b∈[B])(a⟨⇝⟩b)
Since each upwards arrow in
⟨⇝⟩ is half of an
isomorphism, then non-identity arrows in
Ind(⇝) must come from downwards arrows in
⟨⇝⟩; hence, the above further becomes
[A][⇝][B]⟺(∃a∈[A],b∈[B])(a⊇b)
Thus when
representing Ind(⇝) we need only keep around a single
representative of each
isomorphism class. Since these
classes are
closed under union, the natural choice is to store the union of the
classes.
Conjecture Every extrusive
poset is the image of some discrete
preorder. (Ie, just as Google Docs could
swap out
K={view,view+comment,view+comment+edit} with
K={view,comment,edit}, the same can be done anywhere)
Here we take serious the notion that, for instance, anything that makes use of
⇝ should be invariant over
grad(−). That is, we take serious the notion that letting the
space of
⇝ be all of
P(K)2 is too large.
Given a
set K we define the
class rere(K) of
redundance relations over
K as
rere(K)=P(K)2/∼
where
∼ is the
transitive, symmetric, reflexive
closure of the relation which relates
R1,R2⊆P(K) iff any of the following hold:
R2=R1∪{(a,a)} for some
a⊆K — that is,
rere(K) “doesn’t observe reflexive redundancy”
R2=R1∪{(a,c)} for some
aR1bR2c — that is,
rere(K) “doesn’t observe
transitive redundancy”
R2=R1∪{(a,b∪b′)} for some
aR1b,b′ — that is,
rere(K) “doesn’t observe ‘graduality redundancy’"
We would know that this definition is correct if we find that
⇝1∼⇝2⟺⟨⇝1⟩=⟨⇝2⟩
Thus we have a maping
rere:Set→Set. One may ask if we can extend this to an endofunctor. I
think the answer is yes, with the
action on
morphisms given by:
rere(f:K→K′)=(⇝∈P(K)2/∼)↦{(k1,k2)∈P(K)2:f−1[[k1]]⇝f−1[[k2]]}Definition Let
A be a collection of
sets. A
set a is called
atomic (
wrt A) if it cannot be written as a possibly-empty union of elements from
A∖{a}. Otherwise, it is called
molecule [adj] (
wrt A).
It’s worth calling attention to that a set a need not be in A to be classified as atomic or molecule. Hence, for instance, over A={{1,2},{3}} we have that {1} is atomic and {1,2,3} is molecule, despite neither being present in A.
We will use atomic elements as the generators in our c-sets. Useful for doing this is the following coherence property:
Proposition Take
A a collection of
sets,
a a
set, and
b a
set molecule over
A. Then we have the following implications:
Proof
(1 ⇒ 2)By contrapositive. If
a is molecule over
A, then it’s certainly molecule over
A∪{b}⊇A.
(2 ⇒ 1)Say
a is
atomic over
A and
b=a. Assume for contradiction that
a is not
atomic over
A∪{b}. Then we can write it as
a=a1∪a2∪⋯∪an
where each
ai∈A∪{b}∖{a}. Also, it must be that at
least one
ai is equal to
b, since
a is not molecule over just
A. WLOG assume
a1=b and
ai=1=b. Since
b is molecule over
A then we can further expand
a as
a=(b1∪b2∪⋯∪bk)∪a2∪⋯∪an
where each
bi∈A∖{b}. Now we know that
b is not a
term in this
expansion and that
a does not appear as an
ai term (but might appear as a
bi term).
In fact
a does not appear as a
bi term either. Assume for contradiction that it does, and WLOG say that
b1=a and
bi=1=a. Then we have
a=(a∪b2∪⋯∪bk)∪a2∪⋯∪an
which forces that all
ai=1 and
bi=1 must be subsets of
a. In turn this means that
b, which can be written as
b=a∪b2∪⋯∪bk
is equal to
a. We had assumed that this was not the case, and hence this is a contradiction.
We discharge the contradiction to learn that
a does not appear as a
bi term in the
expansion
a=(b1∪b2∪⋯∪bk)∪a2∪⋯∪an
We already knew that it does not appear as an
ai term, either, and we also knew that all
bi and
ai terms are inequal to
b. Altogether this gives that neither
a nor
b appear as a
term to this
expansion, and hence this
expansion witnesses that
a is molecule over
A∖{b} and therefore over
A.
We had assumed that
a is
atomic over
A, and hence this is a contradiction. We discharge this contradiction to conclude that
a is
atomic over
A∪{b}, and the proof is
complete.
(2 ⇒ 3)By contrapositive. If
a is molecule over
A∖{b}, then it’s certainly molecule over
A⊇A∖{b}.
(3 ⇒ 2)Consequence of (2 ⇒ 1). Say
a is
atomic over
A∖{b} and
b=a. Either
b∈/A or
b∈A. If
b∈/A then
A∖{b}=A and so
a is
atomic over
A. If
b∈A then apply (2 ⇒ 1); then
a is
atomic over
A∖{b}∪{b}=A.
This proposition gives us some kind of absoluteness of primality: the primality of a set a∈A does not care about presence of molecules.
It’s also true that the possibly-empty ∪-closure of a collection A does not change as we remove molecule elements. As a result, we get the following:
Corrolary Let
A be a
finite collection of
sets. Consider the process of repeatedly removing molecule elements of
A, chosen at random, until only
prime elements are left; call the result
Pr(A). Then:
Every way to choose molecule elements will produce the same
set; and
Taking the possibly-empty
∪-
closure of
Pr(A) will produce the possibly-empty
∪-
closure of
A
The point is that Pr(A) is a “coherent” choice of generators for Cl(A) in that it is invariant under what order you remove elements.
We also get the following minimality property for Pr(A), which is nice:
Proposition Let
A be a
finite collection of
sets. Then
Pr(A) is the
⊆-
minimum generating
set for
Cl(A)
Proof Let
Q be a
⊆-
minimum generating
set for
Cl(A).
First note
Q⊆A. Say for contradiction that there was some
q∈Q not present in
A. Then
q would also be in the
closure of
Q, meaning that the
closure of
Q would not be
A. Contradiction.
Now note
Q contains all primes from
A. For contradiction, assume that there is some
prime a∈A not present in
Q. Since
a is not molecule over
A and since
Q⊆A this entails that
a is not molecule over
Q; therefore,
a is not in the
closure of
Q. Hence
Q is not a generating
set for
A; contradiction.
Finally note that
Q contains no molecules, since otherwise we could remove a molecule to produce a smaller generating
set.
Hence
Q contains exactly the primes from
A; that is,
Q=Pr(A); done.
Ok great! So the primes of a collection A give a minimal generating set for the possibly-empty closure of Cl(A).
Remark — I think all the above are still true even if we use closure under nonempty union.
We use this to define cSet and its related operations (−)c, ∪c, ∈c, and (−)s. The idea is to represent the closure of a set A as its prime elements; this representation admits defining these operatoins with the desired characteristics.
Definition
Ac:=P(A)
Algorithm Given a
set A, we may compute
Ac=P(A) by repeatedly removing molecules until there are none left. By a previous proposition, this will always produce
P(A).
how to detect a molecule?
Definition
P(A)∪cP(B):=P(P(A)∪P(B))
Algorithm The algoritmh for this is just a
set union followed by a
P(−).
Definition
x∈cP(A):=x∈Cl(P(A))
Algorithm Note that
x∈Cl(P(A)) if and only if
∅=x∖(⋃{s∈P(A):s⊆x})
This may be efficiently computed as follows:
Definition
P(A)s:=Cl(P(A))
Algorithm No way around this one. Just compute the
closure.
With
actual employee allowances/capabilities?
effects systems — ala one MonadThing per affordance
“generating notions” for mathematical fields?
Let
K be the
set of all ‘
topological notions’, containing such things as “
open set” and “
closed set” and “
closure operator” and “
continuous function” and “
limit point” and “
convergent sequence”.
From the notion of “
open set” one can define all other notions. Same with “
closed set” and “
closure operator”.
But perhaps there are
sets of notions which do not generate all other notions? If for a
space I only know what the continous
functions looks like, can I recover the
open sets? What about if I only know
limit points?
Convergence?
If there are any non-generating
sets of notions, then the “can recover” relation
⇝ (eg
{closed sets}⇝{open sets}) gives rise to
isomorphism classes which measure how powerful different notions of
topology are, in
terms of definability.
This math.SE answer claims that two different
topologies can induce the same notion of sequence
convergence, meaning that sequence
convergence is less powerful a notion than openness. Also see
this MO answer, which points out that although
sequence convergence isn’t
universal,
net convergence is.
potentially some application to game
theory, although frankly it seems weak
holy shit! practical application for extrusive
posetswhen doing QA on something, the
space that needs to be searched usually looks something like k × 2ⁿ — you have k things to test under 2ⁿ different scenarios (n different flags). treating this 2ⁿ as a capability
space, we can use the
theory of extrusive
posets to find and eliminate redundancies. for instance, say we’
re testing the backup feature of an application and two of the relevant flags are:
1. user has backup enabled
2. user has files in their account
the point of (2) is to test backup in the trivial case. however, flag (2) is only relevant if flag (1) is on; ie, if the user has backup enabled. if they don’t, then there’s nothing to test, so flag (2) doesn’t matter.
this is a redundancy! and exactly the kind of redundancy that extrusive
posets are designed to handle. One could imagine feeding the flag
set and redundancy
set into an extrusive
poset algorithm and receiving as output the minimized QA search
space
the one big issue i see here is that some “flags” (dimensions) may be of arity 2. maybe instead of “user has backup enabled” there are three possibilities: backup disabled, backup partially enabled, backup fully enabled. as of right now the
theory of extrusive
posets knows only how to handle the binary case
I think in extrusive
posets we can generalize from (
P(K),
∪,
⊆) to a generic symmetrical
monoidal preorder. maybe
even drop some conditions
Not sure what it would give us though. potentially potentially potentially (probably not) ability to work in dimensions other than two
Uhhh.... does something like Prolog just trivialize all this work? Interesting. Here’s a
very formative first stab at doing all this trivially in Prolog:
to(r, o).
to(w, o).
to(u, o).
to(rw, r).
to(ru, r).
to(ru, u).
to(wu, u).
to(rw, w).
to(wu, w).
to(rwu, ru).
to(rwu, rw).
to(rwu, wu).
to(ru, rwu).
to(rw, rwu).
to(u, wu).
too(A, B) :- tooImpl(A, B, []).
tooImpl(A, B, Seen) :- not_member(B, Seen), to(A, B).
tooImpl(A, B, Seen) :- to(A, X), not_member(X, Seen), tooImpl(X, B, [ A | Seen ]).
not_member(_, []).
not_member(X, [H|T]) :- dif(X, H), not_member(X, T).
same(A, B) :- too(A, B), too(B, A).
This is the reference
types example. We add a fact
to(a, b) for every arrow between
sets-of-reference-
types. Then we form the
transitive closure and
isomorphism relation. Now we can ask questions like “what is the iso
class of
RWU" with
?- same(X, rwu)
Proof Say . Then we have a performance path going from to . Since , then those same performances may be applied to ; the result will be some superset of .
On the left we have the performance sequence taking to a superset of . Below we have the performance sequence taking to a superset of .
We then repeatedly apply the 〈🌷 5, lifting lemma〉 lifting lemma to ‘lift’ this second performance to compose with the first. In more detail ...
Then since we note that the transformation which when performed to produces can instead be performed to to produce some . Repeating this we can ‘lift’ the path of performances into one . And since then this acts as witness to .
One very neat thing to note here is that the arrows can be interpreted as logical implication; it is literally true, for instance, that
because we know that
and is isomorphic to (assuming no mistakes made by me):
Worth noting how small the final poset is in comparison to the preorder! The preorder has vertices but the induced poset has only .
Then the translation is
Note how while has three arrows, has only two; this demonstrates how translation is not ‘lossless’. The extrusion is
Due to limitations of my tooling, I’m sadly unable to draw identity arrows on these diagrams. The input relation is supposed to have all identities, and the output relation has some subset of those. Then:
If the operation is swapped out with we obtain an example of extrusions not preserving transitivity.
Equivalently,
If you’ll excuse the inattention, won’t give full proofs of these equivalencies (they are not all that complex). But we will say a few words: is equivalent to the diagrammatic definition essentially by definition; one can consider to be a symbolic expression of the definition of . is equivalent to with a little algebra, and to with a little more.
by choosing we get
in other words, .
Thus despite not being related by .
since is gradual then we may 〈🌷 19, shrink〉 it to conclude that and likewise for , giving:
which entails in particular that
which implies that .
By the lifting lemma this becomes simply , which is to say . Now we are done.
Proof (Diagrammatic). Say and . Then we have
for some . Here the two embedded bowtie diagrams come from the assumed isomorphisms. Dashed arrows are drawn on top and are also true. The fact that holds is because we know and we also know that since know that is the caboose of a performance train starting at .
As subdiagrams we have both of the following
The former diagram entails that , which means that . The latter diagram reorganizes to
which by the lifting lemma means that , meaning that .
Hence , so . Composing with the already-given isomorphisms and we get that
as desired.
Proof