It's much more than that: It's the principal Java library for accessing and creating Word, Excel, Powerpoint, and other Microsoft format documents. And to the point here, it contains an equation solver, so there are possible points of proximity.
But my overarching point is that for some large segment of programmers if you say you're working on a project called POI, they're going to think Apache POI.
who really has a problem disambiguating when searching with other keywords? it's not like search engine are hashtables. have you ever been unable to find the right thing after adding at most two keywords? even more likely that google knows if you're searching for apache poi you're not interested in theorem proving so they point you to the right entity immediately.
People love to name projects after things in physics (particles mainly) which can make googling slightly annoying although luckily 99% of the results I'm looking for are on stackexchange or arxiv.
>this is the most pointless comment genre on hn...who really has a problem disambiguating when searching with other keywords?
Why the snarky reply? Notifying a project of possible conflicts that would reduce its visibility is hardly pointless.
And in this specific case, if you spend a moment looking at Apache POI, you'll see that it contains an equation solver, so yes indeed when looking for one you could need to disambiguate the results.
not x not
o ---------> o o -------> path-space
| | |
and | | or |
V V |
o ---------> o V
not computation
Huh? I don't get it. This is supposed to be DeMorgan's in this weird notation. I know DeMorgan's but I don't get that diagram. I'm reading about path semantics via the links in the github but it seems to me you need to already have a bit of a background in a certain, shall we say, remote, area of either mathematics of computer science, or the mathematics of computer science in order to follow quickly without spending time going down wikipedia rabbit holes.
Anyway, sounds like an interesting thing to spend some free time on. Thanks.
'not' and 'not x not' are paths, 'and' and 'or' are computations. ('not x not' is just the path on a pair that applies 'not' to each of the two elements - products are pairs, sums are either-or). Diagrams like this generally express a theorem as the diagram commuting. So the theorem is that if you compute 'and' and then lift the result along the path 'not', that's the same as lifting the input along the path 'not x not' and computing 'or'. More mind-bendingly, but ultimately more powerfully, it's also the statement that if you lift the whole computation 'and' along this kind of higher-level path that applies 'not' to everything, the result is 'or'.
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...
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.
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.
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.
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.
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.
I talk to the author a bunch and I believe some of this work is based on our convos. I don't fully understand path semantics however, I can tell that it's similar to my pet theories.
Path semantics is still very much a work in progress so it's hard for outsiders to really get into it.
I would expect a theory that has been a ‘work in progress’ for some five years now to have a readily available, comprehensible introduction to its basic concepts and motivation at the very least. I am yet to see such.
How long did it take Voevodsky to write the coq proofs? Path semantics is very much tied to programming and in the process, Sven has created several programming languages to explore the idea.
Also, in the mean time he has worked on other things.
Working on other things didn’t seem to stop him from writing 399 single-page papers, all of which are full of undefined, nonstandard notation and prose that reads like the output of GPT-2:
If that time were spent on writing just one, but clearly written explanation of the core idea, I might have been more sympathetic to the project. As it is though, ‘path semantics’ is an exercise in obscurantism at best and in psychoceramics at worst.
As for what "path-space" notation means, even the author appears confused, since they claim that "and[not] <=> or" corresponds to "If you flip the input and output bits of an `and` function, ..." corresponds to "not(and(a, b)) = or(not(a), not(b))", but this clearly isn't the case: flipping both the inputs and outputs of `and` to get `or` would be "not(and(not(a), not(b))) = or(a, b)".
Thanks, annotating the points does make it easier to follow. For some reason I misunderstood the purpose of this to be getting rid of arguments to functions so it didn't occur to me to do what you did (well, in my head).
1. How is this supposed to be point-free? a and b are clearly arguments. Wouldn't you replace them with obscure projection functions if you really believed that being point-free was useful?
2. What about this are inputs of the system, and what are the outputs? I'm guessing > marks what the user input, and the other lines are rewrites produced by the system. In that case, why did it stop after a few steps when it was clearly able to continue?
3. Don't you need induction to prove this theorem? Where is the induction step? Where is the base case?
4. Are some of the rewrites based on lemmas already proved and stored in the system? If so, wouldn't it be useful to mark such rewrites?
This seems very cool, but I didn’t understand clearly what it is used for. More spelling out of the purpose would help, and discussion of similar software.
36 comments
[ 2.9 ms ] story [ 85.8 ms ] threadBut my overarching point is that for some large segment of programmers if you say you're working on a project called POI, they're going to think Apache POI.
who really has a problem disambiguating when searching with other keywords? it's not like search engine are hashtables. have you ever been unable to find the right thing after adding at most two keywords? even more likely that google knows if you're searching for apache poi you're not interested in theorem proving so they point you to the right entity immediately.
People love to name projects after things in physics (particles mainly) which can make googling slightly annoying although luckily 99% of the results I'm looking for are on stackexchange or arxiv.
Why the snarky reply? Notifying a project of possible conflicts that would reduce its visibility is hardly pointless.
And in this specific case, if you spend a moment looking at Apache POI, you'll see that it contains an equation solver, so yes indeed when looking for one you could need to disambiguate the results.
[1] https://en.m.wikipedia.org/wiki/Poi_(performance_art)
Great work!
Anyway, sounds like an interesting thing to spend some free time on. Thanks.
Oh, please do ELI5 if anyone can.
What's a "path", though? Why is it not a computation to map 0 to 1 and 1 to 0?
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.
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.
But having looked at the reddit thread it sounds like this is some non-standard usage and this dude is a crank.
https://old.reddit.com/r/rust/comments/bn5eoz/since_some_peo...
Path semantics is still very much a work in progress so it's hard for outsiders to really get into it.
For comparison, it took about four years from Voevodsky formulating the univalence axiom to the publication of the HoTT book.
Also, in the mean time he has worked on other things.
https://github.com/advancedresearch/path_semantics/tree/mast...
If that time were spent on writing just one, but clearly written explanation of the core idea, I might have been more sympathetic to the project. As it is though, ‘path semantics’ is an exercise in obscurantism at best and in psychoceramics at worst.
A function "f x g" pairs up f and g and applies them separately to a tuple of arguments: (f x g)(a, b) = (f(a), g(b)).
The commutative diagram becomes clearer when we label the points:
(This is the same as what user lmm wrote in prose in https://news.ycombinator.com/item?id=23203478.)As for what "path-space" notation means, even the author appears confused, since they claim that "and[not] <=> or" corresponds to "If you flip the input and output bits of an `and` function, ..." corresponds to "not(and(a, b)) = or(not(a), not(b))", but this clearly isn't the case: flipping both the inputs and outputs of `and` to get `or` would be "not(and(not(a), not(b))) = or(a, b)".
1. How is this supposed to be point-free? a and b are clearly arguments. Wouldn't you replace them with obscure projection functions if you really believed that being point-free was useful?
2. What about this are inputs of the system, and what are the outputs? I'm guessing > marks what the user input, and the other lines are rewrites produced by the system. In that case, why did it stop after a few steps when it was clearly able to continue?
3. Don't you need induction to prove this theorem? Where is the induction step? Where is the base case?
4. Are some of the rewrites based on lemmas already proved and stored in the system? If so, wouldn't it be useful to mark such rewrites?