|
|
|
|
|
by throwaway13qf85
4419 days ago
|
|
In case anyone is turned off by the expectation of wishy-washy flim-flam, it's worth noting that Graham Priest may be a professor of philosophy, but is most well known for his work in logic, particularly in non-standard logics (i.e. not propositional or predicate logic) that allow non-boolean truth values, or weaken or remove some of the axioms of classical logic. I assume that what's relevant here will be his work on paraconsistent logics (which allow contradictions) but I think an equally interesting line of work is linear logics. It's of interest to computer scientists because of its relationship to linear type theory (in the same way that the Curry-Howard correspondence links type theory and classical logic) and because it has close relationships with quantum computing. In particular, you are not allowed to delete or duplicate elements/propositions/types (corresponding to physical processes that cannot arbitrarily create or destroy particles, the "no deletion theorem" and "no cloning theorem" of quantum information theory), so functions of the type duplicate :: a -> (a, a)
and delete :: a -> ()
are not allowed in a linear type system. Practically, this means that many operations can be optimized by the compiler to in-place mutations, because it is guaranteed that there is only ever one reference to a particular object. |
|
PS: Yet another 1960's discovery that keeps being renamed and rediscovered.