Ah, I have some new thoughts on the "theorem proving + AGI + parsing" side, but will have to wait to type them in till I get a little time at the computer, I'm traveling between meetings and conferences in Europe just now...
On Tue, May 15, 2018 at 12:44 AM, Linas Vepstas <[email protected]> wrote: > > > On Mon, May 14, 2018 at 4:54 PM, Alexey Potapov <[email protected]> wrote: >> >> Hi Linas, >> this is quite an interesting discussion, and I believe we should involve >> Ben and others in it. > > > Ben has been involved in this discussion for a decade; I think he knows the > general outline, even as we argue violently about the details. Anyway, this > is why I say "we should discuss on the mailing list", a dictum that I have > been violating. > >> >> Actually, I have some concerns regarding too strong focus on the formal >> logic and automatic theorem proving in OpenCog since I'm not completely >> convinced of its fundamental role in AGI... ;) > > > Yes, I agree. I am very much trying to pursue a probabilistic approach. The > question is then "probabilities on what?" and I have an answer that I like, > but I have trouble sharing that answer in a way that is understandable. Let > me try to sketch that, in this context. > > You know probabilistic programming very very much better than I, so please > correct my mis-steps. In probabilistic programming, one essentially has > lambda-expressions, and is assigning probabilities to them. For example: > what is the probability of taking this branch (this if-statement) or not? > The probability of running this loop N times? the probability of calling > this routine? The probability of making this list/array longer or shorter? > This might be done with either custom-built probabilistic programming > languages, or with modified versions of C or Lisp. At any rate, these can > be abstractly understood as being lambda-expressions, with probabilities > assigned to them. > > However, as I exhort below, lambdas are closely tied to cartesian products, > and to classical logic, and we have plenty of evidence that suggests that > this is inappropriate for natural, human intelligence. So what is the right > thing? To keep a long story short, for me, it is this concept of "disjoined > connector sets" (aka "jigsaw-puzzle pieces"), and I attach probabilities to > those. More generally, more vaguely, the structures are "patterns", this is > what the pattern miner looks for. There are various theoretical arguments > that show that these are sufficient for general purposes. For example, > theorem-proving is like assembling jigsaw-puzzle pieces, where he > puzzle-pieces are rules of inference; this is why theorem-proving is like > parsing. However, general knowledge representation is also like this: > solving Sherlock Holmes mysteries has long been said to be like "solving a > jigsaw puzzle": well, except now, we have the mathematical formalism to make > this statement precise. I think much of what neural nets and deep learning > do also fits into this general framework; I want to write a paper on this, > but have not had the time yet. > > So, I am not really into formal logic, per-se; rather, I am trying to amass > evidence why probabilistic patterns are the correct approach, while > probabilistic lambdas are too stringent, too constrained, too tight to be > useful. One has to assign probabilities to the patterns, the arrangements, > and NOT to the individual components of the pattern. (Also, I keep saying > "probability" when I actually mean "mutual information" or maybe > "surprisingness", as the case may be. Just as lambda is not quite right, I > get the feeling that probability is not quite right, and that talking about > mutual information and surprisingness is more correct, than talking about > probability. But this intuition remains difficult to explain.). > > -- Linas > >> >> Best regards, >> Alexey. >> >> 2018-05-15 0:13 GMT+03:00 Linas Vepstas <[email protected]>: >>> >>> Alexey, Konstantin, >>> >>> On Mon, May 14, 2018 at 2:41 PM, Константин Тимофеев >>> <[email protected]> wrote: >>>> >>>> Nil, Linas, thanks for the explanations. It seems like I have to learn >>>> some new things before I could understand clearly what is the issue behind >>>> this discussion. Hopefully it will not take too much time. >>> >>> >>> If it doesn't take much time, then you are a super-human genius working >>> in the wrong field. To understand the issue, you'd have to read a book or >>> two on proof theory, along with a large rainbow of related topics. Its taken >>> me ten years to understand what the problem is. I can't magically transfer >>> this knowledge, but I can tell you what keywords to search for and read on. >>> Besides proof theory and model theory, anything that describes linear logic >>> should make clear what the issue with cartesian products is (in proof >>> theory, it corresponds to the rules of weakening and contraction, which are >>> assumed by the lambda abstraction but are forbidden by tensor products.) To >>> understand why products in linguistics are tensor products and not cartesian >>> products, look at the wikipedia article on "pregroup grammar". The earliest >>> reference that I know of that discusses this clearly is Marcus Solomon >>> "Algebraic Linguistics" (1967) which your compatriots in Novosibirsk sent >>> me. The categorial grammars there are discusses in pages 90-120, which you >>> can match up to what the wikipedia pregroup grammar article states. >>> >>> Last time I said that "theorem proving is like parsing", I said it to >>> Ben's son Zar, who is studying theorem proving, and his response was "yeah, >>> so what, everyone knows that". If you already know that, good. My point is >>> that since we know that theorem proving is incompatible with lambda, we >>> should stop using lambda so much. To me, this still remains a deep, >>> important insight; I'm trying to use it to guide the design of atomese. I >>> can't imagine that you will understand in only a few months. A few years, >>> maybe. I'm just saying, now is the time to start reading about it. >>> >>> -- Linas >>>> >>>> >>>> >>>> On Mon, May 14, 2018 at 8:45 PM, Linas Vepstas <[email protected]> >>>> wrote: >>>>> >>>>> >>>>> >>>>> On Mon, May 14, 2018 at 12:54 AM, Nil Geisweiller >>>>> <[email protected]> wrote: >>>>>> >>>>>> Hi, >>>>>> >>>>>> On 05/11/2018 11:36 PM, Linas Vepstas wrote: >>>>>>> >>>>>>> light sprinkling of lambda calculus on top. Nil keeps putting in too >>>>>>> much lambda calculus, I can't seem to get him to stop. It needs more >>>>>>> prolog, I keep telling him. >>>>>> >>>>>> >>>>>> But >>>>> >>>>> >>>>> I meant that to be funny. Like saying "it needs more pepper, no, it >>>>> needs more salt". >>>>> >>>>>> >>>>>> the left hand side term of a prolog fact shares the same goodies I'm >>>>>> after when I use a LambdaLink. It exposes a list of variables, in a >>>>>> determined order, abstracting the body away. >>>>> >>>>> >>>>> But Alexey and Konstantin have not heard this argument before, so let >>>>> me sketch it briefly. >>>>> >>>>> * Yes, lambdas provide abstraction. They're useful. But ... >>>>> * lambda calc is old, it was originally developed in the view of >>>>> Hilbert's program, of providing a foundational basis for classical logic. >>>>> * prolog is new, developed for knowledge representation and theorem >>>>> proving, that is, non-classical logic. >>>>> * lambda calc is the internal language of cartesian, closed categories: >>>>> viz anything with lists, pairs, cartesian products. lambda calc >>>>> corresponds >>>>> to classical logic. >>>>> >>>>> * by contrast, theorem proving is known to NOT use classical logic; the >>>>> logic of theorem proving is intuitionist logic, and more generally, the >>>>> logic of Kripke frames. Insofar as the rule engine and PLN is a >>>>> kind-of-like >>>>> theorem prover, it should be based on the principles given in books on >>>>> proof >>>>> theory, and NOT on classical logic! People who work on proof theory have >>>>> made a lot of advancements since the 1930's. We should know of, >>>>> understand, >>>>> and employ those concepts. Proof theory is a big deal. We should not >>>>> ignore >>>>> it. >>>>> >>>>> * There are other things that classical logic fails to describe, >>>>> besides proof theory: natural language and biochemistry. Both of these >>>>> appear to be described by intuitionistic logic, or, more properly, by >>>>> fragments of linear logic. The difference is that linear logic throws away >>>>> the notion of pairs, lists, cartesian products and lambdas: lambda's >>>>> cannot >>>>> be used to describe language or biochemistry (In physics, the >>>>> failure/incorrectness of lambda is "well-known", and is called the >>>>> "no-cloning theorem". The fundamental reason for this is that tensor >>>>> products violate the assumption of the existence of pairs, lists, >>>>> cartesian >>>>> products. Tensor products are incompatible with cartesian products. >>>>> Insofar >>>>> as the lambda abstracts the cartesian product, it too must be discarded >>>>> from >>>>> the theory, as being incompatible. Any theory that has tensor products >>>>> cannot have lambdas in it. They can't co-exist without contradiction.) >>>>> >>>>> * Insofar as we work with language, learning and theorem proving, where >>>>> there are "well-known" theorems that prove that lambda calc is >>>>> incompatible, >>>>> we should perhaps stop focusing on it so much. Lambda calc has it's place, >>>>> -- lambda is great for abstraction, but not everything can be abstracted >>>>> in >>>>> that way. Most notably (for me), the link-types of link-grammar cannot be >>>>> abstracted by lambdas, because the disjuncts of link-grammar (alternately, >>>>> the VP, NP of phrase-structure grammars) look like tensor products, and >>>>> not >>>>> link cartesian products. >>>>> >>>>> For these reasons, I think we are over-using lambdas. They offer a >>>>> deeply-incorrect, basically-broken view of the world we are interested in: >>>>> proof theory, linguistics, knowledge, biochemistry. >>>>> >>>>>> >>>>>> >>>>>> I know that FreeLink automatically digs up the variables, but it has >>>>>> other problems >>>>>> >>>>>> 1. The variable order depends on their appearances in the body. Even >>>>>> worse, this may depend on the variable names (see >>>>>> https://github.com/opencog/atomspace/issues/1677). >>>>> >>>>> >>>>> Yes, that is the definition of a "free variable". Do you want to >>>>> propose some kind of semi-free variable? >>>>>> >>>>>> >>>>>> 2. There's no way to tell FreeLink to escape some variable (unless a >>>>>> QuoteLink is used). >>>>> >>>>> >>>>> Yeah, quote links are awful. I think a very very high priority is to >>>>> figure out how to do the things we need to do, without having to use >>>>> quotes. >>>>> I'm not sure, but the need for quotes seem to be a side-effect of using >>>>> lambdas or something like that. I don't understand. In all the work I >>>>> do, >>>>> with link-grammar, with language learning, quotes are never needed; the >>>>> concept of lambda abstraction is replaced by connectors and disjuncts; and >>>>> these never need to be quoted. Actually, I can't even imagine how one >>>>> could >>>>> "quote" a connector or disjunct, it doesn't make sense, conceptually. I >>>>> would have to think hard about that. >>>>> >>>>> (Well, there is also no concept of "variables", either. The roll of >>>>> variables are taken up by connectors, which are kind-of-like typed free >>>>> variables. Sort of. Again, this requires deep thought.). >>>>> >>>>> Upshot: maybe if we used lambdas less, then we would not need quotes. >>>>> Maybe they are partners in crime. >>>>> >>>>>> >>>>>> 3. Variables cannot be typed. >>>>> >>>>> >>>>> If they were typed, they would not be free, right? Maybe there is a >>>>> way to have typed free variables, I'm not sure; its certainly not >>>>> obvious; >>>>> but I can also see how it might be possible. You'd have to design it >>>>> carefully, to avoid contradictions. >>>>> >>>>>> >>>>>> >>>>>> For these 3 reasons I generally stay away from FreeLink, even though >>>>>> I'm sure it has good uses, if one is careful. >>>>> >>>>> >>>>> !? I don't recall ever suggesting that we should use FreeLink for >>>>> anything other than what it is currently used for. it provides some basic >>>>> utilities for locating variables in an expression, but that's it. I don't >>>>> understand why you even brought it up... ?? >>>>> >>>>> --linas >>>>> >>>>> -- >>>>> cassette tapes - analog TV - film cameras - you >>>> >>>> >>> >>> >>> >>> -- >>> cassette tapes - analog TV - film cameras - you >> >> > > > > -- > 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/CAHrUA356-6JTNTp1Txct21ZTuBYXwDs6bdMcr781EusGijVT3w%40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. -- Ben Goertzel, PhD http://goertzel.org "Only those who will risk going too far can possibly find out how far they can go." - T.S. Eliot -- 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/CACYTDBfapP_pY7G9139Ca5OAQpZAJPn1%3D7Eh-hSD1RabQkEchA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
