4 ms·

> 'not' and 'not x not' are paths What's a "path", though? Why is it not a computation to map 0 to 1 and 1 to 0?

andrewflnr 6y ago
They seem to be maps between computations. Seems to me that should be a computation on other computations, but I'm sure it's simpler to have nice distinct levels. Honestly I'm confused why you're asking, since I understood that example based on your diagram below...
- tom_mellior 6y ago
  In my diagram everything is a computation (as I understand it): From (a, b) you compute and(a, b), from which you compute not(and(a, b)). Alternatively, from (a, b) you compute (not(a), not(b)), from which you compute or(not(a), not(b)). The "and" and "or" steps are applications of functions, i.e., computations. The "not" steps are also applications of a function, why aren't those computations? I guess you might say that applying the function (not x not) is somehow a higher-order "computation on other computations", so that step might be a "path" (if that's the meaning, the term is ridiculously badly chosen). But the bottom edge is simply applying the "not" function to some binary data.
  - YeGoblynQueenne 6y ago
    So a path is a higher order function? But then why is not also a path?
YeGoblynQueenne 6y ago
Also confused about this, btw. Why are some functions "paths" whereas other functions are "computations"? Additionally, I honestly share no intuition that the term "path" is meant to convey. At a very big guess it sounds to me like the "path" that a bit takes through a theoretical computing machine of some kind. But I really don't understand the term.
- lmm 6y ago
  It's (at least usually; it sounds like this guy is doing something non-standard) meant to give you the intuition of a path through a space - a line from point a to point b that possibly wiggles about a bit in between. Formally it's a continuous function from [0, 1] to the space that sends 0 to a and 1 to b - so if p is a path then p(0.5) is "halfway along" the path, p(0.25) is a quarter of the way along the path, and so on. The concept of a path in the space {true, false} is kind of trivial - any function into that space is (topologically) continuous - but the intuition should be something like a path between two points on a 2D plane.
  - YeGoblynQueenne 6y ago
    Thanks, that's a very clear explanation.
lmm 6y ago
In homotopy type theory, a path from a to b is a (topologically) continuous function from [0, 1] that sends 0 to a and 1 to b. For booleans this distinction doesn't matter because every function to booleans is continuous, but in the general case not every correspondence is a path and you can't lift things along an arbitrary correspondence. But having looked at the reddit thread it sounds like this is some non-standard usage and this dude is a crank.
- tom_mellior 6y ago
  Thanks for the explanation. I can see how "not" fits this definition (as opposed to "and" and "or") by the accident of being a unary function. Whatever the author is trying to illustrate doesn't seem especially deep. Having looked at some other scattered writings, I agree with them being a crackpot.

They seem to be maps between computations. Seems to me that should be a computation on other computations, but I'm sure it's simpler to have nice distinct levels. Honestly I'm confused why you're asking, since I understood that example based on your diagram below...

tom_mellior 6y ago
In my diagram everything is a computation (as I understand it): From (a, b) you compute and(a, b), from which you compute not(and(a, b)). Alternatively, from (a, b) you compute (not(a), not(b)), from which you compute or(not(a), not(b)). The "and" and "or" steps are applications of functions, i.e., computations. The "not" steps are also applications of a function, why aren't those computations? I guess you might say that applying the function (not x not) is somehow a higher-order "computation on other computations", so that step might be a "path" (if that's the meaning, the term is ridiculously badly chosen). But the bottom edge is simply applying the "not" function to some binary data.
- YeGoblynQueenne 6y ago
  So a path is a higher order function? But then why is not also a path?

YeGoblynQueenne 6y ago

Also confused about this, btw. Why are some functions "paths" whereas other functions are "computations"? Additionally, I honestly share no intuition that the term "path" is meant to convey. At a very big guess it sounds to me like the "path" that a bit takes through a theoretical computing machine of some kind. But I really don't understand the term.

lmm 6y ago
It's (at least usually; it sounds like this guy is doing something non-standard) meant to give you the intuition of a path through a space - a line from point a to point b that possibly wiggles about a bit in between. Formally it's a continuous function from [0, 1] to the space that sends 0 to a and 1 to b - so if p is a path then p(0.5) is "halfway along" the path, p(0.25) is a quarter of the way along the path, and so on. The concept of a path in the space {true, false} is kind of trivial - any function into that space is (topologically) continuous - but the intuition should be something like a path between two points on a 2D plane.
- YeGoblynQueenne 6y ago
  Thanks, that's a very clear explanation.

lmm 6y ago

In homotopy type theory, a path from a to b is a (topologically) continuous function from [0, 1] that sends 0 to a and 1 to b. For booleans this distinction doesn't matter because every function to booleans is continuous, but in the general case not every correspondence is a path and you can't lift things along an arbitrary correspondence. But having looked at the reddit thread it sounds like this is some non-standard usage and this dude is a crank.

tom_mellior 6y ago
Thanks for the explanation. I can see how "not" fits this definition (as opposed to "and" and "or") by the accident of being a unary function. Whatever the author is trying to illustrate doesn't seem especially deep. Having looked at some other scattered writings, I agree with them being a crackpot.