Hi Ivan, Good to hear from you. Some remarks, from least important to most
1) the chomsky hierarchy - I always found it useless, in practice. Don't waste time on it. Know it exists, then ignore it. 2) If reading wikipedia, look at "natural deduction" - it provides a nice counter-point to hilbert systems. 3) A lot of the considerations re: hilbert systems vs natural deduction, or etc.etc. have to do with algorithms for auto-discovering proofs, and doing so efficiently. And for that, there's just a huge number of different algorithms, a huge number of different ways of representing rules and axioms and knowledge. So 8 years ago or so I became enamored of "answer set programming", there's some great software for that, and since then many other ways of doing things have come to be, including all sorts of theorem provers, and advances in the theory of type systems, and software for agda and hol and etc. Its now all foggy to me, but only because there are so many ways, possibilities. 4) All of the points in point-3 have to do with "crisp" binary logic. The place to make progress, maybe rapid progress, is to map probabilistic concepts onto the above. There are several ways: first, a naive replacement of true/false by a number between 0-1. (e.g. the fuzzy logic of the 1970's) These kinds of approaches do not seem to be very powerful: all probabilities dissolve into grey quickly. Slightly fancier is PLN, but the ongoing difficulty with PLN and the combinatorial explosion hits a wall (heck, there's a combinatorial explostion even in the crisp theorem provers. Its only made worse in a PLN-style framework) Third approach is neural-nets/deep learning, where use of float-point numbers is central, but one completely discards all structure, and replaces it by vectors. So, instead of having a hilbert-axiom or rule, or whatever, you have ... a vector. Vectors provide a real shitty mapping to rules/axioms/logic/rationality. All its got going for it is that it's fast. There's a reason why vectors work: vectors are described by the tensor category. As it happens, some/much of natural language is described by the same category. This is "the secret", the core reason why word2vec-style neural nets/deep-learning work fairly well for natural language. Note also: small subsets of mathematical logic can also jam into this category. This is also why deep-learning is now hitting the wall: vectors are shitty representations of rules/axioms/structure. My hypothesis/interest is to clarify this further, and then replace the tensor category by a category that is more appropriate to (a) natural language (b) mathematical logic (hilbert system or natural deduction or agda/dependent type or HOL, or whatever). Then, properly identified, rip the vectors out of deep-learning, and plug in this correct category. To repeat myself: keep the insight of deep learning, but throw away the effing vectors, already. What's the correct category? Rather than naming it formally, let me (again) describe it informally: its the category of fitting together jigsaw puzzle pieces. Why? Heck: just look at "judgements" in "natural deduction": they obviously look like jigsaw pieces. Once you are sensitized, they are everywhere. But there's more: the tab-connectors are tensor-like in their behavior, so the whole thing looks "kind of like tensors", anyway, but just a bit whack/off-kilter (e.g. no dagger, etc.) So -- replace the vectors of deep-learning by jigsaw pieces. Hand-wavey presto-magic ta-dahh. I've said this all before, to the point of exhaustion. I've made zero progress on this since last summer. Why? I have a long list of excuses. But they are just excuses. I remain convinced that this is the correct way forward. I strongly encourage investigation into this direction. -- Linas On Tue, Mar 26, 2019 at 8:39 AM Ivan V. <[email protected]> wrote: > *Zar Goertzel* wrote: > >> Briefly asked Chad the logic guru. >> >> He says sounds like the proof-logic for parsing would be something in the >> linear logic direction. Mentions Lambek and >> https://en.wikipedia.org/wiki/Grammatical_Framework. >> But he isn't sure something as detailed/formal as you'd like has been >> done yet... >> > > I'm exploring parsing vs. proof construction. What I've found out for now > is that Hilbert system <https://en.wikipedia.org/wiki/Hilbert_system> (an > analogue to OpenCog unified rule engine) is an equivalent to unrestricted > grammars <https://en.wikipedia.org/wiki/Unrestricted_grammar> from Chomsky > hierarchy <https://en.wikipedia.org/wiki/Chomsky_hierarchy> (Type 0). The > difference is merely in notation direction where Hilbert writes rules from > left to right, while parsing grammar productions reverse left and right > sides. > > The connection is the following (using Hilbert's direction): > > - (cause / string-of-terminals-or-non-terminals-to-be-parsed) *->* > (consequence / match-pattern) > > With a help of common rules (again in Hilbert System): > > - A *->* (A \/ B) > - B *->* (A \/ B) > > > Proving is performed from left to right, while parsing is performed from > right to left. Considering Curry-Howard-Lambek > <https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence> > correspondence, I suppose we may add unrestricted grammars to it also. > Unrestricted grammars are anyway considered Turing machine equivalent > <https://en.wikipedia.org/wiki/Unrestricted_grammar#Equivalence_to_Turing_machines> > rewriting <https://en.wikipedia.org/wiki/Rewriting> mechanisms, so this > should be no surprise at all, although I didn't imagine it would be that > simple and straightforward. > > If anyone is interested in serious parser/proof material written by > professionals, there is excellent Stanford's Introduction to Logic > <http://intrologic.stanford.edu/public/index.php>. Chapter 9.6 - Pseudo > English > <http://intrologic.stanford.edu/public/section.php?section=section_09_06> > covers a kind of context free grammars implemented in logic, and we should > be able to extended it to unrestricted grammars also. > > Stay cool, > Ivan V. > > > pon, 17. pro 2018. u 12:32 Zar Goertzel <[email protected]> napisao je: > >> Briefly asked Chad the logic guru. >> >> He says sounds like the proof-logic for parsing would be something in the >> linear logic direction. Mentions Lambek and >> https://en.wikipedia.org/wiki/Grammatical_Framework. >> But he isn't sure something as detailed/formal as you'd like has been >> done yet... >> >> On Fri, Dec 14, 2018 at 12:27 PM Zar Goertzel <[email protected]> wrote: >> >>> Howdy Linas, >>> >>> Unfortunately, I'm drastically ignorant compared to my senior colleagues >>> and you. >>> >>> Re: URE: So curry-howard says "proofs are programs" and it turns out >>> that theorem proving is a lot like parsing (its identical to >>> parsing???) I DO NOT know of any simple write-up of this topic; I can >>> only wave my hands around. When I mentioned this to Ben's son Zar, he >>> kind-of responded and said "duhh its obvious everyone knows this." >>> >>> Zar, do you know of any nice readable references that explain how >>> theorem-proving and parsing are "the same thing"? >>> >>> >>> We had happened to be talking about it at lunch when you brought that >>> up. It seems likely they're in a similar state to you: it seems obvious and >>> they can wave their hands around, but haven't bothered formally writing it >>> up. >>> >>> Would it be hard to write up formally? >>> >>> On Wed, Dec 12, 2018 at 1:17 AM Linas Vepstas <[email protected]> >>> wrote: >>> >>>> Oh, and one more (minor?) remark: the intermediate states that get >>>> explored during pattern matching are called "Kripke frames", and the >>>> "crisp logic of term re-writing" is one of the modal logics. I know >>>> this to be true in a hand-waving fashion; I have searched long and >>>> hard for a paper or a book that would articulate this in some direct, >>>> detailed fashion. I have not yet found one. >>>> >>>> Zar, so second question, any chance at all you might be aware of >>>> references for this? >>>> >>> >>> The logic of term rewriting is paramodulation? That's not a modal logic >>> though . . . >>> >>> >>>> >>>> --linas >>>> On Tue, Dec 11, 2018 at 2:24 AM Ivan Vodišek <[email protected]> >>>> wrote: >>>> > >>>> > Linas, >>>> > >>>> > Thank you for taking a time to response, I'll try to keep this short. >>>> I might be wrong, but Curry-Howard-Lambek isomorphism inspires me greatly >>>> in a pursuit for one-declarative-language-like-URE-to-rule-them-all. >>>> > >>>> > I see term rewriting simply as basic implication over input and >>>> output terms. A number of term rewriting rules may be bundled together in a >>>> conjunction. Alternate pattern-matching options may form a disjunction. And >>>> pattern exclusion may be expressed as a negation. These are all common >>>> logical operators in a role of defining a term rewriting system. And since >>>> this kind of term rewriting is basically a logic, it can generally be >>>> tested for contradiction, or it can be used for deriving relative indirect >>>> rules - if we want it so. >>>> > >>>> > That's a short version of what I currently work on - a term rewriting >>>> system expressed as a crisp logic - just a few basic logic operators with >>>> no hard-wired constants other than true and false - all wrapped up in a >>>> human friendly code code processor. >>>> > >>>> > - Ivan V. - >>>> > >>>> > uto, 11. pro 2018. u 04:07 Linas Vepstas <[email protected]> >>>> napisao je: >>>> >> >>>> >> On Sun, Dec 9, 2018 at 11:55 AM Ivan Vodišek <[email protected]> >>>> wrote: >>>> >> > >>>> >> > Oh, I see, I must be talking about URE then. All cool, then it >>>> seems reasonable to me (one ring to rule them all - policy). >>>> >> > >>>> >> > I keep persuading myself that a perfect single declarative - logic >>>> + lambda calculus + type theory exists, or could be invented, >>>> >> >>>> >> So, OK, the atomspace is trying to be: >>>> >> >>>> >> + declarative: so kind-of-like datalog or kind-of like SQL or noSQL, >>>> >> or some quasi-generic (graph) data store. But you already know this. >>>> >> >>>> >> - it does NOT have "logic" in it, in any traditional sense of the >>>> word >>>> >> "logic". It does have the ability to perform term-rewriting (pattern >>>> >> re-writing, graph re-writing). >>>> >> >>>> >> - lambda calculus is a form of "string rewriting". Note that string >>>> >> rewriting is closely related to term rewriting (but not quite the >>>> same >>>> >> thing) and that term rewriting is closely related to graph rewriting >>>> >> (but not quite the same thing). >>>> >> >>>> >> When lambda calculus was invented, any distinction between strings, >>>> >> terms, and graphs was unknown and unknowable, until the basic >>>> concepts >>>> >> got worked out. So, due to "historical accident", generic lambda >>>> >> calculus remains a string rewriting system. As stuff got worked out >>>> >> over the 20th century, the concept of "term rewriting" gelled as a >>>> >> distinct concept. (And other mind-bendingly >>>> >> similar-but-slightly-different ideas, like universal algebra, model >>>> >> theory ... and bite my tongue. There's more that's "almost the same >>>> as >>>> >> lambda calc. but not quite". A veritable ocean of closely related >>>> >> ideas.) >>>> >> >>>> >> From practical experience with atomspace, it turns out that trying to >>>> >> pretend that all three rewriting styles (string, term, graph) are the >>>> >> same thing "mostly works", but causes all kinds of friction, >>>> >> confusion, conundrums in detailed little corners. So, for example, >>>> >> BindLink was an early attempt to define a Lambda for declarative >>>> >> graphs. In many/most ways, it really is "just plain-old-lambda". It >>>> >> works, and works great to this day, but, never-the-less, we also >>>> >> created more stuff that is "just like lambda, but different", >>>> >> including LambdaLink, etc. >>>> >> >>>> >> In many ways, its an ongoing experiment. The search for "perfect" has >>>> >> more recently lead to "values", which are a lot like "valuations" in >>>> >> model theory. (and again, recall that model-theory is kind-of-ish >>>> like >>>> >> lambda-calculus, but its typed.) >>>> >> >>>> >> There's no "logic" in the atomspace, but you could add logic by using >>>> >> the URE, and/or by several other ways, including parsing, sheaves, >>>> and >>>> >> openpsi. In short, there's lots of different kinds of logic, and lots >>>> >> of different ways of implementing it, and we are weakly fiddling with >>>> >> several different approaches. And I have more in mind, but lacking >>>> in >>>> >> time. >>>> >> >>>> >> -- Linas >>>> >> -- >>>> >> 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/CAHrUA35V2Uk0YbwERPMkPhpxevriT0DZvaYzLtEPXUQC9TiUHQ%40mail.gmail.com >>>> . >>>> >> 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%3Dj6VaDej%3DGBL3bpMxYArP6ZnkifCiNmStc7-SrJO%2BV3eHQA%40mail.gmail.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/CAHY-%3DHEmBKgtJPAeKTXAOyOaE4gR8cZeouc8v9JhQb3E4jX%2BkQ%40mail.gmail.com >> <https://groups.google.com/d/msgid/opencog/CAHY-%3DHEmBKgtJPAeKTXAOyOaE4gR8cZeouc8v9JhQb3E4jX%2BkQ%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%3Dj6XXTvSx_BCNHsS-CSfzCjH2y0MeedeepUY_%2B5ANx-h99g%40mail.gmail.com > <https://groups.google.com/d/msgid/opencog/CAB5%3Dj6XXTvSx_BCNHsS-CSfzCjH2y0MeedeepUY_%2B5ANx-h99g%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/CAHrUA34JUoVRz%3Dz%2BXGfvv45wFG6qPmXDpKTrqNUjHODzWDLpHQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
