Poi: Pragmatic point-free theorem prover assistant in Rust | Hacker News Reader

Poi: Pragmatic point-free theorem prover assistant in Rust

github.com

71 pointsadamnemecek35 comments

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?

         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.

'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'.

Oh! 'not ⨯ not' I thought 'x' was maybe a variable or something.

> '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?

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.

So a path is a higher order function? But then why is not also a path?

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.

Thanks, that's a very clear explanation.

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.

Nobody except the author seems to understand "path semantics".

https://old.reddit.com/r/rust/comments/bn5eoz/since_some_peo...

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.

The theory is still changing. Five years is not that long of time period.

Some research papers at least?

Surely it can’t be changing so much that it’s impossible to produce an accessible explanation of the fundamentals.

For comparison, it took about four years from Voevodsky formulating the univalence axiom to the publication of the HoTT book.

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:

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.

Harsh, but I had fun reading about J.S. Carberry in Wikipedia :)

Point-free notation is used here mainly as a device for obscuring notation.

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:

                 not x not
         (a, b) ---------> (not(a), not(b))
              |            |
          and |            | or
              V            V
       and(a,b) ---------> not(and(a, b)) = or(not(a), not(b))
                   not

(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)".

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).

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

Great work!

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.

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

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?

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.

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.

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.

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.

>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.

Where are those names coming from-ish?

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)

Reply on news.ycombinator.com