Understanding linear logic in five steps, purely computationally and without semantics. We'll explain linear logic as a _specific_ self-interactive computational system by looking at more and more specific self-interaction computational systems until we arrive at classical linear logic.
CC @robpike.io
Aram Hăvărneanu@xw.is · last yr.Ideas for a next generation text editor (Acme replacement): 1. Keep the Acme UI, but add rows, not just columns. Potentially make each window a full multiplexor (like rio(1), not 100% sure about this). 2. Make it multi-process/multi-machine again (like Sam, but better).
Ideas for a next generation text editor (Acme replacement): 1. Keep the Acme UI, but add rows, not just columns. Potentially make each window a full multiplexor (like rio(1), not 100% sure about this). 2. Make it multi-process/multi-machine again (like Sam, but better).
In a language that uses Curry-Howard you construct terms of some types, and the empty type denotes falsity.
I prefer programming *directly* with meanings (through types), and not indirectly through *codes*, what about you?
Partial evaluation seems to imply some degree of strictness and be at odds with lazy evaluation.
Aram Hăvărneanu@xw.is · 2y agoI believe β-reduction in interaction combinators is not monotonic with respect to partial evaluation. In other words only program reduction (no free variables) is β-optimal. Is this true?
I have a specific counter example in mind but it's for a non-λ-calculus system. I don't know if inets guarantee β-optimality for all computational systems or just for λ-calculus.
Aram Hăvărneanu@xw.is · 2y agoI believe β-reduction in interaction combinators is not monotonic with respect to partial evaluation. In other words only program reduction (no free variables) is β-optimal. Is this true?
I believe β-reduction in interaction combinators is not monotonic with respect to partial evaluation. In other words only program reduction (no free variables) is β-optimal. Is this true?
It’s funny how programmers not familiar with mathematics confuse types with sets, and mathematicians who don’t work in the foundations of mathematics confuse sets with types.