5 ms·

Poi: Pragmatic point-free theorem prover assistant in Rust

71 points by adamnemecek 6y ago

ternaryoperator 6y ago
Sort of an unfortunate name collision with Apache Poi, which is one of the largest projects at the Apache Software Foundation.
- nurettin 6y ago
  Apache Poi and Poi does look similar, but what do you mean by one of the largest? Isn't Apache Poi just an excel reader/writer library?
  - ternaryoperator 6y ago
    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.
- littlestymaar 6y ago
  It may be large somehow, but I had never heard of it before you mentioned it. I suspect the author is in the same situation.
- throwlaplace 6y ago
  this is the most pointless comment genre on hn. 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.
  - deleted 6y ago
    [deleted]
  - mhh__ 6y ago
    It can be fairly annoying. 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.
  - ternaryoperator 6y ago
    >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.
- numpad0 6y ago
  Where are those names coming from-ish?
  - mkl 6y ago
    Well I expect it's not the Māori performance art [1], but that's the first thing New Zealanders will think of. [1] https://en.m.wikipedia.org/wiki/Poi_(performance_art) https://en.m.wikipedia.org/wiki/Poi_(performance_art)
_fq4v 6y ago
Point-free paths sound similar to cubical type theory from HoTT. Is there a relation? Great work!
YeGoblynQueenne 6y ago
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. Oh, please do ELI5 if anyone can.
- lmm 6y ago
  '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'.
  - carapace 6y ago
    Oh! 'not ⨯ not' I thought 'x' was maybe a variable or something.
  - tom_mellior 6y ago
    > '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
Example: > (len . concat)(a, b) (len · concat)(a, b) (len · concat)(a)(b) (concat[len] · (len · fst, len · snd))(a)(b) (add · (len · fst, len · snd))(a)(b) <=> add((len · fst)(a)(b), (len · snd)(a)(b)) > add((len · fst)(a)(b), (len · snd)(a)(b)) add((len · fst)(a)(b), (len · snd)(a)(b)) add((len · fst)(a)(b))((len · snd)(a)(b)) add(len(a))((len · snd)(a)(b)) add(len(a))(len(b)) This raises a few questions: 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?
bo1024 6y ago
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.

71 points by adamnemecek 6y ago

Sort of an unfortunate name collision with Apache Poi, which is one of the largest projects at the Apache Software Foundation.

nurettin 6y ago
Apache Poi and Poi does look similar, but what do you mean by one of the largest? Isn't Apache Poi just an excel reader/writer library?
- ternaryoperator 6y ago
  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.
littlestymaar 6y ago
It may be large somehow, but I had never heard of it before you mentioned it. I suspect the author is in the same situation.
throwlaplace 6y ago
this is the most pointless comment genre on hn. 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.
- deleted 6y ago
  [deleted]
- mhh__ 6y ago
  It can be fairly annoying. 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.
- ternaryoperator 6y ago
  >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.
numpad0 6y ago
Where are those names coming from-ish?
- mkl 6y ago
  Well I expect it's not the Māori performance art [1], but that's the first thing New Zealanders will think of. [1] https://en.m.wikipedia.org/wiki/Poi_(performance_art) https://en.m.wikipedia.org/wiki/Poi_(performance_art)

_fq4v 6y ago

Point-free paths sound similar to cubical type theory from HoTT. Is there a relation? Great work!

YeGoblynQueenne 6y ago

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. Oh, please do ELI5 if anyone can.

lmm 6y ago
'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'.
- carapace 6y ago
  Oh! 'not ⨯ not' I thought 'x' was maybe a variable or something.
- tom_mellior 6y ago
  > '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

Example: > (len . concat)(a, b) (len · concat)(a, b) (len · concat)(a)(b) (concat[len] · (len · fst, len · snd))(a)(b) (add · (len · fst, len · snd))(a)(b) <=> add((len · fst)(a)(b), (len · snd)(a)(b)) > add((len · fst)(a)(b), (len · snd)(a)(b)) add((len · fst)(a)(b), (len · snd)(a)(b)) add((len · fst)(a)(b))((len · snd)(a)(b)) add(len(a))((len · snd)(a)(b)) add(len(a))(len(b)) This raises a few questions: 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?

bo1024 6y ago

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.