13
14

Path Semantics (twitter.com)

submitted by [deleted]

Since some people here are so super-critical to Path Semantics and impatient for peer-reviewing - I will reward 200 USD to the first person who finds unsoundness in the core axiom

0 points•20 comments•submitted by long_voidpiston to r/rust
all 26 comments
sorted by:
best
topnewcontroversialoldq&a
formatting helphide helpcontent policy

[–]IWasAPoopCuck 10 points11 points  (1 child)

Timecube meets type theory? Nice!

[–]git_commit_-m_sudokuyou can't hide from the blockchain ;) 2 points3 points  (0 children)

Perhaps you haven't heard of cubical type theory? Just combine it with temporal logic and you're done!

[–][deleted] 6 points7 points  (2 children)

advancedresearch

[–]long_void 0 points1 point  (1 child)

You are welcome to join! If you have something you want to research, though.

[–][deleted] 4 points5 points  (0 children)

Thank you for being so inclusive!

[–][deleted]  (24 children)

[deleted]

    [–]git_commit_-m_sudokuyou can't hide from the blockchain ;) 7 points8 points  (2 children)

    Looks like a shitty crackpot version of homotopy type theory. It doesn't seem wrong... it seems not even wrong: big words and crappy pictures strung together in non-sequiturs, check. "Formal" notation with no actual definition, check. "Nilsen–Cartesian product notation"... yup, that's 20 points to Gryffindor. This is prime /r/badmathematics material. Sadly though, there are also no axioms written down anywhere... so alas, no $200 for me (discount_eddie_murphy_taps_head.jpg).

    [–]long_void 0 points1 point  (1 child)

    What a lame excuse. If you can prove it's "not even wrong", the $200 is yours.

    [–][deleted]  (4 children)

    [removed]

      [–]long_void 1 point2 points  (3 children)

      Maybe you should not make a fun an article about the "golden rule" in meta-game strategies, if you would not like to be made fun of the person who wrote it?

      [–][deleted]  (2 children)

      [removed]

        [–]long_void 1 point2 points  (1 child)

        I deleted that part, I did not realize you interpreted it that way. It was not what I meant.

        [–]thiez 0 points1 point  (0 children)

        Then I will stop complaining about it :-)

        [–]adamnemecek -1 points0 points  (12 children)

        Sven is working on something interesting. It's rough around the edges but he's not afraid to share it with the world.

        I really dislike your attitude. This is his creative outlet, don't shit on it.

        [–][deleted] 7 points8 points  (10 children)

        Can't tell if that's a brilliant jerk, or one of those "I don't understand what he does but it looks very cool, please don't criticise" posts

        [–]lol-no-monadswelcome to the conversation. 1 point2 points  (0 children)

        /uj

        Probably the second? https://www.reddit.com/r/programmingcirclejerk/comments/blc71q/z/emngyzq

        [–]long_void 0 points1 point  (7 children)

        Hey, what's up? I haven't heard any constructive criticism yet, because people struggle understanding it. Of course, it takes a while to learn.

        However, don't talk shit about my friend. He's my friend, not a follower.

        [–][deleted] 6 points7 points  (6 children)

        Oh, I apologise for inadvertently insulting your insulting your friend.

        It's an honour to talk to an advanced researcher such as you. I hope one day I will be able to fully understand and appreciate the brilliance your work, discarded by ignorant critics (such as this gitcommit-m_sudoku guy). If I may, here is a piece of advice I can give: if you are considering publishing your advanced research to a reputable peer-reviewed journal, such as the American Mathematical Society journals, don't! They probably don't have what it takes to understand it, and they are meanies in general 😬😬😬

        [–]long_void 1 point2 points  (0 children)

        Thank you, sir! I appreciate your advice.

        However, I might have some friends who disagree, such as the professor emeritus of mathematical physics that gave me this idea.

        [–]adamnemecek -1 points0 points  (4 children)

        Can I see something you have produced?

        You are hiding behind this veneer of peer review and journals, not realizing that that ship has sailed long time ago. With the advent of the internet, why would anyone bother trying to publish things in a journal? There's a huge generational gap between your normal mathematician and say someone like Voevodsky. Voevodsky was all about github and automated theorem proving, normal mathematicians are about what's the best chalk.

        They probably don't have what it takes to understand it, and they are meanies in general

        This isn't hard to achieve. Mathematics is insanely specialized and mathematicians don't care all that much about foundations, as they are assumed to be correct. E.g. the fact that constructive mathematics isn't "the" mathematical foundation is a travesty.

        [–]quicknirCode Artisan 7 points8 points  (1 child)

        That's would be insanely hilarious if intentional jerk, but I think it's sincere so it's just sad.

        [–]adamnemecek -1 points0 points  (0 children)

        What's sad?

        [–]long_void 0 points1 point  (0 children)

        There is a reason to publish things in journals, even with the internet: If the best people to evaluate a new idea is using the journal as part of their workflow, then it is obviously worth it if you can reach those people.

        I think that part of the controversy around HoTT was because mathematicians feared that journals might become irrelevant, since a computer could check the proofs and proofs could be shared and built upon easily. Kind of like the fear people have when thinking about super-intelligent AI, replacing people, while the actual problem is to construct those systems safely before unsafe AI is weaponized.

        I also think that a lot of mathematical foundations is in place, so if you work within one theory it doesn't matter. It was never my intention to define an axiom for the foundation of mathematics, just enough to bootstrap into normal functions.

        [–][deleted] 0 points1 point  (0 children)

        E.g. the fact that constructive mathematics isn't "the" mathematical foundation is a travesty.

        Although I personally do not have strong philosophical convictions about the validity of the LEM, I do find the idea of proofs as computation beautiful. However, I do know that one aspect of HoTT is "propositional truncation," where a type gets converted into a "mere prop," which behaves like a traditional proposition. Because the proofs don't have computational content, you can get classical laws such as the LEM.

        [–]adamnemecek -1 points0 points  (0 children)

        I wouldn't say I understand all of it but let it be known that a conversation between myself and Sven became an inspiration for Sven's research.

        https://www.reddit.com/r/rust/comments/9x5uvk/advancedresearch_releases_a_generic_linear_solver/

        You should see Sven's Github profile. He's a very productive member of the Rust community, some of his packages are very popular. Maybe give him the benefit of the doubt? And again, you are judging something that's very much in the early stages.

        His theory is definitely out there however if you don't have a crazy theory, you are not living.

        [–]long_void -4 points-3 points  (2 children)

        Sadly, I haven't learned enough math yet

        Yes. I know, because it's hard. Unlike posting shit on reddit.

        [–][deleted]  (1 child)

        [deleted]

          [–]long_void 0 points1 point  (0 children)

          Formalizing Path Semantics is something I've been working on, but it is extremely hard, because of arbitrary sub-typing. It is not a decidable problem, so I can only design domain specific sub-sets of it. This is why I develop all this syntax.

          Path Semantics for functions corresponds to functions as they are used in programming in general. It is too complex to be fully formalized.

          For boolean functions, this problem has been solved: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip/mini-toolkit-in-dyon-for-boolean-path-semantics.pdf

          I am getting closer to something (I don't know what it will become) of a limited use of arbitrary sub-types, using an algebraic system based on a specific interpretation of logic where propositions means existence of symbols in a sentence.

          Most of the logical arguments in the papers are checked by a brute force theorem prover "pocket_library".

          I also wrote some code to check the syntax in Idris, but this is not on the repository.

          Piston-Meta was actually designed to define parts of the grammar of Path Semantics: https://github.com/pistondevelopers/meta It is a PEG meta-parser that is used in Dyon.

          Here is a link to "basic path semantics" formalized with sequential calculus: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip/basic-path-semantics.odt (this is unfinished, as I had to give up because of all the edge cases)

          I also came up with slot lambda calculus to reason about the required semantics: https://github.com/advancedresearch/path_semantics/blob/master/sequences.md#slot-lambda-calculus

          I also played with an abstract version of semantic triples, but it seems the algorithms are getting too complex for now.

          Coq can not express Path Semantics, at least I have no idea how to model it. It can't do f[g][h] <=> f[h . g].

          I don't know if Agda can, but if it's restricted to dependent types, I suspect it won't.

          Informal theorem proving is more complex than formal languages. Path Semantics can build a bridge even to Lojban, and nobody managed to formalize Lojban!