Embed Notice

@chjara just because I like this and because you could nerd snipe me with a feather, I'll utilize all of my 5k chars to explain this just because it's so degenerate I love this (and I've also gotten interested in theoretical PL theory). |

WARNING: I am trying to uncover this but I have no clue how to explain certain bits or how to say them, especially towards the end, I genuinely tried but this is hard (at least without me having prior knowledge in reversible computation). this shit is cryptic, I have no idea why I spent so much time trying to understand this, why am I nerd sniped so easily, but at least it is something, a starting point, although wow do I feel dumb looking at reversible computation journals

• for the purposes of this, we have left-expressions which can either be a variable, a constructor c which takes multiple left-expressions (think of it like new Foo(1, 2, "deez", f(1, 2, 3)) but each one of those is a left expression) or ⌊l⌋ which will be defined later
• it took me a bit of digging through the article, but it defines ⟨v⟩ and ⟨v, v'⟩ as unary, respectively binary tuples (as a shorthand) (I am so sorry if you don't have a good Unicode font for this)
• ⌊.⌋ is the duplicity/equality operator and is defined as follows: ⌊⟨v⟩⌋ = ⟨v, v⟩ (the duplication part) and ⌊⟨v, v'⟩⌋ is ⟨v⟩ if v = v' and ⟨v, v'⟩ elsewhere (the equality part). it's defined like this because it's self-inverse, so you can use it to determine the input from the output (⌊⟨v, v'⟩⌋ = ⟨v⟩ iff v = v' and viceversa)
• in the article, they also let you pattern match over pairs and the dup/eq operator, but it's not important for our purposes
• CON means constructor and VAR means, obviously, variable
• here's where the meat and potatoes of this whole ass thing is in. specifically, v ⊲ l ⇝ σ represents what's called a "left-exp judgement" (whatever the fuck that means) and σ is named "most general matcher" (which is essentially a generalization of pattern matching, I'll get into that in a little bit)
• a substitution σ is a mapping of variables to values (so think of it a bit like... well, an actual substitution, or more mathematically, {x1 ↦ v1, x2 ↦ v2, ...}). in particular, {} is the identity, (σl) is σ applied to the left-expression l and l↓ is the application of all ⌊.⌋ in l by how I defined it a couple of points ago
• NOW we can get into what the fuck that image means. that's technically how the most general matcher is being defined. what it says is something that's pretty intuitive in a sense, but put in an really abstract way cuz this is theoretical CS
• for VAR, what it says that if you have a value and a variable, your σ is just a substitution, aka you substitute x with v
• for CON it's a bit more complicated, but essentially it says that if you give me a set of individual values and their corresponding left-expressions and you get a set of substitutions (not necessarily unique), then if you make me match a constructor made of that set of values with a constructor made from those left-expressions, the substitution you're making is just the disjoint union of those earlier substitutions, almost like the most encompassing substitution that fits those. think of this as e.g. pattern matching over Box or Result or even pattern matching over S(n) if you're familiar with Peano arithmetic
• DUP/EQ is a bit simpler, it's essentially just transitivity at play. to be specific, ⌊v⌋↓ = v' says that if you apply ⌊.⌋ to ⌊v⌋ and you get a single value v' and if that v' ⊲ l gives you a substitution, then it follows that v ⊲ ⌊l⌋ gives you that same substitution. as I understand it, it would be the same as if you have a monad or some sort of substitution over a boxed integer

just 1% clearer, which is better than 0%... I guess?