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 <zar...@gmail.com> 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 <linasveps...@gmail.com> > 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 <ivan.mo...@gmail.com> >> 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 <linasveps...@gmail.com> >> napisao je: >> >> >> >> On Sun, Dec 9, 2018 at 11:55 AM Ivan Vodišek <ivan.mo...@gmail.com> >> 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 opencog+unsubscr...@googlegroups.com. >> >> To post to this group, send email to opencog@googlegroups.com. >> >> 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 opencog+unsubscr...@googlegroups.com. >> > To post to this group, send email to opencog@googlegroups.com. >> > 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 opencog+unsubscr...@googlegroups.com. To post to this group, send email to opencog@googlegroups.com. 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. For more options, visit https://groups.google.com/d/optout.
