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? --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/CAHrUA37GsrK8UWA1yLkH0D1d9msCT_pgSenWCqzvdcU2K6zZ4w%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
