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-%3DHGbf_Cc%2BsaQ%3DFiEw0bwB8G_607vVNMNY6-Jb3zFYyVf3Q%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
