Hello everyone :) I was having a few thoughts about time complexity of inference I wanted to share with OpenCog community. I'll try to keep this post short, not to take a much time of yours.
Basically, logical deduction relays on finding a universal unificator for two formulas to derive the third formula from them. But to avoid unification, it is possible from two formulas to derive another two, one with substitution relative to the first, one with substitution relative to the second formula. This unification avoiding puts deduction to a position where it is analogous to function calling. Further, all logic formulas can be expressed in disjunctive normal form. Also, this DNF is interchangable with implicational logic (only implication and falsehood). And implicational logic is something that reminds a lot of unrestricted grammars. In fact, isn't implicational logic inference a kind of higher order unrestricted grammar parsing, only with predicates expressed as sequences of constants? So, why am I writing all of this? Suppose that there is a strict isomorphism from logic inference to higher order unrestricted grammar parsing. Usual CFG parsers perform about O(n^3) worst time complexity when parsing a text (relative to the text length). I don't have performance numbers for unrestricted grammar parsing, but I assume that unrestricted grammar parsing wouldn't be much slower (although it would be relative to a length of a path from the top-most rules to the bottom-most tokens). The question about this post is: Does this possible isomorphism mean that an inference would be performed in polynomial time, regarding to a length of a proof, at least in a case of propositional logic? Thank you all, Ivan V. uto, 2. tra 2019. u 23:36 Ivan V. <[email protected]> napisao je: > Linas, > > Tanks for taking time to answer. > > I skimmed over the Stackexchange post and I found it interesting (not that > anyone cares :o). I tried once a while ago to learn about Category theory > from Wikipedia, but it seemed over complicated. I guess I needed examples > closer to my knowledge - not mathematical abstractions, but type theory > oriented - as noted on Stackexchange. Maybe I should give it another try, > I'll see. > > Thanks again, > Ivan V. > > > uto, 2. tra 2019. u 20:05 Linas Vepstas <[email protected]> napisao > je: > >> Hi Ivan: >> >> Google "category theory for computer scientists" I get this: >> >> > [PDF]Category Theory for Computing Science - Mathematics and Statistics >> > http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf >> > by M Barr - Cited by 1642 - Related articles >> > Aug 4, 2012 - This book is a textbook in basic category theory, written >> specifically .... been a major source of interest to computer scientists >> because they are. >> >> I have not read it. I think that "cited by 1642" means its a good, >> high-quality book. There are several of these kinds of books -- one that I >> did skim, maybe a decade ago, gave all of its examples and homework >> problems in CaML -- it was an older book, predating Haskell. >> >> See also this: >> >> https://cs.stackexchange.com/questions/3028/is-category-theory-useful-for-learning-functional-programming >> >> Notice that the answer with largest upvotes says "category theory is type >> theory". For any complete newbies reading this, "int", "float", "char*", >> "class FooBar" and "int FooBar::myMethod(int x)" are all (C/C++/Java) >> examples of types. >> >> I'm making three additional claims, in addition to this highly-upvoted >> answer: >> >> 1) Link-grammar connectors/link-types are types, in the sense of type >> theory. (This is not really a new claim; the original link-grammar authors >> made more-or-less this same claim, in 1993, in one of their original papers) >> >> 2) Deep-learning neural-nets perform classification by classifying into >> types. (type-theoretical types) (this claim is kind-of >> shallow/stupid/"obvious", and needs to be articulated to become interesting >> and non-trivial.) >> >> 3) There is an almost-direct, one-to-one correspondence of deep-learning >> neural-nets types to link-grammar connectors/link-types, if you know where >> to look for them. This is the controversial claim that everyone rejects. >> And perhaps I am hallucinating and completely making this up. Like 2+2=3. >> I'm struggling with this myself, as the details remain unclear and >> confusing. So it's OK if you don't believe this one. But this is the >> claim I'm interested in. >> >> -- Linas >> >> >> On Wed, Mar 27, 2019 at 4:40 PM Ivan V. <[email protected]> wrote: >> >>> Linas, you lost me at Category theory... Nevertheless, I also find the >>> idea of integrating symbolic system into neural networks amusing. The proof >>> I really do is a recent speculation from a paper I'm writing from time to >>> time, just to gather my thoughts (maybe I got this from you at some point, >>> I really don't remember now): >>> >>> Nevertheless, symbolic approach may support structure forms on top of >>>> which artificial neural networks could operate, thus forming a synergy >>>> between the two seemingly opposite philosophies in designing AI. >>>> >>> >>> But then I develop things in symbolic direction because with this, I'm >>> currently interested only in improvement of OpenCog URE engine, as far as I >>> plan to offer contribution around here if the language I'm building passes >>> the stages a, b, c, d, and also e, just in case. >>> >>> Realizing ideas take time, and life is too short to do it all, while I'm >>> not a fan of bossing around... I also like to see creativity in other >>> people too... >>> >>> sri, 27. ožu 2019. u 20:04 Linas Vepstas <[email protected]> >>> napisao je: >>> >>>> Hi Sergei, >>>> >>>> On Wed, Mar 27, 2019 at 12:14 PM Sergei Kaunov <[email protected]> >>>> wrote: >>>> >>>>> Amused by your work, Linas, and you describe it very interesting. >>>>> Where should we watch further progress on the topic? >>>>> >>>> >>>> Thanks! Progress is hard, because several things have to happen in >>>> parallel. >>>> >>>> -- I (or you, or anyone else) has to think hard across multiple >>>> different difficult mathematical abstractions. >>>> >>>> -- Once I (or you, or anyone else) has some "great idea", it has to be >>>> transmitted to others, either by email or by writing papers. >>>> >>>> -- Others can understand those "great ideas" only if they have the >>>> appropriate mathematical background: in Ivan's case: hilbert-systems and >>>> natural deduction and proof theory and type theory and category theory and >>>> neural networks and deep learning and statistical mechanics (for example, >>>> the "objective function" that neural net guys love to minimize/maximize is >>>> exactly the same thing as a boltzmann distribution from statistical >>>> echanics) So my personal progress on the topic is blocked by the >>>> inability to communicate it to others. If you don't understand what I'm >>>> talking about, its deeply frustrating for me. (And this is symmetric: >>>> sometimes, I am told about great ideas, which I don't understand, because I >>>> lack the background knowledge) >>>> >>>> -- A "great idea" is great only if it *actually works*. And, here, that >>>> means (a) writing software (b) running experiments (c) analyzing data. (d) >>>> describing experimental results to others. So, not only are steps a,b,c, >>>> extremely time consuming, but step (d) is often mis-understood/neglected, >>>> because the intended audience didn't understand why the experiment is >>>> important. >>>> >>>> -- After you've conquered steps a,b,c,d then and only then can you do >>>> step e) build an insanely great demo that will wow everyone who sees it, >>>> even if they are a complete moron. For example, "deep fakes". You don't >>>> need math to know that something unusual is happening there. >>>> >>>> The pressure I'm under, that I feel, is that I've got a collection of >>>> "great ideas", I'm trying to articulate them, having trouble finding an >>>> audience, struggling with steps a,b,c,d and meanwhile everyone is shouting >>>> out loud "you guys are a bunch of losers because you don't have step e) you >>>> suck!" and dealing with the psychological and financial fallout from that. >>>> >>>> I'm not unique, here -- most researchers/scientists deal with these >>>> same issue. The commonly accepted solution for this is to create >>>> collaborations and teams -- "division of labor" -- and tehre's >>>> chicken-and-egg problems to solving that, also. >>>> >>>> --linas >>>> >>>> >>>>> >>>>> -- >>>>> You received this message because you are subscribed to the Google >>>>> Groups "opencog" group. >>>>> To unsubscribe from this group and stop receiving emails from it, send >>>>> an email to [email protected]. >>>>> To post to this group, send email to [email protected]. >>>>> Visit this group at https://groups.google.com/group/opencog. >>>>> To view this discussion on the web visit >>>>> https://groups.google.com/d/msgid/opencog/0b258284-cb0c-45ae-8d34-9f74d7ee00f9%40googlegroups.com >>>>> . >>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>> >>>> >>>> -- >>>> cassette tapes - analog TV - film cameras - you >>>> >>>> -- >>>> You received this message because you are subscribed to the Google >>>> Groups "opencog" group. >>>> To unsubscribe from this group and stop receiving emails from it, send >>>> an email to [email protected]. >>>> To post to this group, send email to [email protected]. >>>> Visit this group at https://groups.google.com/group/opencog. >>>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/opencog/CAHrUA355QGo1zA8oCUZ3guEwMFymqJ7-PA5ydTJdMx2Sf%2B-ypQ%40mail.gmail.com >>>> <https://groups.google.com/d/msgid/opencog/CAHrUA355QGo1zA8oCUZ3guEwMFymqJ7-PA5ydTJdMx2Sf%2B-ypQ%40mail.gmail.com?utm_medium=email&utm_source=footer> >>>> . >>>> For more options, visit https://groups.google.com/d/optout. >>>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "opencog" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To post to this group, send email to [email protected]. >>> Visit this group at https://groups.google.com/group/opencog. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/opencog/CAB5%3Dj6Xt0ze729QzdMVFyU4Q%2BYPB7hib_7n%3D4iNguzmJ2Em2SA%40mail.gmail.com >>> <https://groups.google.com/d/msgid/opencog/CAB5%3Dj6Xt0ze729QzdMVFyU4Q%2BYPB7hib_7n%3D4iNguzmJ2Em2SA%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> For more options, visit https://groups.google.com/d/optout. >>> >> >> >> -- >> cassette tapes - analog TV - film cameras - you >> >> -- >> You received this message because you are subscribed to the Google Groups >> "opencog" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To post to this group, send email to [email protected]. >> Visit this group at https://groups.google.com/group/opencog. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/opencog/CAHrUA36XhRzY0Wez4n0VhYSw_NYfZMVY3fU-eOPe2g7h-%2B2ZAQ%40mail.gmail.com >> <https://groups.google.com/d/msgid/opencog/CAHrUA36XhRzY0Wez4n0VhYSw_NYfZMVY3fU-eOPe2g7h-%2B2ZAQ%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> For more options, visit https://groups.google.com/d/optout. >> > -- You received this message because you are subscribed to the Google Groups "opencog" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/opencog. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAB5%3Dj6VfJGNdeSLWUSnZiSrCZzcn19j%3DjrMiJZCq4YdBJM6FbA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
