3 ms·
Reminds me of Baez's Rosetta stone paper [1]. It's about some common threads in physics, math, logic, and programming. A completely different set of connections
by jfoutz 10y ago
Reminds me of Baez's Rosetta stone paper [1]. It's about some common threads in physics, math, logic, and programming. A completely different set of connections that what you'd see in Gödel, Escher, Bach.
I kinda sorta remember linear logic having the option for an infinite source, and an infinite sink for things you might want to deal with. A business has an infinite number of customers, but each specific transaction needs to be handled in a very specific way. You give me a dollar, and i give you a hamburger or french fries, your choice.
A light, accessible overview of linear logic is here [2]. That has a few nice, simple examples. It's easier than the wikipedia article.
[1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf
[2] http://www.csl.sri.com/~lincoln/papers/sigact92.ps.gz http://www.csl.sri.com/~lincoln/papers/sigact92.ps.gz
- tel 10y agoBasically, non-linear variables are those with infinite duplication and sinks (they're "comonoids").
- mafribe 10y agoAnother option is affine types that give you "at most once" semantics, in contrast to linear types' "exactly once". If your language has non-termination then affine is easier to enforce. (Cf Rust.)
- tupshin 10y agoSure, but rust benefits from must_use annotations, which effectively turn those annotated affine types into linear types. Turns out they are both useful in a very overlapping venn-diagram kind of way.
- mafribe 10y agoHow does this deal with non-termination? Eg. declare x (must_use); P; use(x) (I apologies for the non-Rust-conforming pseudo-code.) The type-checker won't be able to tell if P terminates or not, whence x's use can't be enforced. That's a direct consequence of Rice's theorem (which in turn follows directly form the non-computability of the halting predicate).