Optimal reduction with sausages
When trying to write a normalisation algorithm for classical linear logic, it leads me back to optimal reduction.
The original implementation of optimal reduction algorithm has a problem of accumulating control operator nodes. They decide how fan nodes should interact with each other. Without this problem we'd have a fairly nice normaliser there as it can handle additives/exponentials without much trouble.
The original algorithm is simple enough to introduce, so I'll do it quickly. First lets create graph with few nodes like these:
data Tm a= Link a| Drop| Fan Int (Tm a) (Tm a)| Croissant Int (Tm a)| Bracket Int (Tm a)
Each link connects two nodes from their non-principal edges. In addition to this there is a notion of what forms a valid structure.
Two nodes connecting from their principal edges form an active pair that can be cut away. When nodes are same class and numbered in same way, they annihilate each other. Otherwise lower-numbered node is "slid" past the another. If the slid node is croissant, it decrements the index of the another node. If it's a bracket, it increments other node's index.
cut :: Tm a -> Tm a -> State ()cut x y (class x == class y && depth x == depth y) = annihilate x ycut x y (depth x <= depth y) = commute x (effect x y)cut x y = commute y (effect y x)annihilate :: Tm a -> Tm a -> State ()annihilate Drop Drop = pure ()annihilate (Fan _ x y) (Fan z w) = docut x zcut y wannihilate (Croissant _ x) (Croissant _ y) = cut x yannihilate (Bracket _ x) (Bracket _ y) = cut x yeffect :: Tm a -> (Tm a -> Tm a)effect (Croissant _ _) = modify (\x -> x-1)effect (Bracket _ _) = modify (+1)effect _ = idmodify :: (Int -> Int) -> Tm a -> Tm amodify f (Croissant i x) = (Croissant (f i) x)modify f (Bracket i x) = (Bracket (f i) x)modify f (Fan i x y) = (Fan (f i) x y)modify _ a = acommute :: Tm a -> Tm a -> State ()-- commute passes elements past each other and duplicate them.
The index in each node decides whether the structures are related and they should annihilate, or whether they're different and should duplicate each other.
Justifications in nodes
I added some additional nodes and replaced integers with "justification" -structures. I have an implementation ready so I'm using it to explain.
data Tm a b= Link a| Opt b (Tm a b) (Tm a b)| On b (Tm a b) (Tm a b)| Exp b (Tm a b)| At b (Tm a b)| Fan b (Tm a b) (Tm a b)| Pair (Tm a b) (Tm a b)| Index Bool (Tm a b)| Read (Tm a b)| Dropderiving (Show, Eq)data J s= Decided Bool| Duplicated (Maybe (STRef s (J s)))(STRef s (J s))(STRef s (J s))| Erased| Instantiated| Rescoped (STRef s (J s)) (STRef s (J s))| Unbound
Justifications link structures together, Example. We "justify" each "On" with some "Opt".
To understand what's going on here, we need to consider each structure as a strategy to successfully carry out some interaction. For example, this structure might represent a copycat strategy.
*Linc> norm $ Structure (Pair (Link 0) (Link 0)) 1 0 []Structure {term = Pair (Link 0) (Link 0),link_count = 1,opt_count = 0,cuts = [] }
Each cut represents composition of two strategies. For example, here's the same strategy but with bit of indirection:
*Linc> norm $ Structure (Pair (Link 0) (Link 1)) 3 0[ ((Pair (Link 2) (Link 2)), (Pair (Link 1) (Link 0))) ]Structure {term = Pair (Link 0) (Link 0),link_count = 1,opt_count = 0,cuts = [] }
Here's a step-through of the reduction:
Structure {term = Pair (Link 0) (Link 1),link_count = 3,opt_count = 0,cuts = [(Link 2,Link 1),(Link 2,Link 0)] }Structure {term = Pair (Link 0) (Link 1),link_count = 2,opt_count = 0,cuts = [(Link 1,Link 0)] }Structure {term = Pair (Link 0) (Link 0),link_count = 1,opt_count = 0,cuts = [] }
The justifications arise when we introduce additives and exponential modality.
As an example, take this structure that might populate the type (~a⊕b)⅋(~b&a).
Structure {term = Pair (Opt 0 (Link 0) (Link 1))(On 0 (Index True (Link 0)) (Index False (Link 1))),link_count = 2,opt_count = 1,cuts = [] }
So if we present this as a strategy, it shows a strategy where we provide an option on left side and decide something on the right side. Things progress after those decisions.
Now, you could start with (~b&a).
You may either resolve this by Index False {~b} where you supply a hole for b.
Or then by Index True {a} where you supply a.
You get either one of those eventually,
but you can't be certain about what to do
before an option you have to provide is resolved.
You can justify the access to either a or ~b after you construct "On"
with the justification of the option whose contents you want to access.
"Wait for that thing before deciding on what to do here".
The "Exp x" - "At x" form a similar pair as "Opt x" - "On x".
This also justifies an access inside an another structure.
You can access inside !a if you're required to provide ?b,
once you justify that you can do so.
If the item used for justification is resolved, then the justifications must resolve as well. Exponential may resolve through instantiation, brought across a scope or by being discarded or duplicated. Option may resolve through selection, and being discarded or duplicated inside an exponential.
Here's how the earlier construct might resolve when option is filled:
Structure {term = Pair (Link 0) (On 0 (Index True (Link 1))(Index False (Link 2))),link_count = 3,opt_count = 1,cuts = [(Index False (Link 0),Opt 0 (Link 1) (Link 2))] }Structure {term = Pair (Link 0) (Index True (Link 1)),link_count = 2,opt_count = 0,cuts = [(Link 0,Link 1)] }Structure {term = Pair (Link 0) (Index True (Link 0)),link_count = 1,opt_count = 0,cuts = [] }
Note in the earlier one we gave "False", so we chose the left branch. In the next one the right branch is selected:
Structure {term = Pair (Link 0) (On 0 (Index True (Link 1))(Index False (Link 2))),link_count = 3,opt_count = 1,cuts = [(Index True (Link 0),Opt 0 (Link 1) (Link 2))] }Structure {term = Pair (Link 0) (Index False (Link 1)),link_count = 2,opt_count = 0,cuts = [(Link 0,Link 1)] }Structure {term = Pair (Link 0) (Index False (Link 0)),link_count = 1,opt_count = 0,cuts = [] }
The next example revealed a bug in the readback and commutation. That is an one benefit from explaining and documenting things.
I told that Option may be duplicated inside an exponential. Lets illustrate that with a fan in place of that index.
Structure {term = Pair (Pair (Link 0) (Link 1))(On 0 (Index True (Link 2)) (Index False (Link 3))),link_count = 4,opt_count = 2,cuts = [(Fan 1 (Link 0) (Link 1),Opt 0 (Link 2) (Link 3))] }Structure {term = Pair (Pair (Link 0) (Link 1))(Fan 0 (On 1 (Index True (Link 2)) (Index False (Link 3)))(On 2 (Index True (Link 4)) (Index False (Link 5)))),link_count = 10,opt_count = 4,cuts = [(Link 0,Opt 1 (Link 6) (Link 7)),(Link 1,Opt 2 (Link 8) (Link 9)),(Fan 3 (Link 6) (Link 8),Fan 3 (Link 2) (Link 4)),(Fan 3 (Link 7) (Link 9),Fan 3 (Link 3) (Link 5))] }
After that second step, look at the Fan 3 here.
After the "Fan 1 >< Opt 0" reduction takes place,
the justification ends up being splitted.
The original justification is signaled with duplication
and becomes an internal copying fan,
while new justifications are created.
The original fan passes through the On 0, duplicating it in two directions.
If you draw the result, it forms a shape where the "On" -structure between two fans. I remember there was a paper that called these kind of structures "sausages" due to how they look like. It's more clear with "At" -struct where the fan splits the "At" clearly into two.
/------- At x ------\-Fan-I-| |-Fan-J-\------- At y ------/
Anyway, when we continue with the example.
Structure {term = Pair (Pair (Opt 0 (Link 0) (Link 1)) (Link 2))(Fan 1 (On 0 (Index True (Link 3)) (Index False (Link 4)))(On 2 (Index True (Link 5)) (Index False (Link 6)))),link_count = 9,opt_count = 4,cuts = [(Link 2,Opt 2 (Link 7) (Link 8)),(Fan 3 (Link 0) (Link 7),Fan 3 (Link 3) (Link 5)),(Fan 3 (Link 1) (Link 8),Fan 3 (Link 4) (Link 6))] }Structure {term = Pair (Pair (Opt 0 (Link 0) (Link 1)) (Opt 1 (Link 2) (Link 3)))(Fan 2 (On 0 (Index True (Link 4)) (Index False (Link 5)))(On 1 (Index True (Link 6)) (Index False (Link 7)))),link_count = 8,opt_count = 4,cuts = [(Fan 3 (Link 0) (Link 2),Fan 3 (Link 4) (Link 6)),(Fan 3 (Link 1) (Link 3),Fan 3 (Link 5) (Link 7))] }
At this point the Fans are getting resolved. There was not much to copy for them.
Structure {term = Pair (Pair (Opt 0 (Link 0) (Link 1)) (Opt 1 (Link 2) (Link 3)))(Fan 2 (On 0 (Index True (Link 0)) (Index False (Link 4)))(On 1 (Index True (Link 2)) (Index False (Link 5)))),link_count = 6,opt_count = 4,cuts = [(Fan 3 (Link 1) (Link 3),Fan 3 (Link 4) (Link 5))] }Structure {term = Pair (Pair (Opt 0 (Link 0) (Link 1)) (Opt 1 (Link 2) (Link 3)))(Fan 2 (On 0 (Index True (Link 0)) (Index False (Link 1)))(On 1 (Index True (Link 2)) (Index False (Link 3)))),link_count = 4,opt_count = 3,cuts = []}
And we are left with the original fan on the other side of the structure.
Fan behavior & structure
When a fan passes a structure it copies, it essentially passes through the structure but initiates a separate duplication inside that structure that is "justified" with the duplication of the construct.
The fan requires a justification as well though. This allows them to be paired up, but also records the event of duplication that can be then used to erase the fan when the duplication result would be erased anyway.
The duplication is exposed so we end up with fans in the readback structures. This was a last-minute update so it's not visible in the examples. It's visible in the annotated source code though.
Exponents and scoping
So far it's looking plausible, but what to do with "Exp i >< At j" -case?
Since scoping forms justification structures, and they should remain valid during reduction, there's exactly one way how this can be concluded.
Exponent must be "rescoped" inside the structure it enters.
This means that The "At j" must be transmitted through "Exp i".
It is most convenient to replace 'At i x' with "At j (At k x)",
where k is a new justification for the passed exponent.
Structural recursion
Implementing structural recursion into this system should not be a big problem.
You need to introduce structure that fills a type (!(F y) ⅋ ~y) ⊸ (Ind F)
where F is a functor.
I'll try to implement structural recursion later on. Before that I'll try to get some typechecking and maybe some syntax over these structures.
Conclusion
You can download Linc.hs and try your own experiments with it.
Since redundant duplications are erased, and every control structure cannot appear without valid justification, it means that control nodes should no longer accumulate.
I can't be certain that this thing is reducing structures optimally, like the original algorithm did, but I were looking at a normaliser for classical linear logic here. I likely got that one this time.
And if I didn't get it this time, it'll perhaps fail in an interesting way, revealing something about optimal reduction.
Update: The "On >< At" -case is missing. I'd guess quick fix is to just duplicate the exponential into the "On". But it also reveals the justifications require somewhat strict ordering.