Our computational system is now a _symmetric monoidal system with identities_.
September 7, 2025 at 3:12 PM
Our computational system is now a _symmetric monoidal system with identities_.
While the multiplicatives units were about creating resources out of nothing, the additive units are about _computations_ out of nothing. That's why their utility is relegated to discharging _impossible_ hypotheticals.
September 7, 2025 at 3:12 PM
While the multiplicatives units were about creating resources out of nothing, the additive units are about _computations_ out of nothing. That's why their utility is relegated to discharging _impossible_ hypotheticals.
Step 5: 0, ⊤
The multiplicatives have units, it makes sense to ask whether the additives can also have inverses. Indeed we can add them as 0, ⊤.
The multiplicatives have units, it makes sense to ask whether the additives can also have inverses. Indeed we can add them as 0, ⊤.
September 7, 2025 at 3:12 PM
Step 5: 0, ⊤
The multiplicatives have units, it makes sense to ask whether the additives can also have inverses. Indeed we can add them as 0, ⊤.
The multiplicatives have units, it makes sense to ask whether the additives can also have inverses. Indeed we can add them as 0, ⊤.
The penultimate step is convincing yourself that the rules of the linear logic are precisely the ones which _self-dual under completion_. That is, the rules that can produce the richest states (most states) while being dual.
September 7, 2025 at 3:12 PM
The penultimate step is convincing yourself that the rules of the linear logic are precisely the ones which _self-dual under completion_. That is, the rules that can produce the richest states (most states) while being dual.
Step 4: the dualities
What we've said so far was without looking (too much) at the _specific_ interaction rules.
What we've said so far was without looking (too much) at the _specific_ interaction rules.
September 7, 2025 at 3:12 PM
Step 4: the dualities
What we've said so far was without looking (too much) at the _specific_ interaction rules.
What we've said so far was without looking (too much) at the _specific_ interaction rules.
We accept that, of course, _global_ things can simply exist independently of _local_ computation. The interaction rules are still local, however there is global state unperturbed by local interaction.
September 7, 2025 at 3:12 PM
We accept that, of course, _global_ things can simply exist independently of _local_ computation. The interaction rules are still local, however there is global state unperturbed by local interaction.
Step 3: ?, !
We add the exponentials: ?, !. Whereas before we could only refer to transient state, now we can refer to _perennial, stable state_.
We add the exponentials: ?, !. Whereas before we could only refer to transient state, now we can refer to _perennial, stable state_.
September 7, 2025 at 3:12 PM
Step 3: ?, !
We add the exponentials: ?, !. Whereas before we could only refer to transient state, now we can refer to _perennial, stable state_.
We add the exponentials: ?, !. Whereas before we could only refer to transient state, now we can refer to _perennial, stable state_.
Here, state is ephemeral. Whatever this state means (if anything at all), is but a _transient state of an evolving system_. The system can visit a state multiple times, of course, but it has to create it every time (and at this point it can only visit a state a finitely number of times anyway).
September 7, 2025 at 3:12 PM
Here, state is ephemeral. Whatever this state means (if anything at all), is but a _transient state of an evolving system_. The system can visit a state multiple times, of course, but it has to create it every time (and at this point it can only visit a state a finitely number of times anyway).
Because we can make and eliminate things, the dynamics of the possible computational becomes more interesting. In particular we don't need extra-logical initial state.
September 7, 2025 at 3:12 PM
Because we can make and eliminate things, the dynamics of the possible computational becomes more interesting. In particular we don't need extra-logical initial state.
Unlike what we had before, which was a set of _fixed_, conserved resources, we can make 1 out of nothing. The set of resources is now _dynamic_.
September 7, 2025 at 3:12 PM
Unlike what we had before, which was a set of _fixed_, conserved resources, we can make 1 out of nothing. The set of resources is now _dynamic_.
Step 2: 1, ⊥
We add 1, ⊥. These allow making the resources and some of the rules we had before (the multiplicatives) in a monoid. This is useful.
We add 1, ⊥. These allow making the resources and some of the rules we had before (the multiplicatives) in a monoid. This is useful.
September 7, 2025 at 3:12 PM
Step 2: 1, ⊥
We add 1, ⊥. These allow making the resources and some of the rules we had before (the multiplicatives) in a monoid. This is useful.
We add 1, ⊥. These allow making the resources and some of the rules we had before (the multiplicatives) in a monoid. This is useful.
The axiom rule is kinda like a "virtual particle". It can split from nothing into complementary hypothesis, but ultimately it doesn't _do_ anything, merely its "branches" enable other resources to interact via cuts. We need the initial state to really make anything interesting happen.
September 7, 2025 at 3:12 PM
The axiom rule is kinda like a "virtual particle". It can split from nothing into complementary hypothesis, but ultimately it doesn't _do_ anything, merely its "branches" enable other resources to interact via cuts. We need the initial state to really make anything interesting happen.
Also note that we have a bit of a bootstrapping problem here. Where do the resources come from? They initial state had to be given to us "extra-logically".
September 7, 2025 at 3:12 PM
Also note that we have a bit of a bootstrapping problem here. Where do the resources come from? They initial state had to be given to us "extra-logically".
Don't worry about what these resources are, or why the rules are what they are (we'll come back to the specific rules later). Simply observe the symmetry of the rules and internalize the "conservation principle" implied by the computational rules.
September 7, 2025 at 3:12 PM
Don't worry about what these resources are, or why the rules are what they are (we'll come back to the specific rules later). Simply observe the symmetry of the rules and internalize the "conservation principle" implied by the computational rules.
The specific arrangement of resources using ⊗, ⅋, ⊕, & form a _state_, and the rules tells us how the state _evolves_.
September 7, 2025 at 3:12 PM
The specific arrangement of resources using ⊗, ⅋, ⊕, & form a _state_, and the rules tells us how the state _evolves_.
Step 1: ⊗, ⅋, ⊕, &
We're given a finite set of locally-interacting resources. All of them get preserved by interaction. The interaction rules pack and unpack resources using funny-looking symbols: ⊗, ⅋, ⊕, &.
We're given a finite set of locally-interacting resources. All of them get preserved by interaction. The interaction rules pack and unpack resources using funny-looking symbols: ⊗, ⅋, ⊕, &.
September 7, 2025 at 3:12 PM
Step 1: ⊗, ⅋, ⊕, &
We're given a finite set of locally-interacting resources. All of them get preserved by interaction. The interaction rules pack and unpack resources using funny-looking symbols: ⊗, ⅋, ⊕, &.
We're given a finite set of locally-interacting resources. All of them get preserved by interaction. The interaction rules pack and unpack resources using funny-looking symbols: ⊗, ⅋, ⊕, &.
Here we're doing something else, we'll be talking _only_ about the computational content of _sequent calculus itself_, not of any logic contained therein (here, linear logic). Let's begin.
September 7, 2025 at 3:12 PM
Here we're doing something else, we'll be talking _only_ about the computational content of _sequent calculus itself_, not of any logic contained therein (here, linear logic). Let's begin.
Note that when doing Curry-Howard correspondence we're necessarily internalizing logical deduction into internal connectives. For example, we can make a function-an internal object in the theory—out of a meta-level statement (sequent entailment).
September 7, 2025 at 3:12 PM
Note that when doing Curry-Howard correspondence we're necessarily internalizing logical deduction into internal connectives. For example, we can make a function-an internal object in the theory—out of a meta-level statement (sequent entailment).
Because the selection is sticky, you can have B2-execute and B3-search, just don't modify it! A click+release can have the exact same behavior (even if a menu is appears during on-click).
May 13, 2025 at 12:56 PM
Because the selection is sticky, you can have B2-execute and B3-search, just don't modify it! A click+release can have the exact same behavior (even if a menu is appears during on-click).
Of course, keep what is already great:
16. No settings, no options, no themes, no syntax highlighting, no keyboard based interface (the mouse is king).
16. No settings, no options, no themes, no syntax highlighting, no keyboard based interface (the mouse is king).
May 13, 2025 at 12:11 PM
Of course, keep what is already great:
16. No settings, no options, no themes, no syntax highlighting, no keyboard based interface (the mouse is king).
16. No settings, no options, no themes, no syntax highlighting, no keyboard based interface (the mouse is king).
14. Elastic tab support, or some better way of dealing with tabular data.
15. A better way of dealing with resize, right now acme does really bad when moving from a big monitor to a laptop because it preserves layout. I'd like a way to globally set layout independent of Dump.
15. A better way of dealing with resize, right now acme does really bad when moving from a big monitor to a laptop because it preserves layout. I'd like a way to globally set layout independent of Dump.
May 13, 2025 at 12:11 PM
14. Elastic tab support, or some better way of dealing with tabular data.
15. A better way of dealing with resize, right now acme does really bad when moving from a big monitor to a laptop because it preserves layout. I'd like a way to globally set layout independent of Dump.
15. A better way of dealing with resize, right now acme does really bad when moving from a big monitor to a laptop because it preserves layout. I'd like a way to globally set layout independent of Dump.
This should be done by a third party process writing in acme(4), acme(1) should not implement native markdown support or anything like that.
May 13, 2025 at 12:11 PM
This should be done by a third party process writing in acme(4), acme(1) should not implement native markdown support or anything like that.
13. Some sort of minimal markup support. Perhaps with colors. Not arbitrary colors, just like four or five predetermined colors that Acme programs could make use of (for example I'd like to see colors in my diffs).
May 13, 2025 at 12:11 PM
13. Some sort of minimal markup support. Perhaps with colors. Not arbitrary colors, just like four or five predetermined colors that Acme programs could make use of (for example I'd like to see colors in my diffs).